30077d547df388e02aea1a4ff4b3ffed4749b873
[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)"
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 conf_transform :: "tstate \<Rightarrow> conf \<Rightarrow> conf"
57   where "conf_transform (ae, ce, a, as) c = a_transform (ae, a, as) (restr_conf (edom ce) c)"
58
59
60   inductive consistent :: "tstate \<Rightarrow> conf \<Rightarrow> bool" where
61     consistentI[intro!]: 
62     "a_consistent (ae, a, as) (restr_conf (edom ce) (\<Gamma>, e, S))
63     \<Longrightarrow> edom ae = edom ce
64     \<Longrightarrow> prognosis ae as a (\<Gamma>, e, S) \<sqsubseteq> ce
65     \<Longrightarrow> (\<And> x. x \<in> thunks \<Gamma> \<Longrightarrow> many \<sqsubseteq> ce x \<Longrightarrow> ae x = up\<cdot>0)
66     \<Longrightarrow> consistent (ae, ce, a, as) (\<Gamma>, e, S)"  
67   inductive_cases consistentE[elim!]: "consistent (ae, ce, a, as) (\<Gamma>, e, S)"
68
69   lemma closed_consistent:
70     assumes "fv e = ({}::var set)"
71     shows "consistent (\<bottom>, \<bottom>, 0, []) ([], e, [])"
72   proof-
73     from assms
74     have "edom (prognosis \<bottom> [] 0 ([], e, [])) = {}"
75      by (auto dest!: set_mp[OF edom_prognosis])
76     thus ?thesis
77       by (auto simp add: edom_empty_iff_bot closed_a_consistent[OF assms])
78   qed
79
80   lemma foo:
81     fixes c c' R 
82     assumes "c \<Rightarrow>\<^sup>* c'" and "\<not> boring_step c'" and "consistent (ae,ce,a,as) c"
83     shows "\<exists>ae' ce' a' as'. consistent (ae',ce',a',as') c' \<and> conf_transform (ae,ce,a,as) c \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae',ce',a',as') c'"
84   using assms
85   proof(induction c c' arbitrary: ae ce a as rule:step_induction)
86   case (app\<^sub>1 \<Gamma> e x S)
87     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)
88     with app\<^sub>1 have "consistent (ae, ce, inc\<cdot>a, as) (\<Gamma>, e, Arg x # S)"
89       by (auto intro: a_consistent_app\<^sub>1 elim: below_trans)
90     moreover
91     have "conf_transform (ae, ce, a, as) (\<Gamma>, App e x, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, inc\<cdot>a, as) (\<Gamma>, e, Arg x # S)"
92       by simp rule
93     ultimately
94     show ?case by (blast del: consistentI consistentE)
95   next
96   case (app\<^sub>2 \<Gamma> y e x S)
97     have "prognosis ae as (pred\<cdot>a) (\<Gamma>, e[y::=x], S) \<sqsubseteq> prognosis ae as a (\<Gamma>, (Lam [y]. e), Arg x # S)"
98        by (rule prognosis_subst_Lam)
99     then
100     have "consistent (ae, ce, pred\<cdot>a, as) (\<Gamma>, e[y::=x], S)" using app\<^sub>2
101       by (auto 4 3 intro: a_consistent_app\<^sub>2 elim: below_trans)
102     moreover
103     have "conf_transform (ae, ce, a, as) (\<Gamma>, Lam [y]. e, Arg x # S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, pred \<cdot> a, as) (\<Gamma>, e[y::=x], S)" by (simp add: subst_transform[symmetric]) rule
104     ultimately
105     show ?case by (blast  del: consistentI consistentE)
106   next
107   case (thunk \<Gamma> x e S)
108     hence "x \<in> thunks \<Gamma>" by auto
109     hence [simp]: "x \<in> domA \<Gamma>" by (rule set_mp[OF thunks_domA])
110
111     from thunk have "prognosis ae as a (\<Gamma>, Var x, S) \<sqsubseteq> ce" by auto
112     from below_trans[OF prognosis_called fun_belowD[OF this] ]
113     have [simp]: "x \<in> edom ce" by (auto simp add: edom_def)
114
115     have "x \<notin> upds S" using thunk by (auto dest!: a_consistent_heap_upds_okD  heap_upds_okE)
116
117     have "x \<in> edom ae" using thunk by auto
118     then obtain u where "ae x = up\<cdot>u" by (cases "ae x") (auto simp add: edom_def)
119   
120
121     show ?case
122     proof(cases "ce x" rule:two_cases)
123       case none
124       with `x \<in> edom ce` have False by (auto simp add: edom_def)
125       thus ?thesis..
126     next
127       case once
128
129       from `prognosis ae as a (\<Gamma>, Var x, S) \<sqsubseteq> ce`
130       have "prognosis ae as a (\<Gamma>, Var x, S) x \<sqsubseteq> once"
131         using once by (metis (mono_tags) fun_belowD)
132       hence "x \<notin> ap S" using prognosis_ap[of ae as a \<Gamma> "(Var x)" S] by auto
133       
134   
135       from `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `\<not> isVal e`
136       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))"
137         by (rule prognosis_Var_thunk)
138   
139       from `prognosis ae as a (\<Gamma>, Var x, S) x \<sqsubseteq> once`
140       have "(record_call x \<cdot> (prognosis ae as a (\<Gamma>, Var x, S))) x = none"
141         by (simp add: two_pred_none)
142       hence **: "prognosis ae as u (delete x \<Gamma>, e, Upd x # S) x = none" using fun_belowD[OF *, where x = x] by auto
143
144       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)"
145         by (rule prognosis_env_cong) simp
146
147       have [simp]: "restr_stack (edom ce - {x}) S = restr_stack (edom ce) S" 
148         using `x \<notin> upds S` by (auto intro: restr_stack_cong)
149     
150       have "prognosis (env_delete x ae) as u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> env_delete x ce"
151         unfolding eq
152         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]
153         by (rule below_env_deleteI)
154       moreover
155
156       have *: "a_consistent (env_delete x ae, u, as) (delete x (restrictA (edom ce) \<Gamma>), e, restr_stack (edom ce) S)" using thunk `ae x = up\<cdot>u`
157           by (auto intro!: a_consistent_thunk_once simp del: restr_delete)
158       ultimately
159
160       have "consistent (env_delete x ae, env_delete x ce, u, as) (delete x \<Gamma>, e, Upd x # S)" using thunk
161         by (auto  simp add:   restr_delete_twist elim:below_trans )
162       moreover
163
164       from *
165       have "Astack (transform_alts as (restr_stack (edom ce) S)) \<sqsubseteq> u" by (auto elim: a_consistent_stackD)
166       
167       {
168       from  `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` once
169       have "map_of (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (edom ce) \<Gamma>))) x = Some (Aeta_expand u (transform u e))"
170         by (simp add: map_of_map_transform)
171       hence "conf_transform (ae, ce, a, as) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G
172              (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (edom ce) \<Gamma>))), Aeta_expand u (ccTransform u e), Upd x # transform_alts as (restr_stack (edom ce) S))"
173           by (auto simp add:  map_transform_delete delete_map_transform_env_delete insert_absorb restr_delete_twist simp del: restr_delete)
174       also
175       have "\<dots> \<Rightarrow>\<^sub>G\<^sup>* (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (edom ce) \<Gamma>))), Aeta_expand u (ccTransform u e), transform_alts as (restr_stack (edom ce) S))"
176         by (rule r_into_rtranclp, rule)
177       also
178       have "\<dots> \<Rightarrow>\<^sub>G\<^sup>* (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae  (restrictA (edom ce) \<Gamma>))), ccTransform u e, transform_alts as (restr_stack (edom ce) S))"
179         by (intro normal_trans Aeta_expand_correct `Astack (transform_alts as (restr_stack (edom ce) S)) \<sqsubseteq> u`)
180       also(rtranclp_trans)
181       have "\<dots> = conf_transform (env_delete x ae, env_delete x ce, u, as) (delete x \<Gamma>, e, Upd x # S)" 
182         by (auto intro!: map_transform_cong simp add:  map_transform_delete[symmetric]  restr_delete_twist)
183       finally(back_subst)
184       have "conf_transform (ae, ce, a, as) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (env_delete x ae, env_delete x ce, u, as) (delete x \<Gamma>, e, Upd x # S)".
185       }
186       ultimately
187       show ?thesis by (blast del: consistentI consistentE)
188   
189     next
190       case many
191   
192       from `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `\<not> isVal e`
193       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))"
194         by (rule prognosis_Var_thunk)
195       also note record_call_below_arg
196       finally
197       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
198   
199       have "ae x = up\<cdot>0" using thunk many `x \<in> thunks \<Gamma>` by (auto)
200       hence "u = 0" using `ae x = up\<cdot>u` by simp
201   
202       
203       have "prognosis ae as 0 (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> ce" using *[unfolded `u=0`] thunk by (auto elim: below_trans)
204       moreover
205       have "a_consistent (ae, 0, as) (delete x (restrictA (edom ce) \<Gamma>), e, Upd x # restr_stack (edom ce) S)" using thunk `ae x = up\<cdot>0`
206         by (auto intro!: a_consistent_thunk_0 simp del: restr_delete)
207       ultimately
208       have "consistent (ae, ce, 0, as) (delete x \<Gamma>, e, Upd x # S)" using thunk `ae x = up\<cdot>u` `u = 0`
209         by (auto simp add:  restr_delete_twist)
210       moreover
211   
212       from  `map_of \<Gamma> x = Some e` `ae x = up\<cdot>0` many
213       have "map_of (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (edom ce) \<Gamma>))) x = Some (transform 0 e)"
214         by (simp add: map_of_map_transform)
215       with `\<not> isVal e`
216       have "conf_transform (ae, ce, a, as) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 0, as) (delete x \<Gamma>, e, Upd x # S)"
217         by (auto simp add: map_transform_delete restr_delete_twist intro!: step.intros  simp del: restr_delete)
218       ultimately
219       show ?thesis by (blast del: consistentI consistentE)
220     qed
221   next
222   case (lamvar \<Gamma> x e S)
223     from lamvar(1) have [simp]: "x \<in> domA \<Gamma>" by (metis domI dom_map_of_conv_domA)
224
225     from lamvar have "prognosis ae as a (\<Gamma>, Var x, S) \<sqsubseteq> ce" by auto
226     from below_trans[OF prognosis_called fun_belowD[OF this] ]
227     have [simp]: "x \<in> edom ce" by (auto simp add: edom_def)
228     then obtain c where "ce x = up\<cdot>c" by (cases "ce x") (auto simp add: edom_def)
229
230     then have "x \<in> edom ae" using lamvar by auto
231     then obtain  u where "ae x = up\<cdot>u"  by (cases "ae x") (auto simp add: edom_def)
232
233
234     have "prognosis ae as u ((x, e) # delete x \<Gamma>, e, S) = prognosis ae as u (\<Gamma>, e, S)"
235       using `map_of \<Gamma> x = Some e` by (auto intro!: prognosis_reorder)
236     also have "\<dots> \<sqsubseteq> record_call x \<cdot> (prognosis ae as a (\<Gamma>, Var x, S))"
237        using `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `isVal e`  by (rule prognosis_Var_lam)
238     also have "\<dots> \<sqsubseteq> prognosis ae as a (\<Gamma>, Var x, S)" by (rule record_call_below_arg)
239     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
240     moreover
241     have "a_consistent (ae, u, as) ((x,e) # delete x (restrictA (edom ce) \<Gamma>), e, restr_stack (edom ce) S)" using lamvar `ae x = up\<cdot>u`
242       by (auto intro!: a_consistent_lamvar simp del: restr_delete)
243     ultimately
244     have "consistent (ae, ce, u, as) ((x, e) # delete x \<Gamma>, e, S)"
245       using lamvar edom_mono[OF *] by (auto simp add:  thunks_Cons restr_delete_twist elim: below_trans)
246     moreover
247
248     from `a_consistent _ _`
249     have "Astack (transform_alts as (restr_stack (edom ce) S)) \<sqsubseteq> u" by (auto elim: a_consistent_stackD)
250   
251     {
252     from `isVal e`
253     have "isVal (transform u e)" by simp
254     hence "isVal (Aeta_expand u (transform u e))" by (rule isVal_Aeta_expand)
255     moreover
256     from  `map_of \<Gamma> x = Some e`  `ae x = up \<cdot> u` `ce x = up\<cdot>c` `isVal (transform u e)`
257     have "map_of (map_transform Aeta_expand ae (map_transform transform ae (restrictA (edom ce) \<Gamma>))) x = Some (Aeta_expand u (transform u e))"
258       by (simp add: map_of_map_transform)
259     ultimately
260     have "conf_transform (ae, ce, a, as) (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>*
261           ((x, Aeta_expand u (transform u e)) # delete x (map_transform Aeta_expand ae (map_transform transform ae (restrictA (edom ce) \<Gamma>))), Aeta_expand u (transform u e), transform_alts as (restr_stack (edom ce) S))"
262        by (auto intro: lambda_var simp add: map_transform_delete simp del: restr_delete)
263     also have "\<dots> = ((map_transform Aeta_expand ae (map_transform transform ae ((x,e) # delete x (restrictA (edom ce) \<Gamma>)))), Aeta_expand u  (transform u e), transform_alts as (restr_stack (edom ce) S))"
264       using `ae x = up \<cdot> u` `ce x = up\<cdot>c` `isVal (transform u e)`
265       by (simp add: map_transform_Cons map_transform_delete restr_delete_twist del: restr_delete)
266     also(subst[rotated]) have "\<dots> \<Rightarrow>\<^sup>* conf_transform (ae, ce, u, as) ((x, e) # delete x \<Gamma>, e, S)"
267       by (simp add: restr_delete_twist) (rule Aeta_expand_correct[OF `Astack _ \<sqsubseteq> u`])
268     finally(rtranclp_trans)
269     have "conf_transform (ae, ce, a, as) (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* conf_transform (ae, ce, u, as) ((x, e) # delete x \<Gamma>, e, S)".
270     }
271     ultimately show ?case by (blast intro: normal_trans del: consistentI consistentE)
272   next
273   case (var\<^sub>2 \<Gamma> x e S)
274     show ?case
275     proof(cases "x \<in> edom ce")
276       case True[simp]
277       hence "ce x \<noteq> \<bottom>" using var\<^sub>2 by (auto simp add: edom_def)
278       from True have "x \<in> edom ae" using var\<^sub>2 by auto
279  
280       obtain c where "ce x = up\<cdot>c" using `ce x \<noteq> \<bottom>` by (cases "ce x") auto
281   
282       from var\<^sub>2
283       have "a_consistent (ae, a, as) (restrictA (edom ce) \<Gamma>, e, Upd x # restr_stack (edom ce) S)" by auto
284       from a_consistent_UpdD[OF this  `x \<in> edom ae`]
285       have "ae x = up\<cdot>0" and "a = 0".
286   
287       from `isVal e` `x \<notin> domA \<Gamma>`
288       have *: "prognosis ae as 0 ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae as 0 (\<Gamma>, e, Upd x # S)" by (rule prognosis_Var2)
289       moreover
290       have "a_consistent (ae, a, as) ((x, e) # restrictA (edom ce) \<Gamma>, e, restr_stack (edom ce) S)"
291         using var\<^sub>2 by (auto intro!: a_consistent_var\<^sub>2)
292       ultimately
293       have "consistent (ae, ce, 0, as) ((x, e) # \<Gamma>, e, S)"
294         using var\<^sub>2 `a = 0`
295         by (auto simp add: thunks_Cons elim: below_trans)
296       moreover
297       have "conf_transform (ae, ce, a, as) (\<Gamma>, e, Upd x # S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 0, as) ((x, e) # \<Gamma>, e, S)"
298         using `ae x = up\<cdot>0` `a = 0` var\<^sub>2 `ce x = up\<cdot>c`
299         by (auto intro!: step.intros simp add: map_transform_Cons)
300       ultimately show ?thesis by (blast del: consistentI consistentE)
301     next
302       case False[simp]
303       hence "ce x = \<bottom>" using var\<^sub>2 by (auto simp add: edom_def)
304
305       from False have "x \<notin> edom ae" using var\<^sub>2 by auto
306       hence [simp]: "ae x = \<bottom>" by (auto simp add: edom_def)
307
308       
309       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)
310       also
311        
312       from `ae x = \<bottom>`
313       have "prognosis ae as a ((x, e) # \<Gamma>, e, Upd x # S) \<sqsubseteq> prognosis ae as a (delete x ((x,e) # \<Gamma>), e, Upd x # S)"
314         by (rule prognosis_not_called)
315       also have  "delete x ((x,e)#\<Gamma>) = \<Gamma>" using `x \<notin> domA \<Gamma>` by simp
316       finally
317       have *: "prognosis ae as a ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae as a (\<Gamma>, e, Upd x # S)" by this simp
318       then
319       have "consistent (ae, ce, a, as) ((x, e) # \<Gamma>, e, S)" using var\<^sub>2
320         by (auto simp add: thunks_Cons  elim:below_trans)
321       moreover
322       have "conf_transform (ae, ce, a, as) (\<Gamma>, e, Upd x # S) = conf_transform (ae, ce, a, as) ((x, e) # \<Gamma>, e, S)"
323         by(simp add: map_transform_restrA[symmetric])
324       ultimately show ?thesis by (auto del: consistentI consistentE simp del:conf_transform.simps)
325     qed
326   next
327     case (let\<^sub>1 \<Delta> \<Gamma> e S)
328     let ?ae = "Aheap \<Delta> e\<cdot>a"
329     let ?ce = "cHeap \<Delta> e\<cdot>a"
330   
331     have "domA \<Delta> \<inter> upds S = {}" using fresh_distinct_fv[OF let\<^sub>1(2)] by (auto dest: set_mp[OF ups_fv_subset])
332     hence *: "\<And> x. x \<in> upds S \<Longrightarrow> x \<notin> edom ?ae" by (auto simp add: edom_cHeap dest!: set_mp[OF edom_Aheap])
333     have restr_stack_simp2: "restr_stack (edom (?ae \<squnion> ae)) S = restr_stack (edom ae) S"
334       by (auto intro: restr_stack_cong dest!: *)
335
336     have "edom ce = edom ae" using let\<^sub>1 by auto
337   
338     have "edom ae \<subseteq> domA \<Gamma> \<union> upds S" using let\<^sub>1 by (auto dest!: a_consistent_edom_subsetD)
339     from set_mp[OF this] fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_fv[OF let\<^sub>1(2)]
340     have "edom ae \<inter> domA \<Delta> = {}" by (auto dest: set_mp[OF ups_fv_subset])
341
342     from `edom ae \<inter> domA \<Delta> = {}`
343     have [simp]: "edom (Aheap \<Delta> e\<cdot>a) \<inter> edom ae = {}" by (auto dest!: set_mp[OF edom_Aheap]) 
344
345     from fresh_distinct[OF let\<^sub>1(1)]
346     have [simp]: "restrictA (edom ae \<union> edom (Aheap \<Delta> e\<cdot>a)) \<Gamma> = restrictA (edom ae) \<Gamma>"
347       by (auto intro: restrictA_cong dest!: set_mp[OF edom_Aheap]) 
348
349     {
350     have "edom (?ae \<squnion> ae) = edom (?ce \<squnion> ce)"
351       using let\<^sub>1(3) by (auto simp add: edom_cHeap)
352     moreover
353     { fix x e'
354       assume "x \<in> thunks \<Gamma>"
355       hence "x \<notin> edom ?ce" using fresh_distinct[OF let\<^sub>1(1)]
356         by (auto simp add: edom_cHeap dest: set_mp[OF edom_Aheap]  set_mp[OF thunks_domA])
357       hence [simp]: "?ce x = \<bottom>" unfolding edomIff by auto
358     
359       assume "many \<sqsubseteq> (?ce \<squnion> ce) x"
360       with let\<^sub>1 `x \<in> thunks \<Gamma>`
361       have "(?ae \<squnion> ae) x = up \<cdot>0" by auto
362     }
363     moreover
364     { fix x e'
365       assume "x \<in> thunks \<Delta>" 
366       hence "x \<notin> domA \<Gamma>" and "x \<notin> upds S"
367         using fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_fv[OF let\<^sub>1(2)]
368         by (auto dest!: set_mp[OF thunks_domA] set_mp[OF ups_fv_subset])
369       hence "x \<notin> edom ce" using `edom ae \<subseteq> domA \<Gamma> \<union> upds S` `edom ce = edom ae` by auto
370       hence [simp]: "ce x = \<bottom>"  by (auto simp add: edomIff)
371   
372       assume "many \<sqsubseteq> (?ce \<squnion> ce) x" with `x \<in> thunks \<Delta>`
373       have "(?ae \<squnion> ae) x = up\<cdot>0" by (auto simp add: Aheap_heap3)
374     }
375     moreover
376     {
377     from let\<^sub>1(1,2) `edom ae \<subseteq> domA \<Gamma> \<union> upds S`
378     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)
379     also have "prognosis ae as a (\<Gamma>, Let \<Delta> e, S) \<sqsubseteq> ce" using let\<^sub>1 by auto
380     finally have "prognosis (?ae \<squnion> ae) as a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> ?ce \<squnion> ce" by this simp
381     }
382     moreover
383     
384     have "a_consistent (ae, a, as) (restrictA (edom ce) \<Gamma>, Let \<Delta> e, restr_stack (edom ce) S)"
385       using let\<^sub>1 by auto
386     hence "a_consistent (?ae \<squnion> ae, a, as) (\<Delta> @ restrictA (edom ce) \<Gamma>, e, restr_stack (edom ce) S)"
387       using let\<^sub>1(1,2) `edom ae \<inter> domA \<Delta> = {}` 
388       by (auto intro!:  a_consistent_let simp del: join_comm)
389     hence "a_consistent (?ae \<squnion> ae, a, as) (restrictA (edom (?ae \<squnion> ae)) (\<Delta> @ restrictA (edom ce) \<Gamma>), e, restr_stack (edom ce) S)"
390       by (rule a_consistent_restrictA[OF _ order_refl])
391     hence "a_consistent (?ae \<squnion> ae, a, as) (restrictA (edom (?ce \<squnion> ce)) (\<Delta> @ \<Gamma>), e, restr_stack (edom (?ce \<squnion> ce)) S)"
392       by (simp add: restrictA_append restr_stack_simp2[simplified] edom_cHeap `edom ce = edom ae` Int_Un_distrib2)
393     ultimately
394     have "consistent (?ae \<squnion> ae, ?ce \<squnion> ce, a, as) (\<Delta> @ \<Gamma>, e, S)"
395       by auto
396     }
397     moreover
398     {
399       have "\<And> x. x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> edom ?ae" "\<And> x. x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> edom ?ce"
400         using fresh_distinct[OF let\<^sub>1(1)]
401         by (auto simp add: edom_cHeap dest!: set_mp[OF edom_Aheap])
402       hence "map_transform Aeta_expand (?ae \<squnion> ae) (map_transform transform (?ae \<squnion> ae) (restrictA (edom (?ce \<squnion> ce)) \<Gamma>))
403          = map_transform Aeta_expand ae (map_transform transform ae (restrictA (edom ce) \<Gamma>))"
404          by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
405       moreover
406   
407       from `edom ae \<subseteq> domA \<Gamma> \<union> upds S` `edom ce = edom ae`
408       have "\<And> x. x \<in> domA \<Delta> \<Longrightarrow> x \<notin> edom ce" and  "\<And> x. x \<in> domA \<Delta> \<Longrightarrow> x \<notin> edom ae"
409          using fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_fv[OF let\<^sub>1(2)] 
410          by (auto dest!:  set_mp[OF ups_fv_subset])
411       hence "map_transform Aeta_expand (?ae \<squnion> ae) (map_transform transform (?ae \<squnion> ae) (restrictA (edom (?ce \<squnion> ce)) \<Delta>))
412          = map_transform Aeta_expand ?ae (map_transform transform ?ae (restrictA (edom ?ce) \<Delta>))"
413          by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
414       ultimately
415       
416       
417       have "conf_transform (ae, ce, a, as) (\<Gamma>, Let \<Delta> e, S) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (?ae \<squnion> ae, ?ce \<squnion> ce, a, as) (\<Delta> @ \<Gamma>, e, S)"
418         using restr_stack_simp2 let\<^sub>1(1,2) `edom ce = edom ae`
419         apply (auto simp add: map_transform_append restrictA_append edom_cHeap restr_stack_simp2[simplified] map_transform_restrA)
420         apply (rule let_and_restrict)
421         apply (auto dest: set_mp[OF edom_Aheap])
422         done
423     }
424     ultimately
425     show ?case by (blast del: consistentI consistentE)
426   next
427     case (if\<^sub>1 \<Gamma> scrut e1 e2 S)
428     have "prognosis ae as a (\<Gamma>, scrut ? e1 : e2, S) \<sqsubseteq> ce" using if\<^sub>1 by auto
429     hence "prognosis ae (a#as) 0 (\<Gamma>, scrut, Alts e1 e2 # S) \<sqsubseteq> ce"
430       by (rule below_trans[OF prognosis_IfThenElse])
431     hence "consistent (ae, ce, 0, a#as) (\<Gamma>, scrut, Alts e1 e2 # S)"
432       using if\<^sub>1  by (auto dest: a_consistent_if\<^sub>1)
433     moreover
434     have "conf_transform (ae, ce, a, as) (\<Gamma>, scrut ? e1 : e2, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 0, a#as) (\<Gamma>, scrut, Alts e1 e2 # S)"
435       by (auto intro: normal step.intros)
436     ultimately
437     show ?case by (blast del: consistentI consistentE)
438   next
439     case (if\<^sub>2 \<Gamma> b e1 e2 S)
440     hence "a_consistent (ae, a, as) (restrictA (edom ce) \<Gamma>, Bool b, Alts e1 e2 # restr_stack (edom ce) S)" by auto
441     then  obtain a' as' where [simp]: "as = a' # as'" "a = 0"
442       by (rule a_consistent_alts_on_stack)
443
444     {
445     have "prognosis ae (a'#as') 0 (\<Gamma>, Bool b, Alts e1 e2 # S) \<sqsubseteq> ce" using if\<^sub>2 by auto
446     hence "prognosis ae as' a' (\<Gamma>, if b then e1 else e2, S) \<sqsubseteq> ce" by (rule below_trans[OF prognosis_Alts])
447     then
448     have "consistent (ae, ce, a', as') (\<Gamma>, if b then e1 else e2, S)" 
449       using if\<^sub>2 by (auto dest!: a_consistent_if\<^sub>2)
450     }
451     moreover
452     have "conf_transform (ae, ce, a, as) (\<Gamma>, Bool b, Alts e1 e2 # S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, a', as') (\<Gamma>, if b then e1 else e2, S)"
453       by (auto intro:normal  step.if\<^sub>2[where b = True, simplified] step.if\<^sub>2[where b = False, simplified])
454     ultimately
455     show ?case by (blast del: consistentI consistentE)
456   next
457     case refl thus ?case by auto
458   next
459     case (trans c c' c'')
460       from trans(3)[OF trans(5)]
461       obtain ae' ce' a' as' where "consistent (ae', ce', a', as') c'" and *: "conf_transform (ae, ce, a, as) c \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae', ce', a', as') c'" by blast
462       from trans(4)[OF this(1)]
463       obtain ae'' ce'' a'' as'' where "consistent (ae'', ce'', a'', as'') c''" and **: "conf_transform (ae', ce', a', as') c' \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae'', ce'', a'', as'') c''" by blast
464       from this(1) rtranclp_trans[OF * **]
465       show ?case by blast
466   qed
467 end
468
469 end