5 |
5 |
6 nominal_datatype cpsctxt = |
6 nominal_datatype cpsctxt = |
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 bind x in c |
10 | CAbs x::name c::cpsctxt binds x in c |
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> = Abs 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) |
23 apply (auto simp add: fresh_star_def) |
23 apply (auto simp add: fresh_star_def) |
27 apply (simp add: finite_supp) |
27 apply (simp add: finite_supp) |
28 apply (simp add: fresh_Pair) |
28 apply (simp add: fresh_Pair) |
29 apply (simp add: eqvt_at_def swap_fresh_fresh) |
29 apply (simp add: eqvt_at_def swap_fresh_fresh) |
30 done |
30 done |
31 |
31 |
32 termination |
32 termination (eqvt) by lexicographic_order |
33 by (relation "measure (\<lambda>(x, _). size x)") (auto simp add: cpsctxt.size) |
|
34 |
|
35 lemma [eqvt]: "p \<bullet> fill c t = fill (p \<bullet> c) (p \<bullet> t)" |
|
36 by (nominal_induct c avoiding: t rule: cpsctxt.strong_induct) simp_all |
|
37 |
33 |
38 nominal_primrec |
34 nominal_primrec |
39 ccomp :: "cpsctxt => cpsctxt => cpsctxt" |
35 ccomp :: "cpsctxt => cpsctxt => cpsctxt" |
40 where |
36 where |
41 "ccomp Hole C = C" |
37 "ccomp Hole C = C" |
54 apply (simp add: finite_supp) |
50 apply (simp add: finite_supp) |
55 apply (simp add: fresh_Pair) |
51 apply (simp add: fresh_Pair) |
56 apply (simp add: eqvt_at_def swap_fresh_fresh) |
52 apply (simp add: eqvt_at_def swap_fresh_fresh) |
57 done |
53 done |
58 |
54 |
59 termination |
55 termination (eqvt) by lexicographic_order |
60 by (relation "measure (\<lambda>(x, _). size x)") (auto simp add: cpsctxt.size) |
|
61 |
|
62 lemma [eqvt]: "p \<bullet> ccomp c c' = ccomp (p \<bullet> c) (p \<bullet> c')" |
|
63 by (nominal_induct c avoiding: c' rule: cpsctxt.strong_induct) simp_all |
|
64 |
56 |
65 nominal_primrec |
57 nominal_primrec |
66 CPSv :: "lt => lt" |
58 CPSv :: "lt => lt" |
67 and CPS :: "lt => cpsctxt" where |
59 and CPS :: "lt => cpsctxt" where |
68 "CPSv (Var x) = x~" |
60 "CPSv (Var x) = x~" |
69 | "CPS (Var x) = CFun Hole (x~)" |
61 | "CPS (Var x) = CFun Hole (x~)" |
70 | "atom b \<sharp> M \<Longrightarrow> CPSv (Abs y M) = Abs y (Abs b ((CPS M)<Var b>))" |
62 | "atom b \<sharp> M \<Longrightarrow> CPSv (Lam y M) = Lam y (Lam b ((CPS M)<Var b>))" |
71 | "atom b \<sharp> M \<Longrightarrow> CPS (Abs y M) = CFun Hole (Abs y (Abs b ((CPS M)<Var b>)))" |
63 | "atom b \<sharp> M \<Longrightarrow> CPS (Lam y M) = CFun Hole (Lam y (Lam b ((CPS M)<Var b>)))" |
72 | "CPSv (M $ N) = Abs x (Var x)" |
64 | "CPSv (M $ N) = Lam x (Var x)" |
73 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> CPS (M $ N) = CArg (CPSv M $ CPSv N) Hole" |
65 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> CPS (M $ N) = CArg (CPSv M $ CPSv N) Hole" |
74 | "isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> M \<Longrightarrow> CPS (M $ N) = |
66 | "isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> M \<Longrightarrow> CPS (M $ N) = |
75 ccomp (CPS N) (CAbs a (CArg (CPSv M $ Var a) Hole))" |
67 ccomp (CPS N) (CAbs a (CArg (CPSv M $ Var a) Hole))" |
76 | "~isValue M \<Longrightarrow> isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $ N) = |
68 | "~isValue M \<Longrightarrow> isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $ N) = |
77 ccomp (CPS M) (CAbs a (CArg (Var a $ (CPSv N)) Hole))" |
69 ccomp (CPS M) (CAbs a (CArg (Var a $ (CPSv N)) Hole))" |
95 apply (simp add: fresh_Pair_elim) |
87 apply (simp add: fresh_Pair_elim) |
96 apply (case_tac "isValue lt1", case_tac [!] "isValue lt2")[1] |
88 apply (case_tac "isValue lt1", case_tac [!] "isValue lt2")[1] |
97 apply (simp_all add: fresh_Pair)[4] |
89 apply (simp_all add: fresh_Pair)[4] |
98 --"" |
90 --"" |
99 apply (rule_tac x="(y, ya, b, ba, M, Ma)" and ?'a="name" in obtain_fresh) |
91 apply (rule_tac x="(y, ya, b, ba, M, Ma)" and ?'a="name" in obtain_fresh) |
100 apply (subgoal_tac "Abs b (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Abs a (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(a~)>)") |
92 apply (subgoal_tac "Lam b (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(a~)>)") |
101 apply (subgoal_tac "Abs ba (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(ba~)>) = Abs a (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(a~)>)") |
93 apply (subgoal_tac "Lam ba (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(ba~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(a~)>)") |
102 apply (simp only:) |
94 apply (simp only:) |
103 apply (erule Abs_lst1_fcb) |
95 apply (erule Abs_lst1_fcb) |
104 apply (simp add: Abs_fresh_iff) |
96 apply (simp add: Abs_fresh_iff) |
105 apply (simp_all add: Abs_fresh_iff lt.fresh fresh_Pair_elim fresh_at_base swap_fresh_fresh)[2] |
97 apply (simp_all add: Abs_fresh_iff lt.fresh fresh_Pair_elim fresh_at_base swap_fresh_fresh)[2] |
106 (* need an invariant to get eqvt_at (Proj) *) |
98 (* need an invariant to get eqvt_at (Proj) *) |