equal
deleted
inserted
replaced
1 header {* CPS conversion *} |
1 header {* CPS conversion *} |
2 theory CPS1_Plotkin |
2 theory CPS1_Plotkin |
3 imports Lt |
3 imports Lt |
4 begin |
4 begin |
5 |
5 |
6 nominal_primrec |
6 nominal_function |
7 CPS :: "lt \<Rightarrow> lt" ("_*" [250] 250) |
7 CPS :: "lt \<Rightarrow> lt" ("_*" [250] 250) |
8 where |
8 where |
9 "atom k \<sharp> x \<Longrightarrow> (x~)* = (Lam k ((k~) $$ (x~)))" |
9 "atom k \<sharp> x \<Longrightarrow> (x~)* = (Lam k ((k~) $$ (x~)))" |
10 | "atom k \<sharp> (x, M) \<Longrightarrow> (Lam x M)* = Lam k (k~ $$ Lam x (M*))" |
10 | "atom k \<sharp> (x, M) \<Longrightarrow> (Lam x M)* = Lam k (k~ $$ Lam x (M*))" |
11 | "atom k \<sharp> (M, N) \<Longrightarrow> atom m \<sharp> (N, k) \<Longrightarrow> atom n \<sharp> (k, m) \<Longrightarrow> |
11 | "atom k \<sharp> (M, N) \<Longrightarrow> atom m \<sharp> (N, k) \<Longrightarrow> atom n \<sharp> (k, m) \<Longrightarrow> |
72 (simp_all only: atom_eq_iff[symmetric], blast+) |
72 (simp_all only: atom_eq_iff[symmetric], blast+) |
73 |
73 |
74 lemma [simp]: "x \<sharp> M* = x \<sharp> M" |
74 lemma [simp]: "x \<sharp> M* = x \<sharp> M" |
75 unfolding fresh_def by simp |
75 unfolding fresh_def by simp |
76 |
76 |
77 nominal_primrec |
77 nominal_function |
78 convert:: "lt => lt" ("_+" [250] 250) |
78 convert:: "lt => lt" ("_+" [250] 250) |
79 where |
79 where |
80 "(Var x)+ = Var x" |
80 "(Var x)+ = Var x" |
81 | "(Lam x M)+ = Lam x (M*)" |
81 | "(Lam x M)+ = Lam x (M*)" |
82 | "(M $$ N)+ = M $$ N" |
82 | "(M $$ N)+ = M $$ N" |
102 |
102 |
103 lemma [simp]: |
103 lemma [simp]: |
104 shows "isValue (p \<bullet> (M::lt)) = isValue M" |
104 shows "isValue (p \<bullet> (M::lt)) = isValue M" |
105 by (nominal_induct M rule: lt.strong_induct) auto |
105 by (nominal_induct M rule: lt.strong_induct) auto |
106 |
106 |
107 nominal_primrec |
107 nominal_function |
108 Kapply :: "lt \<Rightarrow> lt \<Rightarrow> lt" (infixl ";" 100) |
108 Kapply :: "lt \<Rightarrow> lt \<Rightarrow> lt" (infixl ";" 100) |
109 where |
109 where |
110 "Kapply (Lam x M) K = K $$ (Lam x M)+" |
110 "Kapply (Lam x M) K = K $$ (Lam x M)+" |
111 | "Kapply (Var x) K = K $$ Var x" |
111 | "Kapply (Var x) K = K $$ Var x" |
112 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> Kapply (M $$ N) K = M+ $$ N+ $$ K" |
112 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> Kapply (M $$ N) K = M+ $$ N+ $$ K" |