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