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