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