1.1 --- a/src/HOL/SetInterval.thy	Tue Mar 01 05:44:13 2005 +0100
     1.2 +++ b/src/HOL/SetInterval.thy	Tue Mar 01 18:48:52 2005 +0100
     1.3 @@ -168,26 +168,18 @@
     1.4  
     1.5  subsection {*Two-sided intervals*}
     1.6  
     1.7 -text {* @{text greaterThanLessThan} *}
     1.8 -
     1.9  lemma greaterThanLessThan_iff [simp]:
    1.10    "(i : {l<..<u}) = (l < i & i < u)"
    1.11  by (simp add: greaterThanLessThan_def)
    1.12  
    1.13 -text {* @{text atLeastLessThan} *}
    1.14 -
    1.15  lemma atLeastLessThan_iff [simp]:
    1.16    "(i : {l..<u}) = (l <= i & i < u)"
    1.17  by (simp add: atLeastLessThan_def)
    1.18  
    1.19 -text {* @{text greaterThanAtMost} *}
    1.20 -
    1.21  lemma greaterThanAtMost_iff [simp]:
    1.22    "(i : {l<..u}) = (l < i & i <= u)"
    1.23  by (simp add: greaterThanAtMost_def)
    1.24  
    1.25 -text {* @{text atLeastAtMost} *}
    1.26 -
    1.27  lemma atLeastAtMost_iff [simp]:
    1.28    "(i : {l..u}) = (l <= i & i <= u)"
    1.29  by (simp add: atLeastAtMost_def)
    1.30 @@ -196,6 +188,16 @@
    1.31    If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int}
    1.32    seems to take forever (more than one hour). *}
    1.33  
    1.34 +subsubsection{* Emptyness and singletons *}
    1.35 +
    1.36 +lemma atLeastAtMost_empty [simp]: "n < m ==> {m::'a::order..n} = {}";
    1.37 +  by (auto simp add: atLeastAtMost_def atMost_def atLeast_def);
    1.38 +
    1.39 +lemma atLeastLessThan_empty[simp]: "n \<le> m ==> {m..<n::'a::order} = {}"
    1.40 +by (auto simp add: atLeastLessThan_def)
    1.41 +
    1.42 +lemma atLeastAtMost_singleton [simp]: "{a::'a::order..a} = {a}";
    1.43 +  by (auto simp add: atLeastAtMost_def atMost_def atLeast_def);
    1.44  
    1.45  subsection {* Intervals of natural numbers *}
    1.46  
    1.47 @@ -268,12 +270,6 @@
    1.48  lemma atLeastLessThan0 [simp]: "{m..<0::nat} = {}"
    1.49  by (simp add: atLeastLessThan_def)
    1.50  
    1.51 -lemma atLeastLessThan_self [simp]: "{n::'a::order..<n} = {}"
    1.52 -by (auto simp add: atLeastLessThan_def)
    1.53 -
    1.54 -lemma atLeastLessThan_empty: "n \<le> m ==> {m..<n::'a::order} = {}"
    1.55 -by (auto simp add: atLeastLessThan_def)
    1.56 -
    1.57  subsubsection {* Intervals of nats with @{term Suc} *}
    1.58  
    1.59  text{*Not a simprule because the RHS is too messy.*}
    1.60 @@ -301,6 +297,9 @@
    1.61    by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def
    1.62      greaterThanLessThan_def)
    1.63  
    1.64 +lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
    1.65 +by (auto simp add: atLeastAtMost_def)
    1.66 +
    1.67  subsubsection {* Finiteness *}
    1.68  
    1.69  lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}"
    1.70 @@ -389,8 +388,6 @@
    1.71    apply (subst image_atLeastZeroLessThan_int, assumption)
    1.72    apply (rule finite_imageI)
    1.73    apply auto
    1.74 -  apply (subgoal_tac "{0..<u} = {}")
    1.75 -  apply auto
    1.76    done
    1.77  
    1.78  lemma image_atLeastLessThan_int_shift:
    1.79 @@ -615,8 +612,14 @@
    1.80   setsum f {a..<b} = setsum g {c..<d}"
    1.81  by(rule setsum_cong, simp_all)
    1.82  
    1.83 +lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==>
    1.84 +    (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
    1.85 +by (auto simp:add_ac atLeastAtMostSuc_conv)
    1.86 +
    1.87 +(* FIXME delete
    1.88  lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
    1.89  by (simp add:lessThan_Suc)
    1.90 +*)
    1.91  
    1.92  lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
    1.93    setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"