equal
deleted
inserted
replaced
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_aux_def |
20 apply perm_simp |
20 apply simp |
21 using [[simproc del: alpha_lst]] |
21 using [[simproc del: alpha_lst]] |
22 apply auto |
22 apply auto |
23 apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust) |
23 apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust) |
24 using [[simproc del: alpha_lst]] |
24 using [[simproc del: alpha_lst]] |
25 apply (auto simp add: fresh_star_def) |
25 apply (auto simp add: fresh_star_def) |
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')" |
43 | "ccomp (CFun C N) C' = CFun (ccomp C C') N" |
43 | "ccomp (CFun C N) C' = CFun (ccomp C C') N" |
44 unfolding eqvt_def ccomp_graph_def |
44 unfolding eqvt_def ccomp_graph_aux_def |
45 apply perm_simp |
45 apply simp |
46 using [[simproc del: alpha_lst]] |
46 using [[simproc del: alpha_lst]] |
47 apply auto |
47 apply auto |
48 apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust) |
48 apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust) |
49 using [[simproc del: alpha_lst]] |
49 using [[simproc del: alpha_lst]] |
50 apply (auto simp add: fresh_star_def) |
50 apply (auto simp add: fresh_star_def) |