# HG changeset patch
# User nipkow
# Date 1079690813 -3600
# Node ID bdf6b7adc3ec3b81e8b546ef01756627a896848b
# Parent  cc61fd03e589c9714c732ec86ef625389a702032
added a few 0 and Suc lemmas

diff -r cc61fd03e589 -r bdf6b7adc3ec src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Fri Mar 19 10:51:03 2004 +0100
+++ b/src/HOL/SetInterval.thy	Fri Mar 19 11:06:53 2004 +0100
@@ -208,12 +208,25 @@
   "(i : {)l..u(}) = (l < i & i < u)"
 by (simp add: greaterThanLessThan_def)
 
+lemma greaterThanLessThan_0 [simp]: "{)l..0::nat(} == {}"
+by (simp add: greaterThanLessThan_def)
+
+lemma greaterThanLessThan_Suc_greaterThanAtMost:
+  "{)l..Suc n(} = {)l..n}"
+by (auto simp add: greaterThanLessThan_def greaterThanAtMost_def)
+
 (* atLeastLessThan *)
 
 lemma atLeastLessThan_iff [simp]:
   "(i : {l..u(}) = (l <= i & i < u)"
 by (simp add: atLeastLessThan_def)
 
+lemma atLeastLessThan_0 [simp]: "{l..0::nat(} == {}"
+by (simp add: atLeastLessThan_def)
+
+lemma atLeastLessThan_Suc_atLeastAtMost: "{l..Suc n(} = {l..n}"
+by (auto simp add: atLeastLessThan_def atLeastAtMost_def)
+
 (* greaterThanAtMost *)
 
 lemma greaterThanAtMost_iff [simp]:
@@ -226,6 +239,7 @@
   "(i : {l..u}) = (l <= i & i <= u)"
 by (simp add: atLeastAtMost_def)
 
+
 (* The above four lemmas could be declared as iffs.
    If we do so, a call to blast in Hyperreal/Star.ML, lemma STAR_Int
    seems to take forever (more than one hour). *)