# HG changeset patch
# User hoelzl
# Date 1305901344 -7200
# Node ID e2f4736719377f3cb107e1b00327fe4a4997313f
# Parent  bb78de1c7d688ed39b34a43eb200165f90cdc44e
simp rules for empty intervals on dense linear order

diff -r bb78de1c7d68 -r e2f473671937 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Fri May 20 14:12:59 2011 +0200
+++ b/src/HOL/SetInterval.thy	Fri May 20 16:22:24 2011 +0200
@@ -258,6 +258,19 @@
 
 end
 
+context dense_linorder
+begin
+
+lemma greaterThanLessThan_empty_iff[simp]:
+  "{ a <..< b } = {} \<longleftrightarrow> b \<le> a"
+  using dense[of a b] by (cases "a < b") auto
+
+lemma greaterThanLessThan_empty_iff2[simp]:
+  "{} = { a <..< b } \<longleftrightarrow> b \<le> a"
+  using dense[of a b] by (cases "a < b") auto
+
+end
+
 lemma (in linorder) atLeastLessThan_subset_iff:
   "{a..<b} <= {c..<d} \<Longrightarrow> b <= a | c<=a & b<=d"
 apply (auto simp:subset_eq Ball_def)