24 thm lam_bp_induct |
24 thm lam_bp_induct |
25 thm lam_bp_distinct |
25 thm lam_bp_distinct |
26 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} |
26 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} |
27 |
27 |
28 term "supp (x :: lam)" |
28 term "supp (x :: lam)" |
29 |
29 lemmas lam_bp_inducts = lam_raw_bp_raw.inducts[quot_lifted] |
30 (* compat should be |
30 |
31 compat (BP x t) pi (BP x' t') |
31 lemma infinite_Un: |
32 \<equiv> alpha_trm t t' \<and> pi o x = x' |
32 shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T" |
33 *) |
33 apply(auto) |
|
34 done |
|
35 |
|
36 lemma bi_eqvt: |
|
37 shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)" |
|
38 sorry |
|
39 |
|
40 lemma supp_fv: |
|
41 "supp t = fv_lam t" and |
|
42 "supp b = fv_bp b" |
|
43 apply(induct t and b rule: lam_bp_inducts) |
|
44 apply(simp_all add: lam_bp_fv) |
|
45 (* VAR case *) |
|
46 apply(simp only: supp_def) |
|
47 apply(simp only: lam_bp_perm) |
|
48 apply(simp only: lam_bp_inject) |
|
49 apply(simp only: supp_def[symmetric]) |
|
50 apply(simp only: supp_at_base) |
|
51 (* APP case *) |
|
52 apply(simp only: supp_def) |
|
53 apply(simp only: lam_bp_perm) |
|
54 apply(simp only: lam_bp_inject) |
|
55 apply(simp only: de_Morgan_conj) |
|
56 apply(simp only: Collect_disj_eq) |
|
57 apply(simp only: infinite_Un) |
|
58 apply(simp only: Collect_disj_eq) |
|
59 (* LET case *) |
|
60 defer |
|
61 (* BP case *) |
|
62 apply(simp only: supp_def) |
|
63 apply(simp only: lam_bp_perm) |
|
64 apply(simp only: lam_bp_inject) |
|
65 apply(simp only: de_Morgan_conj) |
|
66 apply(simp only: Collect_disj_eq) |
|
67 apply(simp only: infinite_Un) |
|
68 apply(simp only: Collect_disj_eq) |
|
69 apply(simp only: supp_def[symmetric]) |
|
70 apply(simp only: supp_at_base) |
|
71 apply(simp) |
|
72 (* LET case *) |
|
73 apply(simp only: supp_def) |
|
74 apply(simp only: lam_bp_perm) |
|
75 apply(simp only: lam_bp_inject) |
|
76 apply(simp only: alpha_gen) |
|
77 |
|
78 thm alpha_gen |
|
79 thm lam_bp_fv |
|
80 thm lam_bp_inject |
|
81 oops |
|
82 |
|
83 |
34 |
84 |
35 text {* example 2 *} |
85 text {* example 2 *} |
36 |
86 |
37 nominal_datatype trm' = |
87 nominal_datatype trm' = |
38 Var "name" |
88 Var "name" |