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