11 |
11 |
12 nominal_primrec |
12 nominal_primrec |
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>)" |
18 | fill_abs : "atom x \<sharp> M \<Longrightarrow> (CAbs x C)<M> = Lam x (C<M>)" |
18 | fill_abs : "atom x \<sharp> M \<Longrightarrow> (CAbs x C)<M> = Lam x (C<M>)" |
19 unfolding eqvt_def fill_graph_def |
19 unfolding eqvt_def fill_graph_def |
20 apply perm_simp |
20 apply perm_simp |
21 apply auto |
21 apply auto |
22 apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust) |
22 apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust) |
62 and CPS :: "lt => cpsctxt" where |
62 and CPS :: "lt => cpsctxt" where |
63 "CPSv (Var x) = x~" |
63 "CPSv (Var x) = x~" |
64 | "CPS (Var x) = CFun Hole (x~)" |
64 | "CPS (Var x) = CFun Hole (x~)" |
65 | "atom b \<sharp> M \<Longrightarrow> CPSv (Lam y M) = Lam y (Lam b ((CPS M)<Var b>))" |
65 | "atom b \<sharp> M \<Longrightarrow> CPSv (Lam y M) = Lam y (Lam b ((CPS M)<Var b>))" |
66 | "atom b \<sharp> M \<Longrightarrow> CPS (Lam y M) = CFun Hole (Lam y (Lam b ((CPS M)<Var b>)))" |
66 | "atom b \<sharp> M \<Longrightarrow> CPS (Lam y M) = CFun Hole (Lam y (Lam b ((CPS M)<Var b>)))" |
67 | "CPSv (M $ N) = Lam x (Var x)" |
67 | "CPSv (M $$ N) = Lam x (Var x)" |
68 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> CPS (M $ N) = CArg (CPSv M $ CPSv N) Hole" |
68 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> CPS (M $$ N) = CArg (CPSv M $$ CPSv N) Hole" |
69 | "isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> M \<Longrightarrow> CPS (M $ N) = |
69 | "isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> M \<Longrightarrow> CPS (M $$ N) = |
70 ccomp (CPS N) (CAbs a (CArg (CPSv M $ Var a) Hole))" |
70 ccomp (CPS N) (CAbs a (CArg (CPSv M $$ Var a) Hole))" |
71 | "~isValue M \<Longrightarrow> isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $ N) = |
71 | "~isValue M \<Longrightarrow> isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $$ N) = |
72 ccomp (CPS M) (CAbs a (CArg (Var a $ (CPSv N)) Hole))" |
72 ccomp (CPS M) (CAbs a (CArg (Var a $$ (CPSv N)) Hole))" |
73 | "~isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> (N, b) \<Longrightarrow> CPS (M $ N) = |
73 | "~isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> (N, b) \<Longrightarrow> CPS (M $$ N) = |
74 ccomp (CPS M) (CAbs a (ccomp (CPS N) (CAbs b (CArg (Var a $ Var b) Hole))))" |
74 ccomp (CPS M) (CAbs a (ccomp (CPS N) (CAbs b (CArg (Var a $$ Var b) Hole))))" |
75 apply auto |
75 apply auto |
76 defer |
76 defer |
77 apply (case_tac x) |
77 apply (case_tac x) |
78 apply (rule_tac y="a" in lt.exhaust) |
78 apply (rule_tac y="a" in lt.exhaust) |
79 apply auto |
79 apply auto |