Split CoCallCardinality into CoCall* modules
[darcs-mirror-isa-launchbury.git] / Launchbury / CoCallImplCorrect.thy
1 theory CoCallImplCorrect
2 imports CoCallAnalysisImpl CoCallAnalysisSpec ArityAnalysisFixProps
3 begin
4
5 lemma ccField_fup_CCexp:
6   "ccField (fup\<cdot>(CCexp e)\<cdot>n) \<subseteq> fv e"
7 by (cases n) (auto dest: set_mp[OF ccField_CCexp])
8
9 lemma cc_restr_fup_ccExp_useless[simp]: "cc_restr (fv e) (fup\<cdot>(CCexp e)\<cdot>n) = fup\<cdot>(CCexp e)\<cdot>n"
10   by (rule cc_restr_noop[OF ccField_fup_CCexp])
11
12 interpretation ArityAnalysis Aexp.
13
14 lemma Aexp_edom': "edom (Aexp e\<cdot>a) \<subseteq> fv e"
15   by (induction e arbitrary: a rule: exp_induct_rec)(auto)
16
17
18 interpretation EdomArityAnalysis Aexp by default (rule Aexp_edom')
19  
20 lemma ccField_CCfix: "ccField (CCfix \<Gamma>\<cdot>(ae, CCexp  e\<cdot>a)) \<subseteq> fv \<Gamma> \<union> fv e"
21   unfolding CCfix_def
22   apply simp
23   apply (rule fix_ind)
24   apply simp_all
25   apply (auto simp add: ccBindsExtra_simp ccBinds_eq ccBind_eq ccField_ccProd
26              dest: set_mp[OF ccField_CCexp]
27              dest!: set_mp[OF ccField_fup_CCexp]
28              dest: set_mp[OF map_of_Some_fv_subset]
29              dest!: elem_to_ccField
30              split: if_splits)
31   done
32
33 lemma Aexp_lam_simp[simp]: "Aexp (Lam [x]. e) \<cdot> n = env_delete x (Aexp e \<cdot> (pred \<cdot> n))"
34 proof-
35   have "Aexp (Lam [x]. e) \<cdot> n = Aexp e\<cdot>(pred\<cdot>n) f|` (fv e - {x})" by simp
36   also have "... = env_delete x (Aexp e\<cdot>(pred\<cdot>n)) f|` (fv e - {x})" by simp
37   also have "\<dots> = env_delete x (Aexp e\<cdot>(pred\<cdot>n))"
38      by (rule env_restr_useless) (auto dest: set_mp[OF Aexp_edom])
39   finally show ?thesis.
40 qed
41 declare Aexp_simps(2)[simp del]
42
43 lemma Aexp_Let_simp1[simp]:
44   "\<not> nonrec \<Gamma> \<Longrightarrow> Aexp (Let \<Gamma> e)\<cdot>n = (Afix \<Gamma>\<cdot>(Aexp e\<cdot>n \<squnion> (\<lambda>_.up\<cdot>0) f|` thunks \<Gamma>)) f|` (- domA \<Gamma>)"
45   unfolding Aexp_simps
46   by (rule env_restr_cong) (auto dest!: set_mp[OF Afix_edom] set_mp[OF Aexp_edom] set_mp[OF thunks_domA])
47
48 lemma Aexp_Let_simp2[simp]:
49   "atom x \<sharp> e \<Longrightarrow> Aexp (let x be e in exp)\<cdot>n = env_delete x (fup\<cdot>(Aexp e)\<cdot>(ABind_nonrec x e \<cdot> (Aexp exp\<cdot>n, CCexp exp\<cdot>n)) \<squnion> Aexp exp\<cdot>n)"
50   unfolding Aexp_simps env_delete_restr
51   by (rule env_restr_cong) (auto dest!: set_mp[OF fup_Aexp_edom]  set_mp[OF Aexp_edom])
52
53 declare Aexp_simps(4)[simp del]
54 declare Aexp_simps(5)[simp del]
55
56
57 lemma CCexp_Let_simp1[simp]:
58   "\<not> nonrec \<Gamma> \<Longrightarrow> CCexp (Let \<Gamma> e)\<cdot>n = cc_restr (- domA \<Gamma>) (CCfix \<Gamma>\<cdot>(Afix \<Gamma>\<cdot>(Aexp e\<cdot>n \<squnion> (\<lambda>_.up\<cdot>0) f|` (thunks \<Gamma>)), CCexp e\<cdot>n))"
59   unfolding CCexp_simps
60   by (rule cc_restr_intersect)  (auto dest!: set_mp[OF ccField_CCfix])
61
62 lemma CCexp_Let_simp2[simp]:
63   "atom x \<sharp> e \<Longrightarrow> CCexp (let x be e in exp)\<cdot>n = cc_restr (- {x}) (ccBind x e \<cdot>(Aheap_nonrec x e\<cdot>(Aexp exp\<cdot>n, CCexp exp\<cdot>n), CCexp exp\<cdot>n) \<squnion> ccProd (fv e) (ccNeighbors x (CCexp exp\<cdot>n) - (if isLam e then {} else {x})) \<squnion> CCexp exp\<cdot>n)"
64   unfolding CCexp_simps
65   by (rule cc_restr_intersect)
66      (auto simp add: ccField_ccProd ccBind_eq dest!: set_mp[OF ccField_CCexp]  set_mp[OF ccField_fup_CCexp] set_mp[OF ccField_cc_restr] set_mp[OF ccNeighbors_ccField])
67 declare CCexp_simps(4)[simp del]
68 declare CCexp_simps(5)[simp del]
69
70 lemma ccNeighbors_Int_ccrestr: "(ccNeighbors x G \<inter> S) = ccNeighbors x (cc_restr (insert x S) G) \<inter> S"
71   by transfer auto
72   
73 lemma 
74   assumes "x \<notin> S" and "y \<notin> S"
75   shows CCexp_subst: "cc_restr S (CCexp e[y::=x]\<cdot>a) = cc_restr S (CCexp e\<cdot>a)"
76     and Aexp_restr_subst: "(Aexp e[y::=x]\<cdot>a) f|` S = (Aexp e\<cdot>a) f|` S"
77 using assms
78 proof (nominal_induct e avoiding: x y  arbitrary: a  S rule: exp_strong_induct_rec_set)
79   case (Var b v) 
80   case 1 show ?case by auto
81   case 2 thus ?case by auto
82 next
83   case (App e v)
84   case 1
85     with App show ?case
86     by (auto simp add: Int_insert_left fv_subst_int simp del: join_comm intro: join_mono)
87   case 2
88     with App show ?case
89      by (auto simp add: env_restr_join simp del: fun_meet_simp)
90 next
91   case (Lam v e)
92   case 1
93     with Lam
94     show ?case
95       by (auto simp add: cc_restr_predCC  Diff_Int_distrib2 fv_subst_int env_restr_join env_delete_env_restr_swap[symmetric])
96   case 2
97     with Lam
98     show ?case
99       by (auto simp add: env_restr_join env_delete_env_restr_swap[symmetric]  simp del: fun_meet_simp)
100 next
101   case (Let \<Gamma> e x y)
102   hence [simp]: "x \<notin> domA \<Gamma> " "y \<notin> domA \<Gamma>"
103     by (metis (erased, hide_lams) bn_subst domA_not_fresh fresh_def fresh_star_at_base fresh_star_def obtain_fresh subst_is_fresh(2))+
104
105   note Let(1,2)[simp]
106
107   from Let(3)
108   have "\<not> nonrec (\<Gamma>[y::h=x])"  by (simp add: nonrec_subst)
109
110   case 1[simp]
111   have "cc_restr (S \<union> domA \<Gamma>) (CCfix \<Gamma>[y::h=x]\<cdot>(Afix \<Gamma>[y::h=x]\<cdot>(Aexp e[y::=x]\<cdot>a \<squnion> (\<lambda>_. up\<cdot>0) f|` thunks \<Gamma>), CCexp e[y::=x]\<cdot>a)) =
112         cc_restr (S \<union> domA \<Gamma>) (CCfix \<Gamma>\<cdot>        (Afix \<Gamma>\<cdot>        (Aexp e\<cdot>       a \<squnion> (\<lambda>_. up\<cdot>0) f|` thunks \<Gamma>), CCexp e\<cdot>       a))"
113     apply (subst CCfix_restr_subst')
114       apply (erule Let(4))
115       apply auto[5]
116     apply (subst CCfix_restr) back
117       apply simp
118     apply (subst Afix_restr_subst')
119       apply (erule Let(5))
120       apply auto[5]
121     apply (subst Afix_restr) back
122       apply simp
123     apply (simp only: env_restr_join)
124     apply (subst Let(7))
125       apply auto[2]
126     apply (subst Let(6))
127       apply auto[2]
128     apply rule
129     done
130   thus ?case using Let(1,2) `\<not> nonrec \<Gamma>` `\<not> nonrec (\<Gamma>[y::h=x])`
131     by (auto simp add: fresh_star_Pair  elim: cc_restr_eq_subset[rotated] )
132
133   case 2[simp]
134   have "Afix \<Gamma>[y::h=x]\<cdot>(Aexp e[y::=x]\<cdot>a \<squnion> (\<lambda>_. up\<cdot>0) f|` (thunks \<Gamma>)) f|` (S \<union> domA \<Gamma>) = Afix \<Gamma>\<cdot>(Aexp e\<cdot>a \<squnion> (\<lambda>_. up\<cdot>0) f|` (thunks \<Gamma>)) f|` (S \<union> domA \<Gamma>)"
135     apply (subst Afix_restr_subst')
136       apply (erule Let(5))
137       apply auto[5]
138     apply (subst Afix_restr) back
139       apply auto[1]
140     apply (simp only: env_restr_join)
141     apply (subst Let(7))
142       apply auto[2]
143     apply rule
144     done
145   thus ?case using Let(1,2)
146     using `\<not> nonrec \<Gamma>` `\<not> nonrec (\<Gamma>[y::h=x])`
147     by (auto simp add: fresh_star_Pair elim:env_restr_eq_subset[rotated])
148 next
149   case (Let_nonrec x' e exp x y)
150
151   from Let_nonrec(1,2)
152   have [simp]: "x \<noteq> x'" "y \<noteq> x'" by (simp_all add: fresh_at_base)
153
154   note Let_nonrec(1,2,3)[simp]
155   
156   have [simp]: "atom x' \<sharp> e[y::=x]"
157     by (simp add: subst_pres_fresh2)
158
159   case 1[simp]
160
161   have "\<And> a. cc_restr {x'} (CCexp exp[y::=x]\<cdot>a) = cc_restr {x'} (CCexp exp\<cdot>a)"
162    by (rule Let_nonrec(6)) auto
163   from arg_cong[where f = "\<lambda>x.  x'--x'\<in>x", OF this]
164   have [simp]: "x'--x'\<in>CCexp  exp[y::=x]\<cdot>a \<longleftrightarrow> x'--x'\<in>CCexp exp\<cdot>a" by auto
165
166   have [simp]: "\<And> a. Aexp e[y::=x]\<cdot>a f|` S = Aexp e\<cdot>a f|` S"
167     by (rule Let_nonrec(5)) auto
168
169   have [simp]: "\<And> a. fup\<cdot>(Aexp e[y::=x])\<cdot>a f|` S = fup\<cdot>(Aexp e)\<cdot>a f|` S"
170     by (case_tac a) auto
171
172   have [simp]: "Aexp  exp[y::=x]\<cdot>a f|` S = Aexp exp\<cdot>a f|` S"
173     by (rule Let_nonrec(7)) auto
174
175   have "Aexp exp[y::=x]\<cdot>a f|` {x'} = Aexp exp\<cdot>a f|` {x'}"
176     by (rule Let_nonrec(7)) auto
177   from fun_cong[OF this, where x = x']
178   have [simp]: "(Aexp exp[y::=x]\<cdot>a) x' = (Aexp exp\<cdot>a) x'" by auto
179
180   have [simp]:  "\<And> a. cc_restr S (CCexp exp[y::=x]\<cdot>a) = cc_restr S (CCexp exp\<cdot>a)"
181     by (rule Let_nonrec(6)) auto
182
183   have [simp]:  "\<And> a. cc_restr S (CCexp e[y::=x]\<cdot>a) = cc_restr S (CCexp e\<cdot>a)"
184     by (rule Let_nonrec(4)) auto
185
186   have [simp]: "\<And> a. cc_restr S (fup\<cdot>(CCexp e[y::=x])\<cdot>a) = cc_restr S (fup\<cdot>(CCexp e)\<cdot>a)"
187     by (rule fup_ccExp_restr_subst') simp
188
189   have [simp]: "fv e[y::=x] \<inter> S = fv e \<inter> S"
190     by (auto simp add: fv_subst_eq)
191
192   have [simp]:
193     "ccNeighbors x' (CCexp exp[y::=x]\<cdot>a) \<inter> - {x'} \<inter> S = ccNeighbors x' (CCexp exp\<cdot>a)  \<inter> - {x'} \<inter> S"
194     apply (simp only: Int_assoc)
195     apply (subst (1 2) ccNeighbors_Int_ccrestr)
196     apply (subst Let_nonrec(6))
197       apply auto[2]
198     apply rule
199     done
200
201   have [simp]:
202     "ccNeighbors x' (CCexp exp[y::=x]\<cdot>a) \<inter> S = ccNeighbors x' (CCexp exp\<cdot>a) \<inter> S"
203     apply (subst (1 2) ccNeighbors_Int_ccrestr)
204     apply (subst Let_nonrec(6))
205       apply auto[2]
206     apply rule
207     done
208
209   show "cc_restr S (CCexp (let x' be e in exp )[y::=x]\<cdot>a) = cc_restr S (CCexp (let x' be e in exp )\<cdot>a)"
210     apply (subst subst_let_be)
211       apply auto[2]
212     apply (subst (1 2) CCexp_Let_simp2)
213       apply fact+
214     apply (simp only:  cc_restr_twist[where S = S] )
215     apply (rule arg_cong) back
216     apply (simp add:  Diff_eq ccBind_eq ABind_nonrec_eq)
217     done
218
219   show "Aexp (let x' be e in exp )[y::=x]\<cdot>a f|` S = Aexp (let x' be e in exp )\<cdot>a f|` S"
220     by (simp add: env_restr_join env_delete_env_restr_swap[symmetric] ABind_nonrec_eq)
221 qed
222    
223 interpretation CorrectArityAnalysis Aexp
224   by default (simp_all add:Aexp_restr_subst)
225
226 definition Aheap where
227   "Aheap \<Gamma> e = (\<Lambda> a. if nonrec \<Gamma> then (split Aheap_nonrec (hd \<Gamma>))\<cdot>(Aexp e\<cdot>a, CCexp e\<cdot>a) else  (Afix \<Gamma> \<cdot> (Aexp e\<cdot>a \<squnion> (\<lambda>_.up\<cdot>0) f|` thunks \<Gamma>)) f|` domA \<Gamma>)"
228
229 lemma Aheap_simp1[simp]:
230   "\<not> nonrec \<Gamma> \<Longrightarrow> Aheap \<Gamma> e \<cdot>a = (Afix \<Gamma> \<cdot> (Aexp e\<cdot>a \<squnion> (\<lambda>_.up\<cdot>0) f|` thunks \<Gamma>)) f|` domA \<Gamma>"
231   unfolding Aheap_def by simp
232
233 lemma Aheap_simp2[simp]:
234   "atom x \<sharp> e' \<Longrightarrow> Aheap [(x,e')] e \<cdot>a = Aheap_nonrec x e'\<cdot>(Aexp e\<cdot>a, CCexp e\<cdot>a)"
235   unfolding Aheap_def by (simp add: nonrec_def)
236
237 lemma Aheap_eqvt'[eqvt]:
238   "\<pi> \<bullet> (Aheap \<Gamma> e) = Aheap (\<pi> \<bullet> \<Gamma>) (\<pi> \<bullet> e)"
239   apply (rule cfun_eqvtI)
240   apply (cases nonrec \<pi> rule: eqvt_cases[where x = \<Gamma>])
241   apply simp
242   apply (erule nonrecE)
243   apply simp
244   apply (perm_simp, rule)
245   apply simp
246   apply (perm_simp, rule)
247   done
248
249 interpretation CorrectArityAnalysisLet Aexp Aheap
250 proof default
251   fix \<pi> show "\<pi> \<bullet> Aheap = Aheap"
252     by perm_simp rule
253 next
254   fix \<Gamma> e a
255   show "edom (Aheap \<Gamma> e\<cdot>a) \<subseteq> domA \<Gamma>"
256     by (cases "nonrec \<Gamma>")
257        (auto simp add: Aheap_nonrec_simp dest: set_mp[OF edom_esing_subset] elim!: nonrecE)
258 next
259   fix x y :: var and \<Gamma> :: heap and e :: exp
260   assume assms: "x \<notin> domA \<Gamma>"  "y \<notin> domA \<Gamma>"
261
262   from Aexp_restr_subst[OF assms(2,1)]
263   have **: "\<And> a. Aexp e[x::=y]\<cdot>a f|` domA \<Gamma> = Aexp e\<cdot>a f|` domA \<Gamma>".
264
265   show "Aheap \<Gamma>[x::h=y] e[x::=y] = Aheap \<Gamma> e"
266   proof(cases "nonrec \<Gamma>")
267     case False[simp]
268
269     from assms
270     have "atom ` domA \<Gamma> \<sharp>* x" and "atom ` domA \<Gamma> \<sharp>* y"
271       by (auto simp add: fresh_star_at_base image_iff)
272     hence [simp]: "\<not> nonrec (\<Gamma>[x::h=y])"
273       by (simp add: nonrec_subst)
274
275     show ?thesis
276     apply (rule cfun_eqI)
277     apply simp
278     apply (subst Afix_restr_subst[OF assms subset_refl])
279     apply (subst Afix_restr[OF  subset_refl]) back
280     apply (simp add: env_restr_join)
281     apply (subst **)
282     apply simp
283     done
284   next
285     case True
286     
287     from assms
288     have "atom ` domA \<Gamma> \<sharp>* x" and "atom ` domA \<Gamma> \<sharp>* y"
289       by (auto simp add: fresh_star_at_base image_iff)
290     with True
291     have *: "nonrec (\<Gamma>[x::h=y])" by (simp add: nonrec_subst)
292
293     from True
294     obtain x' e' where [simp]: "\<Gamma> = [(x',e')]" "atom x' \<sharp> e'" by (auto elim: nonrecE)
295
296     from * have [simp]: "atom x' \<sharp> e'[x::=y]"
297       by (auto simp add: nonrec_def)
298
299     from fun_cong[OF **, where x = x']
300     have [simp]: "\<And> a. (Aexp e[x::=y]\<cdot>a) x' = (Aexp e\<cdot>a) x'" by simp
301
302     from CCexp_subst[OF assms(2,1)]
303     have "\<And> a.  cc_restr {x'} (CCexp e[x::=y]\<cdot>a) = cc_restr {x'} (CCexp e\<cdot>a)" by simp
304     from arg_cong[where f = "\<lambda>x.  x'--x'\<in>x", OF this]
305     have [simp]: "\<And> a. x'--x'\<in>(CCexp e[x::=y]\<cdot>a) \<longleftrightarrow> x'--x'\<in>(CCexp e\<cdot>a)" by simp
306     
307     show ?thesis
308       apply -
309       apply (rule cfun_eqI)
310       apply (auto simp add: Aheap_nonrec_simp ABind_nonrec_eq)
311       done
312   qed
313 next
314   fix \<Gamma> e a
315   show "ABinds \<Gamma>\<cdot>(Aheap \<Gamma> e\<cdot>a) \<squnion> Aexp e\<cdot>a \<sqsubseteq> Aheap \<Gamma> e\<cdot>a \<squnion> Aexp (Let \<Gamma> e)\<cdot>a"
316   proof(cases "nonrec \<Gamma>")
317     case False
318     thus ?thesis
319       by (auto simp add: Aheap_def join_below_iff env_restr_join2 Compl_partition intro:  below_trans[OF _ Afix_above_arg])
320   next
321     case True
322     then obtain x e' where [simp]: "\<Gamma> = [(x,e')]" "atom x \<sharp> e'" by (auto elim: nonrecE)
323
324     from `atom x \<sharp> e'`
325     have "x \<notin> fv e'" by (simp add: fv_def fresh_def)
326
327     hence "\<And> a. x \<notin> edom (fup\<cdot>(Aexp e')\<cdot>a)"
328       by (auto dest:set_mp[OF fup_Aexp_edom])
329     hence [simp]: "\<And> a. (fup\<cdot>(Aexp e')\<cdot>a) x = \<bottom>" by (simp add: edomIff)
330
331     show ?thesis
332       apply (rule env_restr_below_split[where S = "{x}"])
333       apply (rule env_restr_belowI2)
334       apply (auto simp add:  Aheap_nonrec_simp  join_below_iff env_restr_join env_delete_restr)
335       apply (rule ABind_nonrec_above_arg)
336       apply (rule below_trans[OF _ join_above2])
337       apply (rule below_trans[OF _ join_above2])
338       apply (rule below_refl)
339       done
340   qed
341 qed
342
343 definition ccHeap_nonrec
344   where "ccHeap_nonrec x e exp = (\<Lambda> n. CCfix_nonrec x e\<cdot>(Aexp exp\<cdot>n, CCexp exp\<cdot>n))"
345
346 lemma ccHeap_nonrec_eq:
347    "ccHeap_nonrec x e exp\<cdot>n = CCfix_nonrec x e\<cdot>(Aexp exp\<cdot>n, CCexp exp\<cdot>n)"
348 unfolding ccHeap_nonrec_def by (rule beta_cfun) (intro cont2cont)
349
350 definition ccHeap_rec :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> CoCalls"
351   where "ccHeap_rec \<Gamma> e  = (\<Lambda> a. CCfix \<Gamma>\<cdot>(Afix \<Gamma>\<cdot>(Aexp e\<cdot>a \<squnion> (\<lambda>_.up\<cdot>0) f|` (thunks \<Gamma>)), CCexp e\<cdot>a))"
352
353 lemma ccHeap_rec_eq:
354   "ccHeap_rec \<Gamma> e\<cdot>a = CCfix \<Gamma>\<cdot>(Afix \<Gamma>\<cdot>(Aexp e\<cdot>a \<squnion> (\<lambda>_.up\<cdot>0) f|` (thunks \<Gamma>)), CCexp e\<cdot>a)"
355 unfolding ccHeap_rec_def by simp
356
357 definition ccHeap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> CoCalls"
358   where "ccHeap \<Gamma>  = (if nonrec \<Gamma> then split ccHeap_nonrec (hd \<Gamma>) else ccHeap_rec \<Gamma>)"
359
360 lemma ccHeap_simp1:
361   "\<not> nonrec \<Gamma> \<Longrightarrow> ccHeap \<Gamma> e\<cdot>a = CCfix \<Gamma>\<cdot>(Afix \<Gamma>\<cdot>(Aexp e\<cdot>a \<squnion> (\<lambda>_.up\<cdot>0) f|` (thunks \<Gamma>)), CCexp e\<cdot>a)"
362   by (simp add: ccHeap_def ccHeap_rec_eq)
363
364 lemma ccHeap_simp2:
365   "atom x \<sharp> e \<Longrightarrow> ccHeap [(x,e)] exp\<cdot>n = CCfix_nonrec x e\<cdot>(Aexp exp\<cdot>n, CCexp exp\<cdot>n)"
366   by (simp add: ccHeap_def ccHeap_nonrec_eq nonrec_def)
367
368
369 interpretation CoCallArityCorrect CCexp Aexp ccHeap Aheap
370 proof
371   fix e a x
372   show "CCexp e\<cdot>(inc\<cdot>a) \<squnion> ccProd {x} (insert x (fv e)) \<sqsubseteq> CCexp (App e x)\<cdot>a"
373     by simp
374 next
375   fix y e n
376   show "cc_restr (fv (Lam [y]. e)) (CCexp e\<cdot>(pred\<cdot>n)) \<sqsubseteq> CCexp (Lam [y]. e)\<cdot>n"
377     by (auto simp add: predCC_eq dest!: set_mp[OF ccField_cc_restr])
378 next
379   fix x y :: var and S e a
380   assume "x \<notin> S"  and "y \<notin> S"
381   thus "cc_restr S (CCexp e[y::=x]\<cdot>a) \<sqsubseteq> cc_restr S (CCexp e\<cdot>a)"
382     by (rule eq_imp_below[OF CCexp_subst])
383 next
384   fix e
385   assume "isLam e"
386   thus "CCexp  e\<cdot>0 = ccSquare (fv e)"
387     by (induction e rule: isLam.induct) (auto simp add: predCC_eq)
388 next
389   fix \<Gamma> e a
390   show "cc_restr (- domA \<Gamma>) (ccHeap \<Gamma> e\<cdot>a) \<sqsubseteq> CCexp (Let \<Gamma> e)\<cdot>a"
391   proof(cases "nonrec \<Gamma>")
392     case False[simp]
393     have "ccField  (ccHeap \<Gamma> e\<cdot>a) \<subseteq> fv \<Gamma> \<union> fv e"
394       unfolding ccHeap_simp1[OF False]
395       by (rule ccField_CCfix)
396     thus "cc_restr (- domA \<Gamma>) (ccHeap \<Gamma> e\<cdot>a) \<sqsubseteq> CCexp (Let \<Gamma> e)\<cdot>a"
397       by (simp add: ccHeap_simp1[OF False, symmetric])
398   next
399     case True
400     thus ?thesis
401       by (auto simp add: ccHeap_simp2 Diff_eq elim!: nonrecE)
402   qed
403 next
404   fix \<Delta> :: heap and e a
405
406   show "CCexp e\<cdot>a \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
407     by (cases "nonrec \<Delta>")
408        (auto simp add: ccHeap_simp1 ccHeap_simp2 arg_cong[OF CCfix_unroll, where f = "op \<sqsubseteq> x" for x ] elim!: nonrecE)
409
410   fix x e' a'
411   assume "map_of \<Delta> x = Some e'"
412   hence [simp]: "x \<in> domA \<Delta>" by (metis domI dom_map_of_conv_domA) 
413   assume "(Aheap \<Delta> e\<cdot>a) x = up\<cdot>a'"
414   show "CCexp e'\<cdot>a' \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
415   proof(cases "nonrec \<Delta>")
416     case False
417
418     from `(Aheap \<Delta> e\<cdot>a) x = up\<cdot>a'` False
419     have "(Afix \<Delta>\<cdot>(Aexp e\<cdot>a \<squnion> (\<lambda>_.up\<cdot>0)f|` (thunks \<Delta>))) x = up\<cdot>a'" 
420       by (simp add: Aheap_def)
421     hence "CCexp e'\<cdot>a' \<sqsubseteq> ccBind x e'\<cdot>(Afix \<Delta>\<cdot>(Aexp e\<cdot>a \<squnion> (\<lambda>_.up\<cdot>0)f|` (thunks \<Delta>)), CCfix \<Delta>\<cdot>(Afix \<Delta>\<cdot>(Aexp e\<cdot>a \<squnion> (\<lambda>_.up\<cdot>0)f|` (thunks \<Delta>)), CCexp e\<cdot>a))"
422       by (auto simp add: ccBind_eq dest: set_mp[OF ccField_CCexp])
423     also
424     have "ccBind x e'\<cdot>(Afix \<Delta>\<cdot>(Aexp e\<cdot>a \<squnion> (\<lambda>_.up\<cdot>0)f|` (thunks \<Delta>)), CCfix \<Delta>\<cdot>(Afix \<Delta>\<cdot>(Aexp e\<cdot>a \<squnion> (\<lambda>_.up\<cdot>0)f|` (thunks \<Delta>)), CCexp e\<cdot>a)) \<sqsubseteq>  ccHeap \<Delta> e\<cdot>a"
425       using `map_of \<Delta> x = Some e'` False
426       by (fastforce simp add: ccHeap_simp1 ccHeap_rec_eq ccBindsExtra_simp  ccBinds_eq  arg_cong[OF CCfix_unroll, where f = "op \<sqsubseteq> x" for x ]
427                   intro: below_trans[OF _ join_above2])
428     finally
429     show "CCexp e'\<cdot>a' \<sqsubseteq> ccHeap \<Delta> e\<cdot>a" by this simp_all
430   next
431     case True
432     with `map_of \<Delta> x = Some e'`
433     have [simp]: "\<Delta> = [(x,e')]" "atom x \<sharp> e'" by (auto elim!: nonrecE split: if_splits)
434     hence [simp]: "x \<notin> fv e'" by (auto simp add: fresh_def fv_def)
435
436     show ?thesis
437     proof(cases "x--x\<notin>CCexp e\<cdot>a \<or> isLam e'")
438       case True
439       with `(Aheap \<Delta> e\<cdot>a) x = up\<cdot>a'`
440       have [simp]: "(CoCallArityAnalysis.Aexp cCCexp e\<cdot>a) x = up\<cdot>a'"
441         by (auto simp add: Aheap_nonrec_simp ABind_nonrec_eq split: if_splits)
442
443       have "CCexp e'\<cdot>a' \<sqsubseteq> ccSquare (fv e')"
444         unfolding below_ccSquare
445         by (rule ccField_CCexp)
446       then
447       show ?thesis using True
448         by (auto simp add: ccHeap_simp2 ccBind_eq Aheap_nonrec_simp ABind_nonrec_eq below_trans[OF _ join_above2] simp del: below_ccSquare )
449     next
450       case False
451
452       from `(Aheap \<Delta> e\<cdot>a) x = up\<cdot>a'`
453       have [simp]: "a' = 0" using  False
454         by (auto simp add: Aheap_nonrec_simp ABind_nonrec_eq split: if_splits)
455
456       show ?thesis using False
457         by (auto simp add: ccHeap_simp2 ccBind_eq Aheap_nonrec_simp ABind_nonrec_eq simp del: below_ccSquare )
458     qed
459   qed
460
461   show "ccProd (fv e') (ccNeighbors x (ccHeap \<Delta> e\<cdot>a) - {x} \<inter> thunks \<Delta>) \<sqsubseteq> ccHeap \<Delta> e\<cdot>a" 
462   proof (cases "nonrec \<Delta>")
463     case False[simp]
464
465     have "ccProd (fv e') (ccNeighbors x (ccHeap \<Delta> e\<cdot>a) - {x} \<inter> thunks \<Delta>) \<sqsubseteq> ccProd (fv e') (ccNeighbors x (ccHeap \<Delta> e\<cdot>a))"
466       by (rule ccProd_mono2) auto
467     also have "\<dots> \<sqsubseteq> (\<Squnion>x\<mapsto>e'\<in>map_of \<Delta>. ccProd (fv e') (ccNeighbors x (ccHeap \<Delta> e\<cdot>a)))" 
468       using `map_of \<Delta> x = Some e'` by (rule below_lubmapI)
469     also have "\<dots> \<sqsubseteq> ccBindsExtra \<Delta>\<cdot>(Afix \<Delta>\<cdot>(Aexp e\<cdot>a \<squnion> (\<lambda>_.up\<cdot>0)f|` (thunks \<Delta>)), ccHeap \<Delta> e\<cdot>a)"
470       by (simp add: ccBindsExtra_simp  below_trans[OF _ join_above2])
471     also have "\<dots> \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
472       by (simp add: ccHeap_simp1  arg_cong[OF CCfix_unroll, where f = "op \<sqsubseteq> x" for x])
473     finally
474     show ?thesis by this simp_all
475   next
476     case True
477     with `map_of \<Delta> x = Some e'`
478     have [simp]: "\<Delta> = [(x,e')]" "atom x \<sharp> e'" by (auto elim!: nonrecE split: if_splits)
479     hence [simp]: "x \<notin> fv e'" by (auto simp add: fresh_def fv_def)
480
481     have [simp]: "(ccNeighbors x (ccBind x e'\<cdot>(Aexp e\<cdot>a, CCexp e\<cdot>a))) = {}"
482      by (auto simp add: ccBind_eq dest!: set_mp[OF ccField_cc_restr] set_mp[OF ccField_fup_CCexp])
483
484     show ?thesis
485     proof(cases "isLam e' \<and> x--x\<in>CCexp e\<cdot>a")
486     case True
487
488     have "ccNeighbors x (ccHeap \<Delta> e\<cdot>a) =
489         ccNeighbors x (ccBind x e'\<cdot>(Aheap_nonrec x e'\<cdot>(Aexp e\<cdot>a, CCexp e\<cdot>a), CCexp e\<cdot>a)) \<union>
490         ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a) - (if isLam e' then {} else {x}))) \<union>
491         ccNeighbors x (CCexp e\<cdot>a)" by (auto simp add: ccHeap_simp2 )
492     also have "ccNeighbors x (ccBind  x e'\<cdot>(Aheap_nonrec x e'\<cdot>(Aexp e\<cdot>a, CCexp e\<cdot>a), CCexp e\<cdot>a)) = {}"
493        by (auto simp add: ccBind_eq dest!: set_mp[OF ccField_cc_restr] set_mp[OF ccField_fup_CCexp])
494     also have "ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a) - (if isLam e' then {} else {x})))
495       \<subseteq> ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a)))" by (simp add: ccNeighbors_ccProd)
496     also have "\<dots> \<subseteq> fv e'" by (simp add: ccNeighbors_ccProd)
497     finally
498     have "ccNeighbors x (ccHeap \<Delta> e\<cdot>a)  - {x} \<inter> thunks \<Delta> \<subseteq> ccNeighbors x (CCexp e\<cdot>a) \<union> fv e'" by auto
499     hence "ccProd (fv e') (ccNeighbors x (ccHeap \<Delta> e\<cdot>a) - {x} \<inter> thunks \<Delta>) \<sqsubseteq> ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a) \<union> fv e')" by (rule ccProd_mono2)
500     also have "\<dots> \<sqsubseteq> ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a)) \<squnion> ccProd (fv e') (fv e')" by simp
501     also have "ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a)) \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
502       using `map_of \<Delta> x = Some e'` `(Aheap \<Delta> e\<cdot>a) x = up\<cdot>a'` True
503       by (auto simp add: ccHeap_simp2  below_trans[OF _ join_above2])
504     also have "ccProd (fv e') (fv e') = ccSquare (fv e')" by (simp add: ccSquare_def)
505     also have "\<dots> \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
506       using `map_of \<Delta> x = Some e'` `(Aheap \<Delta> e\<cdot>a) x = up\<cdot>a'` True
507       by (auto simp add: ccHeap_simp2  ccBind_eq below_trans[OF _ join_above2])
508     also note join_self
509     finally show ?thesis by this simp_all
510   next
511     case False
512     have "ccNeighbors x (ccHeap \<Delta> e\<cdot>a) =
513         ccNeighbors x (ccBind x e'\<cdot>(Aheap_nonrec x e'\<cdot>(Aexp e\<cdot>a, CCexp e\<cdot>a), CCexp e\<cdot>a)) \<union>
514         ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a) - (if isLam e' then {} else {x}))) \<union>
515         ccNeighbors x (CCexp e\<cdot>a)" by (auto simp add: ccHeap_simp2 )
516     also have "ccNeighbors x (ccBind  x e'\<cdot>(Aheap_nonrec x e'\<cdot>(Aexp e\<cdot>a, CCexp e\<cdot>a), CCexp e\<cdot>a)) = {}"
517        by (auto simp add: ccBind_eq dest!: set_mp[OF ccField_cc_restr] set_mp[OF ccField_fup_CCexp])
518     also have  "ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a) - (if isLam e' then {} else {x}) )) 
519       = {}" using False by (auto simp add: ccNeighbors_ccProd)
520     finally
521     have "ccNeighbors x (ccHeap \<Delta> e\<cdot>a) \<subseteq> ccNeighbors x (CCexp e\<cdot>a)" by auto
522     hence"ccNeighbors x (ccHeap \<Delta> e\<cdot>a)  - {x} \<inter> thunks \<Delta> \<subseteq> ccNeighbors x (CCexp e\<cdot>a)   - {x} \<inter> thunks \<Delta>" by auto
523     hence "ccProd (fv e') (ccNeighbors x (ccHeap \<Delta> e\<cdot>a) - {x} \<inter> thunks \<Delta> ) \<sqsubseteq> ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a)  - {x} \<inter> thunks \<Delta> )" by (rule ccProd_mono2)
524     also have "\<dots> \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
525       using `map_of \<Delta> x = Some e'` `(Aheap \<Delta> e\<cdot>a) x = up\<cdot>a'` False
526       by (auto simp add: ccHeap_simp2  thunks_Cons below_trans[OF _ join_above2])
527     finally show ?thesis by this simp_all
528    qed
529   qed
530
531 next
532   fix x \<Gamma> e a
533   assume [simp]: "\<not> nonrec \<Gamma>"
534   assume "x \<in> thunks \<Gamma>"
535   hence [simp]: "x \<in> domA \<Gamma>" by (rule set_mp[OF thunks_domA])
536   assume "x \<in> edom (Aheap \<Gamma> e\<cdot>a)"
537
538   from `x \<in> thunks \<Gamma>`
539   have "(Afix \<Gamma>\<cdot>(Aexp e\<cdot>a \<squnion> (\<lambda>_.up\<cdot>0)f|` (thunks \<Gamma>))) x = up\<cdot>0" 
540     by (subst Afix_unroll) simp
541
542   thus "(Aheap \<Gamma> e\<cdot>a) x = up\<cdot>0" by simp
543 next
544   fix x \<Gamma> e a
545   assume "nonrec \<Gamma>"
546   then obtain x' e' where [simp]: "\<Gamma> = [(x',e')]" "atom x' \<sharp> e'" by (auto elim: nonrecE)
547   assume "x \<in> thunks \<Gamma>"
548   hence [simp]: "x = x'" "\<not> isLam e'" by (auto simp add: thunks_Cons split: if_splits)
549
550   assume "x \<in> ccManyCalls (CCexp e\<cdot>a)"
551   hence [simp]: "x'--x'\<in> CCexp  e\<cdot>a" by simp
552
553   from `x \<in> thunks \<Gamma>`
554   have "(Afix \<Gamma>\<cdot>(Aexp e\<cdot>a \<squnion> (\<lambda>_.up\<cdot>0)f|` (thunks \<Gamma>))) x = up\<cdot>0" 
555     by (subst Afix_unroll) simp
556
557   show "(Aheap \<Gamma> e\<cdot>a) x = up\<cdot>0" by (auto simp add: Aheap_nonrec_simp ABind_nonrec_eq)
558 qed
559
560 end