equal
deleted
inserted
replaced
7 Hole |
7 Hole |
8 | CFun cpsctxt lt |
8 | CFun cpsctxt lt |
9 | CArg lt cpsctxt |
9 | CArg lt cpsctxt |
10 | CAbs x::name c::cpsctxt binds x in c |
10 | CAbs x::name c::cpsctxt binds x in c |
11 |
11 |
12 nominal_primrec |
12 nominal_function |
13 fill :: "cpsctxt \<Rightarrow> lt \<Rightarrow> lt" ("_<_>" [200, 200] 100) |
13 fill :: "cpsctxt \<Rightarrow> lt \<Rightarrow> lt" ("_<_>" [200, 200] 100) |
14 where |
14 where |
15 fill_hole : "Hole<M> = M" |
15 fill_hole : "Hole<M> = M" |
16 | fill_fun : "(CFun C N)<M> = (C<M>) $$ N" |
16 | fill_fun : "(CFun C N)<M> = (C<M>) $$ N" |
17 | fill_arg : "(CArg N C)<M> = N $$ (C<M>)" |
17 | fill_arg : "(CArg N C)<M> = N $$ (C<M>)" |
32 apply (simp add: flip_fresh_fresh) |
32 apply (simp add: flip_fresh_fresh) |
33 done |
33 done |
34 |
34 |
35 termination (eqvt) by lexicographic_order |
35 termination (eqvt) by lexicographic_order |
36 |
36 |
37 nominal_primrec |
37 nominal_function |
38 ccomp :: "cpsctxt => cpsctxt => cpsctxt" |
38 ccomp :: "cpsctxt => cpsctxt => cpsctxt" |
39 where |
39 where |
40 "ccomp Hole C = C" |
40 "ccomp Hole C = C" |
41 | "atom x \<sharp> C' \<Longrightarrow> ccomp (CAbs x C) C' = CAbs x (ccomp C C')" |
41 | "atom x \<sharp> C' \<Longrightarrow> ccomp (CAbs x C) C' = CAbs x (ccomp C C')" |
42 | "ccomp (CArg N C) C' = CArg N (ccomp C C')" |
42 | "ccomp (CArg N C) C' = CArg N (ccomp C C')" |
57 apply (simp add: flip_fresh_fresh) |
57 apply (simp add: flip_fresh_fresh) |
58 done |
58 done |
59 |
59 |
60 termination (eqvt) by lexicographic_order |
60 termination (eqvt) by lexicographic_order |
61 |
61 |
62 nominal_primrec |
62 nominal_function |
63 CPSv :: "lt => lt" |
63 CPSv :: "lt => lt" |
64 and CPS :: "lt => cpsctxt" where |
64 and CPS :: "lt => cpsctxt" where |
65 "CPSv (Var x) = x~" |
65 "CPSv (Var x) = x~" |
66 | "CPS (Var x) = CFun Hole (x~)" |
66 | "CPS (Var x) = CFun Hole (x~)" |
67 | "atom b \<sharp> M \<Longrightarrow> CPSv (Lam y M) = Lam y (Lam b ((CPS M)<Var b>))" |
67 | "atom b \<sharp> M \<Longrightarrow> CPSv (Lam y M) = Lam y (Lam b ((CPS M)<Var b>))" |