equal
deleted
inserted
replaced
27 BP "name" "lam" |
27 BP "name" "lam" |
28 binder |
28 binder |
29 bi::"bp \<Rightarrow> atom set" |
29 bi::"bp \<Rightarrow> atom set" |
30 where |
30 where |
31 "bi (BP x t) = {atom x}" |
31 "bi (BP x t) = {atom x}" |
|
32 |
|
33 (* compat should be |
|
34 compat (BP x t) pi (BP x' t') |
|
35 \<equiv> alpha_trm t t' \<and> pi o x = x' |
|
36 *) |
32 |
37 |
33 typ lam_raw |
38 typ lam_raw |
34 term VAR_raw |
39 term VAR_raw |
35 term APP_raw |
40 term APP_raw |
36 term LET_raw |
41 term LET_raw |
62 where |
67 where |
63 "f PN = {}" |
68 "f PN = {}" |
64 | "f (PS x) = {atom x}" |
69 | "f (PS x) = {atom x}" |
65 | "f (PD x y) = {atom x, atom y}" |
70 | "f (PD x y) = {atom x, atom y}" |
66 |
71 |
|
72 (* compat should be |
|
73 compat (PN) pi (PN) \<equiv> TRue |
|
74 compat (PS x) pi (PS x') \<equiv> pi o x = x' |
|
75 compat (PD p1 p2) pi (PD p1' p2') \<equiv> compat p1 pi p1' \<and> compat p2 pi p2' |
|
76 *) |
|
77 |
67 |
78 |
68 thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars] |
79 thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars] |
69 thm fv_trm'_raw_fv_pat'_raw.simps[no_vars] |
80 thm fv_trm'_raw_fv_pat'_raw.simps[no_vars] |
70 thm f_raw.simps |
81 thm f_raw.simps |
71 (*thm trm'_pat'_induct |
82 (*thm trm'_pat'_induct |
146 binder |
157 binder |
147 bv2 |
158 bv2 |
148 where |
159 where |
149 "bv2 (As x t) = {atom x}" |
160 "bv2 (As x t) = {atom x}" |
150 |
161 |
151 (* example 3 from Terms.thy *) |
162 (* compat should be |
|
163 compat (As x t) pi (As x' t') \<equiv> pi o x = x' \<and> alpha t t' |
|
164 *) |
|
165 |
|
166 |
|
167 thm fv_trm2_raw_fv_assign_raw.simps[no_vars] |
|
168 thm alpha_trm2_raw_alpha_assign_raw.intros[no_vars] |
|
169 |
|
170 |
|
171 |
|
172 text {* example 3 from Terms.thy *} |
152 |
173 |
153 nominal_datatype trm3 = |
174 nominal_datatype trm3 = |
154 Vr3 "name" |
175 Vr3 "name" |
155 | Ap3 "trm3" "trm3" |
176 | Ap3 "trm3" "trm3" |
156 | Lm3 x::"name" t::"trm3" bind x in t |
177 | Lm3 x::"name" t::"trm3" bind x in t |
161 binder |
182 binder |
162 bv3 |
183 bv3 |
163 where |
184 where |
164 "bv3 ANil = {}" |
185 "bv3 ANil = {}" |
165 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
186 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
|
187 |
|
188 |
|
189 (* compat should be |
|
190 compat (ANil) pi (PNil) \<equiv> TRue |
|
191 compat (ACons x t ts) pi (ACons x' t' ts') \<equiv> pi o x = x' \<and> alpha t t' \<and> compat ts pi ts' |
|
192 *) |
166 |
193 |
167 (* example 4 from Terms.thy *) |
194 (* example 4 from Terms.thy *) |
168 |
195 |
169 (* fv_eqvt does not work, we need to repaire defined permute functions |
196 (* fv_eqvt does not work, we need to repaire defined permute functions |
170 defined fv and defined alpha... *) |
197 defined fv and defined alpha... *) |