src/HOL/Set_Interval.thy

 lemma atLeastLessThan_eq_iff:
   fixes a b c d :: "'a::linorder"
   assumes "a < b" "c < d"
   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)
 
 lemma (in order_top) atMost_eq_UNIV_iff: "{..x} = UNIV \<longleftrightarrow> x = top"

 lemma Int_greaterThanLessThan[simp]: "{a<..<b} Int {c<..<d} = {max a c <..< min b d}"
 by auto
 
 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
 begin