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~)" |
|
10 | "eqvt k \<Longrightarrow> (M$N)*k = M*(%m. (N*(%n.((m $ n) $ (Lam c (k (c~)))))))" |
|
11 | "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)*k = k (Lam x (Lam c (M^(c~))))" |
|
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))))" |
|
15 | "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $ (Lam x (Lam c (M^(c~))))" |
|
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 --"-" |
|
34 apply (subgoal_tac "Lam c (ka (c~)) = Lam ca (ka (ca~))") |
|
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) |
|
51 apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))") |
|
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) |
|
62 apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))") |
|
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) |
|
73 apply (simp only:) |
|
74 apply (simp (no_asm)) |
|
75 apply (erule_tac c="a" in Abs_lst1_fcb2') |
|
76 apply (simp add: Abs_fresh_iff lt.fresh) |
|
77 apply (simp add: fresh_star_def fresh_Pair_elim lt.fresh fresh_at_base) |
|
78 oops |
|
79 |
|
80 end |
|
81 |
|
82 |
|
83 |
|