# HG changeset patch
# User hoelzl
# Date 1309767349 -7200
# Node ID 537ea3846f649a02e32506865cc7b3f35639e768
# Parent  9ece732627467671f8d50b14638c94319dab13c9
equalities of subsets of atLeastLessThan

diff -r 9ece73262746 -r 537ea3846f64 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Sun Jul 03 09:59:25 2011 +0200
+++ b/src/HOL/SetInterval.thy	Mon Jul 04 10:15:49 2011 +0200
@@ -284,6 +284,21 @@
   using dense[of "a" "min c b"] dense[of "max a d" "b"]
   by (force simp: subset_eq Ball_def not_less[symmetric])
 
+lemma atLeastAtMost_subseteq_atLeastLessThan_iff:
+  "{a .. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a \<le> b \<longrightarrow> c \<le> a \<and> b < d)"
+  using dense[of "max a d" "b"]
+  by (force simp: subset_eq Ball_def not_less[symmetric])
+
+lemma greaterThanAtMost_subseteq_atLeastLessThan_iff:
+  "{a <.. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b < d)"
+  using dense[of "a" "min c b"]
+  by (force simp: subset_eq Ball_def not_less[symmetric])
+
+lemma greaterThanLessThan_subseteq_atLeastLessThan_iff:
+  "{a <..< b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
+  using dense[of "a" "min c b"] dense[of "max a d" "b"]
+  by (force simp: subset_eq Ball_def not_less[symmetric])
+
 end
 
 lemma (in linorder) atLeastLessThan_subset_iff: