| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Fri, 19 Aug 2011 12:49:38 +0900 | |
| changeset 2998 | f0fab367453a |
| parent 2984 | 1b39ba5db2c1 |
| child 3089 | 9bcf02a6eea9 |
| permissions | -rw-r--r-- |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
header {* CPS transformation of Danvy and Filinski *}
|
|
2895
65efa1c7563c
Theory name changes for JEdit
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2882
diff
changeset
|
2 |
theory CPS3_DanvyFilinski imports Lt begin |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
|
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
nominal_primrec |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100)
|
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
and |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100)
|
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
where |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
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>
parents:
2984
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>
parents:
2984
diff
changeset
|
11 |
| "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)*k = k (Lam x (Lam c (M^(c~))))" |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
| "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t" |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
| "(x~)^l = l $ (x~)" |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
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>
parents:
2984
diff
changeset
|
15 |
| "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $ (Lam x (Lam c (M^(c~))))" |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
apply (simp only: eqvt_def CPS1_CPS2_graph_def) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
apply (rule, perm_simp, rule) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
apply auto |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
apply (case_tac x) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
apply (case_tac a) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
apply (case_tac "eqvt b") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
apply (rule_tac y="aa" in lt.strong_exhaust) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
apply auto[4] |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
24 |
apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
25 |
apply (simp add: fresh_at_base Abs1_eq_iff) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
26 |
apply (case_tac b) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
apply (rule_tac y="a" in lt.strong_exhaust) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
apply auto[3] |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
29 |
apply blast |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
30 |
apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
31 |
apply (simp add: fresh_at_base Abs1_eq_iff) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
32 |
apply blast |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
33 |
--"-" |
|
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2984
diff
changeset
|
34 |
apply (subgoal_tac "Lam c (ka (c~)) = Lam ca (ka (ca~))") |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
35 |
apply (simp only:) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
36 |
apply (simp add: Abs1_eq_iff) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
37 |
apply (case_tac "c=ca") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
38 |
apply simp_all[2] |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
39 |
apply rule |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
40 |
apply (perm_simp) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
41 |
apply (simp add: eqvt_def) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
42 |
apply (simp add: fresh_def) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
43 |
apply (rule contra_subsetD[OF supp_fun_app]) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
44 |
back |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
45 |
apply (simp add: supp_fun_eqvt lt.supp supp_at_base) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
46 |
--"-" |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
47 |
apply (rule arg_cong) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
48 |
back |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
49 |
apply simp |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
50 |
apply (thin_tac "eqvt ka") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
51 |
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>
parents:
2984
diff
changeset
|
52 |
apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))") |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
53 |
prefer 2 |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
54 |
apply (simp add: Abs1_eq_iff') |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
55 |
apply (case_tac "c = a") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
56 |
apply simp_all[2] |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
57 |
apply rule |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
58 |
apply (simp add: eqvt_at_def) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
59 |
apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
60 |
apply (erule fresh_eqvt_at) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
61 |
apply (simp add: supp_Inr finite_supp) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
62 |
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>
parents:
2984
diff
changeset
|
63 |
apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))") |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
64 |
prefer 2 |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
65 |
apply (simp add: Abs1_eq_iff') |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
66 |
apply (case_tac "ca = a") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
67 |
apply simp_all[2] |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
68 |
apply rule |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
69 |
apply (simp add: eqvt_at_def) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
70 |
apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
71 |
apply (erule fresh_eqvt_at) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
72 |
apply (simp add: supp_Inr finite_supp) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
73 |
apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
74 |
apply (simp only: ) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
75 |
apply (erule Abs_lst1_fcb) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
76 |
apply (simp add: Abs_fresh_iff) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
77 |
apply (drule sym) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
78 |
apply (simp only:) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
79 |
apply (simp add: Abs_fresh_iff lt.fresh) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
80 |
apply clarify |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
81 |
apply (erule fresh_eqvt_at) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
82 |
apply (simp add: supp_Inr finite_supp) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
83 |
apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
84 |
apply (drule sym) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
85 |
apply (drule sym) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
86 |
apply (drule sym) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
87 |
apply (simp only:) |
|
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2984
diff
changeset
|
88 |
apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (M, a~))) = Lam c (CPS1_CPS2_sumC (Inr (M, c~)))") |
|
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2984
diff
changeset
|
89 |
apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))") |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
90 |
apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
91 |
apply (simp add: fresh_Pair_elim) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
92 |
apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]]) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
93 |
back |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
94 |
back |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
95 |
back |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
96 |
apply assumption |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
97 |
apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
98 |
apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
99 |
apply simp_all[3] |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
100 |
apply rule |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
101 |
apply (case_tac "c = xa") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
102 |
apply simp_all[2] |
|
2963
8b22497c25b9
Experiment with permuting eqvt_at
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2895
diff
changeset
|
103 |
apply (rotate_tac 1) |
| 2965 | 104 |
apply (drule_tac q="(atom ca \<rightleftharpoons> atom x)" in eqvt_at_perm) |
|
2963
8b22497c25b9
Experiment with permuting eqvt_at
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2895
diff
changeset
|
105 |
apply (simp add: swap_fresh_fresh) |
|
8b22497c25b9
Experiment with permuting eqvt_at
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2895
diff
changeset
|
106 |
apply (simp add: eqvt_at_def swap_fresh_fresh) |
|
8b22497c25b9
Experiment with permuting eqvt_at
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2895
diff
changeset
|
107 |
apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))") |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
108 |
apply (simp add: eqvt_at_def) |
|
2963
8b22497c25b9
Experiment with permuting eqvt_at
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2895
diff
changeset
|
109 |
apply (drule_tac x="(atom ca \<rightleftharpoons> atom c)" in spec) |
|
8b22497c25b9
Experiment with permuting eqvt_at
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2895
diff
changeset
|
110 |
apply simp |
|
8b22497c25b9
Experiment with permuting eqvt_at
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2895
diff
changeset
|
111 |
apply (metis (no_types) atom_eq_iff fresh_permute_iff permute_swap_cancel swap_atom_simps(3) swap_fresh_fresh) |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
112 |
apply (case_tac "c = xa") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
113 |
apply simp |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
114 |
apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
115 |
apply (simp add: atom_eqvt eqvt_at_def) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
116 |
apply (simp add: flip_fresh_fresh) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
117 |
apply (subst fresh_permute_iff) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
118 |
apply (erule fresh_eqvt_at) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
119 |
apply (simp add: supp_Inr finite_supp) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
120 |
apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
121 |
apply simp |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
122 |
apply clarify |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
123 |
apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
124 |
apply (simp add: eqvt_at_def) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
125 |
apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
126 |
apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
127 |
apply (erule fresh_eqvt_at) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
128 |
apply (simp add: finite_supp supp_Inr) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
129 |
apply (simp add: fresh_Inr fresh_Pair lt.fresh) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
130 |
apply rule |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
131 |
apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
132 |
apply (simp add: fresh_def supp_at_base) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
133 |
apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
134 |
--"-" |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
135 |
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>
parents:
2984
diff
changeset
|
136 |
apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))") |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
137 |
prefer 2 |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
138 |
apply (simp add: Abs1_eq_iff') |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
139 |
apply (case_tac "c = a") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
140 |
apply simp_all[2] |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
141 |
apply rule |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
142 |
apply (simp add: eqvt_at_def) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
143 |
apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
144 |
apply (erule fresh_eqvt_at) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
145 |
apply (simp add: supp_Inr finite_supp) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
146 |
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>
parents:
2984
diff
changeset
|
147 |
apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))") |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
148 |
prefer 2 |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
149 |
apply (simp add: Abs1_eq_iff') |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
150 |
apply (case_tac "ca = a") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
151 |
apply simp_all[2] |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
152 |
apply rule |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
153 |
apply (simp add: eqvt_at_def) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
154 |
apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
155 |
apply (erule fresh_eqvt_at) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
156 |
apply (simp add: supp_Inr finite_supp) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
157 |
apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
158 |
apply (simp only: ) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
159 |
apply (erule Abs_lst1_fcb) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
160 |
apply (simp add: Abs_fresh_iff) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
161 |
apply (drule sym) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
162 |
apply (simp only:) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
163 |
apply (simp add: Abs_fresh_iff lt.fresh) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
164 |
apply clarify |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
165 |
apply (erule fresh_eqvt_at) |
|
2963
8b22497c25b9
Experiment with permuting eqvt_at
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2895
diff
changeset
|
166 |
apply (simp add: supp_Inr finite_supp) (* TODO put sum of fs into fs typeclass *) |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
167 |
apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
168 |
apply (drule sym) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
169 |
apply (drule sym) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
170 |
apply (drule sym) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
171 |
apply (simp only:) |
|
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2984
diff
changeset
|
172 |
apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (M, a~))) = Lam c (CPS1_CPS2_sumC (Inr (M, c~)))") |
|
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2984
diff
changeset
|
173 |
apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))") |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
174 |
apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
175 |
apply (simp add: fresh_Pair_elim) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
176 |
apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]]) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
177 |
back |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
178 |
back |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
179 |
back |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
180 |
apply assumption |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
181 |
apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
182 |
apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
183 |
apply simp_all[3] |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
184 |
apply rule |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
185 |
apply (case_tac "c = xa") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
186 |
apply simp_all[2] |
|
2963
8b22497c25b9
Experiment with permuting eqvt_at
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2895
diff
changeset
|
187 |
apply (rotate_tac 1) |
| 2965 | 188 |
apply (drule_tac q="(atom ca \<rightleftharpoons> atom x)" in eqvt_at_perm) |
|
2963
8b22497c25b9
Experiment with permuting eqvt_at
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2895
diff
changeset
|
189 |
apply (simp add: swap_fresh_fresh) |
|
8b22497c25b9
Experiment with permuting eqvt_at
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2895
diff
changeset
|
190 |
apply (simp add: eqvt_at_def swap_fresh_fresh) |
|
8b22497c25b9
Experiment with permuting eqvt_at
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2895
diff
changeset
|
191 |
apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))") |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
192 |
apply (simp add: eqvt_at_def) |
|
2963
8b22497c25b9
Experiment with permuting eqvt_at
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2895
diff
changeset
|
193 |
apply (drule_tac x="(atom ca \<rightleftharpoons> atom c)" in spec) |
|
8b22497c25b9
Experiment with permuting eqvt_at
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2895
diff
changeset
|
194 |
apply simp |
|
8b22497c25b9
Experiment with permuting eqvt_at
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2895
diff
changeset
|
195 |
apply (metis (no_types) atom_eq_iff fresh_permute_iff permute_swap_cancel swap_atom_simps(3) swap_fresh_fresh) |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
196 |
apply (case_tac "c = xa") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
197 |
apply simp |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
198 |
apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
199 |
apply (simp add: atom_eqvt eqvt_at_def) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
200 |
apply (simp add: flip_fresh_fresh) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
201 |
apply (subst fresh_permute_iff) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
202 |
apply (erule fresh_eqvt_at) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
203 |
apply (simp add: supp_Inr finite_supp) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
204 |
apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
205 |
apply simp |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
206 |
apply clarify |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
207 |
apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
208 |
apply (simp add: eqvt_at_def) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
209 |
apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))") |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
210 |
apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
211 |
apply (erule fresh_eqvt_at) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
212 |
apply (simp add: finite_supp supp_Inr) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
213 |
apply (simp add: fresh_Inr fresh_Pair lt.fresh) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
214 |
apply rule |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
215 |
apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
216 |
apply (simp add: fresh_def supp_at_base) |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
217 |
apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) |
|
2865
a30d0bb76869
CPS3 can be defined with eqvt_rhs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2861
diff
changeset
|
218 |
done |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
219 |
|
|
2984
1b39ba5db2c1
update to 'termination (eqvt)'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2965
diff
changeset
|
220 |
termination (eqvt) |
|
2865
a30d0bb76869
CPS3 can be defined with eqvt_rhs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2861
diff
changeset
|
221 |
by lexicographic_order |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
222 |
|
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
223 |
definition psi:: "lt => lt" |
| 2882 | 224 |
where [simp]: "psi V == V*(\<lambda>x. x)" |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
225 |
|
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
226 |
section {* Simple consequence of CPS *}
|
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
227 |
|
| 2882 | 228 |
lemma [simp]: "eqvt (\<lambda>x\<Colon>lt. x)" |
229 |
by (simp add: eqvt_def eqvt_bound eqvt_lambda) |
|
230 |
||
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
231 |
lemma value_eq1 : "isValue V \<Longrightarrow> eqvt k \<Longrightarrow> V*k = k (psi V)" |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
232 |
apply (cases V rule: lt.exhaust) |
| 2882 | 233 |
apply simp_all |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
234 |
apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
| 2882 | 235 |
apply simp |
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
236 |
done |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
237 |
|
| 2882 | 238 |
lemma value_eq2 : "isValue V \<Longrightarrow> V^K = K $ (psi V)" |
239 |
apply (cases V rule: lt.exhaust) |
|
240 |
apply simp_all |
|
241 |
apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
|
242 |
apply simp |
|
243 |
done |
|
244 |
||
|
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2984
diff
changeset
|
245 |
lemma value_eq3' : "~isValue M \<Longrightarrow> eqvt k \<Longrightarrow> M*k = (M^(Lam n (k (Var n))))" |
| 2882 | 246 |
by (cases M rule: lt.exhaust) auto |
247 |
||
248 |
||
249 |
||
|
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
250 |
end |
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
251 |
|
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
252 |
|
|
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
253 |