equal
deleted
inserted
replaced
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 using [[simproc del: alpha_lst]] |
21 apply auto |
22 apply auto |
22 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]] |
23 apply (auto simp add: fresh_star_def) |
25 apply (auto simp add: fresh_star_def) |
24 apply (erule Abs_lst1_fcb) |
26 apply (erule Abs_lst1_fcb) |
25 apply (simp_all add: Abs_fresh_iff)[2] |
27 apply (simp_all add: Abs_fresh_iff)[2] |
26 apply (erule fresh_eqvt_at) |
28 apply (erule fresh_eqvt_at) |
27 apply (simp add: finite_supp) |
29 apply (simp add: finite_supp) |
39 | "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')" |
40 | "ccomp (CArg N C) C' = CArg N (ccomp C C')" |
42 | "ccomp (CArg N C) C' = CArg N (ccomp C C')" |
41 | "ccomp (CFun C N) C' = CFun (ccomp C C') N" |
43 | "ccomp (CFun C N) C' = CFun (ccomp C C') N" |
42 unfolding eqvt_def ccomp_graph_def |
44 unfolding eqvt_def ccomp_graph_def |
43 apply perm_simp |
45 apply perm_simp |
|
46 using [[simproc del: alpha_lst]] |
44 apply auto |
47 apply auto |
45 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]] |
46 apply (auto simp add: fresh_star_def) |
50 apply (auto simp add: fresh_star_def) |
47 apply blast+ |
51 apply blast+ |
48 apply (erule Abs_lst1_fcb) |
52 apply (erule Abs_lst1_fcb) |
49 apply (simp_all add: Abs_fresh_iff) |
53 apply (simp_all add: Abs_fresh_iff) |
50 apply (erule fresh_eqvt_at) |
54 apply (erule fresh_eqvt_at) |
69 ccomp (CPS N) (CAbs a (CArg (CPSv M $$ Var a) Hole))" |
73 ccomp (CPS N) (CAbs a (CArg (CPSv M $$ Var a) Hole))" |
70 | "~isValue M \<Longrightarrow> isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $$ N) = |
74 | "~isValue M \<Longrightarrow> isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $$ N) = |
71 ccomp (CPS M) (CAbs a (CArg (Var a $$ (CPSv N)) Hole))" |
75 ccomp (CPS M) (CAbs a (CArg (Var a $$ (CPSv N)) Hole))" |
72 | "~isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> (N, b) \<Longrightarrow> CPS (M $$ N) = |
76 | "~isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> (N, b) \<Longrightarrow> CPS (M $$ N) = |
73 ccomp (CPS M) (CAbs a (ccomp (CPS N) (CAbs b (CArg (Var a $$ Var b) Hole))))" |
77 ccomp (CPS M) (CAbs a (ccomp (CPS N) (CAbs b (CArg (Var a $$ Var b) Hole))))" |
|
78 using [[simproc del: alpha_lst]] |
74 apply auto |
79 apply auto |
75 defer |
80 defer |
76 apply (case_tac x) |
81 apply (case_tac x) |
77 apply (rule_tac y="a" in lt.exhaust) |
82 apply (rule_tac y="a" in lt.exhaust) |
|
83 using [[simproc del: alpha_lst]] |
78 apply auto |
84 apply auto |
79 apply blast |
85 apply blast |
80 apply (rule_tac x="lt" and ?'a="name" in obtain_fresh) |
86 apply (rule_tac x="lt" and ?'a="name" in obtain_fresh) |
81 apply (simp add: Abs1_eq_iff) |
87 apply (simp add: Abs1_eq_iff) |
82 apply blast+ |
88 apply blast+ |