3b1cb7b682eaf9ffd51a95037b97c8e47b0f8e2b
[darcs-mirror-isa-launchbury.git] / Launchbury / CardinalityEtaExpandCorrect.thy
1 theory CardinalityEtaExpandCorrect
2 imports ArityEtaExpand CardinalityAnalysisSpec AbstractTransform Sestoft SestoftGC ArityEtaExpansionSestoft ArityAnalysisStack 
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 conf_transform :: "tstate \<Rightarrow> conf \<Rightarrow> conf"
48   where "conf_transform (ae, ce, a, as) (\<Gamma>, e, S) =
49     (restrictA (edom ce) (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>)), 
50      ccTransform a e,
51      transform_alts as (restr_stack (edom ce) S))"
52
53   inductive stack_consistent :: "Arity list \<Rightarrow> stack \<Rightarrow> bool"
54     where 
55       "stack_consistent [] []"
56     | "Astack S \<sqsubseteq> a \<Longrightarrow> stack_consistent as S \<Longrightarrow> stack_consistent (a#as) (Alts e1 e2 # S)"
57     | "stack_consistent as S \<Longrightarrow> stack_consistent as (Upd x # S)"
58     | "stack_consistent as S \<Longrightarrow> stack_consistent as (Arg x # S)"
59   inductive_simps stack_consistent_foo[simp]:
60     "stack_consistent [] []" "stack_consistent (a#as) (Alts e1 e2 # S)" "stack_consistent as (Upd x # S)" "stack_consistent as (Arg x # S)"
61   inductive_cases [elim!]: "stack_consistent as (Alts e1 e2 # S)"
62
63   inductive consistent :: "tstate \<Rightarrow> conf \<Rightarrow> bool" where
64     consistentI[intro!]: 
65     "edom ce \<subseteq> domA \<Gamma> \<union> upds S
66     \<Longrightarrow> heap_upds_ok (\<Gamma>, S)
67     \<Longrightarrow> edom ae = edom ce
68     \<Longrightarrow> Astack (restr_stack (edom ce) S) \<sqsubseteq> a
69     \<Longrightarrow> prognosis ae as a (\<Gamma>, e, S) \<sqsubseteq> ce
70     \<Longrightarrow> (ABinds \<Gamma>\<cdot>ae \<squnion> Aexp e\<cdot>a \<squnion> AEstack as S) f|` edom ce \<sqsubseteq> ae
71     \<Longrightarrow> (\<And> x. x \<in> thunks \<Gamma> \<Longrightarrow> many \<sqsubseteq> ce x \<Longrightarrow> ae x = up\<cdot>0)
72     \<Longrightarrow> stack_consistent as (restr_stack (edom ce) S)
73     \<Longrightarrow> consistent (ae, ce, a, as) (\<Gamma>, e, S)"  
74   inductive_cases consistentE[elim!]: "consistent (ae, ce, a, as) (\<Gamma>, e, S)"
75
76   lemma closed_consistent:
77     assumes "fv e = ({}::var set)"
78     shows "consistent (\<bottom>, \<bottom>, 0, []) ([], e, [])"
79   proof-
80     from assms
81     have "edom (Aexp e\<cdot>0) = {}"
82       by (auto dest!: set_mp[OF Aexp_edom])
83     moreover
84     from assms
85     have "edom (prognosis \<bottom> [] 0 ([], e, [])) = {}"
86      by (auto dest!: set_mp[OF edom_prognosis])
87     ultimately
88     show ?thesis
89       by (auto simp add: edom_empty_iff_bot)
90   qed
91
92   lemma foo:
93     fixes c c' R 
94     assumes "c \<Rightarrow>\<^sup>* c'" and "\<not> boring_step c'" and "consistent (ae,ce,a,as) c"
95     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'"
96   using assms
97   proof(induction c c' arbitrary: ae ce a as rule:step_induction)
98   case (app\<^sub>1 \<Gamma> e x S)
99     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)
100     with app\<^sub>1 have "consistent (ae, ce, inc\<cdot>a, as) (\<Gamma>, e, Arg x # S)"
101       by (cases "x \<in> edom ce") (auto simp add: join_below_iff env_restr_join dest!: below_trans[OF env_restr_mono[OF Aexp_App]] elim: below_trans)
102     moreover
103     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)"
104       by simp rule
105     ultimately
106     show ?case by (blast del: consistentI consistentE)
107   next
108   case (app\<^sub>2 \<Gamma> y e x S)
109     have "prognosis ae as (pred\<cdot>a) (\<Gamma>, e[y::=x], S) \<sqsubseteq> prognosis ae as a (\<Gamma>, (Lam [y]. e), Arg x # S)"
110        by (rule prognosis_subst_Lam)
111     moreover
112     {
113     have "Aexp (e[y::=x])\<cdot>(pred\<cdot>a) f|` edom ce  \<sqsubseteq> (env_delete y ((Aexp e)\<cdot>(pred\<cdot>a)) \<squnion> esing x\<cdot>(up\<cdot>0)) f|` edom ce" by (rule env_restr_mono[OF Aexp_subst])
114     also have "\<dots> =  env_delete y ((Aexp e)\<cdot>(pred\<cdot>a))  f|` edom ce \<squnion> esing x\<cdot>(up\<cdot>0)  f|` edom ce" by (simp add: env_restr_join)
115     also have "env_delete y ((Aexp e)\<cdot>(pred\<cdot>a)) \<sqsubseteq> Aexp (Lam [y]. e)\<cdot>a" by (rule Aexp_Lam)
116     also have "\<dots> f|` edom ce \<sqsubseteq> ae" using app\<^sub>2 by (auto simp add: join_below_iff env_restr_join)
117     also have "esing x\<cdot>(up\<cdot>0) f|` edom ce  \<sqsubseteq> ae" using app\<^sub>2
118       by (cases "x\<in>edom ce") (auto simp add: env_restr_join join_below_iff)
119     also have "ae \<squnion> ae = ae" by simp
120     finally  have "Aexp (e[y::=x])\<cdot>(pred\<cdot>a) f|` edom ce \<sqsubseteq> ae" by this simp_all
121     }
122     ultimately
123     have "consistent (ae, ce, pred\<cdot>a, as) (\<Gamma>, e[y::=x], S)" using app\<^sub>2
124       by (auto elim: below_trans edom_mono  simp add: join_below_iff env_restr_join)
125     moreover
126     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
127     ultimately
128     show ?case by (blast  del: consistentI consistentE)
129   next
130   case (thunk \<Gamma> x e S)
131     hence "x \<in> thunks \<Gamma>" by auto
132     hence [simp]: "x \<in> domA \<Gamma>" by (rule set_mp[OF thunks_domA])
133     hence "x \<notin> upds S" using thunk by (auto elim!: heap_upds_okE)
134
135     from thunk have "prognosis ae as a (\<Gamma>, Var x, S) \<sqsubseteq> ce" by auto
136     from below_trans[OF prognosis_called fun_belowD[OF this] ]
137     have [simp]: "x \<in> edom ce" by (auto simp add: edom_def)
138   
139     from thunk
140     have "Aexp (Var x)\<cdot>a  f|` edom ce \<sqsubseteq> ae" by (auto simp add: join_below_iff env_restr_join)
141     from fun_belowD[where x = x, OF this] 
142     have "(Aexp (Var x)\<cdot>a) x \<sqsubseteq> ae x" by simp
143     from below_trans[OF  Aexp_Var this]
144     have "up\<cdot>a \<sqsubseteq> ae x".    
145     then obtain u where "ae x = up\<cdot>u" and "a \<sqsubseteq> u" by (cases "ae x") auto
146     hence [simp]: "x \<in> edom ae" by (simp add: edom_def)
147
148     have "Astack (restr_stack (edom ce) S) \<sqsubseteq> u" using thunk `a \<sqsubseteq> u` by (auto elim: below_trans)
149   
150     from Abinds_reorder1[OF `map_of \<Gamma> x = Some e`] `ae x = up\<cdot>u`
151     have "ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u = ABinds \<Gamma>\<cdot>ae" by (auto intro: join_comm)
152     moreover have "(\<dots> \<squnion> AEstack as S) f|` edom ce \<sqsubseteq> ae" using thunk by (auto simp add: join_below_iff env_restr_join)
153     ultimately have "(ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u \<squnion> AEstack as S) f|` edom ce \<sqsubseteq> ae" by simp
154
155     show ?case
156     proof(cases "ce x" rule:two_cases)
157       case none
158       with `x \<in> edom ce` have False by (auto simp add: edom_def)
159       thus ?thesis..
160     next
161       case once
162
163       note `ae x = up\<cdot>u` 
164       moreover
165   
166       from `prognosis ae as a (\<Gamma>, Var x, S) \<sqsubseteq> ce`
167       have "prognosis ae as a (\<Gamma>, Var x, S) x \<sqsubseteq> once"
168         using once by (metis (mono_tags) fun_belowD)
169       hence "x \<notin> ap S" using prognosis_ap[of ae as a \<Gamma> "(Var x)" S] by auto
170       
171   
172       from `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `\<not> isVal e`
173       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))"
174         by (rule prognosis_Var_thunk)
175   
176       from `prognosis ae as a (\<Gamma>, Var x, S) x \<sqsubseteq> once`
177       have "(record_call x \<cdot> (prognosis ae as a (\<Gamma>, Var x, S))) x = none"
178         by (simp add: two_pred_none)
179       hence **: "prognosis ae as u (delete x \<Gamma>, e, Upd x # S) x = none" using fun_belowD[OF *, where x = x] by auto
180
181       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)"
182         by (rule prognosis_env_cong) simp
183
184       have [simp]: "restr_stack (edom ce - {x}) S = restr_stack (edom ce) S" 
185         using `x \<notin> upds S` by (auto intro: restr_stack_cong)
186     
187       have "prognosis (env_delete x ae) as u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> env_delete x ce"
188         unfolding eq
189         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]
190         by (rule below_env_deleteI)
191       moreover
192
193       have "ABinds (delete x \<Gamma>)\<cdot>(env_delete x ae) = ABinds (delete x \<Gamma>)\<cdot>ae" by (rule Abinds_env_cong) simp
194       with `(ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u \<squnion> AEstack as S) f|\` edom ce \<sqsubseteq> ae`
195       have "(ABinds (delete x \<Gamma>)\<cdot>(env_delete x ae) \<squnion> Aexp e\<cdot>u  \<squnion> AEstack as S) f|` edom ce \<sqsubseteq> ae" by simp
196       from env_restr_mono[where S = "-{x}", OF this]
197       have "(ABinds (delete x \<Gamma>)\<cdot>(env_delete x ae) \<squnion> Aexp e\<cdot>u  \<squnion> AEstack as S) f|` edom (env_delete x ce) \<sqsubseteq> env_delete x ae"
198         by (auto simp add: Diff_eq Int_commute env_delete_restr)
199
200       ultimately
201
202       have "consistent (env_delete x ae, env_delete x ce, u, as) (delete x \<Gamma>, e, Upd x # S)" using thunk `a \<sqsubseteq> u`
203         by (auto simp add: join_below_iff env_restr_join insert_absorb restr_delete_twist elim:below_trans below_trans[OF env_restr_mono2, rotated])
204         
205         
206       moreover
207
208       from `Astack (restr_stack (edom ce) S) \<sqsubseteq> u`
209       have "Astack (transform_alts as (restr_stack (edom ce) S)) \<sqsubseteq> u" by simp
210       
211       {
212       from  `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` once
213       have "map_of (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>)) x = Some (Aeta_expand u (transform u e))"
214         by (simp add: map_of_map_transform)
215       hence "conf_transform (ae, ce, a, as) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G
216              (restrictA (edom ce) (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>))), Aeta_expand u (ccTransform u e), Upd x # transform_alts as (restr_stack (edom ce) S))"
217           by (auto simp add:  map_transform_delete delete_map_transform_env_delete insert_absorb restr_delete_twist simp del: restr_delete)
218       also
219       have "\<dots> \<Rightarrow>\<^sub>G\<^sup>* (restrictA (edom ce) (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>))), Aeta_expand u (ccTransform u e), transform_alts as (restr_stack (edom ce) S))"
220         by (rule r_into_rtranclp, rule)
221       also
222       have "\<dots> \<Rightarrow>\<^sub>G\<^sup>* (restrictA (edom ce)  (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>))), ccTransform u e, transform_alts as (restr_stack (edom ce) S))"
223         by (intro normal_trans Aeta_expand_correct `Astack (transform_alts as (restr_stack (edom ce) S)) \<sqsubseteq> u`)
224       also(rtranclp_trans)
225       have "\<dots> = conf_transform (env_delete x ae, env_delete x ce, u, as) (delete x \<Gamma>, e, Upd x # S)" 
226         by (auto simp add:  map_transform_delete delete_map_transform_env_delete insert_absorb restr_delete_twist)
227       finally(back_subst)
228       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)".
229       }
230       ultimately
231       show ?thesis by (blast del: consistentI consistentE)
232   
233     next
234       case many
235   
236       from `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `\<not> isVal e`
237       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))"
238         by (rule prognosis_Var_thunk)
239       also note record_call_below_arg
240       finally
241       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
242   
243       have "ae x = up\<cdot>0" using thunk many `x \<in> thunks \<Gamma>` by (auto)
244       hence "u = 0" using `ae x = up\<cdot>u` by simp
245   
246       
247       have "prognosis ae as 0 (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> ce" using *[unfolded `u=0`] thunk by (auto elim: below_trans)
248       moreover
249       note `(ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u  \<squnion> AEstack as S) f|\` edom ce \<sqsubseteq> ae`
250       ultimately
251       have "consistent (ae, ce, 0, as) (delete x \<Gamma>, e, Upd x # S)" using thunk `ae x = up\<cdot>u` `u = 0`
252         by (auto simp add: env_restr_join join_below_iff)
253       moreover
254   
255       from  `map_of \<Gamma> x = Some e` `ae x = up\<cdot>0` many
256       have "map_of (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>)) x = Some (transform 0 e)"
257         by (simp add: map_of_map_transform)
258       with `\<not> isVal e`
259       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)"
260         by (auto simp add: map_transform_delete restr_delete_twist intro!: step.intros  simp del: restr_delete)
261       ultimately
262       show ?thesis by (blast del: consistentI consistentE)
263     qed
264   next
265   case (lamvar \<Gamma> x e S)
266     from lamvar have "prognosis ae as a (\<Gamma>, Var x, S) \<sqsubseteq> ce" by auto
267     from below_trans[OF prognosis_called fun_belowD[OF this] ]
268     have [simp]: "x \<in> edom ce" by (auto simp add: edom_def)
269     then obtain c where "ce x = up\<cdot>c" by (cases "ce x") (auto simp add: edom_def)
270
271     from lamvar have [simp]: "x \<in> domA \<Gamma>" by auto (metis domI dom_map_of_conv_domA)
272     from lamvar have "Aexp (Var x)\<cdot>a f|` edom ce \<sqsubseteq> ae" by (auto simp add: join_below_iff env_restr_join)
273     from fun_belowD[where x = x, OF this] 
274     have "(Aexp (Var x)\<cdot>a) x \<sqsubseteq> ae x" by simp
275     from below_trans[OF Aexp_Var this]
276     have "up\<cdot>a \<sqsubseteq> ae x".
277     then obtain u where "ae x = up\<cdot>u" and "a \<sqsubseteq> u" by (cases "ae x") auto
278     hence "x \<in> edom ae" by (auto simp add: edom_def)
279
280     from Abinds_reorder1[OF `map_of \<Gamma> x = Some e`] `ae x = up\<cdot>u`
281     have "ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u = ABinds \<Gamma>\<cdot>ae" by (auto intro: join_comm)
282     moreover have "\<dots> f|` edom ce \<sqsubseteq> ae" using lamvar by (auto simp add: join_below_iff env_restr_join)
283     ultimately have "(ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u) f|` edom ce \<sqsubseteq> ae" by simp
284
285     have "prognosis ae as u ((x, e) # delete x \<Gamma>, e, S) = prognosis ae as u (\<Gamma>, e, S)"
286       using `map_of \<Gamma> x = Some e` by (auto intro!: prognosis_reorder)
287     also have "\<dots> \<sqsubseteq> record_call x \<cdot> (prognosis ae as a (\<Gamma>, Var x, S))"
288        using `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `isVal e`  by (rule prognosis_Var_lam)
289     also have "\<dots> \<sqsubseteq> prognosis ae as a (\<Gamma>, Var x, S)" by (rule record_call_below_arg)
290     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
291   
292     have "consistent (ae, ce, u, as) ((x, e) # delete x \<Gamma>, e, S)"
293       using lamvar `(ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u) f|\` edom ce \<sqsubseteq> ae`   `ae x = up\<cdot>u` edom_mono[OF *]
294       by (auto simp add: join_below_iff env_restr_join thunks_Cons restr_delete_twist split:if_splits intro: below_trans[OF _ `a \<sqsubseteq> u`] below_trans[OF *])
295     moreover
296   
297     have "Astack (transform_alts as (restr_stack (edom ce) S)) \<sqsubseteq> u" using lamvar below_trans[OF _ `a \<sqsubseteq> u`] by auto
298   
299     {
300     from `isVal e`
301     have "isVal (transform u e)" by simp
302     hence "isVal (Aeta_expand u (transform u e))" by (rule isVal_Aeta_expand)
303     moreover
304     from  `map_of \<Gamma> x = Some e`  `ae x = up \<cdot> u` `ce x = up\<cdot>c` `isVal (transform u e)`
305     have "map_of (restrictA (edom ce) (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>))) x = Some (Aeta_expand u (transform u e))"
306       by (simp add: map_of_map_transform)
307     ultimately
308     have "conf_transform (ae, ce, a, as) (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>*
309           ((x, Aeta_expand u (transform u e)) # delete x (restrictA (edom ce) (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>))), Aeta_expand u  (transform u e), transform_alts as (restr_stack (edom ce) S))"
310        by (auto intro: lambda_var simp add: map_transform_delete simp del: restr_delete)
311     also have "\<dots> = (restrictA (edom ce) ((map_transform Aeta_expand ae (map_transform transform ae ((x,e) # delete x \<Gamma>)))), Aeta_expand u  (transform u e), transform_alts as (restr_stack (edom ce) S))"
312       using `ae x = up \<cdot> u` `ce x = up\<cdot>c` `isVal (transform u e)`
313       by (simp add: map_transform_Cons map_transform_delete restr_delete_twist del: restr_delete)
314     also(subst[rotated]) have "\<dots> \<Rightarrow>\<^sup>* conf_transform (ae, ce, u, as) ((x, e) # delete x \<Gamma>, e, S)"
315       by simp (rule Aeta_expand_correct[OF `Astack _ \<sqsubseteq> u`])
316     finally(rtranclp_trans)
317     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)".
318     }
319     ultimately show ?case by (blast intro: normal_trans del: consistentI consistentE)
320   next
321   case (var\<^sub>2 \<Gamma> x e S)
322     show ?case
323     proof(cases "x \<in> edom ce")
324       case True[simp]
325       hence "ce x \<noteq> \<bottom>" using var\<^sub>2 by (auto simp add: edom_def)
326       hence "ae x = up\<cdot>a" using var\<^sub>2 by (auto simp add: env_restr_join join_below_iff)
327   
328       obtain c where "ce x = up\<cdot>c" using `ce x \<noteq> \<bottom>` by (cases "ce x") auto
329   
330       have "Astack (Upd x # S) \<sqsubseteq> a" using var\<^sub>2 by auto
331       hence "a = 0" by auto
332   
333       from `isVal e` `x \<notin> domA \<Gamma>`
334       have *: "prognosis ae as 0 ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae as 0 (\<Gamma>, e, Upd x # S)" by (rule prognosis_Var2)
335
336       have "consistent (ae, ce, 0, as) ((x, e) # \<Gamma>, e, S)"
337         using var\<^sub>2
338         by (auto simp add: join_below_iff env_restr_join thunks_Cons split:if_splits elim:below_trans[OF *])
339       moreover
340       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)"
341         using `ae x = up\<cdot>a` `a = 0` var\<^sub>2 `ce x = up\<cdot>c`
342         by (auto intro!: step.intros simp add: map_transform_Cons)
343       ultimately show ?thesis by (blast del: consistentI consistentE)
344     next
345       case False[simp]
346       hence "ce x = \<bottom>" using var\<^sub>2 by (auto simp add: edom_def)
347
348       from False have "x \<notin> edom ae" using var\<^sub>2 by auto
349       hence [simp]: "ae x = \<bottom>" by (auto simp add: edom_def)
350
351       
352       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)
353       also
354        
355       from `ae x = \<bottom>`
356       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)"
357         by (rule prognosis_not_called)
358       also have  "delete x ((x,e)#\<Gamma>) = \<Gamma>" using `x \<notin> domA \<Gamma>` by simp
359       finally
360       have *: "prognosis ae as a ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae as a (\<Gamma>, e, Upd x # S)" by this simp
361
362       have "consistent (ae, ce, a, as) ((x, e) # \<Gamma>, e, S)" using var\<^sub>2
363         by (auto simp add: join_below_iff env_restr_join `ce x = \<bottom>` thunks_Cons split:if_splits elim:below_trans[OF *])
364       moreover
365       have "conf_transform (ae, ce, a, as) (\<Gamma>, e, Upd x # S) = conf_transform (ae, ce, a, as) ((x, e) # \<Gamma>, e, S)"
366         by(simp add: map_transform_restrA[symmetric])
367       ultimately show ?thesis by (auto del: consistentI consistentE)
368     qed
369   next
370     case (let\<^sub>1 \<Delta> \<Gamma> e S)
371   
372     let ?ae = "Aheap \<Delta> e\<cdot>a"
373     let ?new = "(domA (\<Delta> @ \<Gamma>) \<union> upds S - (domA \<Gamma> \<union> upds S))"
374     have new: "?new = domA \<Delta>"
375       using fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_fv[OF let\<^sub>1(2)]
376       by (auto dest: set_mp[OF ups_fv_subset])
377   
378     let ?ce = "cHeap \<Delta> e\<cdot>a"
379   
380     have "domA \<Delta> \<inter> upds S = {}" using fresh_distinct_fv[OF let\<^sub>1(2)] by (auto dest: set_mp[OF ups_fv_subset])
381     hence *: "\<And> x. x \<in> upds S \<Longrightarrow> x \<notin> edom ?ce" by (auto simp add: edom_cHeap dest!: set_mp[OF edom_Aheap])
382   
383     have restr_stack_simp2: "restr_stack (edom (?ce \<squnion> ce)) S = restr_stack (edom ce) S"
384       by (auto intro: restr_stack_cong dest!: *)
385   
386     have "edom ae \<subseteq> domA \<Gamma> \<union> upds S" using let\<^sub>1 by auto
387     from set_mp[OF this] fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_fv[OF let\<^sub>1(2)]
388     have "edom ae \<inter> domA \<Delta> = {}" by (auto dest: set_mp[OF ups_fv_subset])
389     hence [simp]: "\<And> S. S \<subseteq> domA \<Delta> \<Longrightarrow> ae f|` S = \<bottom>" by auto
390
391     have "edom ce \<subseteq> domA \<Gamma> \<union> upds S" using let\<^sub>1 by auto
392     from set_mp[OF this] fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_fv[OF let\<^sub>1(2)]
393     have "edom ce \<inter> domA \<Delta> = {}"
394        by (auto dest: set_mp[OF ups_fv_subset])
395
396     from fresh_distinct[OF let\<^sub>1(1)]
397     have "edom ?ae \<inter> domA \<Gamma> = {}" by (auto dest: set_mp[OF edom_Aheap])
398     hence "edom ?ce \<inter> domA \<Gamma> = {}" by (simp add: edom_cHeap)
399
400   
401     from  fresh_distinct[OF let\<^sub>1(1)]
402     have [simp]: "\<And> S. S \<subseteq> domA \<Gamma> \<Longrightarrow> ?ae f|` S = \<bottom>" by (auto dest!: set_mp[OF edom_Aheap])
403   
404     {
405     have "edom (?ce \<squnion> ce) \<subseteq> domA (\<Delta> @ \<Gamma>) \<union> upds S"
406       using let\<^sub>1(3) by (auto simp add: edom_cHeap dest: set_mp[OF edom_Aheap])
407     moreover
408     have "edom (?ae \<squnion> ae) = edom (?ce \<squnion> ce)"
409       using let\<^sub>1(3) by (auto simp add: edom_cHeap)
410     moreover
411     { fix x e'
412       assume "x \<in> thunks \<Gamma>"
413       hence "x \<notin> edom ?ce" using fresh_distinct[OF let\<^sub>1(1)]
414         by (auto simp add: edom_cHeap dest: set_mp[OF edom_Aheap]  set_mp[OF thunks_domA])
415       hence [simp]: "?ce x = \<bottom>" unfolding edomIff by auto
416     
417       assume "many \<sqsubseteq> (?ce \<squnion> ce) x"
418       with let\<^sub>1 `x \<in> thunks \<Gamma>`
419       have "(?ae \<squnion> ae) x = up \<cdot>0" by auto
420     }
421     moreover
422     { fix x e'
423       assume "x \<in> thunks \<Delta>" 
424       hence "x \<notin> domA \<Gamma>" and "x \<notin> upds S"
425         using fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_fv[OF let\<^sub>1(2)]
426         by (auto dest!: set_mp[OF thunks_domA] set_mp[OF ups_fv_subset])
427       hence "x \<notin> edom ce" using let\<^sub>1 by auto
428       hence [simp]: "ce x = \<bottom>"  by (auto simp add: edomIff)
429   
430       assume "many \<sqsubseteq> (?ce \<squnion> ce) x" with `x \<in> thunks \<Delta>`
431       have "(?ae \<squnion> ae) x = up\<cdot>0" by (auto simp add: Aheap_heap3)
432     }
433     moreover
434     have [simp]: "ap S \<inter> edom (cHeap \<Delta> e\<cdot>a) = {}"
435       using fresh_distinct_fv[OF let\<^sub>1(2)] 
436       by (auto simp add: edom_cHeap dest!: set_mp[OF edom_Aheap] set_mp[OF ap_fv_subset])
437
438     have "stack_consistent as (restr_stack (edom ce) S)" using let\<^sub>1 by auto 
439     hence "stack_consistent as (restr_stack (edom (?ce \<squnion> ce)) S)" unfolding restr_stack_simp2.
440     moreover
441     have "Astack (restr_stack (edom (?ce \<squnion> ce)) S) \<sqsubseteq> a" unfolding restr_stack_simp2 using let\<^sub>1 by auto
442     moreover
443     have "edom (?ce \<squnion> ce) \<subseteq> edom (?ae \<squnion> ae)" using let\<^sub>1 by (auto simp add: edom_cHeap)
444     moreover
445     {
446     from let\<^sub>1(1,2) `edom ae \<subseteq> domA \<Gamma> \<union> upds S`
447     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)
448     also have "prognosis ae as a (\<Gamma>, Let \<Delta> e, S) \<sqsubseteq> ce" using let\<^sub>1 by auto
449     finally have "prognosis (?ae \<squnion> ae) as a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> ?ce \<squnion> ce" by this simp
450     }
451     moreover
452     have "heap_upds_ok (\<Gamma>, S)" using let\<^sub>1 by auto
453     with fresh_distinct[OF let\<^sub>1(1)]  `domA \<Delta> \<inter> upds S = {}`
454     have "heap_upds_ok (\<Delta> @ \<Gamma>, S)" by (rule heap_upds_ok_append)
455     moreover
456     {
457     have "ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae) = ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)"
458       by (rule Abinds_env_restr_cong) (simp add: env_restr_join)
459     moreover
460     have "ABinds \<Gamma>\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae) = ABinds \<Gamma>\<cdot>ae"
461       by (rule Abinds_env_restr_cong) (simp add: env_restr_join)
462     moreover
463     have "ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a) \<squnion> Aexp e\<cdot>a \<sqsubseteq> Aheap \<Delta> e\<cdot>a \<squnion> Aexp (Let \<Delta> e)\<cdot>a" by (rule Aexp_Let)
464     moreover
465     have "(ABinds \<Gamma>\<cdot>ae \<squnion> Aexp (Let \<Delta> e)\<cdot>a \<squnion> AEstack as S) f|` edom ce \<sqsubseteq> ae" using let\<^sub>1 by auto
466     moreover
467     have "Aexp (Terms.Let \<Delta> e)\<cdot>a f|` (edom ce \<union> edom (cHeap \<Delta> e\<cdot>a)) = Aexp (Terms.Let \<Delta> e)\<cdot>a f|` edom ce"
468       by (rule env_restr_cong) (auto simp add: edom_cHeap dest!: set_mp[OF Aexp_edom]  set_mp[OF edom_Aheap])
469     moreover
470     have "ABinds \<Gamma>\<cdot>ae f|` (edom ce \<union> edom (cHeap \<Delta> e\<cdot>a)) = ABinds \<Gamma>\<cdot>ae f|` edom ce" 
471       using fresh_distinct_fv[OF let\<^sub>1(1)]
472       by (auto intro: env_restr_cong  simp add: edom_cHeap dest!: set_mp[OF Aexp_edom]  set_mp[OF edom_Aheap] set_mp[OF edom_AnalBinds])
473     moreover
474     thm env_restr_cong
475     have "AEstack as S f|` (edom ce \<union> edom (cHeap \<Delta> e\<cdot>a)) = AEstack as S f|` (edom ce)" 
476       using fresh_distinct_fv[OF let\<^sub>1(2)]
477       by (auto intro: env_restr_cong simp add: edom_cHeap dest!: set_mp[OF edom_Aheap] set_mp[OF edom_AEstack])
478     ultimately
479     have "(ABinds (\<Delta> @ \<Gamma>) \<cdot> (Aheap \<Delta> e\<cdot>a \<squnion> ae) \<squnion> Aexp e\<cdot>a \<squnion> AEstack as S) f|` edom (?ce \<squnion> ce) \<sqsubseteq> Aheap \<Delta> e\<cdot>a \<squnion> ae"
480       by (simp only: join_assoc[symmetric] restrictA_append Abinds_append_disjoint[OF fresh_distinct[OF let\<^sub>1(1)]] join_below_iff env_restr_join)
481          (auto 4 4 simp add: join_below_iff env_restr_join intro: below_trans[OF env_restr_below_self] elim!: below_trans[OF env_restr_mono] below_trans)
482     }
483     ultimately
484     have "consistent (?ae \<squnion> ae, ?ce \<squnion> ce, a, as) (\<Delta> @ \<Gamma>, e, S)"
485       by auto
486     }
487     moreover
488     {
489       have "\<And> x. x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> edom ?ae" "\<And> x. x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> edom ?ce"
490         using fresh_distinct[OF let\<^sub>1(1)]
491         by (auto simp add: edom_cHeap dest!: set_mp[OF edom_Aheap])
492       hence "restrictA (edom (?ce \<squnion> ce)) (map_transform Aeta_expand (?ae \<squnion> ae) (map_transform transform (?ae \<squnion> ae) \<Gamma>))
493          = restrictA (edom ce) (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>))"
494          by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
495       moreover
496   
497       from let\<^sub>1 have *: "edom ce \<subseteq> domA \<Gamma> \<union> upds S"  "edom ae \<subseteq> domA \<Gamma> \<union> upds S" by auto
498       have "\<And> x. x \<in> domA \<Delta> \<Longrightarrow> x \<notin> edom ce" and  "\<And> x. x \<in> domA \<Delta> \<Longrightarrow> x \<notin> edom ae"
499          using fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_fv[OF let\<^sub>1(2)] 
500          by (auto dest!: set_mp[OF *(1)] set_mp[OF *(2)] set_mp[OF ups_fv_subset])
501       hence "restrictA (edom (?ce \<squnion> ce)) (map_transform Aeta_expand (?ae \<squnion> ae) (map_transform transform (?ae \<squnion> ae) \<Delta>))
502          = restrictA (edom ?ce) (map_transform Aeta_expand ?ae (map_transform transform ?ae \<Delta>))"
503          by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
504       ultimately
505   
506       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)"
507         using restr_stack_simp2 let\<^sub>1(1,2)
508         by (fastforce intro!: let_and_restrict simp  add: map_transform_append restrictA_append  edom_cHeap  dest: set_mp[OF edom_Aheap])
509     }
510     ultimately
511     show ?case by (blast del: consistentI consistentE)
512   next
513     case (if\<^sub>1 \<Gamma> scrut e1 e2 S)
514     {
515     have "Aexp (scrut ? e1 : e2)\<cdot>a f|` edom ce \<sqsubseteq> ae" using if\<^sub>1 by (auto simp add: env_restr_join join_below_iff)
516     hence "(Aexp scrut\<cdot>0 \<squnion> Aexp e1\<cdot>a \<squnion> Aexp e2\<cdot>a) f|` edom ce \<sqsubseteq> ae"
517       by (rule below_trans[OF env_restr_mono[OF Aexp_IfThenElse]])
518     moreover
519     have "prognosis ae as a (\<Gamma>, scrut ? e1 : e2, S) \<sqsubseteq> ce" using if\<^sub>1 by auto
520     hence "prognosis ae (a#as) 0 (\<Gamma>, scrut, Alts e1 e2 # S) \<sqsubseteq> ce"
521       by (rule below_trans[OF prognosis_IfThenElse])
522     ultimately
523     have "consistent (ae, ce, 0, a#as) (\<Gamma>, scrut, Alts e1 e2 # S)"
524       using if\<^sub>1  by (auto simp add: env_restr_join join_below_iff)
525     }
526     moreover
527     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)"
528       by (auto intro: normal step.intros)
529     ultimately
530     show ?case by (blast del: consistentI consistentE)
531   next
532     case (if\<^sub>2 \<Gamma> b e1 e2 S)
533     from if\<^sub>2 obtain a' as' where [simp]: "as = a' # as'" by auto
534     from if\<^sub>2 have [simp]: "a = 0" by auto
535
536     {
537     have "prognosis ae (a'#as') 0 (\<Gamma>, Bool b, Alts e1 e2 # S) \<sqsubseteq> ce" using if\<^sub>2 by auto
538     hence "prognosis ae as' a' (\<Gamma>, if b then e1 else e2, S) \<sqsubseteq> ce" by (rule below_trans[OF prognosis_Alts])
539     then
540     have "consistent (ae, ce, a', as') (\<Gamma>, if b then e1 else e2, S)" 
541       using if\<^sub>2 by (auto simp add: env_restr_join join_below_iff)
542     }
543     moreover
544     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)"
545       by (auto intro:normal  step.if\<^sub>2[where b = True, simplified] step.if\<^sub>2[where b = False, simplified])
546     ultimately
547     show ?case by (blast del: consistentI consistentE)
548   next
549     case refl thus ?case by auto
550   next
551     case (trans c c' c'')
552       from trans(3)[OF trans(5)]
553       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
554       from trans(4)[OF this(1)]
555       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
556       from this(1) rtranclp_trans[OF * **]
557       show ?case by blast
558   qed
559 end
560
561 end