equal
deleted
inserted
replaced
3 begin |
3 begin |
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 |
|
9 ML {* val cheat_alpha_eqvt = ref false *} |
|
10 ML {* val cheat_fv_eqvt = ref false *} |
8 |
11 |
9 (* |
12 (* |
10 nominal_datatype lam = |
13 nominal_datatype lam = |
11 VAR "name" |
14 VAR "name" |
12 | APP "lam" "lam" |
15 | APP "lam" "lam" |
35 thm lam_bp_fv |
38 thm lam_bp_fv |
36 thm lam_bp_inject |
39 thm lam_bp_inject |
37 thm lam_bp_bn |
40 thm lam_bp_bn |
38 thm lam_bp_perm |
41 thm lam_bp_perm |
39 thm lam_bp_induct |
42 thm lam_bp_induct |
|
43 thm lam_bp_inducts |
40 thm lam_bp_distinct |
44 thm lam_bp_distinct |
41 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} |
45 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} |
42 |
46 |
43 term "supp (x :: lam)" |
47 term "supp (x :: lam)" |
44 lemmas lam_bp_inducts = lam_raw_bp_raw.inducts[quot_lifted] |
|
45 |
48 |
46 (* maybe should be added to Infinite.thy *) |
49 (* maybe should be added to Infinite.thy *) |
47 lemma infinite_Un: |
50 lemma infinite_Un: |
48 shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T" |
51 shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T" |
49 by simp |
52 by simp |
50 |
53 |
51 lemma bi_eqvt: |
54 lemma bi_eqvt: |
52 shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)" |
55 shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)" |
53 apply(induct b rule: lam_bp_inducts(2)) |
56 by (rule eqvts) |
54 apply(simp) |
|
55 apply(simp) |
|
56 apply(simp) |
|
57 apply(simp add: lam_bp_bn lam_bp_perm) |
|
58 apply(simp add: eqvts) |
|
59 done |
|
60 |
57 |
61 term alpha_bi |
58 term alpha_bi |
62 |
59 |
63 lemma alpha_bi: |
60 lemma alpha_bi: |
64 shows "alpha_bi pi b b' = True" |
61 shows "alpha_bi pi b b' = True" |
364 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_fv |
361 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_fv |
365 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_inject |
362 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_inject |
366 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_bn |
363 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_bn |
367 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_perm |
364 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_perm |
368 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_induct |
365 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_induct |
|
366 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_inducts |
369 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_distinct |
367 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_distinct |
370 |
368 |
371 (* example 3 from Peter Sewell's bestiary *) |
369 (* example 3 from Peter Sewell's bestiary *) |
372 |
370 |
373 nominal_datatype exp = |
371 nominal_datatype exp = |