# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1473945289 -3600
# Node ID 15bbf6360339dc4c89837b9a068b2991d4a4d67f
# Parent  b4051d3f4e94a9ef786679b0193a84f9e256bbd3
simple new lemmas, mostly about sets

diff -r b4051d3f4e94 -r 15bbf6360339 src/HOL/Archimedean_Field.thy
--- 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>
 
diff -r b4051d3f4e94 -r 15bbf6360339 src/HOL/Complete_Lattices.thy
--- 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>
 
diff -r b4051d3f4e94 -r 15bbf6360339 src/HOL/Set.thy
--- 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
 
diff -r b4051d3f4e94 -r 15bbf6360339 src/HOL/Set_Interval.thy
--- 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)