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