| author | Christian Urban <urbanc@in.tum.de> |
| Thu, 19 Apr 2018 13:57:17 +0100 | |
| changeset 3245 | 017e33849f4d |
| parent 3235 | 5ebd327ffb96 |
| permissions | -rw-r--r-- |
|
3245
017e33849f4d
updated to Isabelle 2016-1
Christian Urban <urbanc@in.tum.de>
parents:
3235
diff
changeset
|
1 |
(* 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 |
|
|
3235
5ebd327ffb96
changed nominal_primrec into the more appropriate nominal_function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3231
diff
changeset
|
4 |
nominal_function |
|
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
|
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~)" |
|
3187
b3d97424b130
added finfun-type to Nominal
Christian Urban <urbanc@in.tum.de>
parents:
3186
diff
changeset
|
10 |
| "eqvt k \<Longrightarrow> (M$$N)*k = M*(%m. (N*(%n.((m $$ n) $$ (Lam c (k (c~)))))))" |
|
2998
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" |
|
3187
b3d97424b130
added finfun-type to Nominal
Christian Urban <urbanc@in.tum.de>
parents:
3186
diff
changeset
|
13 |
| "(x~)^l = l $$ (x~)" |
|
b3d97424b130
added finfun-type to Nominal
Christian Urban <urbanc@in.tum.de>
parents:
3186
diff
changeset
|
14 |
| "(M$$N)^l = M*(%m. (N*(%n.((m $$ n) $$ l))))" |
|
b3d97424b130
added finfun-type to Nominal
Christian Urban <urbanc@in.tum.de>
parents:
3186
diff
changeset
|
15 |
| "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $$ (Lam x (Lam c (M^(c~))))" |
|
3197
25d11b449e92
definition of an auxiliary graph in nominal-primrec definitions
Christian Urban <urbanc@in.tum.de>
parents:
3192
diff
changeset
|
16 |
apply (simp add: eqvt_def CPS1_CPS2_graph_aux_def) |
|
3192
14c7d7e29c44
added a simproc for alpha-equivalence to the simplifier
Christian Urban <urbanc@in.tum.de>
parents:
3187
diff
changeset
|
17 |
using [[simproc del: alpha_lst]] |
|
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
|
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 (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
|
30 |
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
|
31 |
--"-" |
|
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2984
diff
changeset
|
32 |
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
|
33 |
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
|
34 |
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
|
35 |
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
|
36 |
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
|
37 |
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
|
38 |
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
|
39 |
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
|
40 |
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
|
41 |
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
|
42 |
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
|
43 |
apply (simp add: supp_fun_eqvt lt.supp supp_at_base) |
|
3186
425b4c406d80
added CPS files to test (not all proofs have been completed)
Christian Urban <urbanc@in.tum.de>
parents:
3089
diff
changeset
|
44 |
oops |
| 2882 | 45 |
|
46 |
||
|
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
|
47 |
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
|
48 |
|
|
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 |
|
|
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 |