--- 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). *)