294 |
294 |
295 (* nominal_datatype2 does the following things in order: |
295 (* nominal_datatype2 does the following things in order: |
296 |
296 |
297 Parser.thy/raw_nominal_decls |
297 Parser.thy/raw_nominal_decls |
298 1) define the raw datatype |
298 1) define the raw datatype |
299 2) define the raw binding functions |
299 2) define the raw binding functions |
|
300 |
300 Perm.thy/define_raw_perms |
301 Perm.thy/define_raw_perms |
301 3) define permutations of the raw datatype and show that raw type is in the pt typeclass |
302 3) define permutations of the raw datatype and show that the raw type is |
|
303 in the pt typeclass |
|
304 |
302 Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha |
305 Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha |
303 4) define fv and fv_bn |
306 4) define fv and fv_bn |
304 5) define alpha and alpha_bn |
307 5) define alpha and alpha_bn |
|
308 |
305 Perm.thy/distinct_rel |
309 Perm.thy/distinct_rel |
306 6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...) (Proof by cases; simp) |
310 6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...) (Proof by cases; simp) |
|
311 |
307 Tacs.thy/build_rel_inj |
312 Tacs.thy/build_rel_inj |
308 6) prove alpha_eq_iff (C1 x = C2 y \<leftrightarrow> P x y ...) |
313 6) prove alpha_eq_iff (C1 x = C2 y \<leftrightarrow> P x y ...) |
309 (left-to-right by intro rule, right-to-left by cases; simp) |
314 (left-to-right by intro rule, right-to-left by cases; simp) |
310 Equivp.thy/prove_eqvt |
315 Equivp.thy/prove_eqvt |
311 7) prove bn_eqvt (common induction on the raw datatype) |
316 7) prove bn_eqvt (common induction on the raw datatype) |