equal
deleted
inserted
replaced
129 thm lam'_bp'_induct |
129 thm lam'_bp'_induct |
130 thm lam'_bp'_inducts |
130 thm lam'_bp'_inducts |
131 thm lam'_bp'_distinct |
131 thm lam'_bp'_distinct |
132 ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *} |
132 ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *} |
133 |
133 |
134 lemma supp_fv: |
134 lemma supp_fv': |
135 shows "supp t = fv_lam' t" |
135 shows "supp t = fv_lam' t" |
136 and "supp bp = fv_bp' bp" |
136 and "supp bp = fv_bp' bp" |
137 apply(induct t and bp rule: lam'_bp'_inducts) |
137 apply(induct t and bp rule: lam'_bp'_inducts) |
138 apply(simp_all add: lam'_bp'_fv) |
138 apply(simp_all add: lam'_bp'_fv) |
139 (* VAR case *) |
139 (* VAR case *) |
172 apply(simp only: Abs_eq_iff) |
172 apply(simp only: Abs_eq_iff) |
173 apply(simp only: alpha_gen) |
173 apply(simp only: alpha_gen) |
174 apply(simp only: eqvts split_def fst_conv snd_conv) |
174 apply(simp only: eqvts split_def fst_conv snd_conv) |
175 apply(simp only: eqvts[symmetric] supp_Pair) |
175 apply(simp only: eqvts[symmetric] supp_Pair) |
176 apply(simp only: eqvts Pair_eq) |
176 apply(simp only: eqvts Pair_eq) |
177 oops |
177 apply(simp add: supp_Abs supp_Pair) |
178 |
178 apply blast |
179 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]] |
179 apply(simp only: supp_def) |
|
180 apply(simp only: lam'_bp'_perm) |
|
181 apply(simp only: lam'_bp'_inject) |
|
182 apply(simp only: de_Morgan_conj) |
|
183 apply(simp only: Collect_disj_eq) |
|
184 apply(simp only: infinite_Un) |
|
185 apply(simp only: Collect_disj_eq) |
|
186 apply(simp only: supp_def[symmetric]) |
|
187 apply(simp only: supp_at_base supp_atom) |
|
188 apply simp |
|
189 done |
|
190 |
|
191 thm lam'_bp'_fv[simplified supp_fv'[symmetric]] |
180 |
192 |
181 |
193 |
182 text {* example 2 *} |
194 text {* example 2 *} |
183 |
195 |
184 ML {* val _ = recursive := false *} |
196 ML {* val _ = recursive := false *} |