simplifier trace info; Suc-intervals
authornipkow
Mon May 23 11:06:41 2005 +0200 (2005-05-23)
changeset 160415a8736668ced
parent 16040 6e7616eba0b8
child 16042 8e15ff79851a
simplifier trace info; Suc-intervals
src/HOL/Matrix/SparseMatrix.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Matrix/SparseMatrix.thy	Mon May 23 10:49:25 2005 +0200
     1.2 +++ b/src/HOL/Matrix/SparseMatrix.thy	Mon May 23 11:06:41 2005 +0200
     1.3 @@ -595,7 +595,7 @@
     1.4    disj_matrices :: "('a::zero) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
     1.5    "disj_matrices A B == (! j i. (Rep_matrix A j i \<noteq> 0) \<longrightarrow> (Rep_matrix B j i = 0)) & (! j i. (Rep_matrix B j i \<noteq> 0) \<longrightarrow> (Rep_matrix A j i = 0))"  
     1.6  
     1.7 -ML {* simp_depth_limit := 2 *}
     1.8 +ML {* simp_depth_limit := 6 *}
     1.9  
    1.10  lemma disj_matrices_contr1: "disj_matrices A B \<Longrightarrow> Rep_matrix A j i \<noteq> 0 \<Longrightarrow> Rep_matrix B j i = 0"
    1.11     by (simp add: disj_matrices_def)
     2.1 --- a/src/HOL/SetInterval.thy	Mon May 23 10:49:25 2005 +0200
     2.2 +++ b/src/HOL/SetInterval.thy	Mon May 23 11:06:41 2005 +0200
     2.3 @@ -266,10 +266,10 @@
     2.4    of @{term atLeastLessThan}*}
     2.5  lemma atLeast0LessThan: "{0::nat..<n} = {..<n}"
     2.6  by(simp add:lessThan_def atLeastLessThan_def)
     2.7 -
     2.8 +(*
     2.9  lemma atLeastLessThan0 [simp]: "{m..<0::nat} = {}"
    2.10  by (simp add: atLeastLessThan_def)
    2.11 -
    2.12 +*)
    2.13  subsubsection {* Intervals of nats with @{term Suc} *}
    2.14  
    2.15  text{*Not a simprule because the RHS is too messy.*}
    2.16 @@ -279,13 +279,13 @@
    2.17  
    2.18  lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}"
    2.19  by (auto simp add: atLeastLessThan_def)
    2.20 -
    2.21 +(*
    2.22  lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}"
    2.23  by (induct k, simp_all add: atLeastLessThanSuc)
    2.24  
    2.25  lemma atLeastSucLessThan [simp]: "{Suc n..<n} = {}"
    2.26  by (auto simp add: atLeastLessThan_def)
    2.27 -
    2.28 +*)
    2.29  lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}"
    2.30    by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
    2.31  
    2.32 @@ -612,10 +612,11 @@
    2.33   setsum f {a..<b} = setsum g {c..<d}"
    2.34  by(rule setsum_cong, simp_all)
    2.35  
    2.36 -(* FIXME delete
    2.37 -lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
    2.38 -by (simp add:lessThan_Suc)
    2.39 -*)
    2.40 +(* FIXME why are the following simp rules but the corresponding eqns
    2.41 +on intervals are not? *)
    2.42 +
    2.43 +lemma setsum_lessThan_Suc[simp]: "(\<Sum>i < Suc n. f i) = (\<Sum>i < n. f i) + f n"
    2.44 +by (simp add:lessThan_Suc add_ac)
    2.45  
    2.46  lemma setsum_cl_ivl_Suc[simp]:
    2.47    "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"
    2.48 @@ -624,11 +625,11 @@
    2.49  lemma setsum_op_ivl_Suc[simp]:
    2.50    "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
    2.51  by (auto simp:add_ac atLeastLessThanSuc)
    2.52 -
    2.53 +(*
    2.54  lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==>
    2.55      (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
    2.56  by (auto simp:add_ac atLeastAtMostSuc_conv)
    2.57 -
    2.58 +*)
    2.59  lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
    2.60    setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
    2.61  by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un)