# HG changeset patch
# User nipkow
# Date 1251276492 -7200
# Node ID 6c62363cf0d724aaaa5a61c63327ff487a4cb9a3
# Parent  cb3c5189ea8568040a7cd5f5ab57c4c4723c3270
new lemmas

diff -r cb3c5189ea85 -r 6c62363cf0d7 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Fri Aug 21 19:06:12 2009 +0200
+++ b/src/HOL/SetInterval.thy	Wed Aug 26 10:48:12 2009 +0200
@@ -186,26 +186,60 @@
   seems to take forever (more than one hour). *}
 end
 
-subsubsection{* Emptyness and singletons *}
+subsubsection{* Emptyness, singletons, subset *}
 
 context order
 begin
 
-lemma atLeastAtMost_empty [simp]: "n < m ==> {m..n} = {}";
-by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
+lemma atLeastatMost_empty[simp]:
+  "b < a \<Longrightarrow> {a..b} = {}"
+by(auto simp: atLeastAtMost_def atLeast_def atMost_def)
+
+lemma atLeastatMost_empty_iff[simp]:
+  "{a..b} = {} \<longleftrightarrow> (~ a <= b)"
+by auto (blast intro: order_trans)
+
+lemma atLeastatMost_empty_iff2[simp]:
+  "{} = {a..b} \<longleftrightarrow> (~ a <= b)"
+by auto (blast intro: order_trans)
+
+lemma atLeastLessThan_empty[simp]:
+  "b <= a \<Longrightarrow> {a..<b} = {}"
+by(auto simp: atLeastLessThan_def)
 
-lemma atLeastLessThan_empty[simp]: "n \<le> m ==> {m..<n} = {}"
-by (auto simp add: atLeastLessThan_def)
+lemma atLeastLessThan_empty_iff[simp]:
+  "{a..<b} = {} \<longleftrightarrow> (~ a < b)"
+by auto (blast intro: le_less_trans)
+
+lemma atLeastLessThan_empty_iff2[simp]:
+  "{} = {a..<b} \<longleftrightarrow> (~ a < b)"
+by auto (blast intro: le_less_trans)
 
-lemma greaterThanAtMost_empty[simp]:"l \<le> k ==> {k<..l} = {}"
+lemma greaterThanAtMost_empty[simp]: "l \<le> k ==> {k<..l} = {}"
 by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)
 
+lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \<longleftrightarrow> ~ k < l"
+by auto (blast intro: less_le_trans)
+
+lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \<longleftrightarrow> ~ k < l"
+by auto (blast intro: less_le_trans)
+
 lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..<l} = {}"
 by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)
 
 lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}"
 by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
 
+lemma atLeastatMost_subset_iff[simp]:
+  "{a..b} <= {c..d} \<longleftrightarrow> (~ a <= b) | c <= a & b <= d"
+unfolding atLeastAtMost_def atLeast_def atMost_def
+by (blast intro: order_trans)
+
+lemma atLeastatMost_psubset_iff:
+  "{a..b} < {c..d} \<longleftrightarrow>
+   ((~ a <= b) | c <= a & b <= d & (c < a | b < d))  &  c <= d"
+by(simp add: psubset_eq expand_set_eq less_le_not_le)(blast intro: order_trans)
+
 end
 
 subsection {* Intervals of natural numbers *}