equal
deleted
inserted
replaced
13 binder |
13 binder |
14 bi::"bp \<Rightarrow> atom set" |
14 bi::"bp \<Rightarrow> atom set" |
15 where |
15 where |
16 "bi (BP x t) = {atom x}" |
16 "bi (BP x t) = {atom x}" |
17 |
17 |
|
18 thm lam_bp_fv |
|
19 thm lam_bp_inject |
|
20 thm lam_bp_bn |
|
21 thm lam_bp_perm |
|
22 thm lam_bp_induct |
|
23 thm lam_bp_distinct |
|
24 |
18 (* compat should be |
25 (* compat should be |
19 compat (BP x t) pi (BP x' t') |
26 compat (BP x t) pi (BP x' t') |
20 \<equiv> alpha_trm t t' \<and> pi o x = x' |
27 \<equiv> alpha_trm t t' \<and> pi o x = x' |
21 *) |
28 *) |
22 |
|
23 typ lam_raw |
|
24 term VAR_raw |
|
25 term APP_raw |
|
26 term LET_raw |
|
27 term Test.BP_raw |
|
28 thm bi_raw.simps |
|
29 thm permute_lam_raw_permute_bp_raw.simps |
|
30 thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros[no_vars] |
|
31 (*thm fv_lam_raw_fv_bp_raw.simps[no_vars]*) |
|
32 |
29 |
33 text {* example 2 *} |
30 text {* example 2 *} |
34 |
31 |
35 nominal_datatype trm' = |
32 nominal_datatype trm' = |
36 Var "name" |
33 Var "name" |
46 where |
43 where |
47 "f PN = {}" |
44 "f PN = {}" |
48 | "f (PD x y) = {atom x, atom y}" |
45 | "f (PD x y) = {atom x, atom y}" |
49 | "f (PS x) = {atom x}" |
46 | "f (PS x) = {atom x}" |
50 |
47 |
|
48 thm trm'_pat'_fv |
|
49 thm trm'_pat'_inject |
|
50 thm trm'_pat'_bn |
|
51 thm trm'_pat'_perm |
|
52 thm trm'_pat'_induct |
|
53 thm trm'_pat'_distinct |
51 |
54 |
52 (* compat should be |
55 (* compat should be |
53 compat (PN) pi (PN) == True |
56 compat (PN) pi (PN) == True |
54 compat (PS x) pi (PS x') == pi o x = x' |
57 compat (PS x) pi (PS x') == pi o x = x' |
55 compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2' |
58 compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2' |
56 *) |
59 *) |
57 |
|
58 |
|
59 thm alpha_trm'_raw_alpha_pat'_raw_alpha_f_raw.intros[no_vars] |
|
60 (*thm fv_trm'_raw_fv_pat'_raw.simps[no_vars]*) |
|
61 thm f_raw.simps |
|
62 (*thm trm'_pat'_induct |
|
63 thm trm'_pat'_perm |
|
64 thm trm'_pat'_fv |
|
65 thm trm'_pat'_bn |
|
66 thm trm'_pat'_inject*) |
|
67 |
60 |
68 nominal_datatype trm0 = |
61 nominal_datatype trm0 = |
69 Var0 "name" |
62 Var0 "name" |
70 | App0 "trm0" "trm0" |
63 | App0 "trm0" "trm0" |
71 | Lam0 x::"name" t::"trm0" bind x in t |
64 | Lam0 x::"name" t::"trm0" bind x in t |
79 where |
72 where |
80 "f0 PN0 = {}" |
73 "f0 PN0 = {}" |
81 | "f0 (PS0 x) = {atom x}" |
74 | "f0 (PS0 x) = {atom x}" |
82 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)" |
75 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)" |
83 |
76 |
84 thm f0_raw.simps |
77 thm trm0_pat0_fv |
85 (*thm trm0_pat0_induct |
78 thm trm0_pat0_inject |
|
79 thm trm0_pat0_bn |
86 thm trm0_pat0_perm |
80 thm trm0_pat0_perm |
87 thm trm0_pat0_fv |
81 thm trm0_pat0_induct |
88 thm trm0_pat0_bn*) |
82 thm trm0_pat0_distinct |
89 |
83 |
90 text {* example type schemes *} |
84 text {* example type schemes *} |
91 |
85 |
92 nominal_datatype t = |
86 nominal_datatype t = |
93 VarTS "name" |
87 VarTS "name" |
94 | FunTS "t" "t" |
88 | FunTS "t" "t" |
95 and tyS = |
89 and tyS = |
96 All xs::"name set" ty::"t" bind xs in ty |
90 All xs::"name set" ty::"t" bind xs in ty |
|
91 |
|
92 thm t_tyS_fv |
|
93 thm t_tyS_inject |
|
94 thm t_tyS_bn |
|
95 thm t_tyS_perm |
|
96 thm t_tyS_induct |
|
97 thm t_tyS_distinct |
97 |
98 |
98 (* example 1 from Terms.thy *) |
99 (* example 1 from Terms.thy *) |
99 |
100 |
100 nominal_datatype trm1 = |
101 nominal_datatype trm1 = |
101 Vr1 "name" |
102 Vr1 "name" |
111 where |
112 where |
112 "bv1 (BUnit1) = {}" |
113 "bv1 (BUnit1) = {}" |
113 | "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
114 | "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
114 | "bv1 (BV1 x) = {atom x}" |
115 | "bv1 (BV1 x) = {atom x}" |
115 |
116 |
116 |
117 thm trm1_bp1_fv |
117 thm bv1_raw.simps |
118 thm trm1_bp1_inject |
|
119 thm trm1_bp1_bn |
|
120 thm trm1_bp1_perm |
|
121 thm trm1_bp1_induct |
|
122 thm trm1_bp1_distinct |
118 |
123 |
119 text {* example 3 from Terms.thy *} |
124 text {* example 3 from Terms.thy *} |
120 |
125 |
121 nominal_datatype trm3 = |
126 nominal_datatype trm3 = |
122 Vr3 "name" |
127 Vr3 "name" |
130 bv3 |
135 bv3 |
131 where |
136 where |
132 "bv3 ANil = {}" |
137 "bv3 ANil = {}" |
133 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
138 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
134 |
139 |
|
140 thm trm3_rassigns3_fv |
|
141 thm trm3_rassigns3_inject |
|
142 thm trm3_rassigns3_bn |
|
143 thm trm3_rassigns3_perm |
|
144 thm trm3_rassigns3_induct |
|
145 thm trm3_rassigns3_distinct |
135 |
146 |
136 (* compat should be |
147 (* compat should be |
137 compat (ANil) pi (PNil) \<equiv> TRue |
148 compat (ANil) pi (PNil) \<equiv> TRue |
138 compat (ACons x t ts) pi (ACons x' t' ts') \<equiv> pi o x = x' \<and> alpha t t' \<and> compat ts pi ts' |
149 compat (ACons x t ts) pi (ACons x' t' ts') \<equiv> pi o x = x' \<and> alpha t t' \<and> compat ts pi ts' |
139 *) |
150 *) |
150 binder |
161 binder |
151 bv5 |
162 bv5 |
152 where |
163 where |
153 "bv5 Lnil = {}" |
164 "bv5 Lnil = {}" |
154 | "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)" |
165 | "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)" |
|
166 |
|
167 thm trm5_lts_fv |
|
168 thm trm5_lts_inject |
|
169 thm trm5_lts_bn |
|
170 thm trm5_lts_perm |
|
171 thm trm5_lts_induct |
|
172 thm trm5_lts_distinct |
155 |
173 |
156 (* example from my PHD *) |
174 (* example from my PHD *) |
157 |
175 |
158 atom_decl coname |
176 atom_decl coname |
159 |
177 |
164 | AndL1 n::"name" t::"phd" "name" bind n in t |
182 | AndL1 n::"name" t::"phd" "name" bind n in t |
165 | AndL2 n::"name" t::"phd" "name" bind n in t |
183 | AndL2 n::"name" t::"phd" "name" bind n in t |
166 | ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2 |
184 | ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2 |
167 | ImpR c::"coname" n::"name" t::"phd" "coname" bind n in t, bind c in t |
185 | ImpR c::"coname" n::"name" t::"phd" "coname" bind n in t, bind c in t |
168 |
186 |
169 thm alpha_phd_raw.intros[no_vars] |
187 thm phd_fv |
170 thm fv_phd_raw.simps[no_vars] |
188 thm phd_inject |
171 |
189 thm phd_bn |
|
190 thm phd_perm |
|
191 thm phd_induct |
|
192 thm phd_distinct |
172 |
193 |
173 (* example form Leroy 96 about modules; OTT *) |
194 (* example form Leroy 96 about modules; OTT *) |
174 |
195 |
175 nominal_datatype mexp = |
196 nominal_datatype mexp = |
176 Acc "path" |
197 Acc "path" |
221 | "Cbinders (Type1 t) = {atom t}" |
242 | "Cbinders (Type1 t) = {atom t}" |
222 | "Cbinders (Type2 t T) = {atom t}" |
243 | "Cbinders (Type2 t T) = {atom t}" |
223 | "Cbinders (SStru x S) = {atom x}" |
244 | "Cbinders (SStru x S) = {atom x}" |
224 | "Cbinders (SVal v T) = {atom v}" |
245 | "Cbinders (SVal v T) = {atom v}" |
225 |
246 |
|
247 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_fv |
|
248 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_inject |
|
249 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_bn |
|
250 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_perm |
|
251 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_induct |
|
252 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_distinct |
226 |
253 |
227 (* example 3 from Peter Sewell's bestiary *) |
254 (* example 3 from Peter Sewell's bestiary *) |
|
255 |
228 nominal_datatype exp = |
256 nominal_datatype exp = |
229 VarP "name" |
257 VarP "name" |
230 | AppP "exp" "exp" |
258 | AppP "exp" "exp" |
231 | LamP x::"name" e::"exp" bind x in e |
259 | LamP x::"name" e::"exp" bind x in e |
232 | LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp' p" in e1 |
260 | LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp' p" in e1 |
238 bp' :: "pat3 \<Rightarrow> atom set" |
266 bp' :: "pat3 \<Rightarrow> atom set" |
239 where |
267 where |
240 "bp' (PVar x) = {atom x}" |
268 "bp' (PVar x) = {atom x}" |
241 | "bp' (PUnit) = {}" |
269 | "bp' (PUnit) = {}" |
242 | "bp' (PPair p1 p2) = bp' p1 \<union> bp' p2" |
270 | "bp' (PPair p1 p2) = bp' p1 \<union> bp' p2" |
243 thm alpha_exp_raw_alpha_pat3_raw_alpha_bp'_raw.intros |
271 |
|
272 thm exp_pat3_fv |
|
273 thm exp_pat3_inject |
|
274 thm exp_pat3_bn |
|
275 thm exp_pat3_perm |
|
276 thm exp_pat3_induct |
|
277 thm exp_pat3_distinct |
244 |
278 |
245 (* example 6 from Peter Sewell's bestiary *) |
279 (* example 6 from Peter Sewell's bestiary *) |
246 nominal_datatype exp6 = |
280 nominal_datatype exp6 = |
247 EVar name |
281 EVar name |
248 | EPair exp6 exp6 |
282 | EPair exp6 exp6 |
255 bp6 :: "pat6 \<Rightarrow> atom set" |
289 bp6 :: "pat6 \<Rightarrow> atom set" |
256 where |
290 where |
257 "bp6 (PVar' x) = {atom x}" |
291 "bp6 (PVar' x) = {atom x}" |
258 | "bp6 (PUnit') = {}" |
292 | "bp6 (PUnit') = {}" |
259 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2" |
293 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2" |
260 thm alpha_exp6_raw_alpha_pat6_raw_alpha_bp6_raw.intros |
294 |
|
295 thm exp6_pat6_fv |
|
296 thm exp6_pat6_inject |
|
297 thm exp6_pat6_bn |
|
298 thm exp6_pat6_perm |
|
299 thm exp6_pat6_induct |
|
300 thm exp6_pat6_distinct |
261 |
301 |
262 (* THE REST ARE NOT SUPPOSED TO WORK YET *) |
302 (* THE REST ARE NOT SUPPOSED TO WORK YET *) |
263 |
303 |
264 (* example 7 from Peter Sewell's bestiary *) |
304 (* example 7 from Peter Sewell's bestiary *) |
265 nominal_datatype exp7 = |
305 nominal_datatype exp7 = |