Module name: CoCallAnalysisSig
[darcs-mirror-isa-launchbury.git] / Launchbury / CoCallFix.thy
1 theory CoCallFix
2 imports CoCallAnalysisSig CoCallAnalysisBinds ArityAnalysisSig "Env-Nominal"  ArityAnalysisFix
3 begin
4
5
6 locale CoCallArityAnalysis =
7   fixes cccExp :: "exp \<Rightarrow> (Arity \<rightarrow> AEnv \<times> CoCalls)"
8 begin
9 definition Aexp :: "exp \<Rightarrow> (Arity \<rightarrow> AEnv)" where "Aexp e = (\<Lambda> a. fst (cccExp e \<cdot> a))"
10
11 lemma Aexp_eq:
12   "Aexp e\<cdot>a = fst (cccExp e \<cdot> a)"
13   unfolding Aexp_def by (rule beta_cfun) (intro cont2cont)
14
15 lemma fup_Aexp_eq:
16   "fup\<cdot>(Aexp e)\<cdot>a = fst (fup\<cdot>(cccExp e)\<cdot>a)"
17   by (cases a)(simp_all add: Aexp_eq)
18   
19
20 definition CCexp :: "exp \<Rightarrow> (Arity \<rightarrow> CoCalls)" where "CCexp \<Gamma> = (\<Lambda> a. snd (cccExp \<Gamma>\<cdot>a))"
21 lemma CCexp_eq:
22   "CCexp e\<cdot>a = snd (cccExp e \<cdot> a)"
23   unfolding CCexp_def by (rule beta_cfun) (intro cont2cont)
24
25 lemma fup_CCexp_eq:
26   "fup\<cdot>(CCexp e)\<cdot>a = snd (fup\<cdot>(cccExp e)\<cdot>a)"
27   by (cases a)(simp_all add: CCexp_eq)
28
29 sublocale ArityAnalysis Aexp.
30 sublocale CoCallAnalysis CCexp.
31
32 definition CCfix :: "heap \<Rightarrow> (AEnv \<times> CoCalls) \<rightarrow> CoCalls"
33   where "CCfix \<Gamma> = (\<Lambda> aeG. (\<mu> G'. ccBindsExtra \<Gamma>\<cdot>(fst aeG , G') \<squnion> snd aeG))"
34
35 lemma CCfix_unroll: "CCfix \<Gamma>\<cdot>(ae,G) = ccBindsExtra \<Gamma>\<cdot>(ae, CCfix \<Gamma>\<cdot>(ae,G)) \<squnion> G"
36   unfolding  CCfix_def
37   apply simp
38   apply (subst fix_eq)
39   apply simp
40   done
41
42 lemma fup_ccExp_restr_subst': 
43   assumes "\<And> a. cc_restr S (CCexp e[x::=y]\<cdot>a) = cc_restr S (CCexp e\<cdot>a)"
44   shows "cc_restr S (fup\<cdot>(CCexp e[x::=y])\<cdot>a) = cc_restr S (fup\<cdot>(CCexp e)\<cdot>a)"
45   using assms
46   by (cases a) (auto simp del: cc_restr_cc_restr simp add: cc_restr_cc_restr[symmetric])
47
48 lemma ccBindsExtra_restr_subst': 
49   assumes "\<And> x' e a. (x',e) \<in> set \<Gamma> \<Longrightarrow> cc_restr S (CCexp e[x::=y]\<cdot>a) = cc_restr S (CCexp e\<cdot>a)"
50   assumes "x \<notin> S"
51   assumes "y \<notin> S"
52   assumes "domA \<Gamma> \<subseteq> S"
53   shows  "cc_restr S (ccBindsExtra  \<Gamma>[x::h=y]\<cdot>(ae, G)) 
54        = cc_restr S (ccBindsExtra  \<Gamma>\<cdot>(ae f|` S , cc_restr S G))"
55   apply (simp add: ccBindsExtra_simp ccBinds_eq ccBind_eq Int_absorb2[OF assms(4)] fv_subst_int[OF assms(3,2)])
56   apply (intro arg_cong2[where f = "op \<squnion>"] refl  arg_cong[OF mapCollect_cong])
57   apply (subgoal_tac "k \<in> S")
58   apply (auto intro: fup_ccExp_restr_subst'[OF assms(1)[OF map_of_SomeD]] simp add: fv_subst_int[OF assms(3,2)]   fv_subst_int2[OF assms(3,2)] ccSquare_def)[1]
59   apply (metis assms(4) contra_subsetD domI dom_map_of_conv_domA)
60   apply (subgoal_tac "k \<in> S")
61   apply (auto intro: fup_ccExp_restr_subst'[OF assms(1)[OF map_of_SomeD]]
62               simp add: fv_subst_int[OF assms(3,2)]   fv_subst_int2[OF assms(3,2)] ccSquare_def cc_restr_twist[where S = S] simp del: cc_restr_cc_restr)[1]
63   apply (subst fup_ccExp_restr_subst'[OF assms(1)[OF map_of_SomeD]], assumption)
64   apply (simp add: fv_subst_int[OF assms(3,2)]   fv_subst_int2[OF assms(3,2)] )
65   apply (subst fup_ccExp_restr_subst'[OF assms(1)[OF map_of_SomeD]], assumption)
66   apply (simp add: fv_subst_int[OF assms(3,2)]   fv_subst_int2[OF assms(3,2)] )
67   apply (metis assms(4) contra_subsetD domI dom_map_of_conv_domA)
68   done
69
70 lemma ccBindsExtra_restr:
71   assumes "domA \<Gamma> \<subseteq> S"
72   shows "cc_restr S (ccBindsExtra \<Gamma>\<cdot>(ae, G)) = cc_restr S (ccBindsExtra \<Gamma>\<cdot>(ae f|` S, cc_restr S G))"
73   using assms
74   apply (simp add: ccBindsExtra_simp ccBinds_eq ccBind_eq Int_absorb2)
75   apply (intro arg_cong2[where f = "op \<squnion>"] refl arg_cong[OF mapCollect_cong])
76   apply (subgoal_tac "k \<in> S")
77   apply simp
78   apply (metis contra_subsetD domI dom_map_of_conv_domA)
79   apply (subgoal_tac "k \<in> S")
80   apply simp
81   apply (metis contra_subsetD domI dom_map_of_conv_domA)
82   done
83
84 lemma CCfix_restr:
85   assumes "domA \<Gamma> \<subseteq> S"
86   shows "cc_restr S (CCfix \<Gamma>\<cdot>(ae, G)) = cc_restr S (CCfix \<Gamma>\<cdot>(ae f|` S, cc_restr S G))"
87   unfolding CCfix_def
88   apply simp
89   apply (rule parallel_fix_ind[where P = "\<lambda> x y . cc_restr S x = cc_restr S y"])
90   apply simp
91   apply rule
92   apply simp
93   apply (subst (1 2) ccBindsExtra_restr[OF assms])
94   apply (auto)
95   done
96
97 lemma CCfix_restr_subst':
98   assumes "\<And> x' e a. (x',e) \<in> set \<Gamma> \<Longrightarrow> cc_restr S (CCexp e[x::=y]\<cdot>a) = cc_restr S (CCexp e\<cdot>a)"
99   assumes "x \<notin> S"
100   assumes "y \<notin> S"
101   assumes "domA \<Gamma> \<subseteq> S"
102   shows "cc_restr S (CCfix \<Gamma>[x::h=y]\<cdot>(ae, G)) = cc_restr S (CCfix \<Gamma>\<cdot>(ae f|` S, cc_restr S G))"
103   unfolding CCfix_def
104   apply simp
105   apply (rule parallel_fix_ind[where P = "\<lambda> x y . cc_restr S x = cc_restr S y"])
106   apply simp
107   apply rule
108   apply simp
109   apply (subst  ccBindsExtra_restr_subst'[OF assms], assumption)
110   apply (subst ccBindsExtra_restr[OF assms(4)]) back 
111   apply (auto)
112   done
113
114
115 end
116
117 lemma Aexp_eqvt[eqvt]:  "\<pi> \<bullet> (CoCallArityAnalysis.Aexp cccExp e) = CoCallArityAnalysis.Aexp (\<pi> \<bullet> cccExp) (\<pi> \<bullet> e)"
118   apply (rule cfun_eqvtI) unfolding CoCallArityAnalysis.Aexp_eq by perm_simp rule
119
120 lemma CCexp_eqvt[eqvt]:  "\<pi> \<bullet> (CoCallArityAnalysis.CCexp cccExp e) = CoCallArityAnalysis.CCexp (\<pi> \<bullet> cccExp) (\<pi> \<bullet> e)"
121   apply (rule cfun_eqvtI) unfolding CoCallArityAnalysis.CCexp_eq by perm_simp rule
122
123 lemma CCfix_eqvt[eqvt]: "\<pi> \<bullet> (CoCallArityAnalysis.CCfix cccExp \<Gamma>) = CoCallArityAnalysis.CCfix (\<pi> \<bullet> cccExp) (\<pi> \<bullet> \<Gamma>)"
124   unfolding CoCallArityAnalysis.CCfix_def by perm_simp (simp_all add: Abs_cfun_eqvt)
125
126 lemma ccFix_cong[fundef_cong]:
127   "\<lbrakk> (\<And> e. e \<in> snd ` set heap2 \<Longrightarrow> cccexp1 e = cccexp2 e); heap1 = heap2 \<rbrakk>
128       \<Longrightarrow> CoCallArityAnalysis.CCfix cccexp1 heap1 = CoCallArityAnalysis.CCfix cccexp2 heap2"
129    unfolding CoCallArityAnalysis.CCfix_def
130    apply (rule arg_cong) back
131    apply (rule ccBindsExtra_cong)
132    apply (auto simp add: CoCallArityAnalysis.CCexp_def)
133    done
134
135
136 context CoCallArityAnalysis
137 begin
138 definition cccFix ::  "heap \<Rightarrow> ((AEnv \<times> CoCalls) \<rightarrow> (AEnv \<times> CoCalls))"
139   where "cccFix \<Gamma> = (\<Lambda> i. (Afix \<Gamma>\<cdot>(fst i \<squnion> (\<lambda>_.up\<cdot>0) f|` thunks \<Gamma>), CCfix \<Gamma>\<cdot>(Afix \<Gamma>\<cdot>(fst i  \<squnion> (\<lambda>_.up\<cdot>0) f|` (thunks \<Gamma>)), snd i)))"
140
141 lemma cccFix_eq:
142   "cccFix \<Gamma>\<cdot>i = (Afix \<Gamma>\<cdot>(fst i \<squnion> (\<lambda>_.up\<cdot>0) f|` thunks \<Gamma>), CCfix \<Gamma>\<cdot>(Afix \<Gamma>\<cdot>(fst i  \<squnion> (\<lambda>_.up\<cdot>0) f|` (thunks \<Gamma>)), snd i))"
143   unfolding cccFix_def
144   by (rule beta_cfun)(intro cont2cont)
145 end
146
147 lemma cccFix_eqvt[eqvt]: "\<pi> \<bullet> (CoCallArityAnalysis.cccFix cccExp \<Gamma>) = CoCallArityAnalysis.cccFix  (\<pi> \<bullet> cccExp) (\<pi> \<bullet> \<Gamma>)"
148   apply (rule cfun_eqvtI) unfolding CoCallArityAnalysis.cccFix_eq by perm_simp rule
149
150 lemma cccFix_cong[fundef_cong]:
151   "\<lbrakk> (\<And> e. e \<in> snd ` set heap2 \<Longrightarrow> cccexp1 e = cccexp2 e); heap1 = heap2 \<rbrakk>
152       \<Longrightarrow> CoCallArityAnalysis.cccFix cccexp1 heap1 = CoCallArityAnalysis.cccFix cccexp2 heap2"
153    unfolding CoCallArityAnalysis.cccFix_def
154    apply (rule cfun_eqI)
155    apply auto
156    apply (rule arg_cong[OF Afix_cong], auto simp add: CoCallArityAnalysis.Aexp_def)[1]
157    apply (rule arg_cong2[OF ccFix_cong Afix_cong ])
158    apply (auto simp add: CoCallArityAnalysis.Aexp_def)
159    done
160
161
162 subsubsection {* The non-recursive case *}
163
164 definition ABind_nonrec :: "var \<Rightarrow> exp \<Rightarrow> AEnv \<times> CoCalls \<rightarrow> Arity\<^sub>\<bottom>"
165 where
166   "ABind_nonrec x e = (\<Lambda> i. (if isLam e \<or> x--x\<notin>(snd i) then fst i x else up\<cdot>0))"
167
168 lemma ABind_nonrec_eq:
169   "ABind_nonrec x e \<cdot> i = (if isLam e \<or> x--x\<notin>(snd i) then fst i x else up\<cdot>0)"
170   unfolding ABind_nonrec_def
171   apply (rule beta_cfun)
172   apply (rule cont_if_else_above)
173   apply auto
174   by (metis in_join join_self_below(4))
175
176 lemma ABind_nonrec_eqvt[eqvt]: "\<pi> \<bullet> (ABind_nonrec x e) = ABind_nonrec (\<pi> \<bullet> x) (\<pi> \<bullet> e)"
177   apply (rule cfun_eqvtI)
178   unfolding ABind_nonrec_eq
179   by perm_simp rule
180
181 lemma ABind_nonrec_above_arg:
182   "ae x \<sqsubseteq> ABind_nonrec x e \<cdot> (ae, G)"
183 unfolding ABind_nonrec_eq by auto
184
185 definition Aheap_nonrec where
186   "Aheap_nonrec x e = (\<Lambda> i. esing x\<cdot>(ABind_nonrec x e\<cdot>i))"
187
188 lemma Aheap_nonrec_simp:
189   "Aheap_nonrec x e\<cdot>i = esing x\<cdot>(ABind_nonrec x e\<cdot>i)"
190   unfolding Aheap_nonrec_def by simp
191
192 lemma Aheap_nonrec_lookup[simp]:
193   "(Aheap_nonrec x e\<cdot>i) x = ABind_nonrec x e\<cdot>i"
194   unfolding Aheap_nonrec_simp by simp
195
196 lemma Aheap_nonrec_eqvt'[eqvt]:
197   "\<pi> \<bullet> (Aheap_nonrec x e) = Aheap_nonrec (\<pi> \<bullet> x) (\<pi> \<bullet> e)"
198   apply (rule cfun_eqvtI)
199   unfolding Aheap_nonrec_simp
200   by (perm_simp, rule)
201
202
203 context CoCallArityAnalysis
204 begin
205
206   definition Afix_nonrec
207    where "Afix_nonrec x e = (\<Lambda> i. fup\<cdot>(Aexp e)\<cdot>(ABind_nonrec x e \<cdot> i) \<squnion> fst i)"
208
209   lemma Afix_nonrec_eq[simp]:
210     "Afix_nonrec x e \<cdot> i = fup\<cdot>(Aexp e)\<cdot>(ABind_nonrec x e \<cdot> i) \<squnion> fst i"
211     unfolding Afix_nonrec_def
212     by (rule beta_cfun) simp
213
214   definition CCfix_nonrec
215    where "CCfix_nonrec x e = (\<Lambda> i. ccBind x e \<cdot> (Aheap_nonrec x e\<cdot>i, snd i)  \<squnion> ccProd (fv e) (ccNeighbors x (snd i) - (if isLam e then {} else {x})) \<squnion> snd i)"
216
217   lemma CCfix_nonrec_eq[simp]:
218     "CCfix_nonrec x e \<cdot> i = ccBind x e\<cdot>(Aheap_nonrec x e\<cdot>i, snd i)  \<squnion> ccProd (fv e) (ccNeighbors x (snd i) - (if isLam e then {} else {x})) \<squnion> snd i"
219     unfolding CCfix_nonrec_def
220     by (rule beta_cfun) (intro cont2cont)
221
222   definition cccFix_nonrec ::  "var \<Rightarrow> exp \<Rightarrow> ((AEnv \<times> CoCalls) \<rightarrow> (AEnv \<times> CoCalls))"
223     where "cccFix_nonrec x e = (\<Lambda> i. (Afix_nonrec x e \<cdot>i , CCfix_nonrec x e \<cdot>i))"
224
225   lemma cccFix_nonrec_eq[simp]:
226     "cccFix_nonrec x e\<cdot>i = (Afix_nonrec x e \<cdot>i , CCfix_nonrec x e \<cdot>i)"
227     unfolding cccFix_nonrec_def
228     by (rule beta_cfun) (intro cont2cont)
229
230 end
231
232
233 lemma AFix_nonrec_eqvt[eqvt]: "\<pi> \<bullet> (CoCallArityAnalysis.Afix_nonrec cccExp x e) = CoCallArityAnalysis.Afix_nonrec (\<pi> \<bullet> cccExp) (\<pi> \<bullet> x) (\<pi> \<bullet> e)"
234   apply (rule cfun_eqvtI)
235   unfolding CoCallArityAnalysis.Afix_nonrec_eq
236   by perm_simp rule
237
238
239 lemma CCFix_nonrec_eqvt[eqvt]: "\<pi> \<bullet> (CoCallArityAnalysis.CCfix_nonrec cccExp x e) = CoCallArityAnalysis.CCfix_nonrec (\<pi> \<bullet> cccExp) (\<pi> \<bullet> x) (\<pi> \<bullet> e)"
240   apply (rule cfun_eqvtI)
241   unfolding CoCallArityAnalysis.CCfix_nonrec_eq
242   by perm_simp rule
243
244 lemma cccFix_nonrec_eqvt[eqvt]: "\<pi> \<bullet> (CoCallArityAnalysis.cccFix_nonrec cccExp x e) = CoCallArityAnalysis.cccFix_nonrec (\<pi> \<bullet> cccExp) (\<pi> \<bullet> x) (\<pi> \<bullet> e)"
245   apply (rule cfun_eqvtI)
246   unfolding CoCallArityAnalysis.cccFix_nonrec_eq
247   by perm_simp rule
248
249 subsubsection {* Combining the cases *}
250
251 context CoCallArityAnalysis
252 begin
253   definition cccFix_choose ::  "heap \<Rightarrow> ((AEnv \<times> CoCalls) \<rightarrow> (AEnv \<times> CoCalls))"
254     where "cccFix_choose \<Gamma> = (if nonrec \<Gamma> then split cccFix_nonrec (hd \<Gamma>) else cccFix \<Gamma>)"
255
256   lemma cccFix_choose_simp1[simp]:
257     "\<not> nonrec \<Gamma> \<Longrightarrow> cccFix_choose \<Gamma> = cccFix \<Gamma>"
258   unfolding cccFix_choose_def by simp
259
260   lemma cccFix_choose_simp2[simp]:
261     "atom x \<sharp> e \<Longrightarrow> cccFix_choose [(x,e)] = cccFix_nonrec x e"
262   unfolding cccFix_choose_def nonrec_def by auto
263
264 end
265
266 lemma cccFix_choose_eqvt[eqvt]: "\<pi> \<bullet> (CoCallArityAnalysis.cccFix_choose cccExp \<Gamma>) = CoCallArityAnalysis.cccFix_choose (\<pi> \<bullet> cccExp) (\<pi> \<bullet> \<Gamma>)"
267   unfolding CoCallArityAnalysis.cccFix_choose_def 
268   apply (cases nonrec \<pi>  rule: eqvt_cases[where x = \<Gamma>])
269   apply (perm_simp, rule)
270   apply simp
271   apply (erule nonrecE)
272   apply (simp )
273
274   apply simp
275   done
276
277 lemma cccFix_nonrec_cong[fundef_cong]:
278   "cccexp1 e = cccexp2 e  \<Longrightarrow> CoCallArityAnalysis.cccFix_nonrec cccexp1 x e = CoCallArityAnalysis.cccFix_nonrec cccexp2 x e"
279    apply (rule cfun_eqI)
280    unfolding CoCallArityAnalysis.cccFix_nonrec_eq
281    unfolding CoCallArityAnalysis.Afix_nonrec_eq
282    unfolding CoCallArityAnalysis.CCfix_nonrec_eq
283    unfolding CoCallArityAnalysis.fup_Aexp_eq
284    apply (simp only: )
285    apply (rule arg_cong[OF ccBind_cong])
286    apply simp
287    unfolding CoCallArityAnalysis.CCexp_def
288    apply simp
289    done
290
291 lemma cccFix_choose_cong[fundef_cong]:
292   "\<lbrakk> (\<And> e. e \<in> snd ` set heap2 \<Longrightarrow> cccexp1 e = cccexp2 e); heap1 = heap2 \<rbrakk>
293       \<Longrightarrow> CoCallArityAnalysis.cccFix_choose cccexp1 heap1 = CoCallArityAnalysis.cccFix_choose cccexp2 heap2"
294    unfolding CoCallArityAnalysis.cccFix_choose_def
295    apply (rule cfun_eqI)
296    apply (auto elim!: nonrecE)
297    apply (rule arg_cong[OF cccFix_nonrec_cong], auto)
298    apply (rule arg_cong[OF cccFix_cong], auto)[1]
299    done
300
301 end