1.1 --- a/src/HOL/SetInterval.thy	Mon May 23 10:49:25 2005 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Mon May 23 11:06:41 2005 +0200
     1.3 @@ -266,10 +266,10 @@
     1.4    of @{term atLeastLessThan}*}
     1.5  lemma atLeast0LessThan: "{0::nat..<n} = {..<n}"
     1.6  by(simp add:lessThan_def atLeastLessThan_def)
     1.7 -
     1.8 +(*
     1.9  lemma atLeastLessThan0 [simp]: "{m..<0::nat} = {}"
    1.10  by (simp add: atLeastLessThan_def)
    1.11 -
    1.12 +*)
    1.13  subsubsection {* Intervals of nats with @{term Suc} *}
    1.14  
    1.15  text{*Not a simprule because the RHS is too messy.*}
    1.16 @@ -279,13 +279,13 @@
    1.17  
    1.18  lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}"
    1.19  by (auto simp add: atLeastLessThan_def)
    1.20 -
    1.21 +(*
    1.22  lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}"
    1.23  by (induct k, simp_all add: atLeastLessThanSuc)
    1.24  
    1.25  lemma atLeastSucLessThan [simp]: "{Suc n..<n} = {}"
    1.26  by (auto simp add: atLeastLessThan_def)
    1.27 -
    1.28 +*)
    1.29  lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}"
    1.30    by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
    1.31  
    1.32 @@ -612,10 +612,11 @@
    1.33   setsum f {a..<b} = setsum g {c..<d}"
    1.34  by(rule setsum_cong, simp_all)
    1.35  
    1.36 -(* FIXME delete
    1.37 -lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
    1.38 -by (simp add:lessThan_Suc)
    1.39 -*)
    1.40 +(* FIXME why are the following simp rules but the corresponding eqns
    1.41 +on intervals are not? *)
    1.42 +
    1.43 +lemma setsum_lessThan_Suc[simp]: "(\<Sum>i < Suc n. f i) = (\<Sum>i < n. f i) + f n"
    1.44 +by (simp add:lessThan_Suc add_ac)
    1.45  
    1.46  lemma setsum_cl_ivl_Suc[simp]:
    1.47    "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"
    1.48 @@ -624,11 +625,11 @@
    1.49  lemma setsum_op_ivl_Suc[simp]:
    1.50    "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
    1.51  by (auto simp:add_ac atLeastLessThanSuc)
    1.52 -
    1.53 +(*
    1.54  lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==>
    1.55      (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
    1.56  by (auto simp:add_ac atLeastAtMostSuc_conv)
    1.57 -
    1.58 +*)
    1.59  lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
    1.60    setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
    1.61  by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un)