# HG changeset patch
# User hoelzl
# Date 1305920312 -7200
# Node ID e35cf2b25f488232c412bc6d03dbad5a3310cc1d
# Parent  d96e53d0c638709fd5ae40a4a454f79d678f3ed8
equations for subsets of atLeastAtMost

diff -r d96e53d0c638 -r e35cf2b25f48 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Fri May 20 18:12:12 2011 +0200
+++ b/src/HOL/SetInterval.thy	Fri May 20 21:38:32 2011 +0200
@@ -269,6 +269,21 @@
   "{} = { a <..< b } \<longleftrightarrow> b \<le> a"
   using dense[of a b] by (cases "a < b") auto
 
+lemma atLeastLessThan_subseteq_atLeastAtMost_iff:
+  "{a ..< b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
+  using dense[of "max a d" "b"]
+  by (force simp: subset_eq Ball_def not_less[symmetric])
+
+lemma greaterThanAtMost_subseteq_atLeastAtMost_iff:
+  "{a <.. b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
+  using dense[of "a" "min c b"]
+  by (force simp: subset_eq Ball_def not_less[symmetric])
+
+lemma greaterThanLessThan_subseteq_atLeastAtMost_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: