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