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