|
2934
|
1 |
header {* CPS transformation of Danvy and Filinski *}
|
|
|
2 |
theory CPS3_DanvyFilinski imports Lt begin
|
|
|
3 |
|
|
|
4 |
nominal_primrec
|
|
|
5 |
CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100)
|
|
|
6 |
and
|
|
|
7 |
CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100)
|
|
|
8 |
where
|
|
|
9 |
"eqvt k \<Longrightarrow> (x~)*k = k (x~)"
|
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
10 |
| "eqvt k \<Longrightarrow> (M$N)*k = M*(%m. (N*(%n.((m $ n) $ (Lam c (k (c~)))))))"
|
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
11 |
| "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)*k = k (Lam x (Lam c (M^(c~))))"
|
|
2934
|
12 |
| "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t"
|
|
|
13 |
| "(x~)^l = l $ (x~)"
|
|
|
14 |
| "(M$N)^l = M*(%m. (N*(%n.((m $ n) $ l))))"
|
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
15 |
| "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $ (Lam x (Lam c (M^(c~))))"
|
|
2934
|
16 |
apply (simp only: eqvt_def CPS1_CPS2_graph_def)
|
|
|
17 |
apply (rule, perm_simp, rule)
|
|
|
18 |
apply auto
|
|
|
19 |
apply (case_tac x)
|
|
|
20 |
apply (case_tac a)
|
|
|
21 |
apply (case_tac "eqvt b")
|
|
|
22 |
apply (rule_tac y="aa" in lt.strong_exhaust)
|
|
|
23 |
apply auto[4]
|
|
|
24 |
apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
|
|
|
25 |
apply (simp add: fresh_at_base Abs1_eq_iff)
|
|
|
26 |
apply (case_tac b)
|
|
|
27 |
apply (rule_tac y="a" in lt.strong_exhaust)
|
|
|
28 |
apply auto[3]
|
|
|
29 |
apply blast
|
|
|
30 |
apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
|
|
|
31 |
apply (simp add: fresh_at_base Abs1_eq_iff)
|
|
|
32 |
apply blast
|
|
|
33 |
--"-"
|
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
34 |
apply (subgoal_tac "Lam c (ka (c~)) = Lam ca (ka (ca~))")
|
|
2934
|
35 |
apply (simp only:)
|
|
|
36 |
apply (simp add: Abs1_eq_iff)
|
|
|
37 |
apply (case_tac "c=ca")
|
|
|
38 |
apply simp_all[2]
|
|
|
39 |
apply rule
|
|
|
40 |
apply (perm_simp)
|
|
|
41 |
apply (simp add: eqvt_def)
|
|
|
42 |
apply (simp add: fresh_def)
|
|
|
43 |
apply (rule contra_subsetD[OF supp_fun_app])
|
|
|
44 |
back
|
|
|
45 |
apply (simp add: supp_fun_eqvt lt.supp supp_at_base)
|
|
|
46 |
--"-"
|
|
|
47 |
apply (rule arg_cong)
|
|
|
48 |
back
|
|
|
49 |
apply (thin_tac "eqvt ka")
|
|
|
50 |
apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
|
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
51 |
apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))")
|
|
2934
|
52 |
prefer 2
|
|
|
53 |
apply (simp add: Abs1_eq_iff')
|
|
|
54 |
apply (case_tac "c = a")
|
|
|
55 |
apply simp_all[2]
|
|
|
56 |
apply rule
|
|
|
57 |
apply (simp add: eqvt_at_def)
|
|
|
58 |
apply (simp add: swap_fresh_fresh fresh_Pair_elim)
|
|
|
59 |
apply (erule fresh_eqvt_at)
|
|
|
60 |
apply (simp add: supp_Inr finite_supp)
|
|
|
61 |
apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
|
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
62 |
apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
|
|
2934
|
63 |
prefer 2
|
|
|
64 |
apply (simp add: Abs1_eq_iff')
|
|
|
65 |
apply (case_tac "ca = a")
|
|
|
66 |
apply simp_all[2]
|
|
|
67 |
apply rule
|
|
|
68 |
apply (simp add: eqvt_at_def)
|
|
|
69 |
apply (simp add: swap_fresh_fresh fresh_Pair_elim)
|
|
|
70 |
apply (erule fresh_eqvt_at)
|
|
|
71 |
apply (simp add: supp_Inr finite_supp)
|
|
|
72 |
apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
|
|
2965
|
73 |
apply (simp only:)
|
|
|
74 |
apply (simp (no_asm))
|
|
2964
|
75 |
apply (erule_tac c="a" in Abs_lst1_fcb2')
|
|
|
76 |
apply (simp add: Abs_fresh_iff lt.fresh)
|
|
2934
|
77 |
apply (simp add: fresh_star_def fresh_Pair_elim lt.fresh fresh_at_base)
|
|
2964
|
78 |
oops
|
|
2934
|
79 |
|
|
|
80 |
end
|
|
|
81 |
|
|
|
82 |
|
|
|
83 |
|