src/HOL/Fun.thy
 changeset 46420 92b629f568c4 parent 46419 e139d0e29ca1 child 46586 abbec6fa25c8
```     1.1 --- a/src/HOL/Fun.thy	Sun Feb 05 08:36:41 2012 +0100
1.2 +++ b/src/HOL/Fun.thy	Sun Feb 05 08:47:13 2012 +0100
1.3 @@ -427,28 +427,6 @@
1.4    using * by blast
1.5  qed
1.6
1.7 -(* FIXME: bij_betw_Disj_Un is special case of bij_betw_combine -- should be removed *)
1.8 -lemma bij_betw_Disj_Un:
1.9 -  assumes DISJ: "A \<inter> B = {}" and DISJ': "A' \<inter> B' = {}" and
1.10 -          B1: "bij_betw f A A'" and B2: "bij_betw f B B'"
1.11 -  shows "bij_betw f (A \<union> B) (A' \<union> B')"
1.12 -proof-
1.13 -  have 1: "inj_on f A \<and> inj_on f B"
1.14 -  using B1 B2 by (auto simp add: bij_betw_def)
1.15 -  have 2: "f`A = A' \<and> f`B = B'"
1.16 -  using B1 B2 by (auto simp add: bij_betw_def)
1.17 -  hence "f`(A - B) \<inter> f`(B - A) = {}"
1.18 -  using DISJ DISJ' by blast
1.19 -  hence "inj_on f (A \<union> B)"
1.20 -  using 1 by (auto simp add: inj_on_Un)
1.21 -  (*  *)
1.22 -  moreover
1.23 -  have "f`(A \<union> B) = A' \<union> B'"
1.24 -  using 2 by auto
1.25 -  ultimately show ?thesis
1.26 -  unfolding bij_betw_def by auto
1.27 -qed
1.28 -
1.29  lemma bij_betw_subset:
1.30    assumes BIJ: "bij_betw f A A'" and
1.31            SUB: "B \<le> A" and IM: "f ` B = B'"
```