--- a/src/HOL/Set_Interval.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Set_Interval.thy Mon Jun 30 15:45:21 2014 +0200
@@ -457,6 +457,15 @@
shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d"
using atLeastLessThan_inj assms by auto
+lemma (in linorder) Ioc_inj: "{a <.. b} = {c <.. d} \<longleftrightarrow> (b \<le> a \<and> d \<le> c) \<or> a = c \<and> b = d"
+ by (metis eq_iff greaterThanAtMost_empty_iff2 greaterThanAtMost_iff le_cases not_le)
+
+lemma (in order) Iio_Int_singleton: "{..<k} \<inter> {x} = (if x < k then {x} else {})"
+ by auto
+
+lemma (in linorder) Ioc_subset_iff: "{a<..b} \<subseteq> {c<..d} \<longleftrightarrow> (b \<le> a \<or> c \<le> a \<and> b \<le> d)"
+ by (auto simp: subset_eq Ball_def) (metis less_le not_less)
+
lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
by (auto simp: set_eq_iff intro: le_bot)
@@ -588,6 +597,9 @@
lemma Int_atMost[simp]: "{..a} \<inter> {..b} = {.. min a b}"
by (auto simp: min_def)
+lemma Ioc_disjoint: "{a<..b} \<inter> {c<..d} = {} \<longleftrightarrow> b \<le> a \<or> d \<le> c \<or> b \<le> c \<or> d \<le> a"
+ using assms by auto
+
end
context complete_lattice