4 |
4 |
5 text {* example 1, equivalent to example 2 from Terms *} |
5 text {* example 1, equivalent to example 2 from Terms *} |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
|
9 (* |
9 nominal_datatype lam = |
10 nominal_datatype lam = |
10 VAR "name" |
11 VAR "name" |
11 | APP "lam" "lam" |
12 | APP "lam" "lam" |
|
13 | LAM x::"name" t::"lam" bind x in t |
12 | LET bp::"bp" t::"lam" bind "bi bp" in t |
14 | LET bp::"bp" t::"lam" bind "bi bp" in t |
13 and bp = |
15 and bp = |
14 BP "name" "lam" |
16 BP "name" "lam" |
15 binder |
17 binder |
16 bi::"bp \<Rightarrow> atom set" |
18 bi::"bp \<Rightarrow> atom set" |
17 where |
19 where |
18 "bi (BP x t) = {atom x}" |
20 "bi (BP x t) = {atom x}" |
|
21 *) |
|
22 |
|
23 nominal_datatype lam = |
|
24 VAR "name" |
|
25 | APP "lam" "lam" |
|
26 | LAM x::"name" t::"lam" bind x in t |
|
27 | LET bp::"bp" t::"lam" bind "bi bp" in t |
|
28 and bp = |
|
29 BP "name" |
|
30 binder |
|
31 bi::"bp \<Rightarrow> atom set" |
|
32 where |
|
33 "bi (BP x) = {atom x}" |
19 |
34 |
20 thm lam_bp_fv |
35 thm lam_bp_fv |
21 thm lam_bp_inject |
36 thm lam_bp_inject |
22 thm lam_bp_bn |
37 thm lam_bp_bn |
23 thm lam_bp_perm |
38 thm lam_bp_perm |
60 apply(simp only: lam_bp_inject) |
90 apply(simp only: lam_bp_inject) |
61 apply(simp only: de_Morgan_conj) |
91 apply(simp only: de_Morgan_conj) |
62 apply(simp only: Collect_disj_eq) |
92 apply(simp only: Collect_disj_eq) |
63 apply(simp only: infinite_Un) |
93 apply(simp only: infinite_Un) |
64 apply(simp only: Collect_disj_eq) |
94 apply(simp only: Collect_disj_eq) |
|
95 (* LAM case *) |
|
96 apply(rule_tac t="supp (LAM name lam_raw)" and s="supp (Abs {atom name} lam_raw)" in subst) |
|
97 apply(simp (no_asm) only: supp_def) |
|
98 apply(simp only: lam_bp_perm) |
|
99 apply(simp only: permute_ABS) |
|
100 apply(simp only: lam_bp_inject) |
|
101 apply(simp only: Abs_eq_iff) |
|
102 apply(simp only: insert_eqvt atom_eqvt empty_eqvt) |
|
103 apply(simp only: alpha_gen) |
|
104 apply(simp only: supp_eqvt[symmetric]) |
|
105 apply(simp only: eqvts) |
|
106 apply(simp only: supp_Abs) |
65 (* LET case *) |
107 (* LET case *) |
66 defer |
108 defer |
67 (* BP case *) |
109 (* BP case *) |
68 apply(simp only: supp_def) |
110 apply(simp only: supp_def) |
69 apply(simp only: lam_bp_perm) |
111 apply(simp only: lam_bp_perm) |
70 apply(simp only: lam_bp_inject) |
112 apply(simp only: lam_bp_inject) |
|
113 (* |
71 apply(simp only: de_Morgan_conj) |
114 apply(simp only: de_Morgan_conj) |
72 apply(simp only: Collect_disj_eq) |
115 apply(simp only: Collect_disj_eq) |
73 apply(simp only: infinite_Un) |
116 apply(simp only: infinite_Un) |
74 apply(simp only: Collect_disj_eq) |
117 apply(simp only: Collect_disj_eq) |
|
118 *) |
75 apply(simp only: supp_def[symmetric]) |
119 apply(simp only: supp_def[symmetric]) |
76 apply(simp only: supp_at_base) |
120 apply(simp only: supp_at_base) |
|
121 (*apply(simp)*) |
|
122 (* LET case *) |
|
123 apply(rule_tac t="supp (LET bp_raw lam_raw)" and s="supp (Abs_tst bi bp_raw lam_raw)" in subst) |
|
124 apply(simp (no_asm) only: supp_def) |
|
125 apply(simp only: lam_bp_perm) |
|
126 apply(simp only: permute_ABS_tst) |
|
127 apply(simp only: lam_bp_inject) |
|
128 apply(simp only: eqvts_raw) |
|
129 apply(simp only: Abs_tst_eq_iff) |
|
130 apply(simp only: alpha_bi) |
|
131 apply(simp only: alpha_gen) |
|
132 apply(simp only: alpha_tst) |
|
133 apply(simp only: supp_eqvt[symmetric]) |
|
134 apply(simp only: eqvts) |
|
135 defer (* hacking *) |
|
136 apply(simp add: supp_Abs_tst) |
|
137 apply(simp add: fv_bi) |
|
138 apply(rule Collect_cong) |
|
139 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
77 apply(simp) |
140 apply(simp) |
78 (* LET case *) |
141 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
79 apply(simp only: supp_def) |
142 apply(simp) |
80 apply(simp only: lam_bp_perm) |
143 apply(rule Collect_cong) |
81 apply(simp only: lam_bp_inject) |
144 apply(blast) |
82 apply(simp only: alpha_gen) |
145 done |
83 |
|
84 thm alpha_gen |
|
85 thm lam_bp_fv |
|
86 thm lam_bp_inject |
|
87 oops |
|
88 |
|
89 |
|
90 |
146 |
91 text {* example 2 *} |
147 text {* example 2 *} |
92 |
148 |
93 nominal_datatype trm' = |
149 nominal_datatype trm' = |
94 Var "name" |
150 Var "name" |