equal
deleted
inserted
replaced
193 done |
193 done |
194 |
194 |
195 lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}" |
195 lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}" |
196 by (simp add: Collect_imp_eq Collect_neg_eq[symmetric]) |
196 by (simp add: Collect_imp_eq Collect_neg_eq[symmetric]) |
197 |
197 |
198 lemma inf_or: "(infinite x \<or> infinite y) = infinite (x \<union> y)" |
|
199 by (simp add: finite_Un) |
|
200 |
|
201 lemma supp_fv_let: |
198 lemma supp_fv_let: |
202 assumes sa : "fv_bp bp = supp bp" |
199 assumes sa : "fv_bp bp = supp bp" |
203 shows "\<lbrakk>fv_trm1 ta = supp ta; fv_trm1 tb = supp tb; fv_bp bp = supp bp\<rbrakk> |
200 shows "\<lbrakk>fv_trm1 ta = supp ta; fv_trm1 tb = supp tb; fv_bp bp = supp bp\<rbrakk> |
204 \<Longrightarrow> supp (Lt1 bp ta tb) = supp ta \<union> (supp (bp, tb) - supp bp)" |
201 \<Longrightarrow> supp (Lt1 bp ta tb) = supp ta \<union> (supp (bp, tb) - supp bp)" |
205 apply(fold supp_Abs) |
202 apply(fold supp_Abs) |
210 apply(simp only: ex_out) |
207 apply(simp only: ex_out) |
211 apply(simp only: Collect_neg_conj) |
208 apply(simp only: Collect_neg_conj) |
212 apply(simp only: permute_ABS) |
209 apply(simp only: permute_ABS) |
213 apply(simp only: Abs_eq_iff) |
210 apply(simp only: Abs_eq_iff) |
214 apply(simp only: alpha_gen supp_Pair split_conv eqvts) |
211 apply(simp only: alpha_gen supp_Pair split_conv eqvts) |
215 apply(simp only: inf_or[symmetric]) |
212 apply(simp only: infinite_Un) |
216 apply(simp only: Collect_disj_eq) |
213 apply(simp only: Collect_disj_eq) |
217 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) |
214 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) |
218 apply (simp only: eqvts[symmetric] fv_trm1_eqvt[symmetric]) |
215 apply (simp only: eqvts[symmetric] fv_trm1_eqvt[symmetric]) |
219 apply (simp only: eqvts Pair_eq) |
216 apply (simp only: eqvts Pair_eq) |
220 done |
217 done |