simplified proof, moved lemma, added lemma
authornipkow
Mon Nov 05 10:02:21 2018 +0100 (6 months ago)
changeset 692350e156963b636
parent 69234 2dec32c7313f
child 69236 a75aab6d785b
simplified proof, moved lemma, added lemma
src/HOL/Finite_Set.thy
src/HOL/Set_Interval.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Sun Nov 04 17:19:56 2018 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Mon Nov 05 10:02:21 2018 +0100
     1.3 @@ -1872,6 +1872,10 @@
     1.4      using assms by (force intro: card_mono simp: card_image [symmetric])
     1.5  qed
     1.6  
     1.7 +lemma inj_on_iff_card_le:
     1.8 +  "\<lbrakk> finite A; finite B \<rbrakk> \<Longrightarrow> (\<exists>f. inj_on f A \<and> f ` A \<le> B) = (card A \<le> card B)"
     1.9 +using card_inj_on_le[of _ A B] card_le_inj[of A B] by blast
    1.10 +
    1.11  lemma surj_card_le: "finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> card B \<le> card A"
    1.12    by (blast intro: card_image_le card_mono le_trans)
    1.13  
     2.1 --- a/src/HOL/Set_Interval.thy	Sun Nov 04 17:19:56 2018 +0100
     2.2 +++ b/src/HOL/Set_Interval.thy	Mon Nov 05 10:02:21 2018 +0100
     2.3 @@ -1345,25 +1345,6 @@
     2.4    thus "(\<exists>f. bij_betw f A B)" by blast
     2.5  qed (auto simp: bij_betw_same_card)
     2.6  
     2.7 -lemma inj_on_iff_card_le:
     2.8 -  assumes FIN: "finite A" and FIN': "finite B"
     2.9 -  shows "(\<exists>f. inj_on f A \<and> f ` A \<le> B) = (card A \<le> card B)"
    2.10 -proof (safe intro!: card_inj_on_le)
    2.11 -  assume *: "card A \<le> card B"
    2.12 -  obtain f where 1: "inj_on f A" and 2: "f ` A = {0 ..< card A}"
    2.13 -  using FIN ex_bij_betw_finite_nat unfolding bij_betw_def by force
    2.14 -  moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g ` {0 ..< card B} = B"
    2.15 -  using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force
    2.16 -  ultimately have "inj_on g (f ` A)" using subset_inj_on[of g _ "f ` A"] * by force
    2.17 -  hence "inj_on (g \<circ> f) A" using 1 comp_inj_on by blast
    2.18 -  moreover
    2.19 -  {have "{0 ..< card A} \<le> {0 ..< card B}" using * by force
    2.20 -   with 2 have "f ` A  \<le> {0 ..< card B}" by blast
    2.21 -   hence "(g \<circ> f) ` A \<le> B" unfolding comp_def using 3 by force
    2.22 -  }
    2.23 -  ultimately show "(\<exists>f. inj_on f A \<and> f ` A \<le> B)" by blast
    2.24 -qed (insert assms, auto)
    2.25 -
    2.26  lemma subset_eq_atLeast0_lessThan_card:
    2.27    fixes n :: nat
    2.28    assumes "N \<subseteq> {0..<n}"
    2.29 @@ -1374,6 +1355,27 @@
    2.30    then show ?thesis by simp
    2.31  qed
    2.32  
    2.33 +text \<open>Relational version of @{thm [source] card_inj_on_le}:\<close>
    2.34 +lemma card_le_if_inj_on_rel:
    2.35 +assumes "finite B"
    2.36 +  "\<And>a. a \<in> A \<Longrightarrow> \<exists>b. b\<in>B \<and> r a b"
    2.37 +  "\<And>a1 a2 b. \<lbrakk> a1 \<in> A;  a2 \<in> A;  b \<in> B;  r a1 b;  r a2 b \<rbrakk> \<Longrightarrow> a1 = a2"
    2.38 +shows "card A \<le> card B"
    2.39 +proof -
    2.40 +  let ?P = "\<lambda>a b. b \<in> B \<and> r a b"
    2.41 +  let ?f = "\<lambda>a. SOME b. ?P a b"
    2.42 +  have 1: "?f ` A \<subseteq> B"  by (auto intro: someI2_ex[OF assms(2)])
    2.43 +  have "inj_on ?f A"
    2.44 +  proof (auto simp: inj_on_def)
    2.45 +    fix a1 a2 assume asms: "a1 \<in> A" "a2 \<in> A" "?f a1 = ?f a2"
    2.46 +    have 0: "?f a1 \<in> B" using "1" \<open>a1 \<in> A\<close> by blast
    2.47 +    have 1: "r a1 (?f a1)" using someI_ex[OF assms(2)[OF \<open>a1 \<in> A\<close>]] by blast
    2.48 +    have 2: "r a2 (?f a1)" using someI_ex[OF assms(2)[OF \<open>a2 \<in> A\<close>]] asms(3) by auto
    2.49 +    show "a1 = a2" using assms(3)[OF asms(1,2) 0 1 2] .
    2.50 +  qed
    2.51 +  with 1 show ?thesis using card_inj_on_le[of ?f A B] assms(1) by simp
    2.52 +qed
    2.53 +
    2.54  
    2.55  subsection \<open>Intervals of integers\<close>
    2.56