added a few 0 and Suc lemmas
authornipkow
Fri Mar 19 11:06:53 2004 +0100 (2004-03-19)
changeset 14478bdf6b7adc3ec
parent 14477 cc61fd03e589
child 14479 0eca4aabf371
added a few 0 and Suc lemmas
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/SetInterval.thy	Fri Mar 19 10:51:03 2004 +0100
     1.2 +++ b/src/HOL/SetInterval.thy	Fri Mar 19 11:06:53 2004 +0100
     1.3 @@ -208,12 +208,25 @@
     1.4    "(i : {)l..u(}) = (l < i & i < u)"
     1.5  by (simp add: greaterThanLessThan_def)
     1.6  
     1.7 +lemma greaterThanLessThan_0 [simp]: "{)l..0::nat(} == {}"
     1.8 +by (simp add: greaterThanLessThan_def)
     1.9 +
    1.10 +lemma greaterThanLessThan_Suc_greaterThanAtMost:
    1.11 +  "{)l..Suc n(} = {)l..n}"
    1.12 +by (auto simp add: greaterThanLessThan_def greaterThanAtMost_def)
    1.13 +
    1.14  (* atLeastLessThan *)
    1.15  
    1.16  lemma atLeastLessThan_iff [simp]:
    1.17    "(i : {l..u(}) = (l <= i & i < u)"
    1.18  by (simp add: atLeastLessThan_def)
    1.19  
    1.20 +lemma atLeastLessThan_0 [simp]: "{l..0::nat(} == {}"
    1.21 +by (simp add: atLeastLessThan_def)
    1.22 +
    1.23 +lemma atLeastLessThan_Suc_atLeastAtMost: "{l..Suc n(} = {l..n}"
    1.24 +by (auto simp add: atLeastLessThan_def atLeastAtMost_def)
    1.25 +
    1.26  (* greaterThanAtMost *)
    1.27  
    1.28  lemma greaterThanAtMost_iff [simp]:
    1.29 @@ -226,6 +239,7 @@
    1.30    "(i : {l..u}) = (l <= i & i <= u)"
    1.31  by (simp add: atLeastAtMost_def)
    1.32  
    1.33 +
    1.34  (* The above four lemmas could be declared as iffs.
    1.35     If we do so, a call to blast in Hyperreal/Star.ML, lemma STAR_Int
    1.36     seems to take forever (more than one hour). *)