Add Null and (e ? e : e)
[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 | "cCCexp Null =         \<bottom>"
78 | "cCCexp (scrut ? e1 : e2) = \<bottom>"
79 proof-
80 case goal1
81     show ?case
82     unfolding eqvt_def cCCexp_graph_aux_def
83     apply rule
84     apply (perm_simp)
85     apply (simp add: Abs_cfun_eqvt)
86     done
87 next
88 case goal3 thus ?case by (metis Terms.exp_strong_exhaust)
89 next
90 case (goal10 x e x' e')
91   from goal10(9)
92   show ?case
93   proof(rule eqvt_lam_case)
94     fix \<pi> :: perm
95     assume *: "supp (-\<pi>) \<sharp>* (fv (Lam [x]. e) :: var set)" 
96     {
97     fix n
98     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)
99        = 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))"
100       by (rule combined_restrict_perm[symmetric, OF *]) simp
101     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)"
102       by (perm_simp, simp add: eqvt_at_apply[OF goal10(1)] pemute_minus_self Abs_cfun_eqvt)
103     also have "- \<pi> \<bullet> fv (Lam [x]. e) = (fv (Lam [x]. e) :: var set)" by (rule perm_supp_eq[OF *])
104     also note calculation
105     }
106     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))
107         = (\<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
108   qed
109 next
110 case (goal19 \<Gamma> body \<Gamma>' body')
111   from goal19(9)
112   show ?case
113   proof (rule eqvt_let_case)
114     fix \<pi> :: perm
115     assume *: "supp (-\<pi>) \<sharp>* (fv (Terms.Let \<Gamma> body) :: var set)"
116     
117     { fix n
118       have "combined_restrict (fv (Terms.Let \<Gamma> body)) (CoCallArityAnalysis.cccFix_choose cCCexp_sumC (\<pi> \<bullet> \<Gamma>)\<cdot>(cCCexp_sumC (\<pi> \<bullet> body)\<cdot>n))
119       =  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)))"
120         by (rule combined_restrict_perm[OF *, symmetric]) simp
121       also have "- \<pi> \<bullet> (CoCallArityAnalysis.cccFix_choose cCCexp_sumC (\<pi> \<bullet> \<Gamma>)\<cdot>(cCCexp_sumC (\<pi> \<bullet> body)\<cdot>n)) = 
122                        CoCallArityAnalysis.cccFix_choose (- \<pi> \<bullet> cCCexp_sumC) \<Gamma>\<cdot>((- \<pi> \<bullet> cCCexp_sumC) body\<cdot>n)"
123         by (simp add: pemute_minus_self)
124       also have "CoCallArityAnalysis.cccFix_choose (- \<pi> \<bullet> cCCexp_sumC) \<Gamma> = CoCallArityAnalysis.cccFix_choose cCCexp_sumC \<Gamma>"
125         thm cccFix_cong
126         by (rule cccFix_choose_cong[OF eqvt_at_apply[OF goal19(1)] refl])
127       also have "(- \<pi> \<bullet> cCCexp_sumC) body = cCCexp_sumC body"
128         by (rule eqvt_at_apply[OF goal19(2)])
129       also note calculation
130     }
131     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))) =
132          (\<Lambda> n. combined_restrict (fv (Terms.Let \<Gamma> body)) (CoCallArityAnalysis.cccFix_choose cCCexp_sumC \<Gamma>\<cdot>(cCCexp_sumC body\<cdot>n)))" by (simp only:)
133   qed
134 qed auto
135
136 nominal_termination (eqvt) by lexicographic_order
137
138 locale CoCallAnalysisImpl
139 begin
140 sublocale CoCallArityAnalysis cCCexp.
141 sublocale ArityAnalysis Aexp.
142
143 lemma cCCexp_eq[simp]:
144   "cCCexp (Var x)\<cdot>n =      (esing x \<cdot> (up \<cdot> n),                                   \<bottom>)"
145   "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)"
146   "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)))"
147   "cCCexp (Let \<Gamma> e)\<cdot>n =    combined_restrict (fv (Let \<Gamma> e)) (CoCallArityAnalysis.cccFix_choose cCCexp \<Gamma> \<cdot> (cCCexp e\<cdot>n))"
148   "cCCexp Null\<cdot>n = \<bottom>"
149   "cCCexp (scrut ? e1 : e2)\<cdot>n = \<bottom>"
150 by (simp_all)
151 declare cCCexp.simps[simp del]
152
153
154 lemma Aexp_simps[simp]:
155   "Aexp (Var x)\<cdot>n = esing x\<cdot>(up\<cdot>n)"
156   "Aexp (Lam [x]. e)\<cdot>n = Aexp e\<cdot>(pred\<cdot>n) f|` fv (Lam [x]. e)"
157   "Aexp (App e x)\<cdot>n = Aexp e\<cdot>(inc\<cdot>n) \<squnion> esing x\<cdot>(up\<cdot>0)"
158   "\<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))"
159   "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))"
160   "Aexp Null\<cdot>n = \<bottom>"
161   "Aexp (scrut ? e1 : e2)\<cdot>n = \<bottom>"
162  by (simp add: cccFix_eq Aexp_eq fup_Aexp_eq CCexp_eq fup_CCexp_eq)+
163
164
165 lemma CCexp_simps[simp]:
166   "CCexp (Var x)\<cdot>n = \<bottom>"
167   "CCexp (Lam [x]. e)\<cdot>n = predCC (fv (Lam [x]. e)) (CCexp e)\<cdot>n"
168   "CCexp (App e x)\<cdot>n = CCexp e\<cdot>(inc\<cdot>n) \<squnion> ccProd {x} (insert x (fv e))"
169   "\<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))"
170   "atom x \<sharp> e \<Longrightarrow> CCexp (let x be e in exp)\<cdot>n =
171     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)"
172   "CCexp Null\<cdot>n = \<bottom>"
173   "CCexp (scrut ? e1 : e2)\<cdot>n = \<bottom>"
174  by (simp add: cccFix_eq Aexp_eq fup_Aexp_eq CCexp_eq fup_CCexp_eq predCC_eq)+
175
176 lemma ccField_CCexp:
177   "ccField (CCexp e\<cdot>n) \<subseteq> fv e"
178 by (induction e arbitrary: n rule: exp_induct_rec)
179    (auto simp add: ccField_ccProd predCC_eq dest: set_mp[OF ccField_cc_restr])
180
181 lemma cc_restr_CCexp[simp]:
182   "cc_restr (fv e) (CCexp e\<cdot>a) = CCexp e\<cdot>a"
183 by (rule cc_restr_noop[OF ccField_CCexp])
184
185 lemma ccField_fup_CCexp:
186   "ccField (fup\<cdot>(CCexp e)\<cdot>n) \<subseteq> fv e"
187 by (cases n) (auto dest: set_mp[OF ccField_CCexp])
188
189 lemma cc_restr_fup_ccExp_useless[simp]: "cc_restr (fv e) (fup\<cdot>(CCexp e)\<cdot>n) = fup\<cdot>(CCexp e)\<cdot>n"
190   by (rule cc_restr_noop[OF ccField_fup_CCexp])
191
192
193
194 lemma Aexp_edom': "edom (Aexp e\<cdot>a) \<subseteq> fv e"
195   by (induction e arbitrary: a rule: exp_induct_rec)(auto)
196
197 sublocale EdomArityAnalysis Aexp by default (rule Aexp_edom')
198
199
200
201 definition Aheap where
202   "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>)"
203
204 lemma Aheap_simp1[simp]:
205   "\<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>"
206   unfolding Aheap_def by simp
207
208 lemma Aheap_simp2[simp]:
209   "atom x \<sharp> e' \<Longrightarrow> Aheap [(x,e')] e \<cdot>a = Aheap_nonrec x e'\<cdot>(Aexp e\<cdot>a, CCexp e\<cdot>a)"
210   unfolding Aheap_def by (simp add: nonrec_def)
211
212 lemma Aheap_eqvt'[eqvt]:
213   "\<pi> \<bullet> (Aheap \<Gamma> e) = Aheap (\<pi> \<bullet> \<Gamma>) (\<pi> \<bullet> e)"
214   apply (rule cfun_eqvtI)
215   apply (cases nonrec \<pi> rule: eqvt_cases[where x = \<Gamma>])
216   apply simp
217   apply (erule nonrecE)
218   apply simp
219   apply (perm_simp, rule)
220   apply simp
221   apply (perm_simp, rule)
222   done
223
224 sublocale ArityAnalysisHeap Aheap.
225
226 sublocale ArityAnalysisHeapEqvt Aheap
227 proof
228   fix \<pi> show "\<pi> \<bullet> Aheap = Aheap"
229     by perm_simp rule
230 qed
231
232 lemma Aexp_lam_simp[simp]: "Aexp (Lam [x]. e) \<cdot> n = env_delete x (Aexp e \<cdot> (pred \<cdot> n))"
233 proof-
234   have "Aexp (Lam [x]. e) \<cdot> n = Aexp e\<cdot>(pred\<cdot>n) f|` (fv e - {x})" by simp
235   also have "... = env_delete x (Aexp e\<cdot>(pred\<cdot>n)) f|` (fv e - {x})" by simp
236   also have "\<dots> = env_delete x (Aexp e\<cdot>(pred\<cdot>n))"
237      by (rule env_restr_useless) (auto dest: set_mp[OF Aexp_edom])
238   finally show ?thesis.
239 qed
240 declare Aexp_simps(2)[simp del]
241
242 lemma Aexp_Let_simp1[simp]:
243   "\<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>)"
244   unfolding Aexp_simps
245   by (rule env_restr_cong) (auto dest!: set_mp[OF Afix_edom] set_mp[OF Aexp_edom] set_mp[OF thunks_domA])
246
247 lemma Aexp_Let_simp2[simp]:
248   "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)"
249   unfolding Aexp_simps env_delete_restr
250   by (rule env_restr_cong) (auto dest!: set_mp[OF fup_Aexp_edom]  set_mp[OF Aexp_edom])
251
252 declare Aexp_simps(4)[simp del]
253 declare Aexp_simps(5)[simp del]
254
255 end
256
257
258 end
259