8 |
8 |
9 ML {* val _ = cheat_alpha_eqvt := false *} |
9 ML {* val _ = cheat_alpha_eqvt := false *} |
10 ML {* val _ = cheat_fv_eqvt := false *} |
10 ML {* val _ = cheat_fv_eqvt := false *} |
11 ML {* val _ = recursive := false *} |
11 ML {* val _ = recursive := false *} |
12 |
12 |
13 (* |
|
14 nominal_datatype lam = |
13 nominal_datatype lam = |
15 VAR "name" |
14 VAR "name" |
16 | APP "lam" "lam" |
15 | APP "lam" "lam" |
17 | LAM x::"name" t::"lam" bind x in t |
16 | LAM x::"name" t::"lam" bind x in t |
18 | LET bp::"bp" t::"lam" bind "bi bp" in t |
17 | LET bp::"bp" t::"lam" bind "bi bp" in t |
54 |
40 |
55 lemma bi_eqvt: |
41 lemma bi_eqvt: |
56 shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)" |
42 shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)" |
57 by (rule eqvts) |
43 by (rule eqvts) |
58 |
44 |
59 term alpha_bi |
|
60 |
|
61 lemma alpha_bi: |
|
62 shows "alpha_bi b b' = True" |
|
63 apply(induct b rule: lam_bp_inducts(2)) |
|
64 apply(simp_all) |
|
65 apply(induct b' rule: lam_bp_inducts(2)) |
|
66 apply (simp_all add: lam_bp_inject) |
|
67 done |
|
68 |
|
69 lemma fv_bi: |
|
70 shows "fv_bi b = {}" |
|
71 apply(induct b rule: lam_bp_inducts(2)) |
|
72 apply(auto)[1] |
|
73 apply(simp_all) |
|
74 apply(simp add: lam_bp_fv) |
|
75 done |
|
76 |
|
77 lemma supp_fv: |
45 lemma supp_fv: |
78 "supp t = fv_lam t" and |
46 "supp t = fv_lam t" and |
79 "supp b = fv_bp b" |
47 "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}" |
80 apply(induct t and b rule: lam_bp_inducts) |
48 apply(induct t and bp rule: lam_bp_inducts) |
81 apply(simp_all add: lam_bp_fv) |
49 apply(simp_all add: lam_bp_fv) |
82 (* VAR case *) |
50 (* VAR case *) |
83 apply(simp only: supp_def) |
51 apply(simp only: supp_def) |
84 apply(simp only: lam_bp_perm) |
52 apply(simp only: lam_bp_perm) |
85 apply(simp only: lam_bp_inject) |
53 apply(simp only: lam_bp_inject) |
109 defer |
77 defer |
110 (* BP case *) |
78 (* BP case *) |
111 apply(simp only: supp_def) |
79 apply(simp only: supp_def) |
112 apply(simp only: lam_bp_perm) |
80 apply(simp only: lam_bp_perm) |
113 apply(simp only: lam_bp_inject) |
81 apply(simp only: lam_bp_inject) |
114 (* |
|
115 apply(simp only: de_Morgan_conj) |
82 apply(simp only: de_Morgan_conj) |
116 apply(simp only: Collect_disj_eq) |
83 apply(simp only: Collect_disj_eq) |
117 apply(simp only: infinite_Un) |
84 apply(simp only: infinite_Un) |
118 apply(simp only: Collect_disj_eq) |
85 apply(simp only: Collect_disj_eq) |
119 *) |
|
120 apply(simp only: supp_def[symmetric]) |
86 apply(simp only: supp_def[symmetric]) |
121 apply(simp only: supp_at_base) |
87 apply(simp only: supp_at_base) |
122 (*apply(simp)*) |
88 apply(simp) |
123 (* LET case *) |
89 (* LET case *) |
124 apply(rule_tac t="supp (LET bp_raw lam_raw)" and s="supp (Abs_tst bi bp_raw lam_raw)" in subst) |
90 apply(rule_tac t="supp (LET bp_raw lam_raw)" and s="supp (Abs (bi bp_raw) lam_raw) \<union> fv_bi bp_raw" in subst) |
125 apply(simp (no_asm) only: supp_def) |
91 apply(simp (no_asm) only: supp_def) |
126 apply(simp only: lam_bp_perm) |
92 apply(simp only: lam_bp_perm) |
127 apply(simp only: permute_ABS_tst) |
93 apply(simp only: permute_ABS) |
128 apply(simp only: lam_bp_inject) |
94 apply(simp only: lam_bp_inject) |
129 apply(simp only: eqvts_raw) |
95 apply(simp only: eqvts) |
130 apply(simp only: Abs_tst_eq_iff) |
96 apply(simp only: Abs_eq_iff) |
131 apply(simp only: alpha_bi) |
97 apply(simp only: ex_simps) |
|
98 apply(simp only: de_Morgan_conj) |
|
99 apply(simp only: Collect_disj_eq) |
|
100 apply(simp only: infinite_Un) |
|
101 apply(simp only: Collect_disj_eq) |
132 apply(simp only: alpha_gen) |
102 apply(simp only: alpha_gen) |
133 apply(simp only: alpha_tst) |
|
134 apply(simp only: supp_eqvt[symmetric]) |
103 apply(simp only: supp_eqvt[symmetric]) |
135 apply(simp only: eqvts) |
104 apply(simp only: eqvts) |
136 apply simp |
105 apply(blast) |
137 apply(simp add: supp_Abs_tst) |
106 apply(simp add: supp_Abs) |
138 apply(simp add: fv_bi) |
107 apply(blast) |
139 done |
108 done |
140 |
109 |
141 text {* example 2 *} |
110 text {* example 2 *} |
142 |
111 |
143 nominal_datatype trm' = |
112 nominal_datatype trm' = |