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