src/HOL/SetInterval.thy
changeset 40703 d1fc454d6735
parent 39302 d7728f65b353
child 42891 e2f473671937
     1.1 --- a/src/HOL/SetInterval.thy	Mon Nov 22 10:34:33 2010 +0100
     1.2 +++ b/src/HOL/SetInterval.thy	Tue Nov 23 14:14:17 2010 +0100
     1.3 @@ -159,6 +159,10 @@
     1.4   apply simp_all
     1.5  done
     1.6  
     1.7 +lemma lessThan_strict_subset_iff:
     1.8 +  fixes m n :: "'a::linorder"
     1.9 +  shows "{..<m} < {..<n} \<longleftrightarrow> m < n"
    1.10 +  by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq)
    1.11  
    1.12  subsection {*Two-sided intervals*}
    1.13  
    1.14 @@ -262,6 +266,18 @@
    1.15  apply (simp add: less_imp_le)
    1.16  done
    1.17  
    1.18 +lemma atLeastLessThan_inj:
    1.19 +  fixes a b c d :: "'a::linorder"
    1.20 +  assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d"
    1.21 +  shows "a = c" "b = d"
    1.22 +using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le linorder_antisym_conv2 subset_refl)+
    1.23 +
    1.24 +lemma atLeastLessThan_eq_iff:
    1.25 +  fixes a b c d :: "'a::linorder"
    1.26 +  assumes "a < b" "c < d"
    1.27 +  shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d"
    1.28 +  using atLeastLessThan_inj assms by auto
    1.29 +
    1.30  subsubsection {* Intersection *}
    1.31  
    1.32  context linorder
    1.33 @@ -705,6 +721,39 @@
    1.34    "finite M \<Longrightarrow> \<exists>h. bij_betw h {1 .. card M} M"
    1.35  by (rule finite_same_card_bij) auto
    1.36  
    1.37 +lemma bij_betw_iff_card:
    1.38 +  assumes FIN: "finite A" and FIN': "finite B"
    1.39 +  shows BIJ: "(\<exists>f. bij_betw f A B) \<longleftrightarrow> (card A = card B)"
    1.40 +using assms
    1.41 +proof(auto simp add: bij_betw_same_card)
    1.42 +  assume *: "card A = card B"
    1.43 +  obtain f where "bij_betw f A {0 ..< card A}"
    1.44 +  using FIN ex_bij_betw_finite_nat by blast
    1.45 +  moreover obtain g where "bij_betw g {0 ..< card B} B"
    1.46 +  using FIN' ex_bij_betw_nat_finite by blast
    1.47 +  ultimately have "bij_betw (g o f) A B"
    1.48 +  using * by (auto simp add: bij_betw_trans)
    1.49 +  thus "(\<exists>f. bij_betw f A B)" by blast
    1.50 +qed
    1.51 +
    1.52 +lemma inj_on_iff_card_le:
    1.53 +  assumes FIN: "finite A" and FIN': "finite B"
    1.54 +  shows "(\<exists>f. inj_on f A \<and> f ` A \<le> B) = (card A \<le> card B)"
    1.55 +proof (safe intro!: card_inj_on_le)
    1.56 +  assume *: "card A \<le> card B"
    1.57 +  obtain f where 1: "inj_on f A" and 2: "f ` A = {0 ..< card A}"
    1.58 +  using FIN ex_bij_betw_finite_nat unfolding bij_betw_def by force
    1.59 +  moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g ` {0 ..< card B} = B"
    1.60 +  using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force
    1.61 +  ultimately have "inj_on g (f ` A)" using subset_inj_on[of g _ "f ` A"] * by force
    1.62 +  hence "inj_on (g o f) A" using 1 comp_inj_on by blast
    1.63 +  moreover
    1.64 +  {have "{0 ..< card A} \<le> {0 ..< card B}" using * by force
    1.65 +   with 2 have "f ` A  \<le> {0 ..< card B}" by blast
    1.66 +   hence "(g o f) ` A \<le> B" unfolding comp_def using 3 by force
    1.67 +  }
    1.68 +  ultimately show "(\<exists>f. inj_on f A \<and> f ` A \<le> B)" by blast
    1.69 +qed (insert assms, auto)
    1.70  
    1.71  subsection {* Intervals of integers *}
    1.72