8990025573274b7381acbe0f34ef789236f0c3b1
[darcs-mirror-isa-launchbury.git] / Launchbury / CoCallAnalysisImpl.thy
1 theory CoCallAnalysisImpl
2 imports "Arity-Nominal" "Nominal-HOLCF" "Env-Nominal" "Env-HOLCF" CoCallFix
3 begin
4
5 fun combined_restrict :: "var set \<Rightarrow> (AEnv \<times> CoCalls) \<Rightarrow> (AEnv \<times> CoCalls)"
6   where "combined_restrict S (env, G) = (env f|` S, cc_restr S G)"
7
8 lemma fst_combined_restrict[simp]:
9   "fst (combined_restrict S p) = fst p f|` S"
10   by (cases p, simp)
11
12 lemma snd_combined_restrict[simp]:
13   "snd (combined_restrict S p) = cc_restr S (snd p)"
14   by (cases p, simp)
15
16 lemma combined_restrict_eqvt[eqvt]:
17   shows "\<pi> \<bullet> combined_restrict S p = combined_restrict (\<pi> \<bullet> S) (\<pi> \<bullet> p)"
18   by (cases p) auto
19
20 lemma combined_restrict_cont:
21   "cont (\<lambda>x. combined_restrict S x)"
22 proof-
23   have "cont (\<lambda>(env, G). combined_restrict S (env, G))" by simp
24   thus ?thesis by (metis split_eta)
25 qed
26 lemmas cont_compose[OF combined_restrict_cont, cont2cont, simp]
27
28 lemma combined_restrict_perm:
29   assumes "supp \<pi> \<sharp>* S" and [simp]: "finite S"
30   shows "combined_restrict S (\<pi> \<bullet> p) = combined_restrict S p"
31 proof(cases p)
32   fix env :: AEnv and  G :: CoCalls
33   assume "p = (env, G)"
34   moreover 
35   from assms
36   have "env_restr S (\<pi> \<bullet> env) = env_restr S env" by (rule env_restr_perm)
37   moreover
38   from assms
39   have "cc_restr S (\<pi> \<bullet> G) = cc_restr S G" by (rule cc_restr_perm)
40   ultimately
41   show ?thesis by simp
42 qed
43
44 definition predCC :: "var set \<Rightarrow> (Arity \<rightarrow> CoCalls) \<Rightarrow> (Arity \<rightarrow> CoCalls)"
45   where "predCC S f = (\<Lambda> a. if a \<noteq> 0 then cc_restr S (f\<cdot>(pred\<cdot>a)) else ccSquare S)"
46
47 lemma predCC_eq:
48   shows "predCC S f \<cdot> a = (if a \<noteq> 0 then cc_restr S (f\<cdot>(pred\<cdot>a)) else ccSquare S)"
49   unfolding predCC_def
50   apply (rule beta_cfun)
51   apply (rule cont_if_else_above)
52   apply (auto dest: set_mp[OF ccField_cc_restr])
53   done
54
55 lemma predCC_eqvt[eqvt, simp]: "\<pi> \<bullet> (predCC S f) = predCC (\<pi> \<bullet> S) (\<pi> \<bullet> f)"
56   apply (rule cfun_eqvtI)
57   unfolding predCC_eq
58   by perm_simp rule
59
60 lemma cc_restr_predCC:
61   "cc_restr S (predCC S' f\<cdot>n) = (predCC (S' \<inter> S) (\<Lambda> n. cc_restr S (f\<cdot>n)))\<cdot>n"
62   unfolding predCC_eq
63   by (auto simp add: inf_commute ccSquare_def)
64
65 lemma cc_restr_predCC'[simp]:
66   "cc_restr S (predCC S f\<cdot>n) = predCC S f\<cdot>n"
67   unfolding predCC_eq by simp
68
69   
70 nominal_function
71   cCCexp :: "exp \<Rightarrow> (Arity \<rightarrow> AEnv \<times> CoCalls)" 
72 where
73   "cCCexp (Var x) =      (\<Lambda> n . (esing x \<cdot> (up \<cdot> n),                                   \<bottom>))"
74 | "cCCexp (Lam [x]. e) = (\<Lambda> n . combined_restrict (fv (Lam [x]. e)) (fst (cCCexp e\<cdot>(pred\<cdot>n)), predCC (fv (Lam [x]. e)) (\<Lambda> a. snd(cCCexp e\<cdot>a))\<cdot>n))"
75 | "cCCexp (App e x) =    (\<Lambda> n . (fst (cCCexp e\<cdot>(inc\<cdot>n)) \<squnion> (esing x \<cdot> (up\<cdot>0)),          snd (cCCexp e\<cdot>(inc\<cdot>n)) \<squnion> ccProd {x} (insert x (fv e))))"
76 | "cCCexp (Let \<Gamma> e) =    (\<Lambda> n . combined_restrict (fv (Let \<Gamma> e)) (CoCallArityAnalysis.cccFix_choose cCCexp \<Gamma> \<cdot> (cCCexp e\<cdot>n)))"
77 proof-
78 case goal1
79     show ?case
80     unfolding eqvt_def cCCexp_graph_aux_def
81     apply rule
82     apply (perm_simp)
83     apply (simp add: Abs_cfun_eqvt)
84     done
85 next
86 case goal3 thus ?case by (metis Terms.exp_strong_exhaust)
87 next
88 case (goal8 x e x' e')
89   from goal8(9)
90   show ?case
91   proof(rule eqvt_lam_case)
92     fix \<pi> :: perm
93     assume *: "supp (-\<pi>) \<sharp>* (fv (Lam [x]. e) :: var set)" 
94     {
95     fix n
96     have "combined_restrict (fv (Lam [x]. e)) (fst (cCCexp_sumC (\<pi> \<bullet> e)\<cdot>(pred\<cdot>n)), predCC (fv (Lam [x]. e)) (\<Lambda> a. snd(cCCexp_sumC (\<pi> \<bullet> e)\<cdot>a))\<cdot>n)
97        = combined_restrict (fv (Lam [x]. e)) (- \<pi> \<bullet> (fst (cCCexp_sumC (\<pi> \<bullet> e)\<cdot>(pred\<cdot>n)), predCC (fv (Lam [x]. e)) (\<Lambda> a. snd(cCCexp_sumC (\<pi> \<bullet> e)\<cdot>a))\<cdot>n))"
98       by (rule combined_restrict_perm[symmetric, OF *]) simp
99     also have "\<dots> = combined_restrict (fv (Lam [x]. e)) (fst (cCCexp_sumC e\<cdot>(pred\<cdot>n)), predCC (- \<pi> \<bullet> fv (Lam [x]. e)) (\<Lambda> a. snd(cCCexp_sumC e\<cdot>a))\<cdot>n)"
100       by (perm_simp, simp add: eqvt_at_apply[OF goal8(1)] pemute_minus_self Abs_cfun_eqvt)
101     also have "- \<pi> \<bullet> fv (Lam [x]. e) = (fv (Lam [x]. e) :: var set)" by (rule perm_supp_eq[OF *])
102     also note calculation
103     }
104     thus "(\<Lambda> n. combined_restrict (fv (Lam [x]. e)) (fst (cCCexp_sumC (\<pi> \<bullet> e)\<cdot>(pred\<cdot>n)), predCC (fv (Lam [x]. e)) (\<Lambda> a. snd(cCCexp_sumC (\<pi> \<bullet> e)\<cdot>a))\<cdot>n))
105         = (\<Lambda> n. combined_restrict (fv (Lam [x]. e)) (fst (cCCexp_sumC e\<cdot>(pred\<cdot>n)), predCC (fv (Lam [x]. e)) (\<Lambda> a. snd(cCCexp_sumC e\<cdot>a))\<cdot>n))" by simp
106   qed
107 next
108 case (goal13 \<Gamma> body \<Gamma>' body')
109   from goal13(9)
110   show ?case
111   proof (rule eqvt_let_case)
112     fix \<pi> :: perm
113     assume *: "supp (-\<pi>) \<sharp>* (fv (Terms.Let \<Gamma> body) :: var set)"
114     
115     { fix n
116       have "combined_restrict (fv (Terms.Let \<Gamma> body)) (CoCallArityAnalysis.cccFix_choose cCCexp_sumC (\<pi> \<bullet> \<Gamma>)\<cdot>(cCCexp_sumC (\<pi> \<bullet> body)\<cdot>n))
117       =  combined_restrict (fv (Terms.Let \<Gamma> body)) (- \<pi> \<bullet> (CoCallArityAnalysis.cccFix_choose cCCexp_sumC (\<pi> \<bullet> \<Gamma>)\<cdot>(cCCexp_sumC (\<pi> \<bullet> body)\<cdot>n)))"
118         by (rule combined_restrict_perm[OF *, symmetric]) simp
119       also have "- \<pi> \<bullet> (CoCallArityAnalysis.cccFix_choose cCCexp_sumC (\<pi> \<bullet> \<Gamma>)\<cdot>(cCCexp_sumC (\<pi> \<bullet> body)\<cdot>n)) = 
120                        CoCallArityAnalysis.cccFix_choose (- \<pi> \<bullet> cCCexp_sumC) \<Gamma>\<cdot>((- \<pi> \<bullet> cCCexp_sumC) body\<cdot>n)"
121         by (simp add: pemute_minus_self)
122       also have "CoCallArityAnalysis.cccFix_choose (- \<pi> \<bullet> cCCexp_sumC) \<Gamma> = CoCallArityAnalysis.cccFix_choose cCCexp_sumC \<Gamma>"
123         thm cccFix_cong
124         by (rule cccFix_choose_cong[OF eqvt_at_apply[OF goal13(1)] refl])
125       also have "(- \<pi> \<bullet> cCCexp_sumC) body = cCCexp_sumC body"
126         by (rule eqvt_at_apply[OF goal13(2)])
127       also note calculation
128     }
129     thus "(\<Lambda> n. combined_restrict (fv (Terms.Let \<Gamma> body)) (CoCallArityAnalysis.cccFix_choose cCCexp_sumC (\<pi> \<bullet> \<Gamma>)\<cdot>(cCCexp_sumC (\<pi> \<bullet> body)\<cdot>n))) =
130          (\<Lambda> n. combined_restrict (fv (Terms.Let \<Gamma> body)) (CoCallArityAnalysis.cccFix_choose cCCexp_sumC \<Gamma>\<cdot>(cCCexp_sumC body\<cdot>n)))" by (simp only:)
131   qed
132 qed auto
133
134 nominal_termination (eqvt) by lexicographic_order
135
136 locale CoCallAnalysisImpl
137 begin
138 sublocale CoCallArityAnalysis cCCexp.
139 sublocale ArityAnalysis Aexp.
140
141 lemma cCCexp_eq[simp]:
142   "cCCexp (Var x)\<cdot>n =      (esing x \<cdot> (up \<cdot> n),                                   \<bottom>)"
143   "cCCexp (Lam [x]. e)\<cdot>n = combined_restrict (fv (Lam [x]. e)) (fst (cCCexp e\<cdot>(pred\<cdot>n)), predCC (fv (Lam [x]. e)) (\<Lambda> a. snd(cCCexp e\<cdot>a))\<cdot>n)"
144   "cCCexp (App e x)\<cdot>n =    (fst (cCCexp e\<cdot>(inc\<cdot>n)) \<squnion> (esing x \<cdot> (up\<cdot>0)),          snd (cCCexp e\<cdot>(inc\<cdot>n)) \<squnion> ccProd {x} (insert x (fv e)))"
145   "cCCexp (Let \<Gamma> e)\<cdot>n =    combined_restrict (fv (Let \<Gamma> e)) (CoCallArityAnalysis.cccFix_choose cCCexp \<Gamma> \<cdot> (cCCexp e\<cdot>n))"
146 by (simp_all)
147 declare cCCexp.simps[simp del]
148
149
150 lemma Aexp_simps[simp]:
151   "Aexp (Var x)\<cdot>n = esing x\<cdot>(up\<cdot>n)"
152   "Aexp (Lam [x]. e)\<cdot>n = Aexp e\<cdot>(pred\<cdot>n) f|` fv (Lam [x]. e)"
153   "Aexp (App e x)\<cdot>n = Aexp e\<cdot>(inc\<cdot>n) \<squnion> esing x\<cdot>(up\<cdot>0)"
154   "\<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|` (fv (Let \<Gamma> e))"
155   "atom x \<sharp> e \<Longrightarrow> Aexp (let x be e in exp)\<cdot>n = (fup\<cdot>(Aexp e)\<cdot>(ABind_nonrec x e \<cdot> (Aexp exp\<cdot>n, CCexp exp\<cdot>n)) \<squnion> Aexp exp\<cdot>n) f|` (fv (let x be e in exp))"
156  by (simp add: cccFix_eq Aexp_eq fup_Aexp_eq CCexp_eq fup_CCexp_eq)+
157
158
159 lemma CCexp_simps[simp]:
160   "CCexp (Var x)\<cdot>n = \<bottom>"
161   "CCexp (Lam [x]. e)\<cdot>n = predCC (fv (Lam [x]. e)) (CCexp e)\<cdot>n"
162   "CCexp (App e x)\<cdot>n = CCexp e\<cdot>(inc\<cdot>n) \<squnion> ccProd {x} (insert x (fv e))"
163   "\<not> nonrec \<Gamma> \<Longrightarrow> CCexp (Let \<Gamma> e)\<cdot>n = cc_restr (fv (Let \<Gamma> e)) (CCfix \<Gamma>\<cdot>(Afix \<Gamma>\<cdot>(Aexp e\<cdot>n  \<squnion> (\<lambda>_.up\<cdot>0) f|` (thunks \<Gamma>)), CCexp e\<cdot>n))"
164   "atom x \<sharp> e \<Longrightarrow> CCexp (let x be e in exp)\<cdot>n =
165     cc_restr (fv (let x be e in exp)) (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)"
166  by (simp add: cccFix_eq Aexp_eq fup_Aexp_eq CCexp_eq fup_CCexp_eq predCC_eq)+
167
168 lemma ccField_CCexp:
169   "ccField (CCexp e\<cdot>n) \<subseteq> fv e"
170 by (induction e arbitrary: n rule: exp_induct_rec)
171    (auto simp add: ccField_ccProd predCC_eq dest: set_mp[OF ccField_cc_restr])
172
173 lemma cc_restr_CCexp[simp]:
174   "cc_restr (fv e) (CCexp e\<cdot>a) = CCexp e\<cdot>a"
175 by (rule cc_restr_noop[OF ccField_CCexp])
176
177 lemma ccField_fup_CCexp:
178   "ccField (fup\<cdot>(CCexp e)\<cdot>n) \<subseteq> fv e"
179 by (cases n) (auto dest: set_mp[OF ccField_CCexp])
180
181 lemma cc_restr_fup_ccExp_useless[simp]: "cc_restr (fv e) (fup\<cdot>(CCexp e)\<cdot>n) = fup\<cdot>(CCexp e)\<cdot>n"
182   by (rule cc_restr_noop[OF ccField_fup_CCexp])
183
184
185
186 lemma Aexp_edom': "edom (Aexp e\<cdot>a) \<subseteq> fv e"
187   by (induction e arbitrary: a rule: exp_induct_rec)(auto)
188
189 sublocale EdomArityAnalysis Aexp by default (rule Aexp_edom')
190
191
192
193 definition Aheap where
194   "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>)"
195
196 lemma Aheap_simp1[simp]:
197   "\<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>"
198   unfolding Aheap_def by simp
199
200 lemma Aheap_simp2[simp]:
201   "atom x \<sharp> e' \<Longrightarrow> Aheap [(x,e')] e \<cdot>a = Aheap_nonrec x e'\<cdot>(Aexp e\<cdot>a, CCexp e\<cdot>a)"
202   unfolding Aheap_def by (simp add: nonrec_def)
203
204 lemma Aheap_eqvt'[eqvt]:
205   "\<pi> \<bullet> (Aheap \<Gamma> e) = Aheap (\<pi> \<bullet> \<Gamma>) (\<pi> \<bullet> e)"
206   apply (rule cfun_eqvtI)
207   apply (cases nonrec \<pi> rule: eqvt_cases[where x = \<Gamma>])
208   apply simp
209   apply (erule nonrecE)
210   apply simp
211   apply (perm_simp, rule)
212   apply simp
213   apply (perm_simp, rule)
214   done
215
216 sublocale ArityAnalysisHeap Aheap.
217
218 sublocale ArityAnalysisHeapEqvt Aheap
219 proof
220   fix \<pi> show "\<pi> \<bullet> Aheap = Aheap"
221     by perm_simp rule
222 qed
223
224 lemma Aexp_lam_simp[simp]: "Aexp (Lam [x]. e) \<cdot> n = env_delete x (Aexp e \<cdot> (pred \<cdot> n))"
225 proof-
226   have "Aexp (Lam [x]. e) \<cdot> n = Aexp e\<cdot>(pred\<cdot>n) f|` (fv e - {x})" by simp
227   also have "... = env_delete x (Aexp e\<cdot>(pred\<cdot>n)) f|` (fv e - {x})" by simp
228   also have "\<dots> = env_delete x (Aexp e\<cdot>(pred\<cdot>n))"
229      by (rule env_restr_useless) (auto dest: set_mp[OF Aexp_edom])
230   finally show ?thesis.
231 qed
232 declare Aexp_simps(2)[simp del]
233
234 lemma Aexp_Let_simp1[simp]:
235   "\<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>)"
236   unfolding Aexp_simps
237   by (rule env_restr_cong) (auto dest!: set_mp[OF Afix_edom] set_mp[OF Aexp_edom] set_mp[OF thunks_domA])
238
239 lemma Aexp_Let_simp2[simp]:
240   "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)"
241   unfolding Aexp_simps env_delete_restr
242   by (rule env_restr_cong) (auto dest!: set_mp[OF fup_Aexp_edom]  set_mp[OF Aexp_edom])
243
244 declare Aexp_simps(4)[simp del]
245 declare Aexp_simps(5)[simp del]
246
247 end
248
249
250 end
251