Demand more in FutureAnalysisCarrier
[darcs-mirror-isa-launchbury.git] / Launchbury / FTreeCardinality.thy
1 theory FTreeCardinality
2 imports CardinalityAnalysis "FTree-HOLCF" CallFutureCardinality AnalBinds
3 begin
4
5 locale FutureAnalysis =
6  fixes Fexp :: "exp \<Rightarrow> Arity \<rightarrow> var ftree"
7 begin
8   sublocale Fexp!: ExpAnalysis Fexp.
9   abbreviation "FBinds == Fexp.AnalBinds"
10 end
11
12 locale FutureAnalysisCarrier = FutureAnalysis + EdomArityAnalysis +
13   assumes carrier_Fexp: "carrier (Fexp e\<cdot>a) = edom (Aexp e\<cdot>a)"
14
15 locale FutureAnalysisCorrect = FutureAnalysisCarrier +
16   assumes Fexp_App: "many_calls x \<otimes>\<otimes> (Fexp e)\<cdot>(inc\<cdot>a) \<sqsubseteq> Fexp (App e x)\<cdot>a"
17   assumes Fexp_Lam: "without y (Fexp e\<cdot>(pred\<cdot>n)) \<sqsubseteq> Fexp (Lam [y]. e) \<cdot> n"
18   assumes Fexp_subst: "Fexp (e[y::=x])\<cdot>a \<sqsubseteq> many_calls x \<otimes>\<otimes> without y ((Fexp e)\<cdot>a)"
19   assumes Fexp_Var: "single v \<sqsubseteq> Fexp (Var v)\<cdot>a"
20   assumes Fun_repeatable: "isLam e \<Longrightarrow> repeatable (Fexp e\<cdot>0)"
21
22 locale FutureAnalysisCardinalityHeap = 
23   FutureAnalysisCorrect + CorrectArityAnalysisLet' + 
24   fixes Fheap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> var ftree"
25   (* assumes Fheap_eqvt: "\<pi> \<bullet> Fheap = Fheap" *)
26   assumes carrier_Fheap: "carrier (Fheap \<Gamma> e\<cdot>a) = edom (Aheap \<Gamma> e\<cdot>a)"
27   assumes Fheap_thunk: "x \<in> thunks \<Gamma> \<Longrightarrow> p \<in> paths (Fheap \<Gamma> e\<cdot>a) \<Longrightarrow> \<not> one_call_in_path x p \<Longrightarrow> (Aheap \<Gamma> e\<cdot>a) x = up\<cdot>0"
28   assumes Fheap_substitute: "ftree_restr (domA \<Delta>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a)) \<sqsubseteq> Fheap \<Delta> e\<cdot>a"
29   assumes Fexp_Let: "ftree_restr (- domA \<Delta>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a))  (thunks \<Delta>) (Fexp e\<cdot>a)) \<sqsubseteq> Fexp (Terms.Let \<Delta> e)\<cdot>a"
30
31 context FutureAnalysis
32 begin
33
34 fun unstack :: "stack \<Rightarrow> exp \<Rightarrow> exp" where
35   "unstack [] e = e"
36 | "unstack (Upd x # S) e = unstack S e"
37 | "unstack (Arg x # S) e = unstack S (App e x)"
38 | "unstack (Dummy x # S) e = unstack S e"
39
40 fun Fstack :: "stack \<Rightarrow> var ftree"
41   where "Fstack [] = \<bottom>"
42   | "Fstack (Upd x # S) = Fstack S"
43   | "Fstack (Arg x # S) = many_calls x \<otimes>\<otimes> Fstack S"
44   | "Fstack (Dummy x # S) = Fstack S"
45
46 lemma carrier_Fstack[simp]: "carrier (Fstack S) = ap S"
47   by (induction S rule: Fstack.induct) (auto simp add: empty_is_bottom[symmetric])
48
49 fun prognosis :: "AEnv \<Rightarrow> Arity \<Rightarrow> conf \<Rightarrow> var \<Rightarrow> two"
50    where "prognosis ae a (\<Gamma>, e, S) = pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S)))"
51 end
52
53
54 lemma pathsCard_paths_nxt:  "pathsCard (paths (nxt f x)) \<sqsubseteq> record_call x\<cdot>(pathsCard (paths f))"
55   apply transfer
56   apply (rule pathsCard_below)
57   apply auto
58   apply (erule below_trans[OF _ monofun_cfun_arg[OF paths_Card_above], rotated]) back
59   apply (auto intro: fun_belowI simp add: record_call_simp two_pred_two_add_once)
60   done
61
62 lemma pathsCards_none: "pathsCard (paths t) x = none \<Longrightarrow> x \<notin> carrier t"
63   by transfer (auto dest: pathCards_noneD)
64
65 lemma const_on_edom_disj: "const_on f S empty \<longleftrightarrow> edom f \<inter> S = {}"
66   by (auto simp add: empty_is_bottom edom_def)
67
68 context FutureAnalysisCarrier
69 begin
70   lemma carrier_FBinds: "carrier ((FBinds \<Gamma>\<cdot>ae) x) \<subseteq> fv \<Gamma>"
71   apply (simp add: Fexp.AnalBinds_lookup)
72   apply (auto split: option.split simp add: empty_is_bottom[symmetric] )
73   apply (case_tac "ae x")
74   apply (auto simp add: empty_is_bottom[symmetric] carrier_Fexp dest!: set_mp[OF Aexp_edom])
75   by (metis (poly_guards_query) contra_subsetD domA_from_set map_of_fv_subset map_of_is_SomeD option.sel)
76 end
77
78
79
80
81 context FutureAnalysisCorrect
82 begin
83
84   sublocale CardinalityPrognosisCorrect prognosis
85   proof
86     fix \<Gamma> :: heap and ae ae' :: AEnv and u e S
87     assume "ae f|` domA \<Gamma> = ae' f|` domA \<Gamma>"
88     from Fexp.AnalBinds_cong[OF this]
89     show "prognosis ae u (\<Gamma>, e, S) = prognosis ae' u (\<Gamma>, e, S)" by simp
90   next
91     fix ae a \<Gamma> e S
92     show "const_on (prognosis ae a (\<Gamma>, e, S)) (ap S) many"
93     proof
94       fix x
95       assume "x \<in> ap S"
96       hence "[x,x] \<in> paths (Fstack S)"
97         by (induction S rule: Fstack.induct)
98            (auto 4 4 intro: set_mp[OF both_contains_arg1] set_mp[OF both_contains_arg2] paths_Cons_nxt)
99       hence "[x,x] \<in> paths (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S)"
100         by (rule set_mp[OF both_contains_arg2])
101       hence "[x,x] \<in> paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S))" 
102         by (rule set_mp[OF substitute_contains_arg])
103       hence "pathCard [x,x] x \<sqsubseteq> pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S))) x"
104         by (metis fun_belowD paths_Card_above)
105       also have "pathCard [x,x] x = many"  by (auto simp add: pathCard_def)
106       finally
107       show "prognosis ae a (\<Gamma>, e, S) x = many"
108         by (auto intro: below_antisym)
109     qed
110   next
111     fix ae a \<Gamma> e x S
112     have "Fexp e\<cdot>(inc\<cdot>a)  \<otimes>\<otimes> many_calls x \<otimes>\<otimes> Fstack S = many_calls x  \<otimes>\<otimes> (Fexp e)\<cdot>(inc\<cdot>a) \<otimes>\<otimes> Fstack S"
113       by (metis both_assoc both_comm)
114     thus "prognosis ae (inc\<cdot>a) (\<Gamma>, e, Arg x # S) \<sqsubseteq> prognosis ae a (\<Gamma>, App e x, S)"
115       by simp (intro pathsCard_mono' paths_mono substitute_mono2' both_mono1' Fexp_App)
116   next
117     fix ae a \<Gamma> e y x S
118     have "Fexp e[y::=x]\<cdot>(pred\<cdot>a) \<sqsubseteq> many_calls x  \<otimes>\<otimes> Fexp (Lam [y]. e)\<cdot>a"
119       by (rule below_trans[OF Fexp_subst both_mono2'[OF Fexp_Lam]])
120     moreover have "Fexp (Lam [y]. e)\<cdot>a \<otimes>\<otimes> many_calls x \<otimes>\<otimes> Fstack S = many_calls x  \<otimes>\<otimes> Fexp (Lam [y]. e)\<cdot>a \<otimes>\<otimes> Fstack S"
121       by (metis both_assoc both_comm)
122     ultimately  
123     show "prognosis ae (pred\<cdot>a) (\<Gamma>, e[y::=x], S) \<sqsubseteq> prognosis ae a (\<Gamma>, Lam [y]. e, Arg x # S)"
124       by simp (intro pathsCard_mono' paths_mono substitute_mono2' both_mono1')
125   next
126     fix \<Gamma> :: heap and e :: exp and x :: var and ae :: AEnv and u a S
127     assume "map_of \<Gamma> x = Some e"
128     assume "ae x = up\<cdot>u"
129
130     have "pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u \<otimes>\<otimes> Fstack S))) = pathsCard (paths (nxt (and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack S))) x))"
131       by simp
132     also
133     have "\<dots> \<sqsubseteq> record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack S)))))"
134       by (rule pathsCard_paths_nxt)
135     also
136     have "\<dots> = record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fstack S  \<otimes>\<otimes> Fexp e\<cdot>u)))))"
137       by (metis both_comm)
138     also
139     have "\<dots> = record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fstack S  \<otimes>\<otimes> (FBinds \<Gamma>\<cdot>ae) x)))))"
140       using `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` by (simp add: Fexp.AnalBinds_lookup)
141     also
142     assume "isLam e"
143     hence "x \<notin> thunks \<Gamma>" using `map_of \<Gamma> x = Some e` by (metis thunksE)
144     hence "FBinds \<Gamma>\<cdot>ae = f_nxt (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) x" by (auto simp add: f_nxt_def)
145     hence "and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fstack S  \<otimes>\<otimes> (FBinds \<Gamma>\<cdot>ae) x)) = substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (and_then x (Fstack S))"
146       by (simp add: substitute_and_then)
147     also
148     have "and_then x (Fstack S) \<sqsubseteq> FTree.single x \<otimes>\<otimes> Fstack S" by (rule and_then_both_single')
149     note pathsCard_mono'[OF paths_mono[OF substitute_mono2'[OF this]]]
150     also
151     have "FTree.single x \<sqsubseteq> Fexp (Var x)\<cdot>a" by (rule Fexp_Var)
152     note pathsCard_mono'[OF paths_mono[OF substitute_mono2'[OF both_mono1'[OF this]]]]
153     finally
154     have "pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack S))) \<sqsubseteq> record_call x\<cdot>(pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp (Var x)\<cdot>a  \<otimes>\<otimes> Fstack S))))" 
155       by this simp_all
156     thus "prognosis ae u (\<Gamma>, e, S) \<sqsubseteq> record_call x\<cdot>(prognosis ae a (\<Gamma>, Var x, S))" by simp
157   next
158     fix \<Gamma> :: heap and e :: exp and x :: var and ae :: AEnv and u a S
159     assume "map_of \<Gamma> x = Some e"
160     assume "ae x = up\<cdot>u"
161     assume "\<not> isLam e"
162     hence "x \<in> thunks \<Gamma>" using `map_of \<Gamma> x = Some e` by (metis thunksI)
163     hence [simp]: "f_nxt (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) x = FBinds (delete x \<Gamma>)\<cdot>ae" 
164       by (auto simp add: f_nxt_def Fexp.AnalBinds_delete_to_fun_upd empty_is_bottom)
165
166     have "pathsCard (paths (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks (delete x \<Gamma>)) (Fexp e\<cdot>u \<otimes>\<otimes> Fstack S)))
167        =  pathsCard (paths (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u \<otimes>\<otimes> Fstack S)))"
168        by (rule arg_cong[OF substitute_cong_T]) (auto simp add: empty_is_bottom)
169     also have "\<dots>  = pathsCard (paths (nxt (and_then x (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack S))) x))"
170       by simp
171     also
172     have "\<dots> \<sqsubseteq> record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack S)))))"
173       by (rule pathsCard_paths_nxt)
174     also
175     have "\<dots> = record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fstack S  \<otimes>\<otimes> Fexp e\<cdot>u)))))"
176       by (metis both_comm)
177     also
178     have "\<dots> = record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fstack S  \<otimes>\<otimes> (FBinds \<Gamma>\<cdot>ae) x)))))"
179       using `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` by (simp add: Fexp.AnalBinds_lookup)
180     also
181     have "and_then x (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fstack S \<otimes>\<otimes> (FBinds \<Gamma>\<cdot>ae) x)) = substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (and_then x (Fstack S))"
182       by (simp add: substitute_and_then)
183     also
184     have "and_then x (Fstack S) \<sqsubseteq> FTree.single x \<otimes>\<otimes> Fstack S" by (rule and_then_both_single')
185     note pathsCard_mono'[OF paths_mono[OF substitute_mono2'[OF this]]]
186     also
187     have "FTree.single x \<sqsubseteq> Fexp (Var x)\<cdot>a" by (rule Fexp_Var)
188     note pathsCard_mono'[OF paths_mono[OF substitute_mono2'[OF both_mono1'[OF this]]]]
189     finally
190     have "pathsCard (paths (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks (delete x \<Gamma>)) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack S)))
191        \<sqsubseteq> record_call x\<cdot>(pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp (Var x)\<cdot>a  \<otimes>\<otimes> Fstack S))))" 
192       by this simp_all
193     thus "prognosis ae u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x\<cdot>(prognosis ae a (\<Gamma>, Var x, S))" by simp
194   next
195     fix \<Gamma> :: heap and e :: exp and ae :: AEnv and  x :: var and  S
196     assume "isLam e"
197     hence "repeatable (Fexp e\<cdot>0)" by (rule Fun_repeatable)
198
199     assume [simp]: "x \<notin> domA \<Gamma>"
200
201     have [simp]: "thunks ((x, e) # \<Gamma>) = thunks \<Gamma>" 
202       using `isLam e`
203       by (auto simp add: thunks_Cons dest: set_mp[OF thunks_domA])
204
205     have "fup\<cdot>(Fexp e)\<cdot>(ae x) \<sqsubseteq> Fexp e\<cdot>0" by (metis fup2 monofun_cfun_arg up_zero_top)
206     hence "substitute ((FBinds \<Gamma>\<cdot>ae)(x := fup\<cdot>(Fexp e)\<cdot>(ae x))) (thunks \<Gamma>) (Fexp e\<cdot>0 \<otimes>\<otimes> Fstack S) \<sqsubseteq> substitute ((FBinds \<Gamma>\<cdot>ae)(x := Fexp e\<cdot>0)) (thunks \<Gamma>) (Fexp e\<cdot>0 \<otimes>\<otimes> Fstack S)"
207       by (intro substitute_mono1' fun_upd_mono below_refl)
208     also have "\<dots> = substitute (((FBinds \<Gamma>\<cdot>ae)(x := Fexp e\<cdot>0))(x := empty)) (thunks \<Gamma>) (Fexp e\<cdot>0 \<otimes>\<otimes> Fstack S)"
209       using `repeatable (Fexp e\<cdot>0)` by (rule substitute_remove_anyways, simp)
210     also have "((FBinds \<Gamma>\<cdot>ae)(x := Fexp e\<cdot>0))(x := empty) = FBinds \<Gamma>\<cdot>ae"
211       by (simp add: fun_upd_idem Fexp.AnalBinds_not_there empty_is_bottom)
212     finally
213     show "prognosis ae 0 ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae 0 (\<Gamma>, e, Upd x # S)"
214       by (simp, intro pathsCard_mono' paths_mono)
215   next
216     fix \<Gamma> \<Delta> :: heap and e :: exp and ae :: AEnv and u S
217     assume "map_of \<Gamma> = map_of \<Delta>"
218     hence "FBinds \<Gamma> = FBinds \<Delta>" and "thunks \<Gamma> = thunks \<Delta>" by (auto intro!: cfun_eqI  thunks_cong simp add: Fexp.AnalBinds_lookup)
219     thus "prognosis ae u (\<Gamma>, e, S) = prognosis ae u (\<Delta>, e, S)"  by simp
220   next
221     fix \<Gamma> :: heap and e :: exp and ae :: AEnv and u S x
222
223     show "prognosis ae u (delete x \<Gamma>, e, S) \<sqsubseteq> prognosis ae u (\<Gamma>, e, S)"
224       by (simp add: substitute_T_delete empty_is_bottom)
225          (intro pathsCard_mono' paths_mono substitute_mono1' Fexp.AnalBinds_delete_below)
226   next
227     fix \<Gamma> :: heap and e :: exp and ae :: AEnv and u S x
228     show "prognosis ae u (\<Gamma>, e, S) \<sqsubseteq> prognosis ae u (\<Gamma>, e, Upd x # S)" by simp
229   next
230     fix \<Gamma> :: heap and e :: exp and ae :: AEnv and a S x
231     assume "ae x = \<bottom>"
232     (*
233     assume "prognosis ae a (delete x \<Gamma>, e, S) x = none"
234     hence "x \<notin> carrier (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S))" 
235       by (simp add: pathsCards_none)
236     hence "substitute (FBinds \<Gamma>\<cdot>ae) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S) = substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S)"
237       by (auto intro: substitute_cong[symmetric] simp add: Fexp.AnalBinds_lookup delete_conv')
238      *)
239     hence "FBinds (delete x \<Gamma>)\<cdot>ae = FBinds \<Gamma>\<cdot>ae" by (rule Fexp.AnalBinds_delete_bot)
240     moreover
241     hence "((FBinds \<Gamma>\<cdot>ae) x) = \<bottom>" by (metis Fexp.AnalBinds_delete_lookup)
242     ultimately
243     show "prognosis ae a (\<Gamma>, e, S) \<sqsubseteq> prognosis ae a (delete x \<Gamma>, e, S)"
244       by (simp add: substitute_T_delete empty_is_bottom)
245   qed
246 end
247
248 context FutureAnalysisCardinalityHeap
249 begin
250
251   definition cHeap where
252     "cHeap \<Gamma> e = (\<Lambda> a. pathsCard (paths (Fheap \<Gamma> e\<cdot>a)))"
253
254   lemma cHeap_simp: "(cHeap \<Gamma> e)\<cdot>a = pathsCard (paths (Fheap \<Gamma> e\<cdot>a))"
255     unfolding cHeap_def  by (rule beta_cfun) (intro cont2cont)
256   
257   (*
258   lemma cHeap_eqvt: "\<pi> \<bullet> (cHeap \<Gamma> e) = cHeap (\<pi> \<bullet> \<Gamma>) (\<pi> \<bullet> e)"
259     unfolding cHeap_def
260     apply perm_simp
261     apply (simp add: Fheap_eqvt)
262     apply (rule Abs_cfun_eqvt)
263     apply (intro cont2cont)
264     done
265   *)
266
267   sublocale CardinalityHeap Aexp Aheap cHeap
268   proof
269   (*
270     note cHeap_eqvt[eqvt]
271     fix \<pi> show "\<pi> \<bullet> cHeap = cHeap" by perm_simp rule
272   next
273   *)
274     fix x \<Gamma> e a
275     assume "x \<in> thunks \<Gamma>"
276     moreover
277     assume "many \<sqsubseteq> (cHeap \<Gamma> e\<cdot>a) x"
278     hence "many \<sqsubseteq> pathsCard (paths (Fheap \<Gamma> e \<cdot>a)) x" unfolding cHeap_def by simp
279     hence "\<exists>p\<in> (paths (Fheap \<Gamma> e\<cdot>a)). \<not> (one_call_in_path x p)" unfolding pathsCard_def
280       by (auto split: if_splits)
281     ultimately
282     show "(Aheap \<Gamma> e\<cdot>a) x = up\<cdot>0"
283       by (metis Fheap_thunk)
284   next
285     fix \<Gamma> e a
286     show "edom (cHeap \<Gamma> e\<cdot>a) = edom (Aheap \<Gamma> e\<cdot>a)"
287     by (simp add: cHeap_def Union_paths_carrier carrier_Fheap)
288   qed
289
290   sublocale CardinalityPrognosisCorrectLet prognosis Aexp Aheap cHeap
291   proof
292     fix \<Delta> \<Gamma> :: heap and e :: exp and S :: stack and  ae :: AEnv and a :: Arity
293     assume "atom ` domA \<Delta> \<sharp>* \<Gamma>"
294     assume "atom ` domA \<Delta> \<sharp>* S"
295     assume "edom ae \<subseteq> domA \<Gamma> \<union> upds S"
296
297     have "domA \<Delta> \<inter> edom ae = {}"
298       using fresh_distinct[OF `atom \` domA \<Delta> \<sharp>* \<Gamma>`] fresh_distinct_fv[OF `atom \` domA \<Delta> \<sharp>* S`] 
299             `edom ae \<subseteq> domA \<Gamma> \<union> upds S` ups_fv_subset[of S]
300       by auto
301
302     have const_on1:  "\<And> x. const_on (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (carrier ((FBinds \<Gamma>\<cdot>ae) x)) empty"
303       unfolding const_on_edom_disj using fresh_distinct_fv[OF `atom \` domA \<Delta> \<sharp>* \<Gamma>`]
304       by (auto dest!: set_mp[OF carrier_FBinds] set_mp[OF Fexp.edom_AnalBinds])
305     have const_on2:  "const_on (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (carrier (Fstack S)) empty"
306       unfolding const_on_edom_disj using fresh_distinct_fv[OF `atom \` domA \<Delta> \<sharp>* S`]
307       by (auto dest!: set_mp[OF carrier_FBinds] set_mp[OF Fexp.edom_AnalBinds] set_mp[OF ap_fv_subset ])
308     have  const_on3: "const_on (FBinds \<Gamma>\<cdot>ae) (- (- domA \<Delta>)) FTree.empty"
309       and const_on4: "const_on (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (domA \<Gamma>) FTree.empty"
310       unfolding const_on_edom_disj using fresh_distinct[OF `atom \` domA \<Delta> \<sharp>* \<Gamma>`]
311       by (auto dest!:  set_mp[OF Fexp.edom_AnalBinds])
312
313     have disj1: "\<And> x. carrier ((FBinds \<Gamma>\<cdot>ae) x) \<inter> domA \<Delta> = {}"
314       using fresh_distinct_fv[OF `atom \` domA \<Delta> \<sharp>* \<Gamma>`]
315       by (auto dest: set_mp[OF carrier_FBinds])
316     hence disj1': "\<And> x. carrier ((FBinds \<Gamma>\<cdot>ae) x) \<subseteq> - domA \<Delta>" by auto
317     have disj2: "\<And> x. carrier (Fstack S) \<inter> domA \<Delta> = {}"
318       using fresh_distinct_fv[OF `atom \` domA \<Delta> \<sharp>* S`] ap_fv_subset[of S] by auto
319     hence disj2': "carrier (Fstack S) \<subseteq> - domA \<Delta>" by auto
320     
321
322     {
323     fix x
324     have "(FBinds (\<Delta> @ \<Gamma>)\<cdot>(ae \<squnion> Aheap \<Delta> e\<cdot>a)) x = (FBinds \<Gamma>\<cdot>ae) x \<otimes>\<otimes> (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x"
325     proof (cases "x \<in> domA \<Delta>")
326       case True
327       have "map_of \<Gamma> x = None" using True fresh_distinct[OF `atom \` domA \<Delta> \<sharp>* \<Gamma>`] by (metis disjoint_iff_not_equal domA_def map_of_eq_None_iff)
328       moreover
329       have "ae x = \<bottom>" using True `domA \<Delta> \<inter> edom ae = {}` by auto
330       ultimately
331       show ?thesis using True 
332           by (auto simp add: Fexp.AnalBinds_lookup empty_is_bottom[symmetric] cong: option.case_cong)
333     next
334       case False
335       have "map_of \<Delta> x = None" using False by (metis domA_def map_of_eq_None_iff)
336       moreover
337       have "(Aheap \<Delta> e\<cdot>a) x = \<bottom>" using False using edom_Aheap by (metis contra_subsetD edomIff)
338       ultimately
339       show ?thesis using False
340          by (auto simp add: Fexp.AnalBinds_lookup empty_is_bottom[symmetric] cong: option.case_cong)
341     qed
342     }
343     note FBinds = ext[OF this]
344
345     {
346     have "pathsCard (paths (substitute (FBinds (\<Delta> @ \<Gamma>)\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae)) (thunks (\<Delta> @ \<Gamma>)) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S)))
347       = pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks (\<Delta> @ \<Gamma>)) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a))  (thunks (\<Delta> @ \<Gamma>))  (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S))))"
348        by (simp add: substitute_substitute[OF const_on1] FBinds)
349     also have "substitute (FBinds \<Gamma>\<cdot>ae) (thunks (\<Delta> @ \<Gamma>)) = substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>)"
350       apply (rule substitute_cong_T)
351       using const_on3
352       by (auto dest: set_mp[OF thunks_domA])
353     also have "substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks (\<Delta> @ \<Gamma>)) = substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>)"
354       apply (rule substitute_cong_T)
355       using const_on4
356       by (auto dest: set_mp[OF thunks_domA])
357     also have "substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S) = substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a) \<otimes>\<otimes> Fstack S" 
358       by (rule substitute_only_empty_both[OF const_on2])
359     also note calculation
360     }
361     note eq_imp_below[OF this]
362     also
363     note env_restr_split[where S = "domA \<Delta>"]
364     also
365     have "pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a) \<otimes>\<otimes> Fstack S))) f|` domA \<Delta> 
366         = pathsCard (paths (ftree_restr (domA \<Delta>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a))))"
367           by (simp add: filter_paths_conv_free_restr ftree_restr_both ftree_rest_substitute[OF disj1]  ftree_restr_is_empty[OF disj2])
368     also
369     have "ftree_restr (domA \<Delta>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a)) \<sqsubseteq> Fheap \<Delta> e\<cdot>a"  by (rule Fheap_substitute)
370     also
371     have "pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a) \<otimes>\<otimes> Fstack S))) f|` (- domA \<Delta>) =
372           pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (ftree_restr (- domA \<Delta>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a)) \<otimes>\<otimes> Fstack S)))"
373           by (simp add: filter_paths_conv_free_restr2 ftree_rest_substitute2[OF disj1' const_on3] ftree_restr_both  ftree_restr_noop[OF disj2'])
374     also have "ftree_restr (- domA \<Delta>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a))  (thunks \<Delta>)  (Fexp e\<cdot>a)) \<sqsubseteq> Fexp (Terms.Let \<Delta> e)\<cdot>a" by (rule Fexp_Let)
375     finally
376     show "prognosis (Aheap \<Delta> e\<cdot>a \<squnion> ae) a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> cHeap \<Delta> e\<cdot>a \<squnion> prognosis ae a (\<Gamma>, Terms.Let \<Delta> e, S)"
377       by (simp add: cHeap_def del: fun_meet_simp) 
378   qed
379 end
380
381 end