--- a/src/HOL/Archimedean_Field.thy Thu Sep 15 11:44:05 2016 +0200
+++ b/src/HOL/Archimedean_Field.thy Thu Sep 15 14:14:49 2016 +0100
@@ -492,6 +492,18 @@
lemma ceiling_add_le: "\<lceil>x + y\<rceil> \<le> \<lceil>x\<rceil> + \<lceil>y\<rceil>"
by (simp only: ceiling_le_iff of_int_add add_mono le_of_int_ceiling)
+lemma finite_int_segment:
+ fixes a :: "'a::floor_ceiling"
+ shows "finite {x \<in> \<int>. a \<le> x \<and> x \<le> b}"
+proof -
+ have "finite {ceiling a..floor b}"
+ by simp
+ moreover have "{x \<in> \<int>. a \<le> x \<and> x \<le> b} = of_int ` {ceiling a..floor b}"
+ by (auto simp: le_floor_iff ceiling_le_iff elim!: Ints_cases)
+ ultimately show ?thesis
+ by simp
+qed
+
text \<open>Ceiling with numerals.\<close>
--- a/src/HOL/Complete_Lattices.thy Thu Sep 15 11:44:05 2016 +0200
+++ b/src/HOL/Complete_Lattices.thy Thu Sep 15 14:14:49 2016 +0100
@@ -1055,6 +1055,11 @@
lemma Union_subsetI: "(\<And>x. x \<in> A \<Longrightarrow> \<exists>y. y \<in> B \<and> x \<subseteq> y) \<Longrightarrow> \<Union>A \<subseteq> \<Union>B"
by blast
+lemma disjnt_inj_on_iff:
+ "\<lbrakk>inj_on f (\<Union>\<A>); X \<in> \<A>; Y \<in> \<A>\<rbrakk> \<Longrightarrow> disjnt (f ` X) (f ` Y) \<longleftrightarrow> disjnt X Y"
+ apply (auto simp: disjnt_def)
+ using inj_on_eq_iff by fastforce
+
subsubsection \<open>Unions of families\<close>
--- a/src/HOL/Set.thy Thu Sep 15 11:44:05 2016 +0200
+++ b/src/HOL/Set.thy Thu Sep 15 14:14:49 2016 +0100
@@ -1858,6 +1858,24 @@
lemma disjnt_iff: "disjnt A B \<longleftrightarrow> (\<forall>x. \<not> (x \<in> A \<and> x \<in> B))"
by (force simp: disjnt_def)
+lemma disjnt_sym: "disjnt A B \<Longrightarrow> disjnt B A"
+ using disjnt_iff by blast
+
+lemma disjnt_empty1 [simp]: "disjnt {} A" and disjnt_empty2 [simp]: "disjnt A {}"
+ by (auto simp: disjnt_def)
+
+lemma disjnt_insert1 [simp]: "disjnt (insert a X) Y \<longleftrightarrow> a \<notin> Y \<and> disjnt X Y"
+ by (simp add: disjnt_def)
+
+lemma disjnt_insert2 [simp]: "disjnt Y (insert a X) \<longleftrightarrow> a \<notin> Y \<and> disjnt Y X"
+ by (simp add: disjnt_def)
+
+lemma disjnt_subset1 : "\<lbrakk>disjnt X Y; Z \<subseteq> X\<rbrakk> \<Longrightarrow> disjnt Z Y"
+ by (auto simp: disjnt_def)
+
+lemma disjnt_subset2 : "\<lbrakk>disjnt X Y; Z \<subseteq> Y\<rbrakk> \<Longrightarrow> disjnt X Z"
+ by (auto simp: disjnt_def)
+
lemma pairwise_empty [simp]: "pairwise P {}"
by (simp add: pairwise_def)
@@ -1871,6 +1889,9 @@
lemma pairwise_image: "pairwise r (f ` s) \<longleftrightarrow> pairwise (\<lambda>x y. (f x \<noteq> f y) \<longrightarrow> r (f x) (f y)) s"
by (force simp: pairwise_def)
+lemma disjoint_image_subset: "\<lbrakk>pairwise disjnt \<A>; \<And>X. X \<in> \<A> \<Longrightarrow> f X \<subseteq> X\<rbrakk> \<Longrightarrow> pairwise disjnt (f `\<A>)"
+ unfolding disjnt_def pairwise_def by fast
+
lemma Int_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> False) \<Longrightarrow> A \<inter> B = {}"
by blast
--- a/src/HOL/Set_Interval.thy Thu Sep 15 11:44:05 2016 +0200
+++ b/src/HOL/Set_Interval.thy Thu Sep 15 14:14:49 2016 +0100
@@ -130,6 +130,12 @@
subsection \<open>Logical Equivalences for Set Inclusion and Equality\<close>
+lemma atLeast_empty_triv [simp]: "{{}..} = UNIV"
+ by auto
+
+lemma atMost_UNIV_triv [simp]: "{..UNIV} = UNIV"
+ by auto
+
lemma atLeast_subset_iff [iff]:
"(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))"
by (blast intro: order_trans)