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