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.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.12  subsection {*Two-sided intervals*}
1.14 @@ -262,6 +266,18 @@
1.15  apply (simp add: less_imp_le)
1.16  done
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.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.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.71  subsection {* Intervals of integers *}