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'"