e83b5a49704428707feaa28e074f15323f30a7c3
[darcs-mirror-isa-launchbury.git] / Launchbury / CoCallCardinality.thy
1 theory CoCallCardinality
2 imports FTreeCardinality CoCallAnalysisSig "CoCallGraph-FTree"
3 begin
4
5 hide_const Multiset.single
6
7 lemma valid_lists_many_calls:
8   assumes "\<not> one_call_in_path x p"
9   assumes "p \<in> valid_lists S G"
10   shows "x \<in> ccManyCalls G"
11 using assms(2,1)
12 proof(induction rule:valid_lists.induct[case_names Nil Cons])
13   case Nil thus ?case by simp
14 next
15   case (Cons xs x')
16   show ?case
17   proof(cases "one_call_in_path x xs")
18     case False
19     from Cons.IH[OF this]
20     show ?thesis.
21   next
22     case True
23     with `\<not> one_call_in_path x (x' # xs)`
24     have [simp]: "x' = x" by (auto split: if_splits)
25
26     have "x \<in> set xs"
27     proof(rule ccontr)
28       assume "x \<notin> set xs"
29       hence "no_call_in_path x xs" by (metis no_call_in_path_set_conv)
30       hence "one_call_in_path x (x # xs)" by simp
31       with Cons show False by simp
32     qed
33     with `set xs \<subseteq> ccNeighbors x' G`
34     have "x \<in> ccNeighbors x G" by auto
35     thus ?thesis by simp
36   qed
37 qed
38
39
40 locale CoCallCardinality = CoCallAnalysis + CoCallAnalyisHeap + CorrectArityAnalysisLet +
41   assumes ccExp_App: "ccExp e\<cdot>(inc\<cdot>a) \<squnion> ccProd {x} (insert x (fv e)) \<sqsubseteq> ccExp (App e x)\<cdot>a"
42   assumes ccExp_Lam: "cc_restr (fv (Lam [y]. e)) (ccExp e\<cdot>(pred\<cdot>n)) \<sqsubseteq> ccExp (Lam [y]. e)\<cdot>n"
43   assumes ccExp_subst: "x \<notin>  S \<Longrightarrow> y \<notin> S \<Longrightarrow> cc_restr S (ccExp e[y::=x]\<cdot>a) \<sqsubseteq> cc_restr S (ccExp e\<cdot>a)"
44   assumes ccExp_pap: "isLam e \<Longrightarrow> ccExp e\<cdot>0 = ccSquare (fv e)"
45   assumes ccExp_Let: "cc_restr (-domA \<Gamma>) (ccHeap \<Gamma> e\<cdot>a) \<sqsubseteq> ccExp (Let \<Gamma> e)\<cdot>a"
46
47   assumes ccHeap_Exp: "ccExp e\<cdot>a \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
48   assumes ccHeap_Heap: "map_of \<Delta> x = Some e' \<Longrightarrow> (Aheap \<Delta> e\<cdot>a) x= up\<cdot>a' \<Longrightarrow> ccExp e'\<cdot>a' \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
49   assumes ccHeap_Extra_Edges:
50     "map_of \<Delta> x = Some e' \<Longrightarrow> (Aheap \<Delta> e\<cdot>a) x = up\<cdot>a' \<Longrightarrow> ccProd (fv e') (ccNeighbors x (ccHeap \<Delta> e\<cdot>a) - {x} \<inter> thunks \<Delta>) \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
51
52   assumes aHeap_thunks_rec: " \<not> nonrec \<Gamma> \<Longrightarrow> x \<in> thunks \<Gamma> \<Longrightarrow> x \<in> edom (Aheap \<Gamma> e\<cdot>a) \<Longrightarrow> (Aheap \<Gamma> e\<cdot>a) x = up\<cdot>0"
53   assumes aHeap_thunks_nonrec: "nonrec \<Gamma> \<Longrightarrow> x \<in> thunks \<Gamma> \<Longrightarrow> x \<in> ccManyCalls (ccExp e\<cdot>a) \<Longrightarrow> (Aheap \<Gamma> e\<cdot>a) x = up\<cdot>0"
54 begin
55
56 definition Fexp :: "exp \<Rightarrow> Arity \<rightarrow> var ftree"
57   where "Fexp e = (\<Lambda> a. ccFTree (edom (Aexp e \<cdot>a)) (ccExp e\<cdot>a))"
58
59 lemma Fexp_simp: "Fexp e\<cdot>a = ccFTree (edom (Aexp e \<cdot>a)) (ccExp e\<cdot>a)"
60   unfolding Fexp_def by simp
61
62 lemma carrier_Fexp': "carrier (Fexp e\<cdot>a) \<subseteq> fv e"
63   unfolding Fexp_simp carrier_ccFTree
64   by (rule Aexp_edom)
65
66 sublocale FTreeAnalysis Fexp.
67
68 lemma carrier_AnalBinds_below:
69   "carrier ((Fexp.AnalBinds  \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x) \<subseteq> edom ((ABinds \<Delta>)\<cdot>(Aheap \<Delta> e\<cdot>a))"
70 by (auto simp add: Fexp.AnalBinds_lookup Fexp_def split: option.splits 
71          elim!: set_mp[OF edom_mono[OF monofun_cfun_fun[OF ABind_below_ABinds]]])
72
73 sublocale FTreeAnalysisCarrier Fexp
74   apply default unfolding Fexp_simp carrier_ccFTree..
75
76 sublocale FTreeAnalysisCorrect Fexp
77 proof default
78   fix x e a
79
80   from edom_mono[OF Aexp_App]
81   have *: "{x} \<union> edom (Aexp e\<cdot>(inc\<cdot>a)) \<subseteq> edom (Aexp (App e x)\<cdot>a)" by auto
82
83   have **: "{x} \<union> edom (Aexp e\<cdot>(inc\<cdot>a)) \<subseteq> insert x (fv e)"
84     by (intro subset_trans[OF *] subset_trans[OF Aexp_edom]) auto
85
86   have "many_calls x \<otimes>\<otimes> Fexp e\<cdot>(inc\<cdot>a) = many_calls x \<otimes>\<otimes> ccFTree (edom (Aexp e\<cdot>(inc\<cdot>a))) (ccExp e\<cdot>(inc\<cdot>a))"
87     unfolding Fexp_simp..
88   also have "\<dots> = ccFTree {x} (ccProd {x} {x}) \<otimes>\<otimes> ccFTree (edom (Aexp e\<cdot>(inc\<cdot>a))) (ccExp e\<cdot>(inc\<cdot>a))"
89     unfolding many_calls_ccFTree..
90   also have "\<dots> \<sqsubseteq> ccFTree ({x} \<union> edom (Aexp e\<cdot>(inc\<cdot>a))) (ccProd {x} {x} \<squnion> ccExp e\<cdot>(inc\<cdot>a) \<squnion> ccProd {x} (edom (Aexp e\<cdot>(inc\<cdot>a))))"
91     by (rule interleave_ccFTree)
92   also have "\<dots> \<sqsubseteq> ccFTree (edom (Aexp (App e x)\<cdot>a)) (ccProd {x} {x} \<squnion> ccExp e\<cdot>(inc\<cdot>a) \<squnion> ccProd {x} (edom (Aexp e\<cdot>(inc\<cdot>a))))"
93     by (rule ccFTree_mono1[OF *])
94   also have "ccProd {x} {x} \<squnion> ccExp e\<cdot>(inc\<cdot>a) \<squnion> ccProd {x} (edom (Aexp e\<cdot>(inc\<cdot>a))) = ccExp e\<cdot>(inc\<cdot>a) \<squnion> ccProd {x} ({x} \<union> (edom (Aexp e\<cdot>(inc\<cdot>a))))"
95     by (simp add: ccProd_union2[symmetric] del: ccProd_union2)
96   also have "ccProd {x} ({x} \<union> (edom (Aexp e\<cdot>(inc\<cdot>a)))) \<sqsubseteq> ccProd {x} (insert x (fv e))"
97     by (rule ccProd_mono2[OF **])
98   also have "ccExp e\<cdot>(inc\<cdot>a) \<squnion> ccProd {x} (insert x (fv e)) \<sqsubseteq> ccExp (App e x)\<cdot>a"
99     by (rule ccExp_App)
100   also have "ccFTree (edom (Aexp (App e x)\<cdot>a)) (ccExp (App e x)\<cdot>a) =  Fexp (App e x)\<cdot>a"
101     unfolding Fexp_simp..
102   finally
103   show "many_calls x \<otimes>\<otimes> Fexp e\<cdot>(inc\<cdot>a) \<sqsubseteq> Fexp (App e x)\<cdot>a"
104     by this simp_all
105 next
106   fix y e n
107   from edom_mono[OF Aexp_Lam]
108   have *: "edom (Aexp e\<cdot>(pred\<cdot>n)) - {y} \<subseteq> edom (Aexp (Lam [y]. e)\<cdot>n)" by auto
109
110   have "without y (Fexp e\<cdot>(pred\<cdot>n)) = without y (ccFTree (edom (Aexp e\<cdot>(pred\<cdot>n))) (ccExp e\<cdot>(pred\<cdot>n)))"
111     unfolding Fexp_simp..
112   also have "\<dots> = ccFTree (edom (Aexp e\<cdot>(pred\<cdot>n)) - {y}) (ccExp e\<cdot>(pred\<cdot>n))"
113     by (rule  without_ccFTree)
114   also have "\<dots> \<sqsubseteq> ccFTree (edom (Aexp (Lam [y]. e)\<cdot>n)) (ccExp e\<cdot>(pred\<cdot>n))"
115     by (rule ccFTree_mono1[OF *])
116   also have "\<dots> = ccFTree (edom (Aexp (Lam [y]. e)\<cdot>n)) (cc_restr ((edom (Aexp (Lam [y]. e)\<cdot>n))) (ccExp e\<cdot>(pred\<cdot>n)))"
117     by (rule ccFTree_cc_restr)
118   also have "(cc_restr ((edom (Aexp (Lam [y]. e)\<cdot>n))) (ccExp e\<cdot>(pred\<cdot>n))) \<sqsubseteq> (cc_restr (fv (Lam [y]. e)) (ccExp e\<cdot>(pred\<cdot>n)))"
119     by (rule cc_restr_mono1[OF Aexp_edom])
120   also have "\<dots> \<sqsubseteq> ccExp (Lam [y]. e)\<cdot>n"
121     by (rule ccExp_Lam)
122   also have "ccFTree (edom (Aexp (Lam [y]. e)\<cdot>n)) (ccExp (Lam [y]. e)\<cdot>n) = Fexp (Lam [y]. e)\<cdot>n"
123     unfolding Fexp_simp..
124   finally
125   show "without y (Fexp e\<cdot>(pred\<cdot>n)) \<sqsubseteq> Fexp (Lam [y]. e)\<cdot>n" by this simp_all
126 next
127   fix e y x a
128
129   from edom_mono[OF Aexp_subst]
130   have *: "edom (Aexp e[y::=x]\<cdot>a) \<subseteq> insert x (edom (Aexp e\<cdot>a) - {y})" by simp
131
132
133   have "Fexp e[y::=x]\<cdot>a = ccFTree (edom (Aexp e[y::=x]\<cdot>a)) (ccExp e[y::=x]\<cdot>a)"
134     unfolding Fexp_simp..
135   also have "\<dots> \<sqsubseteq> ccFTree (insert x (edom (Aexp e\<cdot>a) - {y})) (ccExp e[y::=x]\<cdot>a)"
136     by (rule ccFTree_mono1[OF *])
137   also have "\<dots> \<sqsubseteq> many_calls x \<otimes>\<otimes> without x (\<dots>)"
138     by (rule paths_many_calls_subset)
139   also have "without x (ccFTree (insert x (edom (Aexp e\<cdot>a) - {y})) (ccExp e[y::=x]\<cdot>a))
140     = ccFTree (edom (Aexp e\<cdot>a) - {y} - {x}) (ccExp e[y::=x]\<cdot>a)"
141     by simp
142   also have "\<dots> \<sqsubseteq> ccFTree (edom (Aexp e\<cdot>a) - {y} - {x}) (ccExp e\<cdot>a)"
143     by (rule ccFTree_cong_below[OF ccExp_subst]) auto
144   also have "\<dots> = without y (ccFTree (edom (Aexp e\<cdot>a) - {x}) (ccExp e\<cdot>a))"
145     by simp (metis Diff_insert Diff_insert2)
146   also have "ccFTree (edom (Aexp e\<cdot>a) - {x}) (ccExp e\<cdot>a) \<sqsubseteq> ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a)"
147     by (rule ccFTree_mono1) auto
148   also have "\<dots> = Fexp e\<cdot>a"
149     unfolding Fexp_simp..
150   finally
151   show "Fexp e[y::=x]\<cdot>a \<sqsubseteq> many_calls x \<otimes>\<otimes> without y (Fexp e\<cdot>a)"
152     by this simp_all
153 next
154   fix v a
155   have "up\<cdot>a \<sqsubseteq> (Aexp (Var v)\<cdot>a) v" by (rule Aexp_Var)
156   hence "v \<in> edom (Aexp (Var v)\<cdot>a)" by (auto simp add: edom_def)
157   hence "[v] \<in> valid_lists (edom (Aexp (Var v)\<cdot>a)) (ccExp (Var v)\<cdot>a)"
158     by auto
159   thus "single v \<sqsubseteq> Fexp (Var v)\<cdot>a"
160     unfolding Fexp_simp by (auto intro: single_below)
161 next
162   fix e
163   assume "isLam e"
164   hence [simp]: "ccExp e\<cdot>0 = ccSquare (fv e)" by (rule ccExp_pap)
165   thus "repeatable (Fexp e\<cdot>0)"
166     unfolding Fexp_simp by (auto intro: repeatable_ccFTree_ccSquare[OF Aexp_edom])
167 qed
168
169 definition Fheap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> var ftree"
170   where "Fheap \<Gamma> e = (\<Lambda> a. if nonrec \<Gamma> then ccFTree (edom (Aheap \<Gamma> e\<cdot>a)) (ccExp e\<cdot>a) else ftree_restr (edom (Aheap \<Gamma> e\<cdot>a)) anything)"
171
172 lemma Fheap_simp: "Fheap \<Gamma> e\<cdot>a = (if nonrec \<Gamma> then ccFTree (edom (Aheap \<Gamma> e\<cdot>a)) (ccExp e\<cdot>a) else ftree_restr (edom (Aheap \<Gamma> e\<cdot>a)) anything)"
173   unfolding Fheap_def by simp
174
175 lemma carrier_Fheap':"carrier (Fheap \<Gamma> e\<cdot>a) = edom (Aheap \<Gamma> e\<cdot>a)"
176     unfolding Fheap_simp carrier_ccFTree by simp
177
178 sublocale FTreeAnalysisCardinalityHeap Fexp Aexp Aheap Fheap
179 proof default
180   fix \<Gamma> e a
181   show "carrier (Fheap \<Gamma> e\<cdot>a) = edom (Aheap \<Gamma> e\<cdot>a)"
182     by (rule carrier_Fheap')
183 next
184   fix x \<Gamma> p e a
185   assume "x \<in> thunks \<Gamma>"
186   
187   assume "\<not> one_call_in_path x p"
188   hence "x \<in> set p" by (rule more_than_one_setD)
189   
190   assume "p \<in> paths (Fheap \<Gamma> e\<cdot>a)" with `x \<in> set p`
191   have "x \<in> carrier (Fheap \<Gamma> e\<cdot>a)" by (auto simp add: Union_paths_carrier[symmetric])
192   hence "x \<in> edom (Aheap \<Gamma> e\<cdot>a)"
193     unfolding Fheap_simp by (auto split: if_splits)
194   
195   show "(Aheap \<Gamma> e\<cdot>a) x = up\<cdot>0"
196   proof(cases "nonrec \<Gamma>")
197     case False
198     from False `x \<in> thunks \<Gamma>`  `x \<in> edom (Aheap \<Gamma> e\<cdot>a)`
199     show ?thesis  by (rule aHeap_thunks_rec)
200   next
201     case True
202     with `p \<in> paths (Fheap \<Gamma> e\<cdot>a)`
203     have "p \<in> valid_lists (edom (Aheap \<Gamma> e\<cdot>a)) (ccExp e\<cdot>a)" by (simp add: Fheap_simp)
204
205     with `\<not> one_call_in_path x p`
206     have "x \<in> ccManyCalls (ccExp e\<cdot>a)" by (rule valid_lists_many_calls)
207   
208     from True `x \<in> thunks \<Gamma>` this
209     show ?thesis by (rule aHeap_thunks_nonrec)
210   qed
211 next
212   fix \<Delta> e a
213
214   show "ftree_restr (- domA \<Delta>) (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>)  (Fexp e\<cdot>a)) \<sqsubseteq> Fexp (Let \<Delta> e)\<cdot>a"
215   unfolding Fexp_simp
216   proof (rule below_ccFTreeI)
217     have "carrier (ftree_restr (- domA \<Delta>) (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a))))
218        = carrier (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a))) - domA \<Delta>"
219         by auto
220     also
221     have "carrier (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a)))
222          \<subseteq> edom (ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a) \<squnion> Aexp e\<cdot>a)"
223     proof (rule carrier_substitute_below)
224     show "carrier (ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a)) \<subseteq> edom (ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a) \<squnion> Aexp e\<cdot>a)" by simp
225     next
226       fix x
227       assume "x \<in> edom (ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a) \<squnion> Aexp e\<cdot>a)"
228       show "carrier ((ExpAnalysis.AnalBinds Fexp \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x) \<subseteq> edom (ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a) \<squnion> Aexp e\<cdot>a)"
229       proof(cases "map_of \<Delta> x")
230         case None thus ?thesis by (simp add: Fexp.AnalBinds_lookup)
231       next
232         case (Some e')
233         hence "carrier ((ExpAnalysis.AnalBinds Fexp \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x) = carrier (fup\<cdot>(Fexp e')\<cdot>((Aheap \<Delta> e\<cdot>a) x))"
234             by (simp add: Fexp.AnalBinds_lookup)
235         also have "\<dots> \<subseteq> edom (fup\<cdot>(Aexp e')\<cdot>((Aheap \<Delta> e\<cdot>a) x))"
236           by (auto simp add: Fexp_simp)
237         also have "\<dots> = edom (ABind x e'\<cdot>(Aheap \<Delta> e\<cdot>a))" by (simp add: ABind_def)
238         also have "\<dots> \<subseteq> edom (ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a))" using Some
239           by (rule edom_mono[OF monofun_cfun_fun[OF ABind_below_ABinds]])
240         also have "\<dots> \<subseteq> edom (ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a) \<squnion> Aexp e\<cdot>a)" by simp
241         finally show ?thesis.
242       qed
243     qed
244     also have "\<dots> \<subseteq> edom (Aheap \<Delta> e\<cdot>a \<squnion> Aexp (Let \<Delta> e)\<cdot>a)"
245       by (rule edom_mono[OF Aexp_Let])
246     also have "edom (Aheap \<Delta> e\<cdot>a \<squnion> Aexp (Let \<Delta> e)\<cdot>a) - domA \<Delta> = edom (Aexp (Let \<Delta> e)\<cdot>a)"
247       by (auto dest: set_mp[OF edom_Aheap] set_mp[OF Aexp_edom])
248     finally
249     show "carrier (ftree_restr (- domA \<Delta>) (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a))))
250           \<subseteq> edom (Aexp (Terms.Let \<Delta> e)\<cdot>a)"  by this auto
251   next
252     let ?x = "ccApprox (ftree_restr (- domA \<Delta>) (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a))))"
253   
254     have "?x = cc_restr (- domA \<Delta>) ?x"  by simp
255     also have "\<dots> \<sqsubseteq> cc_restr (- domA \<Delta>) (ccHeap \<Delta> e\<cdot>a)"
256     proof(rule cc_restr_mono2[OF wild_recursion_thunked])
257     (*
258       have "ccLinear (domA \<Delta>) (ccExp e\<cdot>a)" using linear by (rule linear_Exp)
259       thus "ccLinear (domA \<Delta>) (ccApprox (ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a)))"
260         by auto
261     next
262     *)
263       have "ccExp e\<cdot>a \<sqsubseteq> ccHeap \<Delta> e\<cdot>a" by (rule ccHeap_Exp)
264       thus "ccApprox (ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a)) \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
265         by (auto intro: below_trans[OF cc_restr_below_arg])
266     next
267       fix x
268       assume "x \<notin> domA \<Delta>"
269       thus "(Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x = empty"
270         by (metis Fexp.AnalBinds_not_there empty_is_bottom)
271     next
272       fix x
273       assume "x \<in> domA \<Delta>"
274       then obtain e' where e': "map_of \<Delta> x = Some e'" by (metis domA_map_of_Some_the)
275       
276       (*
277       thus "ccLinear (domA \<Delta>) (ccApprox ((Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x))"
278       proof(cases "(Aheap \<Delta> e\<cdot>a) x")
279         case bottom thus ?thesis using e' by (simp add: Fexp.AnalBinds_lookup)
280       next
281         case (up a')
282         with linear e'
283         have "ccLinear (domA \<Delta>) (ccExp e'\<cdot>a')" by (rule linear_Heap)
284         thus ?thesis using up e' by (auto simp add: Fexp.AnalBinds_lookup Fexp_simp)
285       qed
286       *)
287       
288       show "ccApprox ((Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x) \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
289       proof(cases "(Aheap \<Delta> e\<cdot>a) x")
290         case bottom thus ?thesis using e' by (simp add: Fexp.AnalBinds_lookup)
291       next
292         case (up a')
293         with e'
294         have "ccExp e'\<cdot>a' \<sqsubseteq> ccHeap \<Delta> e\<cdot>a" by (rule ccHeap_Heap)
295         thus ?thesis using up e'
296           by (auto simp add: Fexp.AnalBinds_lookup Fexp_simp  intro: below_trans[OF cc_restr_below_arg])
297       qed
298
299       show "ccProd (ccNeighbors x (ccHeap \<Delta> e\<cdot>a)- {x} \<inter> thunks \<Delta>) (carrier ((Fexp.AnalBinds  \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x)) \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
300       proof(cases "(Aheap \<Delta> e\<cdot>a) x")
301         case bottom thus ?thesis using e' by (simp add: Fexp.AnalBinds_lookup)
302       next
303         case (up a')
304         have subset: "(carrier (fup\<cdot>(Fexp e')\<cdot>((Aheap \<Delta> e\<cdot>a) x))) \<subseteq> fv e'"
305           using up e' by (auto simp add: Fexp.AnalBinds_lookup carrier_Fexp dest!: set_mp[OF Aexp_edom])
306         
307         from e' up
308         have "ccProd (fv e') (ccNeighbors x (ccHeap \<Delta> e\<cdot>a) - {x} \<inter> thunks \<Delta>) \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
309           by (rule ccHeap_Extra_Edges)
310         then
311         show ?thesis using e'
312           by (simp add: Fexp.AnalBinds_lookup  Fexp_simp ccProd_comm  below_trans[OF ccProd_mono1[OF subset]])
313       qed
314     qed
315     also have "\<dots> \<sqsubseteq> ccExp (Let \<Delta> e)\<cdot>a"
316       by (rule ccExp_Let)
317     finally
318     show "ccApprox (ftree_restr (- domA \<Delta>) (substitute (ExpAnalysis.AnalBinds Fexp \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a))))
319         \<sqsubseteq> ccExp (Terms.Let \<Delta> e)\<cdot>a" by this simp_all
320
321   qed
322
323   have "carrier (substitute (ExpAnalysis.AnalBinds Fexp \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a)) \<subseteq> edom (Aheap \<Delta> e\<cdot>a) \<union> edom (Aexp (Let \<Delta> e)\<cdot>a)"
324   proof(rule carrier_substitute_below)
325     from edom_mono[OF Aexp_Let[of \<Delta> e a]]
326     show "carrier (Fexp e\<cdot>a) \<subseteq> edom (Aheap \<Delta> e\<cdot>a) \<union> edom (Aexp (Let \<Delta> e)\<cdot>a)"  by (simp add: Fexp_def)
327   next
328     fix x
329     assume "x \<in> edom (Aheap \<Delta> e\<cdot>a) \<union> edom (Aexp (Let \<Delta> e)\<cdot>a)"
330     hence "x \<in> edom (Aheap \<Delta> e\<cdot>a) \<or> x : (edom (Aexp (Let \<Delta> e)\<cdot>a))" by simp
331     thus "carrier ((Fexp.AnalBinds  \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x) \<subseteq> edom (Aheap \<Delta> e\<cdot>a) \<union> edom (Aexp (Let \<Delta> e)\<cdot>a)"
332     proof
333       assume "x \<in> edom (Aheap \<Delta> e\<cdot>a)"
334       
335       have "carrier ((Fexp.AnalBinds  \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x) \<subseteq> edom (ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a))"
336         by (rule carrier_AnalBinds_below)
337       also have "\<dots> \<subseteq> edom (Aheap \<Delta> e\<cdot>a \<squnion> Aexp (Terms.Let \<Delta> e)\<cdot>a)"
338         using edom_mono[OF Aexp_Let[of \<Delta> e a]] by simp
339       finally show ?thesis by simp
340     next
341       assume "x \<in> edom (Aexp (Terms.Let \<Delta> e)\<cdot>a)"
342       hence "x \<notin> domA \<Delta>" by (auto  dest: set_mp[OF Aexp_edom])
343       hence "(Fexp.AnalBinds  \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x = \<bottom>"
344         by (rule Fexp.AnalBinds_not_there)
345       thus ?thesis by simp
346     qed
347   qed
348   hence "carrier (substitute (ExpAnalysis.AnalBinds Fexp \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a)) \<subseteq> edom (Aheap \<Delta> e\<cdot>a) \<union> - domA \<Delta>"
349     by (rule order_trans) (auto dest: set_mp[OF Aexp_edom])
350   hence "ftree_restr (domA \<Delta>)            (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a))
351       = ftree_restr (edom (Aheap \<Delta> e\<cdot>a)) (ftree_restr (domA \<Delta>) (substitute (Fexp.AnalBinds  \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a)))"
352     by -(rule ftree_restr_noop[symmetric], auto)
353   also
354   have "\<dots> = ftree_restr (edom (Aheap \<Delta> e\<cdot>a)) (substitute (Fexp.AnalBinds  \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a))"
355     by (simp add: inf.absorb2[OF edom_Aheap ])
356   also
357   (*
358   have "substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a) \<sqsubseteq> singles (calledOnce \<Delta> e a)"
359   proof(rule substitute_below_singlesI)
360     show "Fexp e\<cdot>a \<sqsubseteq> singles (calledOnce \<Delta> e a)"
361       unfolding Fexp_simp
362       using calledOnce_exp
363       by (auto intro!: ccFTree_below_singleI)
364   next
365     fix x
366     show "carrier ((Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x) \<inter> calledOnce \<Delta> e a = {}"
367       using calledOnce_heap[unfolded disjoint_iff_not_equal]
368       by (force simp add: Fexp.AnalBinds_lookup Fexp_simp split: option.split)
369   qed
370   hence "ftree_restr (edom (Aheap \<Delta> e\<cdot>a)) (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a))
371       \<sqsubseteq> ftree_restr (edom (Aheap \<Delta> e\<cdot>a)) (singles (calledOnce \<Delta> e a))"
372     by (rule ftree_restr_mono)
373   *)
374   have "\<dots> \<sqsubseteq> Fheap \<Delta> e \<cdot>a"
375   proof(cases "nonrec \<Delta>")
376     case False
377     have "ftree_restr (edom (Aheap \<Delta> e\<cdot>a)) (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a))
378       \<sqsubseteq> ftree_restr (edom (Aheap \<Delta> e\<cdot>a)) anything"
379     by (rule ftree_restr_mono) simp
380     also have "\<dots> = Fheap \<Delta> e\<cdot>a"
381       by (simp add:  Fheap_simp False)
382     finally show ?thesis.
383   next
384     case True[simp]
385
386     from True
387     have "ftree_restr (edom (Aheap \<Delta> e\<cdot>a)) (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a))
388        = ftree_restr (edom (Aheap \<Delta> e\<cdot>a)) (Fexp e\<cdot>a)"
389       by (rule nonrecE) (rule ftree_rest_substitute, auto simp add: carrier_Fexp fv_def fresh_def dest!: set_mp[OF edom_Aheap] set_mp[OF Aexp_edom])
390     also have "\<dots> = ccFTree (edom (Aexp e\<cdot>a) \<inter> edom (Aheap \<Delta> e\<cdot>a)) (ccExp e\<cdot>a)"
391       by (simp add: Fexp_simp)
392     also have "\<dots> \<sqsubseteq> ccFTree (edom (Aexp e\<cdot>a) \<inter> domA \<Delta>) (ccExp e\<cdot>a)"
393       by (rule ccFTree_mono1[OF Int_mono[OF order_refl edom_Aheap]])
394     also have "\<dots> \<sqsubseteq> ccFTree (edom (Aheap \<Delta> e\<cdot>a)) (ccExp e\<cdot>a)"
395       by (rule ccFTree_mono1[OF edom_mono[OF Aheap_nonrec[OF True], simplified]])
396     also have "\<dots> \<sqsubseteq> Fheap \<Delta> e\<cdot>a"
397       by (simp add: Fheap_simp)
398     finally
399     show ?thesis by this simp_all
400   qed
401   finally
402   show "ftree_restr (domA \<Delta>) (substitute (ExpAnalysis.AnalBinds Fexp \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a)) \<sqsubseteq> Fheap \<Delta> e\<cdot>a".
403
404 qed
405 end
406
407 (* TODO: Unused stuff from here, mostly about singles. Might be useful later. *)
408
409
410 lemma paths_singles: "xs \<in> paths (singles S) \<longleftrightarrow> (\<forall>x \<in> S. one_call_in_path x xs)"
411   by transfer (auto simp add: one_call_in_path_filter_conv)
412
413 lemma paths_singles': "xs \<in> paths (singles S) \<longleftrightarrow> (\<forall>x \<in> (set xs \<inter> S). one_call_in_path x xs)"
414   apply transfer
415   apply (auto simp add: one_call_in_path_filter_conv)
416   apply (erule_tac x = x in ballE)
417   apply auto
418   by (metis (poly_guards_query) filter_empty_conv le0 length_0_conv)
419
420 lemma both_below_singles1:
421   assumes "t \<sqsubseteq> singles S"
422   assumes "carrier t' \<inter> S = {}"
423   shows "t \<otimes>\<otimes> t' \<sqsubseteq> singles S"
424 proof (rule ftree_belowI)
425   fix xs
426   assume "xs \<in> paths (t \<otimes>\<otimes> t')"
427   then obtain ys zs where "ys \<in> paths t" and "zs \<in> paths t'" and "xs \<in> ys \<otimes> zs" by (auto simp add: paths_both)
428   with assms 
429   have "ys \<in> paths (singles S)" and "set zs \<inter> S = {}"
430     by (metis below_ftree.rep_eq contra_subsetD paths.rep_eq, auto simp add: Union_paths_carrier[symmetric])
431   with `xs \<in> ys \<otimes> zs`
432   show "xs \<in> paths (singles S)"
433     by (induction) (auto simp add: paths_singles no_call_in_path_set_conv interleave_set dest: more_than_one_setD split: if_splits)
434 qed
435
436
437 lemma paths_ftree_restr_singles: "xs \<in> paths (ftree_restr S' (singles S)) \<longleftrightarrow> set xs \<subseteq> S' \<and> (\<forall>x \<in> S. one_call_in_path x xs)"
438 proof
439   show "xs \<in> paths (ftree_restr S' (singles S)) \<Longrightarrow>  set xs \<subseteq> S' \<and> (\<forall>x \<in> S. one_call_in_path x xs)"
440     by (auto simp add: filter_paths_conv_free_restr[symmetric] paths_singles)
441 next
442   assume *: "set xs \<subseteq> S' \<and> (\<forall>x\<in>S. one_call_in_path x xs)"
443   hence "set xs \<subseteq> S'" by auto
444   hence [simp]: "filter (\<lambda> x'. x' \<in> S') xs = xs" by (auto simp add: filter_id_conv)
445   
446   from *
447   have "xs \<in> paths (singles S)"
448      by (auto simp add: paths_singles')
449   hence "filter (\<lambda> x'. x' \<in> S') xs \<in> filter (\<lambda>x'. x' \<in> S') ` paths (singles S)"
450     by (rule imageI)
451   thus "xs \<in> paths (ftree_restr S' (singles S))"
452     by (auto simp add: filter_paths_conv_free_restr[symmetric] )
453 qed
454
455
456
457 (* TODO: unused *)
458 lemma substitute_not_carrier:
459   assumes "x \<notin> carrier t"
460   assumes "\<And> x'. x \<notin> carrier (f x')"
461   shows "x \<notin>  carrier (substitute f T t)"
462 proof-
463   have "ftree_restr ({x}) (substitute f T t) = ftree_restr ({x}) t"
464   proof(rule ftree_rest_substitute)
465     fix x'
466     from `x \<notin> carrier (f x')`
467     show "carrier (f x') \<inter> {x} = {}" by auto
468   qed
469   hence "x \<notin> carrier (ftree_restr ({x}) (substitute f T t)) \<longleftrightarrow> x \<notin> carrier (ftree_restr ({x}) t)" by metis
470   with assms(1)
471   show ?thesis by simp
472 qed
473
474 (* TODO: unused *)
475 lemma substitute_below_singlesI:
476   assumes "t \<sqsubseteq> singles S"
477   assumes "\<And> x. carrier (f x) \<inter> S = {}"
478   shows "substitute f T t \<sqsubseteq> singles S"
479 proof(rule ftree_belowI)
480   fix xs
481   assume "xs \<in> paths (substitute f T t)"
482   thus "xs \<in> paths (singles S)"
483   using assms
484   proof(induction f T t xs arbitrary: S rule: substitute_induct)
485     case Nil
486     thus ?case by simp
487   next
488     case (Cons f T t x xs)
489
490     from `x#xs \<in> _`
491     have xs: "xs \<in> paths (substitute (f_nxt f T x) T (nxt t x \<otimes>\<otimes> f x))" by auto
492     moreover
493
494     from `t \<sqsubseteq> singles S`
495     have "nxt t x \<sqsubseteq> singles S" 
496       by (metis "FTree-HOLCF.nxt_mono" below_trans nxt_singles_below_singles)
497     from this `carrier (f x) \<inter> S = {}`
498     have "nxt t x \<otimes>\<otimes> f x \<sqsubseteq> singles S"
499       by (rule both_below_singles1)
500     moreover
501     { fix x'
502       from  `carrier (f x') \<inter> S = {}`
503       have "carrier (f_nxt f T x x') \<inter> S = {}"
504         by (auto simp add: f_nxt_def)
505     }
506     ultimately
507     have IH: "xs \<in> paths (singles S)"
508       by (rule Cons.IH) 
509   
510   show ?case
511     proof(cases "x \<in> S")
512       case True
513       with `carrier (f x) \<inter> S = {}`
514       have "x \<notin> carrier (f x)" by auto
515       moreover
516       from `t \<sqsubseteq> singles S`
517       have "nxt t x \<sqsubseteq> nxt (singles S) x" by (rule nxt_mono)
518       hence "carrier (nxt t x) \<subseteq> carrier (nxt (singles S) x)" by (rule carrier_mono)
519       from set_mp[OF this] True
520       have "x \<notin> carrier (nxt t x)" by auto
521       ultimately
522       have "x \<notin> carrier (nxt t x \<otimes>\<otimes> f x)" by simp
523       hence "x \<notin> carrier (substitute (f_nxt f T x) T (nxt t x \<otimes>\<otimes> f x))"
524       proof(rule substitute_not_carrier)
525         fix x'  
526         from `carrier (f x') \<inter> S = {}` `x \<in> S`
527         show "x \<notin> carrier (f_nxt f T x x')" by (auto simp add: f_nxt_def)
528       qed
529       with xs
530       have "x \<notin> set xs" by (auto simp add: Union_paths_carrier[symmetric])
531       with IH
532       have "xs \<in> paths (without x (singles S))" by (rule paths_withoutI)
533       thus ?thesis using True by (simp add: Cons_path)
534     next
535       case False
536       with IH
537       show ?thesis by (simp add: Cons_path)
538     qed
539   qed
540 qed
541
542 (* TODO: Unused. Remove? *)
543 lemma multi_calls_ccFTree:
544   assumes "xs \<in> paths (ccFTree S G)"
545   assumes "\<not> one_call_in_path x xs"
546   shows "x \<in> S" and "x \<in> ccManyCalls G"
547 proof-
548   from assms(1) have "xs \<in> valid_lists S G" by simp 
549
550   have "x \<in> set xs" by (metis assms(2) filter_True one_call_in_path_filter)
551   with `xs \<in> valid_lists S G`
552   show "x \<in> S" by (metis  subsetCE valid_lists_subset)
553
554   show "x \<in> ccManyCalls G"
555   proof(rule ccontr)
556     assume "x \<notin> ccManyCalls G"
557     with `xs \<in> valid_lists S G` 
558     have "one_call_in_path x xs"
559     by (induction rule: valid_lists.induct) (auto simp add: no_call_in_path_set_conv)
560     with assms(2)
561     show False..
562   qed
563 qed
564
565
566 end