Fix end-to-end proof to finally obtain the unmodified semantics
[darcs-mirror-isa-launchbury.git] / Launchbury / CardinalityEtaExpandCorrect.thy
1 theory CardinalityEtaExpandCorrect
2 imports ArityEtaExpand CardinalityAnalysisSpec AbstractTransform Sestoft SestoftGC ArityEtaExpansionSestoft ArityAnalysisStack  ArityConsistent
3 begin
4
5 context CardinalityPrognosisCorrect
6 begin
7   sublocale AbstractTransformBoundSubst
8     "\<lambda> a . inc\<cdot>a"
9     "\<lambda> a . pred\<cdot>a"
10     "\<lambda> \<Delta> e a . (a, Aheap \<Delta> e\<cdot>a)"
11     "fst"
12     "snd"
13     "\<lambda> _. 0"
14     "Aeta_expand"
15     "snd"
16   apply default
17   apply (simp add: Aheap_subst)
18   apply (rule subst_Aeta_expand)
19   done
20
21   abbreviation ccTransform where "ccTransform \<equiv> transform"
22
23   lemma supp_transform: "supp (transform a e) \<subseteq> supp e"
24     by (induction rule: transform.induct)
25        (auto simp add: exp_assn.supp Let_supp dest!: set_mp[OF supp_map_transform] set_mp[OF supp_map_transform_step] )
26   interpretation supp_bounded_transform transform
27     by default (auto simp add: fresh_def supp_transform) 
28
29   type_synonym tstate = "(AEnv \<times> (var \<Rightarrow> two) \<times> Arity \<times> Arity list \<times> var list)"
30
31   fun transform_alts :: "Arity list \<Rightarrow> stack \<Rightarrow> stack"
32     where 
33       "transform_alts _ [] = []"
34     | "transform_alts (a#as) (Alts e1 e2 # S) = (Alts (ccTransform a e1) (ccTransform a e2)) # transform_alts as S"
35     | "transform_alts as (x # S) = x # transform_alts as S"
36
37   lemma transform_alts_Nil[simp]: "transform_alts [] S = S"
38     by (induction  S) auto
39
40   lemma Astack_transform_alts[simp]:
41     "Astack (transform_alts as S) = Astack S"
42    by (induction rule: transform_alts.induct) auto
43
44   lemma fresh_star_transform_alts[intro]: "a \<sharp>* S \<Longrightarrow> a \<sharp>* transform_alts as S"
45    by (induction as S  rule: transform_alts.induct) (auto simp add: fresh_star_Cons)
46
47   fun a_transform :: "astate \<Rightarrow> conf \<Rightarrow> conf"
48   where "a_transform (ae, a, as) (\<Gamma>, e, S) =
49     (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>), 
50      ccTransform a e,
51      transform_alts as  S)"
52
53   fun restr_conf :: "var set \<Rightarrow> conf \<Rightarrow> conf"
54     where "restr_conf V (\<Gamma>, e, S) = (restrictA V \<Gamma>, e, restr_stack V S)"
55
56   fun add_dummies_conf :: "var list \<Rightarrow> conf \<Rightarrow> conf"
57     where "add_dummies_conf l (\<Gamma>, e, S) = (\<Gamma>, e, S @ map Dummy (rev l))"
58
59   fun conf_transform :: "tstate \<Rightarrow> conf \<Rightarrow> conf"
60   where "conf_transform (ae, ce, a, as, r) c = add_dummies_conf r ((a_transform (ae, a, as) (restr_conf (- set r) c)))"
61
62   inductive consistent :: "tstate \<Rightarrow> conf \<Rightarrow> bool" where
63     consistentI[intro!]: 
64     "a_consistent (ae, a, as) (restr_conf (- set r) (\<Gamma>, e, S))
65     \<Longrightarrow> edom ae = edom ce
66     \<Longrightarrow> prognosis ae as a (\<Gamma>, e, S) \<sqsubseteq> ce
67     \<Longrightarrow> (\<And> x. x \<in> thunks \<Gamma> \<Longrightarrow> many \<sqsubseteq> ce x \<Longrightarrow> ae x = up\<cdot>0)
68     \<Longrightarrow> set r \<inter> edom ce = {}
69     \<Longrightarrow> set r \<subseteq> domA \<Gamma> \<union> upds S
70     \<Longrightarrow> upds S - edom ce \<subseteq> set r
71     \<Longrightarrow> consistent (ae, ce, a, as, r) (\<Gamma>, e, S)"  
72   inductive_cases consistentE[elim!]: "consistent (ae, ce, a, as) (\<Gamma>, e, S)"
73
74   lemma closed_consistent:
75     assumes "fv e = ({}::var set)"
76     shows "consistent (\<bottom>, \<bottom>, 0, [], []) ([], e, [])"
77   proof-
78     from assms
79     have "edom (prognosis \<bottom> [] 0 ([], e, [])) = {}"
80      by (auto dest!: set_mp[OF edom_prognosis])
81     thus ?thesis
82       by (auto simp add: edom_empty_iff_bot closed_a_consistent[OF assms])
83   qed
84
85   lemma foo:
86     fixes c c'
87     assumes "c \<Rightarrow>\<^sup>* c'" and "\<not> boring_step c'" and "heap_upds_ok_conf c" and "consistent (ae,ce,a,as,r) c"
88     shows "\<exists>ae' ce' a' as' r'. consistent (ae',ce',a',as',r') c' \<and> conf_transform (ae,ce,a,as,r) c \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae',ce',a',as',r') c'"
89   using assms(1,2) heap_upds_ok_invariant assms(3-)
90   proof(induction c c' arbitrary: ae ce a as r rule:step_invariant_induction)
91   case (app\<^sub>1 \<Gamma> e x S)
92     have "prognosis ae as (inc\<cdot>a) (\<Gamma>, e, Arg x # S) \<sqsubseteq> prognosis ae as a (\<Gamma>, App e x, S)" by (rule prognosis_App)
93     with app\<^sub>1 have "consistent (ae, ce, inc\<cdot>a, as, r) (\<Gamma>, e, Arg x # S)"
94       by (auto intro: a_consistent_app\<^sub>1 elim: below_trans)
95     moreover
96     have "conf_transform (ae, ce, a, as, r) (\<Gamma>, App e x, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, inc\<cdot>a, as, r) (\<Gamma>, e, Arg x # S)"
97       by simp rule
98     ultimately
99     show ?case by (blast del: consistentI consistentE)
100   next
101   case (app\<^sub>2 \<Gamma> y e x S)
102     have "prognosis ae as (pred\<cdot>a) (\<Gamma>, e[y::=x], S) \<sqsubseteq> prognosis ae as a (\<Gamma>, (Lam [y]. e), Arg x # S)"
103        by (rule prognosis_subst_Lam)
104     then
105     have "consistent (ae, ce, pred\<cdot>a, as, r) (\<Gamma>, e[y::=x], S)" using app\<^sub>2
106       by (auto 4 3 intro: a_consistent_app\<^sub>2 elim: below_trans)
107     moreover
108     have "conf_transform (ae, ce, a, as, r) (\<Gamma>, Lam [y]. e, Arg x # S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, pred \<cdot> a, as, r) (\<Gamma>, e[y::=x], S)" by (simp add: subst_transform[symmetric]) rule
109     ultimately
110     show ?case by (blast  del: consistentI consistentE)
111   next
112   case (thunk \<Gamma> x e S)
113     hence "x \<in> thunks \<Gamma>" by auto
114     hence [simp]: "x \<in> domA \<Gamma>" by (rule set_mp[OF thunks_domA])
115
116     from thunk have "prognosis ae as a (\<Gamma>, Var x, S) \<sqsubseteq> ce" by auto
117     from below_trans[OF prognosis_called fun_belowD[OF this] ]
118     have [simp]: "x \<in> edom ce" by (auto simp add: edom_def)
119     hence [simp]: "x \<notin> set r" using thunk by auto
120
121     from `heap_upds_ok_conf (\<Gamma>, Var x, S)`
122     have "x \<notin> upds S" by (auto dest!:  heap_upds_okE)
123
124     have "x \<in> edom ae" using thunk by auto
125     then obtain u where "ae x = up\<cdot>u" by (cases "ae x") (auto simp add: edom_def)
126   
127
128     show ?case
129     proof(cases "ce x" rule:two_cases)
130       case none
131       with `x \<in> edom ce` have False by (auto simp add: edom_def)
132       thus ?thesis..
133     next
134       case once
135
136       from `prognosis ae as a (\<Gamma>, Var x, S) \<sqsubseteq> ce`
137       have "prognosis ae as a (\<Gamma>, Var x, S) x \<sqsubseteq> once"
138         using once by (metis (mono_tags) fun_belowD)
139       hence "x \<notin> ap S" using prognosis_ap[of ae as a \<Gamma> "(Var x)" S] by auto
140       
141   
142       from `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `\<not> isVal e`
143       have *: "prognosis ae as u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x \<cdot> (prognosis ae as a (\<Gamma>, Var x, S))"
144         by (rule prognosis_Var_thunk)
145   
146       from `prognosis ae as a (\<Gamma>, Var x, S) x \<sqsubseteq> once`
147       have "(record_call x \<cdot> (prognosis ae as a (\<Gamma>, Var x, S))) x = none"
148         by (simp add: two_pred_none)
149       hence **: "prognosis ae as u (delete x \<Gamma>, e, Upd x # S) x = none" using fun_belowD[OF *, where x = x] by auto
150
151       have eq: "prognosis (env_delete x ae) as u (delete x \<Gamma>, e, Upd x # S) = prognosis ae as u (delete x \<Gamma>, e, Upd x # S)"
152         by (rule prognosis_env_cong) simp
153
154       have [simp]: "restr_stack (- set r - {x}) S = restr_stack (- set r) S"
155         using `x \<notin> upds S` by (auto intro: restr_stack_cong)
156     
157       have "prognosis (env_delete x ae) as u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> env_delete x ce"
158         unfolding eq
159         using ** below_trans[OF below_trans[OF * Cfun.monofun_cfun_arg[OF `prognosis ae as a (\<Gamma>, Var x, S) \<sqsubseteq> ce`]] record_call_below_arg]
160         by (rule below_env_deleteI)
161       moreover
162
163       have *: "a_consistent (env_delete x ae, u, as) (delete x (restrictA (- set r) \<Gamma>), e, restr_stack (- set r) S)"
164         using thunk `ae x = up\<cdot>u`
165         by (auto intro!: a_consistent_thunk_once simp del: restr_delete)
166       ultimately
167
168       have "consistent (env_delete x ae, env_delete x ce, u, as, x # r) (delete x \<Gamma>, e, Upd x # S)" using thunk
169         by (auto simp add: restr_delete_twist Compl_insert elim:below_trans )
170       moreover
171
172       from *
173       have **: "Astack (transform_alts as (restr_stack (- set r) S) @ map Dummy (rev r) @ [Dummy x]) \<sqsubseteq> u" by (auto elim: a_consistent_stackD)
174       
175       {
176       from  `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` once
177       have "map_of (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (- set r) \<Gamma>))) x = Some (Aeta_expand u (transform u e))"
178         by (simp add: map_of_map_transform)
179       hence "conf_transform (ae, ce, a, as, r) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G
180              add_dummies_conf r (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (- set r) \<Gamma>))), Aeta_expand u (ccTransform u e), Upd x # transform_alts as (restr_stack (- set r) S))"
181           by (auto simp add:  map_transform_delete delete_map_transform_env_delete insert_absorb restr_delete_twist simp del: restr_delete)
182       also
183       have "\<dots> \<Rightarrow>\<^sub>G\<^sup>* add_dummies_conf (x # r) (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (- set r) \<Gamma>))), Aeta_expand u (ccTransform u e), transform_alts as (restr_stack (- set r) S))"
184         apply (rule r_into_rtranclp)
185         apply (simp add: append_assoc[symmetric] del: append_assoc)
186         apply (rule dropUpd)
187         done
188       also
189       have "\<dots> \<Rightarrow>\<^sub>G\<^sup>* add_dummies_conf (x # r) (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae  (restrictA (- set r) \<Gamma>))), ccTransform u e, transform_alts as (restr_stack (- set r) S))"
190         by simp (intro  normal_trans Aeta_expand_correct **)
191       also(rtranclp_trans)
192       have "\<dots> = conf_transform (env_delete x ae, env_delete x ce, u, as, x # r) (delete x \<Gamma>, e, Upd x # S)" 
193         by (auto intro!: map_transform_cong simp add:  map_transform_delete[symmetric]  restr_delete_twist Compl_insert)
194       finally(back_subst)
195       have "conf_transform (ae, ce, a, as, r) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (env_delete x ae, env_delete x ce, u, as, x # r) (delete x \<Gamma>, e, Upd x # S)".
196       }
197       ultimately
198       show ?thesis by (blast del: consistentI consistentE)
199   
200     next
201       case many
202   
203       from `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `\<not> isVal e`
204       have "prognosis ae as u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x \<cdot> (prognosis ae as a (\<Gamma>, Var x, S))"
205         by (rule prognosis_Var_thunk)
206       also note record_call_below_arg
207       finally
208       have *: "prognosis ae as u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> prognosis ae as a (\<Gamma>, Var x, S)" by this simp_all
209   
210       have "ae x = up\<cdot>0" using thunk many `x \<in> thunks \<Gamma>` by (auto)
211       hence "u = 0" using `ae x = up\<cdot>u` by simp
212   
213       
214       have "prognosis ae as 0 (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> ce" using *[unfolded `u=0`] thunk by (auto elim: below_trans)
215       moreover
216       have "a_consistent (ae, 0, as) (delete x (restrictA (- set r) \<Gamma>), e, Upd x # restr_stack (- set r) S)" using thunk `ae x = up\<cdot>0`
217         by (auto intro!: a_consistent_thunk_0 simp del: restr_delete)
218       ultimately
219       have "consistent (ae, ce, 0, as, r) (delete x \<Gamma>, e, Upd x # S)" using thunk `ae x = up\<cdot>u` `u = 0`
220         by (auto simp add:  restr_delete_twist)
221       moreover
222   
223       from  `map_of \<Gamma> x = Some e` `ae x = up\<cdot>0` many
224       have "map_of (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (- set r) \<Gamma>))) x = Some (transform 0 e)"
225         by (simp add: map_of_map_transform)
226       with `\<not> isVal e`
227       have "conf_transform (ae, ce, a, as, r) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 0, as, r) (delete x \<Gamma>, e, Upd x # S)"
228         by (auto intro: gc_step.intros simp add: map_transform_delete restr_delete_twist intro!: step.intros  simp del: restr_delete)
229       ultimately
230       show ?thesis by (blast del: consistentI consistentE)
231     qed
232   next
233   case (lamvar \<Gamma> x e S)
234     from lamvar(1) have [simp]: "x \<in> domA \<Gamma>" by (metis domI dom_map_of_conv_domA)
235
236     from lamvar have "prognosis ae as a (\<Gamma>, Var x, S) \<sqsubseteq> ce" by auto
237     from below_trans[OF prognosis_called fun_belowD[OF this] ]
238     have [simp]: "x \<in> edom ce" by (auto simp add: edom_def)
239     then obtain c where "ce x = up\<cdot>c" by (cases "ce x") (auto simp add: edom_def)
240
241     from lamvar
242     have [simp]: "x \<notin> set r" by auto
243
244     then have "x \<in> edom ae" using lamvar by auto
245     then obtain  u where "ae x = up\<cdot>u"  by (cases "ae x") (auto simp add: edom_def)
246
247
248     have "prognosis ae as u ((x, e) # delete x \<Gamma>, e, S) = prognosis ae as u (\<Gamma>, e, S)"
249       using `map_of \<Gamma> x = Some e` by (auto intro!: prognosis_reorder)
250     also have "\<dots> \<sqsubseteq> record_call x \<cdot> (prognosis ae as a (\<Gamma>, Var x, S))"
251        using `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `isVal e`  by (rule prognosis_Var_lam)
252     also have "\<dots> \<sqsubseteq> prognosis ae as a (\<Gamma>, Var x, S)" by (rule record_call_below_arg)
253     finally have *: "prognosis ae as u ((x, e) # delete x \<Gamma>, e, S) \<sqsubseteq> prognosis ae as a (\<Gamma>, Var x, S)" by this simp_all
254     moreover
255     have "a_consistent (ae, u, as) ((x,e) # delete x (restrictA (- set r) \<Gamma>), e, restr_stack (- set r) S)" using lamvar `ae x = up\<cdot>u`
256       by (auto intro!: a_consistent_lamvar simp del: restr_delete)
257     ultimately
258     have "consistent (ae, ce, u, as, r) ((x, e) # delete x \<Gamma>, e, S)"
259       using lamvar edom_mono[OF *] by (auto simp add:  thunks_Cons restr_delete_twist elim: below_trans)
260     moreover
261
262     from `a_consistent _ _`
263     have **: "Astack (transform_alts as (restr_stack (- set r) S) @ map Dummy (rev r)) \<sqsubseteq> u" by (auto elim: a_consistent_stackD) 
264
265     {
266     from `isVal e`
267     have "isVal (transform u e)" by simp
268     hence "isVal (Aeta_expand u (transform u e))" by (rule isVal_Aeta_expand)
269     moreover
270     from  `map_of \<Gamma> x = Some e`  `ae x = up \<cdot> u` `ce x = up\<cdot>c` `isVal (transform u e)`
271     have "map_of (map_transform Aeta_expand ae (map_transform transform ae (restrictA (- set r) \<Gamma>))) x = Some (Aeta_expand u (transform u e))"
272       by (simp add: map_of_map_transform)
273     ultimately
274     have "conf_transform (ae, ce, a, as, r) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>*
275           add_dummies_conf r ((x, Aeta_expand u (transform u e)) # delete x (map_transform Aeta_expand ae (map_transform transform ae (restrictA (- set r) \<Gamma>))), Aeta_expand u (transform u e), transform_alts as (restr_stack (- set r) S))"
276        by (auto intro!: normal_trans[OF lambda_var] simp add: map_transform_delete simp del: restr_delete)
277     also have "\<dots> = add_dummies_conf r ((map_transform Aeta_expand ae (map_transform transform ae ((x,e) # delete x (restrictA (- set r) \<Gamma>)))), Aeta_expand u  (transform u e), transform_alts as (restr_stack (- set r) S))"
278       using `ae x = up \<cdot> u` `ce x = up\<cdot>c` `isVal (transform u e)`
279       by (simp add: map_transform_Cons map_transform_delete restr_delete_twist del: restr_delete)
280     also(subst[rotated]) have "\<dots> \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae, ce, u, as, r) ((x, e) # delete x \<Gamma>, e, S)"
281       by (simp add: restr_delete_twist) (rule normal_trans[OF Aeta_expand_correct[OF ** ]])
282     finally(rtranclp_trans)
283     have "conf_transform (ae, ce, a, as, r) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae, ce, u, as, r) ((x, e) # delete x \<Gamma>, e, S)".
284     }
285     ultimately show ?case by (blast del: consistentI consistentE)
286   next
287   case (var\<^sub>2 \<Gamma> x e S)
288     show ?case
289     proof(cases "x \<in> edom ce")
290       case True[simp]
291       hence [simp]: "x \<notin> set r" using var\<^sub>2 by auto
292
293       from var\<^sub>2
294       have "a_consistent (ae, a, as) (restrictA (- set r) \<Gamma>, e, Upd x # restr_stack (-set r) S)" by auto
295       from a_consistent_UpdD[OF this]
296       have "ae x = up\<cdot>0" and "a = 0".
297   
298       from `isVal e` `x \<notin> domA \<Gamma>`
299       have *: "prognosis ae as 0 ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae as 0 (\<Gamma>, e, Upd x # S)" by (rule prognosis_Var2)
300       moreover
301       have "a_consistent (ae, a, as) ((x, e) # restrictA (- set r) \<Gamma>, e, restr_stack (- set r) S)"
302         using var\<^sub>2 by (auto intro!: a_consistent_var\<^sub>2)
303       ultimately
304       have "consistent (ae, ce, 0, as, r) ((x, e) # \<Gamma>, e, S)"
305         using var\<^sub>2 `a = 0`
306         by (auto simp add: thunks_Cons elim: below_trans)
307       moreover
308       have "conf_transform (ae, ce, a, as, r) (\<Gamma>, e, Upd x # S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 0, as, r) ((x, e) # \<Gamma>, e, S)"
309         using `ae x = up\<cdot>0` `a = 0` var\<^sub>2 
310         by (auto intro: gc_step.intros simp add: map_transform_Cons)
311       ultimately show ?thesis by (blast del: consistentI consistentE)
312     next
313       case False[simp]
314       hence "ce x = \<bottom>" using var\<^sub>2 by (auto simp add: edom_def)
315
316       from False have "x \<notin> edom ae" using var\<^sub>2 by auto
317       hence [simp]: "ae x = \<bottom>" by (auto simp add: edom_def)
318
319       from False have [simp]: "x \<in> set r" using var\<^sub>2 by auto
320       
321       have "prognosis ae as a ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae as a ((x, e) # \<Gamma>, e, Upd x # S)" by (rule prognosis_upd)
322       also have "\<dots> \<sqsubseteq> prognosis ae as a (delete x ((x,e) # \<Gamma>), e, Upd x # S)"
323         using `ae x = \<bottom>` by (rule prognosis_not_called)
324       also have "delete x ((x,e)#\<Gamma>) = \<Gamma>" using `x \<notin> domA \<Gamma>` by simp
325       finally
326       have *: "prognosis ae as a ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae as a (\<Gamma>, e, Upd x # S)" by this simp
327       then
328       have "consistent (ae, ce, a, as, r) ((x, e) # \<Gamma>, e, S)" using var\<^sub>2
329         by (auto simp add: thunks_Cons  elim:below_trans a_consistent_var\<^sub>2)
330       moreover
331       have "conf_transform (ae, ce, a, as, r) (\<Gamma>, e, Upd x # S) = conf_transform (ae, ce, a, as, r) ((x, e) # \<Gamma>, e, S)"
332         by (auto simp add: map_transform_restrA[symmetric])
333       ultimately show ?thesis
334         by (fastforce del: consistentI consistentE simp del:conf_transform.simps)
335     qed
336   next
337     case (let\<^sub>1 \<Delta> \<Gamma> e S)
338     let ?ae = "Aheap \<Delta> e\<cdot>a"
339     let ?ce = "cHeap \<Delta> e\<cdot>a"
340   
341     have "domA \<Delta> \<inter> upds S = {}" using fresh_distinct_fv[OF let\<^sub>1(2)] by (auto dest: set_mp[OF ups_fv_subset])
342     hence *: "\<And> x. x \<in> upds S \<Longrightarrow> x \<notin> edom ?ae" by (auto simp add: edom_cHeap dest!: set_mp[OF edom_Aheap])
343     have restr_stack_simp2: "restr_stack (edom (?ae \<squnion> ae)) S = restr_stack (edom ae) S"
344       by (auto intro: restr_stack_cong dest!: *)
345
346     have "edom ce = edom ae" using let\<^sub>1 by auto
347   
348     have "edom ae \<subseteq> domA \<Gamma> \<union> upds S" using let\<^sub>1 by (auto dest!: a_consistent_edom_subsetD)
349     from set_mp[OF this] fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_fv[OF let\<^sub>1(2)]
350     have "edom ae \<inter> domA \<Delta> = {}" by (auto dest: set_mp[OF ups_fv_subset])
351
352     from `edom ae \<inter> domA \<Delta> = {}`
353     have [simp]: "edom (Aheap \<Delta> e\<cdot>a) \<inter> edom ae = {}" by (auto dest!: set_mp[OF edom_Aheap]) 
354
355     from fresh_distinct[OF let\<^sub>1(1)]
356     have [simp]: "restrictA (edom ae \<union> edom (Aheap \<Delta> e\<cdot>a)) \<Gamma> = restrictA (edom ae) \<Gamma>"
357       by (auto intro: restrictA_cong dest!: set_mp[OF edom_Aheap]) 
358
359     have "set r \<subseteq> domA \<Gamma> \<union> upds S" using let\<^sub>1 by auto
360     have [simp]: "restrictA (- set r) \<Delta> = \<Delta>"
361       apply (rule restrictA_noop)
362       apply auto
363       by (metis IntI UnE `set r \<subseteq> domA \<Gamma> \<union> upds S` `domA \<Delta> \<inter> domA \<Gamma> = {}` `domA \<Delta> \<inter> upds S = {}` contra_subsetD empty_iff)
364
365     {
366     have "edom (?ae \<squnion> ae) = edom (?ce \<squnion> ce)"
367       using let\<^sub>1(4) by (auto simp add: edom_cHeap)
368     moreover
369     { fix x e'
370       assume "x \<in> thunks \<Gamma>"
371       hence "x \<notin> edom ?ce" using fresh_distinct[OF let\<^sub>1(1)]
372         by (auto simp add: edom_cHeap dest: set_mp[OF edom_Aheap]  set_mp[OF thunks_domA])
373       hence [simp]: "?ce x = \<bottom>" unfolding edomIff by auto
374     
375       assume "many \<sqsubseteq> (?ce \<squnion> ce) x"
376       with let\<^sub>1 `x \<in> thunks \<Gamma>`
377       have "(?ae \<squnion> ae) x = up \<cdot>0" by auto
378     }
379     moreover
380     { fix x e'
381       assume "x \<in> thunks \<Delta>" 
382       hence "x \<notin> domA \<Gamma>" and "x \<notin> upds S"
383         using fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_fv[OF let\<^sub>1(2)]
384         by (auto dest!: set_mp[OF thunks_domA] set_mp[OF ups_fv_subset])
385       hence "x \<notin> edom ce" using `edom ae \<subseteq> domA \<Gamma> \<union> upds S` `edom ce = edom ae` by auto
386       hence [simp]: "ce x = \<bottom>"  by (auto simp add: edomIff)
387   
388       assume "many \<sqsubseteq> (?ce \<squnion> ce) x" with `x \<in> thunks \<Delta>`
389       have "(?ae \<squnion> ae) x = up\<cdot>0" by (auto simp add: Aheap_heap3)
390     }
391     moreover
392     {
393     from let\<^sub>1(1,2) `edom ae \<subseteq> domA \<Gamma> \<union> upds S`
394     have "prognosis (?ae \<squnion> ae) as a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> ?ce \<squnion> prognosis ae as a (\<Gamma>, Let \<Delta> e, S)" by (rule prognosis_Let)
395     also have "prognosis ae as a (\<Gamma>, Let \<Delta> e, S) \<sqsubseteq> ce" using let\<^sub>1 by auto
396     finally have "prognosis (?ae \<squnion> ae) as a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> ?ce \<squnion> ce" by this simp
397     }
398     moreover
399
400     have "a_consistent (ae, a, as) (restrictA (- set r) \<Gamma>, Let \<Delta> e, restr_stack (- set r) S)"
401       using let\<^sub>1 by auto
402     hence "a_consistent (?ae \<squnion> ae, a, as) (\<Delta> @ restrictA (- set r) \<Gamma>, e, restr_stack (- set r) S)"
403       using let\<^sub>1(1,2) `edom ae \<inter> domA \<Delta> = {}` 
404       by (auto intro!:  a_consistent_let simp del: join_comm)
405     hence "a_consistent (?ae \<squnion> ae, a, as) (restrictA (- set r) (\<Delta> @ \<Gamma>), e, restr_stack (- set r) S)"
406       by (simp add: restrictA_append)
407     moreover
408     have "set r \<inter> edom ce = {}" and "upds S - edom ce \<subseteq> set r" and "set r \<subseteq> domA \<Gamma> \<union> upds S" using let\<^sub>1 by auto
409     hence "set r \<inter> edom (?ce \<squnion> ce) = {}" and "upds S - edom (?ce \<squnion> ce) \<subseteq> set r"  and "set r \<subseteq> domA \<Gamma> \<union> upds S"
410       apply (auto simp add: edom_cHeap dest!: set_mp[OF edom_Aheap])
411       by (metis IntI UnE `domA \<Delta> \<inter> domA \<Gamma> = {}` `domA \<Delta> \<inter> upds S = {}` contra_subsetD empty_iff)
412     ultimately
413     have "consistent (?ae \<squnion> ae, ?ce \<squnion> ce, a, as, r) (\<Delta> @ \<Gamma>, e, S)" by auto
414     }
415     moreover
416     {
417       have "\<And> x. x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> edom ?ae" "\<And> x. x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> edom ?ce"
418         using fresh_distinct[OF let\<^sub>1(1)]
419         by (auto simp add: edom_cHeap dest!: set_mp[OF edom_Aheap])
420       hence "map_transform Aeta_expand (?ae \<squnion> ae) (map_transform transform (?ae \<squnion> ae) (restrictA (-set r) \<Gamma>))
421          = map_transform Aeta_expand ae (map_transform transform ae (restrictA (-set r) \<Gamma>))"
422          by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
423       moreover
424   
425       from `edom ae \<subseteq> domA \<Gamma> \<union> upds S` `edom ce = edom ae`
426       have "\<And> x. x \<in> domA \<Delta> \<Longrightarrow> x \<notin> edom ce" and  "\<And> x. x \<in> domA \<Delta> \<Longrightarrow> x \<notin> edom ae"
427          using fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_ups[OF let\<^sub>1(2)]  by auto
428       hence "map_transform Aeta_expand (?ae \<squnion> ae) (map_transform transform (?ae \<squnion> ae) (restrictA (- set r) \<Delta>))
429          = map_transform Aeta_expand ?ae (map_transform transform ?ae (restrictA (- set r) \<Delta>))"
430          by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
431       moreover
432             
433       from  `domA \<Delta> \<inter> domA \<Gamma> = {}`   `domA \<Delta> \<inter> upds S = {}`
434       have "atom ` domA \<Delta> \<sharp>* set r"
435         by (auto simp add: fresh_star_def fresh_at_base fresh_finite_set_at_base dest!: set_mp[OF `set r \<subseteq> domA \<Gamma> \<union> upds S`])
436       hence "atom ` domA \<Delta> \<sharp>* map Dummy (rev r)" 
437         apply -
438         apply (rule eqvt_fresh_star_cong1[where f = "map Dummy"], perm_simp, rule)
439         apply (rule eqvt_fresh_star_cong1[where f = "rev"], perm_simp, rule)
440         apply (auto simp add: fresh_star_def fresh_set)
441         done
442       ultimately
443       
444       
445       have "conf_transform (ae, ce, a, as, r) (\<Gamma>, Let \<Delta> e, S) \<Rightarrow>\<^sub>G conf_transform (?ae \<squnion> ae, ?ce \<squnion> ce, a, as, r) (\<Delta> @ \<Gamma>, e, S)"
446         using restr_stack_simp2 let\<^sub>1(1,2)  `edom ce = edom ae`
447         apply (auto simp add: map_transform_append restrictA_append edom_cHeap restr_stack_simp2[simplified] )
448         apply (rule normal)
449         apply (rule step.let\<^sub>1)
450         apply (auto intro: normal step.let\<^sub>1 dest: set_mp[OF edom_Aheap] simp add: fresh_star_list)
451         done
452     }
453     ultimately
454     show ?case by (blast del: consistentI consistentE)
455   next
456     case (if\<^sub>1 \<Gamma> scrut e1 e2 S)
457     have "prognosis ae as a (\<Gamma>, scrut ? e1 : e2, S) \<sqsubseteq> ce" using if\<^sub>1 by auto
458     hence "prognosis ae (a#as) 0 (\<Gamma>, scrut, Alts e1 e2 # S) \<sqsubseteq> ce"
459       by (rule below_trans[OF prognosis_IfThenElse])
460     hence "consistent (ae, ce, 0, a#as, r) (\<Gamma>, scrut, Alts e1 e2 # S)"
461       using if\<^sub>1  by (auto dest: a_consistent_if\<^sub>1)
462     moreover
463     have "conf_transform (ae, ce, a, as, r) (\<Gamma>, scrut ? e1 : e2, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 0, a#as, r) (\<Gamma>, scrut, Alts e1 e2 # S)"
464       by (auto intro: normal step.intros)
465     ultimately
466     show ?case by (blast del: consistentI consistentE)
467   next
468     case (if\<^sub>2 \<Gamma> b e1 e2 S)
469     hence "a_consistent (ae, a, as) (restrictA (- set r) \<Gamma>, Bool b, Alts e1 e2 # restr_stack (-set r) S)" by auto
470     then  obtain a' as' where [simp]: "as = a' # as'" "a = 0"
471       by (rule a_consistent_alts_on_stack)
472
473     {
474     have "prognosis ae (a'#as') 0 (\<Gamma>, Bool b, Alts e1 e2 # S) \<sqsubseteq> ce" using if\<^sub>2 by auto
475     hence "prognosis ae as' a' (\<Gamma>, if b then e1 else e2, S) \<sqsubseteq> ce" by (rule below_trans[OF prognosis_Alts])
476     then
477     have "consistent (ae, ce, a', as', r) (\<Gamma>, if b then e1 else e2, S)" 
478       using if\<^sub>2 by (auto dest!: a_consistent_if\<^sub>2)
479     }
480     moreover
481     have "conf_transform (ae, ce, a, as, r) (\<Gamma>, Bool b, Alts e1 e2 # S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, a', as', r) (\<Gamma>, if b then e1 else e2, S)"
482       by (auto intro: normal step.if\<^sub>2[where b = True, simplified] step.if\<^sub>2[where b = False, simplified])
483     ultimately
484     show ?case by (blast del: consistentI consistentE)
485   next
486     case refl thus ?case by force
487   next
488     case (trans c c' c'')
489       from trans(3)[OF trans(5)]
490       obtain ae' ce' a' as' r'
491       where "consistent (ae', ce', a', as', r') c'" and *: "conf_transform (ae, ce, a, as, r) c \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae', ce', a', as', r') c'" by blast
492       from trans(4)[OF this(1)]
493       obtain ae'' ce'' a'' as'' r''
494       where "consistent (ae'', ce'', a'', as'', r'') c''" and **: "conf_transform (ae', ce', a', as', r') c' \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae'', ce'', a'', as'', r'') c''" by blast
495       from this(1) rtranclp_trans[OF * **]
496       show ?case by blast
497   qed
498 end
499
500 end