Separate Arity consistency from Cardinality consistency
[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> heap_upds_ok (\<Gamma>, S)
64     \<Longrightarrow> edom ae = edom ce
65     \<Longrightarrow> prognosis ae as a (\<Gamma>, e, S) \<sqsubseteq> ce
66     \<Longrightarrow> (\<And> x. x \<in> thunks \<Gamma> \<Longrightarrow> many \<sqsubseteq> ce x \<Longrightarrow> ae x = up\<cdot>0)
67     \<Longrightarrow> consistent (ae, ce, a, as) (\<Gamma>, e, S)"  
68   inductive_cases consistentE[elim!]: "consistent (ae, ce, a, as) (\<Gamma>, e, S)"
69
70   lemma closed_consistent:
71     assumes "fv e = ({}::var set)"
72     shows "consistent (\<bottom>, \<bottom>, 0, []) ([], e, [])"
73   proof-
74     from assms
75     have "edom (prognosis \<bottom> [] 0 ([], e, [])) = {}"
76      by (auto dest!: set_mp[OF edom_prognosis])
77     thus ?thesis
78       by (auto simp add: edom_empty_iff_bot closed_a_consistent[OF assms])
79   qed
80
81   lemma foo:
82     fixes c c' R 
83     assumes "c \<Rightarrow>\<^sup>* c'" and "\<not> boring_step c'" and "consistent (ae,ce,a,as) c"
84     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'"
85   using assms
86   proof(induction c c' arbitrary: ae ce a as rule:step_induction)
87   case (app\<^sub>1 \<Gamma> e x S)
88     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)
89     with app\<^sub>1 have "consistent (ae, ce, inc\<cdot>a, as) (\<Gamma>, e, Arg x # S)"
90       by (auto intro: a_consistent_app\<^sub>1 elim: below_trans)
91     moreover
92     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)"
93       by simp rule
94     ultimately
95     show ?case by (blast del: consistentI consistentE)
96   next
97   case (app\<^sub>2 \<Gamma> y e x S)
98     have "prognosis ae as (pred\<cdot>a) (\<Gamma>, e[y::=x], S) \<sqsubseteq> prognosis ae as a (\<Gamma>, (Lam [y]. e), Arg x # S)"
99        by (rule prognosis_subst_Lam)
100     then
101     have "consistent (ae, ce, pred\<cdot>a, as) (\<Gamma>, e[y::=x], S)" using app\<^sub>2
102       by (auto 4 3 intro: a_consistent_app\<^sub>2 elim: below_trans)
103     moreover
104     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
105     ultimately
106     show ?case by (blast  del: consistentI consistentE)
107   next
108   case (thunk \<Gamma> x e S)
109     hence "x \<in> thunks \<Gamma>" by auto
110     hence [simp]: "x \<in> domA \<Gamma>" by (rule set_mp[OF thunks_domA])
111     hence "x \<notin> upds S" using thunk by (auto elim!: heap_upds_okE)
112
113     from thunk have "prognosis ae as a (\<Gamma>, Var x, S) \<sqsubseteq> ce" by auto
114     from below_trans[OF prognosis_called fun_belowD[OF this] ]
115     have [simp]: "x \<in> edom ce" by (auto simp add: edom_def)
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     have "heap_upds_ok (\<Gamma>, S)" using let\<^sub>1 by auto
384     with fresh_distinct[OF let\<^sub>1(1)]  `domA \<Delta> \<inter> upds S = {}`
385     have "heap_upds_ok (\<Delta> @ \<Gamma>, S)" by (rule heap_upds_ok_append)
386     moreover
387     
388     have "a_consistent (ae, a, as) (restrictA (edom ce) \<Gamma>, Let \<Delta> e, restr_stack (edom ce) S)"
389       using let\<^sub>1 by auto
390     hence "a_consistent (?ae \<squnion> ae, a, as) (\<Delta> @ restrictA (edom ce) \<Gamma>, e, restr_stack (edom ce) S)"
391       using let\<^sub>1(1,2) `edom ae \<inter> domA \<Delta> = {}` 
392       by (auto intro!:  a_consistent_let simp del: join_comm)
393     hence "a_consistent (?ae \<squnion> ae, a, as) (restrictA (edom (?ae \<squnion> ae)) (\<Delta> @ restrictA (edom ce) \<Gamma>), e, restr_stack (edom ce) S)"
394       by (rule a_consistent_restrictA[OF _ order_refl])
395     hence "a_consistent (?ae \<squnion> ae, a, as) (restrictA (edom (?ce \<squnion> ce)) (\<Delta> @ \<Gamma>), e, restr_stack (edom (?ce \<squnion> ce)) S)"
396       by (simp add: restrictA_append restr_stack_simp2[simplified] edom_cHeap `edom ce = edom ae` Int_Un_distrib2)
397     ultimately
398     have "consistent (?ae \<squnion> ae, ?ce \<squnion> ce, a, as) (\<Delta> @ \<Gamma>, e, S)"
399       by auto
400     }
401     moreover
402     {
403       have "\<And> x. x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> edom ?ae" "\<And> x. x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> edom ?ce"
404         using fresh_distinct[OF let\<^sub>1(1)]
405         by (auto simp add: edom_cHeap dest!: set_mp[OF edom_Aheap])
406       hence "map_transform Aeta_expand (?ae \<squnion> ae) (map_transform transform (?ae \<squnion> ae) (restrictA (edom (?ce \<squnion> ce)) \<Gamma>))
407          = map_transform Aeta_expand ae (map_transform transform ae (restrictA (edom ce) \<Gamma>))"
408          by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
409       moreover
410   
411       from `edom ae \<subseteq> domA \<Gamma> \<union> upds S` `edom ce = edom ae`
412       have "\<And> x. x \<in> domA \<Delta> \<Longrightarrow> x \<notin> edom ce" and  "\<And> x. x \<in> domA \<Delta> \<Longrightarrow> x \<notin> edom ae"
413          using fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_fv[OF let\<^sub>1(2)] 
414          by (auto dest!:  set_mp[OF ups_fv_subset])
415       hence "map_transform Aeta_expand (?ae \<squnion> ae) (map_transform transform (?ae \<squnion> ae) (restrictA (edom (?ce \<squnion> ce)) \<Delta>))
416          = map_transform Aeta_expand ?ae (map_transform transform ?ae (restrictA (edom ?ce) \<Delta>))"
417          by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
418       ultimately
419       
420       
421       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)"
422         using restr_stack_simp2 let\<^sub>1(1,2) `edom ce = edom ae`
423         apply (auto simp add: map_transform_append restrictA_append edom_cHeap restr_stack_simp2[simplified] map_transform_restrA)
424         apply (rule let_and_restrict)
425         apply (auto dest: set_mp[OF edom_Aheap])
426         done
427     }
428     ultimately
429     show ?case by (blast del: consistentI consistentE)
430   next
431     case (if\<^sub>1 \<Gamma> scrut e1 e2 S)
432     have "prognosis ae as a (\<Gamma>, scrut ? e1 : e2, S) \<sqsubseteq> ce" using if\<^sub>1 by auto
433     hence "prognosis ae (a#as) 0 (\<Gamma>, scrut, Alts e1 e2 # S) \<sqsubseteq> ce"
434       by (rule below_trans[OF prognosis_IfThenElse])
435     hence "consistent (ae, ce, 0, a#as) (\<Gamma>, scrut, Alts e1 e2 # S)"
436       using if\<^sub>1  by (auto dest: a_consistent_if\<^sub>1)
437     moreover
438     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)"
439       by (auto intro: normal step.intros)
440     ultimately
441     show ?case by (blast del: consistentI consistentE)
442   next
443     case (if\<^sub>2 \<Gamma> b e1 e2 S)
444     hence "a_consistent (ae, a, as) (restrictA (edom ce) \<Gamma>, Bool b, Alts e1 e2 # restr_stack (edom ce) S)" by auto
445     then  obtain a' as' where [simp]: "as = a' # as'" "a = 0"
446       by (rule a_consistent_alts_on_stack)
447
448     {
449     have "prognosis ae (a'#as') 0 (\<Gamma>, Bool b, Alts e1 e2 # S) \<sqsubseteq> ce" using if\<^sub>2 by auto
450     hence "prognosis ae as' a' (\<Gamma>, if b then e1 else e2, S) \<sqsubseteq> ce" by (rule below_trans[OF prognosis_Alts])
451     then
452     have "consistent (ae, ce, a', as') (\<Gamma>, if b then e1 else e2, S)" 
453       using if\<^sub>2 by (auto dest!: a_consistent_if\<^sub>2)
454     }
455     moreover
456     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)"
457       by (auto intro:normal  step.if\<^sub>2[where b = True, simplified] step.if\<^sub>2[where b = False, simplified])
458     ultimately
459     show ?case by (blast del: consistentI consistentE)
460   next
461     case refl thus ?case by auto
462   next
463     case (trans c c' c'')
464       from trans(3)[OF trans(5)]
465       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
466       from trans(4)[OF this(1)]
467       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
468       from this(1) rtranclp_trans[OF * **]
469       show ?case by blast
470   qed
471 end
472
473 end