make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
authorhuffman
Mon Feb 23 16:25:52 2009 -0800 (2009-02-23)
changeset 30079293b896b9c25
parent 30078 beee83623cc9
child 30080 4cf42465b3da
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
src/HOL/Arith_Tools.thy
src/HOL/Divides.thy
src/HOL/Groebner_Basis.thy
src/HOL/Int.thy
src/HOL/IntDiv.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/NatBin.thy
src/HOL/Power.thy
src/HOL/Relation_Power.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Arith_Tools.thy	Mon Feb 23 13:55:36 2009 -0800
     1.2 +++ b/src/HOL/Arith_Tools.thy	Mon Feb 23 16:25:52 2009 -0800
     1.3 @@ -68,8 +68,9 @@
     1.4  apply (subst add_eq_if)
     1.5  apply (simp split add: nat.split
     1.6              del: nat_numeral_1_eq_1
     1.7 -            add: numeral_1_eq_Suc_0 [symmetric] Let_def
     1.8 -                 neg_imp_number_of_eq_0 neg_number_of_pred_iff_0)
     1.9 +            add: nat_numeral_1_eq_1 [symmetric]
    1.10 +                 numeral_1_eq_Suc_0 [symmetric]
    1.11 +                 neg_number_of_pred_iff_0)
    1.12  done
    1.13  
    1.14  lemma nat_rec_number_of [simp]:
    1.15 @@ -89,7 +90,8 @@
    1.16  apply (subst add_eq_if)
    1.17  apply (simp split add: nat.split
    1.18              del: nat_numeral_1_eq_1
    1.19 -            add: numeral_1_eq_Suc_0 [symmetric] Let_def neg_imp_number_of_eq_0
    1.20 +            add: nat_numeral_1_eq_1 [symmetric]
    1.21 +                 numeral_1_eq_Suc_0 [symmetric]
    1.22                   neg_number_of_pred_iff_0)
    1.23  done
    1.24  
     2.1 --- a/src/HOL/Divides.thy	Mon Feb 23 13:55:36 2009 -0800
     2.2 +++ b/src/HOL/Divides.thy	Mon Feb 23 16:25:52 2009 -0800
     2.3 @@ -490,9 +490,9 @@
     2.4    from divmod_rel have divmod_m_n: "divmod_rel m n (m div n) (m mod n)" .
     2.5    with assms have m_div_n: "m div n \<ge> 1"
     2.6      by (cases "m div n") (auto simp add: divmod_rel_def)
     2.7 -  from assms divmod_m_n have "divmod_rel (m - n) n (m div n - 1) (m mod n)"
     2.8 +  from assms divmod_m_n have "divmod_rel (m - n) n (m div n - Suc 0) (m mod n)"
     2.9      by (cases "m div n") (auto simp add: divmod_rel_def)
    2.10 -  with divmod_eq have "divmod (m - n) n = (m div n - 1, m mod n)" by simp
    2.11 +  with divmod_eq have "divmod (m - n) n = (m div n - Suc 0, m mod n)" by simp
    2.12    moreover from divmod_div_mod have "divmod (m - n) n = ((m - n) div n, (m - n) mod n)" .
    2.13    ultimately have "m div n = Suc ((m - n) div n)"
    2.14      and "m mod n = (m - n) mod n" using m_div_n by simp_all
    2.15 @@ -816,6 +816,9 @@
    2.16  lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
    2.17  by (simp add: dvd_def)
    2.18  
    2.19 +lemma nat_dvd_1_iff_1 [simp]: "m dvd (1::nat) \<longleftrightarrow> m = 1"
    2.20 +by (simp add: dvd_def)
    2.21 +
    2.22  lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
    2.23    unfolding dvd_def
    2.24    by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
     3.1 --- a/src/HOL/Groebner_Basis.thy	Mon Feb 23 13:55:36 2009 -0800
     3.2 +++ b/src/HOL/Groebner_Basis.thy	Mon Feb 23 16:25:52 2009 -0800
     3.3 @@ -147,7 +147,7 @@
     3.4  next show "pwr (mul x y) q = mul (pwr x q) (pwr y q)" by (rule pwr_mul)
     3.5  next show "pwr (pwr x p) q = pwr x (p * q)" by (rule pwr_pwr)
     3.6  next show "pwr x 0 = r1" using pwr_0 .
     3.7 -next show "pwr x 1 = x" by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
     3.8 +next show "pwr x 1 = x" unfolding One_nat_def by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
     3.9  next show "mul x (add y z) = add (mul x y) (mul x z)" using mul_d by simp
    3.10  next show "pwr x (Suc q) = mul x (pwr x q)" using pwr_Suc by simp
    3.11  next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number mul_pwr)
     4.1 --- a/src/HOL/Int.thy	Mon Feb 23 13:55:36 2009 -0800
     4.2 +++ b/src/HOL/Int.thy	Mon Feb 23 16:25:52 2009 -0800
     4.3 @@ -832,8 +832,8 @@
     4.4                               le_imp_0_less [THEN order_less_imp_le])  
     4.5  next
     4.6    case (neg n)
     4.7 -  thus ?thesis by (simp del: of_nat_Suc of_nat_add
     4.8 -    add: algebra_simps of_nat_1 [symmetric] of_nat_add [symmetric])
     4.9 +  thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
    4.10 +    add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
    4.11  qed
    4.12  
    4.13  lemma bin_less_0_simps:
    4.14 @@ -1165,8 +1165,8 @@
    4.15                               le_imp_0_less [THEN order_less_imp_le])  
    4.16  next
    4.17    case (neg n)
    4.18 -  thus ?thesis by (simp del: of_nat_Suc of_nat_add
    4.19 -    add: algebra_simps of_nat_1 [symmetric] of_nat_add [symmetric])
    4.20 +  thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
    4.21 +    add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
    4.22  qed
    4.23  
    4.24  text {* Less-Than or Equals *}
    4.25 @@ -1785,11 +1785,12 @@
    4.26  lemma int_val_lemma:
    4.27       "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
    4.28        f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
    4.29 +unfolding One_nat_def
    4.30  apply (induct n, simp)
    4.31  apply (intro strip)
    4.32  apply (erule impE, simp)
    4.33  apply (erule_tac x = n in allE, simp)
    4.34 -apply (case_tac "k = f (n+1) ")
    4.35 +apply (case_tac "k = f (Suc n)")
    4.36  apply force
    4.37  apply (erule impE)
    4.38   apply (simp add: abs_if split add: split_if_asm)
    4.39 @@ -1803,6 +1804,7 @@
    4.40           f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
    4.41  apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k 
    4.42         in int_val_lemma)
    4.43 +unfolding One_nat_def
    4.44  apply simp
    4.45  apply (erule exE)
    4.46  apply (rule_tac x = "i+m" in exI, arith)
     5.1 --- a/src/HOL/IntDiv.thy	Mon Feb 23 13:55:36 2009 -0800
     5.2 +++ b/src/HOL/IntDiv.thy	Mon Feb 23 16:25:52 2009 -0800
     5.3 @@ -1228,7 +1228,7 @@
     5.4  text{*Suggested by Matthias Daum*}
     5.5  lemma int_power_div_base:
     5.6       "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
     5.7 -apply (subgoal_tac "k ^ m = k ^ ((m - 1) + 1)")
     5.8 +apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")
     5.9   apply (erule ssubst)
    5.10   apply (simp only: power_add)
    5.11   apply simp_all
     6.1 --- a/src/HOL/List.thy	Mon Feb 23 13:55:36 2009 -0800
     6.2 +++ b/src/HOL/List.thy	Mon Feb 23 16:25:52 2009 -0800
     6.3 @@ -1438,10 +1438,10 @@
     6.4  apply (auto split:nat.split)
     6.5  done
     6.6  
     6.7 -lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
     6.8 +lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - Suc 0)"
     6.9  by(induct xs)(auto simp:neq_Nil_conv)
    6.10  
    6.11 -lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
    6.12 +lemma butlast_conv_take: "butlast xs = take (length xs - Suc 0) xs"
    6.13  by (induct xs, simp, case_tac xs, simp_all)
    6.14  
    6.15  
    6.16 @@ -1588,7 +1588,7 @@
    6.17  done
    6.18  
    6.19  lemma butlast_take:
    6.20 -  "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
    6.21 +  "n <= length xs ==> butlast (take n xs) = take (n - Suc 0) xs"
    6.22  by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
    6.23  
    6.24  lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
    6.25 @@ -1639,7 +1639,7 @@
    6.26  done
    6.27  
    6.28  lemma take_hd_drop:
    6.29 -  "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (n+1) xs"
    6.30 +  "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (Suc n) xs"
    6.31  apply(induct xs arbitrary: n)
    6.32  apply simp
    6.33  apply(simp add:drop_Cons split:nat.split)
    6.34 @@ -2458,7 +2458,7 @@
    6.35  done
    6.36  
    6.37  lemma length_remove1:
    6.38 -  "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)"
    6.39 +  "length(remove1 x xs) = (if x : set xs then length xs - Suc 0 else length xs)"
    6.40  apply (induct xs)
    6.41   apply (auto dest!:length_pos_if_in_set)
    6.42  done
     7.1 --- a/src/HOL/Nat.thy	Mon Feb 23 13:55:36 2009 -0800
     7.2 +++ b/src/HOL/Nat.thy	Mon Feb 23 16:25:52 2009 -0800
     7.3 @@ -196,8 +196,8 @@
     7.4  
     7.5  instance proof
     7.6    fix n m q :: nat
     7.7 -  show "0 \<noteq> (1::nat)" by simp
     7.8 -  show "1 * n = n" by simp
     7.9 +  show "0 \<noteq> (1::nat)" unfolding One_nat_def by simp
    7.10 +  show "1 * n = n" unfolding One_nat_def by simp
    7.11    show "n * m = m * n" by (induct n) simp_all
    7.12    show "(n * m) * q = n * (m * q)" by (induct n) (simp_all add: add_mult_distrib)
    7.13    show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib)
    7.14 @@ -307,18 +307,24 @@
    7.15  lemmas nat_distrib =
    7.16    add_mult_distrib add_mult_distrib2 diff_mult_distrib diff_mult_distrib2
    7.17  
    7.18 -lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)"
    7.19 +lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = Suc 0 & n = Suc 0)"
    7.20    apply (induct m)
    7.21     apply simp
    7.22    apply (induct n)
    7.23     apply auto
    7.24    done
    7.25  
    7.26 -lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"
    7.27 +lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
    7.28    apply (rule trans)
    7.29    apply (rule_tac [2] mult_eq_1_iff, fastsimp)
    7.30    done
    7.31  
    7.32 +lemma nat_mult_eq_1_iff [simp]: "m * n = (1::nat) \<longleftrightarrow> m = 1 \<and> n = 1"
    7.33 +  unfolding One_nat_def by (rule mult_eq_1_iff)
    7.34 +
    7.35 +lemma nat_1_eq_mult_iff [simp]: "(1::nat) = m * n \<longleftrightarrow> m = 1 \<and> n = 1"
    7.36 +  unfolding One_nat_def by (rule one_eq_mult_iff)
    7.37 +
    7.38  lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"
    7.39  proof -
    7.40    have "k \<noteq> 0 \<Longrightarrow> k * m = k * n \<Longrightarrow> m = n"
    7.41 @@ -465,11 +471,11 @@
    7.42  lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"
    7.43    unfolding less_Suc_eq_le le_less ..
    7.44  
    7.45 -lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)"
    7.46 +lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
    7.47    by (simp add: less_Suc_eq)
    7.48  
    7.49 -lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
    7.50 -  by (simp add: less_Suc_eq)
    7.51 +lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)"
    7.52 +  unfolding One_nat_def by (rule less_Suc0)
    7.53  
    7.54  lemma Suc_mono: "m < n ==> Suc m < Suc n"
    7.55    by simp
    7.56 @@ -800,6 +806,7 @@
    7.57    done
    7.58  
    7.59  lemma ex_least_nat_less: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not>P i) & P(k+1)"
    7.60 +  unfolding One_nat_def
    7.61    apply (cases n)
    7.62     apply blast
    7.63    apply (frule (1) ex_least_nat_le)
    7.64 @@ -1089,7 +1096,7 @@
    7.65     apply simp_all
    7.66    done
    7.67  
    7.68 -lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (1 \<le> m & 1 \<le> n)"
    7.69 +lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (Suc 0 \<le> m & Suc 0 \<le> n)"
    7.70    apply (induct m)
    7.71     apply simp
    7.72    apply (case_tac n)
    7.73 @@ -1125,7 +1132,7 @@
    7.74    by (cases m) (auto intro: le_add1)
    7.75  
    7.76  text {* Lemma for @{text gcd} *}
    7.77 -lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
    7.78 +lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = Suc 0 | m = 0"
    7.79    apply (drule sym)
    7.80    apply (rule disjCI)
    7.81    apply (rule nat_less_cases, erule_tac [2] _)
    7.82 @@ -1164,7 +1171,7 @@
    7.83    | of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
    7.84  
    7.85  lemma of_nat_1 [simp]: "of_nat 1 = 1"
    7.86 -  by simp
    7.87 +  unfolding One_nat_def by simp
    7.88  
    7.89  lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
    7.90    by (induct m) (simp_all add: add_ac)
    7.91 @@ -1276,7 +1283,7 @@
    7.92  end
    7.93  
    7.94  lemma of_nat_id [simp]: "of_nat n = n"
    7.95 -  by (induct n) auto
    7.96 +  by (induct n) (auto simp add: One_nat_def)
    7.97  
    7.98  lemma of_nat_eq_id [simp]: "of_nat = id"
    7.99    by (auto simp add: expand_fun_eq)
   7.100 @@ -1381,7 +1388,7 @@
   7.101  apply(induct_tac k)
   7.102   apply simp
   7.103  apply(erule_tac x="m+n" in meta_allE)
   7.104 -apply(erule_tac x="m+n+1" in meta_allE)
   7.105 +apply(erule_tac x="Suc(m+n)" in meta_allE)
   7.106  apply simp
   7.107  done
   7.108  
     8.1 --- a/src/HOL/NatBin.thy	Mon Feb 23 13:55:36 2009 -0800
     8.2 +++ b/src/HOL/NatBin.thy	Mon Feb 23 16:25:52 2009 -0800
     8.3 @@ -442,19 +442,13 @@
     8.4  (* These two can be useful when m = number_of... *)
     8.5  
     8.6  lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
     8.7 -apply (case_tac "m")
     8.8 -apply (simp_all add: numerals)
     8.9 -done
    8.10 +  unfolding One_nat_def by (cases m) simp_all
    8.11  
    8.12  lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"
    8.13 -apply (case_tac "m")
    8.14 -apply (simp_all add: numerals)
    8.15 -done
    8.16 +  unfolding One_nat_def by (cases m) simp_all
    8.17  
    8.18  lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
    8.19 -apply (case_tac "m")
    8.20 -apply (simp_all add: numerals)
    8.21 -done
    8.22 +  unfolding One_nat_def by (cases m) simp_all
    8.23  
    8.24  
    8.25  subsection{*Comparisons involving (0::nat) *}
     9.1 --- a/src/HOL/Power.thy	Mon Feb 23 13:55:36 2009 -0800
     9.2 +++ b/src/HOL/Power.thy	Mon Feb 23 16:25:52 2009 -0800
     9.3 @@ -31,7 +31,7 @@
     9.4    by (induct n) (simp_all add: power_Suc)
     9.5  
     9.6  lemma power_one_right [simp]: "(a::'a::recpower) ^ 1 = a"
     9.7 -  by (simp add: power_Suc)
     9.8 +  unfolding One_nat_def by (simp add: power_Suc)
     9.9  
    9.10  lemma power_commutes: "(a::'a::recpower) ^ n * a = a * a ^ n"
    9.11    by (induct n) (simp_all add: power_Suc mult_assoc)
    9.12 @@ -366,8 +366,8 @@
    9.13    "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
    9.14  by (induct n, simp_all add: power_Suc of_nat_mult)
    9.15  
    9.16 -lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
    9.17 -by (insert one_le_power [of i n], simp)
    9.18 +lemma nat_one_le_power [simp]: "Suc 0 \<le> i ==> Suc 0 \<le> i^n"
    9.19 +by (rule one_le_power [of i n, unfolded One_nat_def])
    9.20  
    9.21  lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
    9.22  by (induct "n", auto)
    9.23 @@ -452,4 +452,3 @@
    9.24  *}
    9.25  
    9.26  end
    9.27 -
    10.1 --- a/src/HOL/Relation_Power.thy	Mon Feb 23 13:55:36 2009 -0800
    10.2 +++ b/src/HOL/Relation_Power.thy	Mon Feb 23 16:25:52 2009 -0800
    10.3 @@ -61,16 +61,16 @@
    10.4  
    10.5  lemma funpow_swap1: "f((f^n) x) = (f^n)(f x)"
    10.6  proof -
    10.7 -  have "f((f^n) x) = (f^(n+1)) x" by simp
    10.8 +  have "f((f^n) x) = (f^(n+1)) x" unfolding One_nat_def by simp
    10.9    also have "\<dots>  = (f^n o f^1) x" by (simp only: funpow_add)
   10.10 -  also have "\<dots> = (f^n)(f x)" by simp
   10.11 +  also have "\<dots> = (f^n)(f x)" unfolding One_nat_def by simp
   10.12    finally show ?thesis .
   10.13  qed
   10.14  
   10.15  lemma rel_pow_1 [simp]:
   10.16    fixes R :: "('a*'a)set"
   10.17    shows "R^1 = R"
   10.18 -  by simp
   10.19 +  unfolding One_nat_def by simp
   10.20  
   10.21  lemma rel_pow_0_I: "(x,x) : R^0"
   10.22    by simp
    11.1 --- a/src/HOL/SetInterval.thy	Mon Feb 23 13:55:36 2009 -0800
    11.2 +++ b/src/HOL/SetInterval.thy	Mon Feb 23 16:25:52 2009 -0800
    11.3 @@ -352,11 +352,11 @@
    11.4  
    11.5  corollary image_Suc_atLeastAtMost[simp]:
    11.6    "Suc ` {i..j} = {Suc i..Suc j}"
    11.7 -using image_add_atLeastAtMost[where k=1] by simp
    11.8 +using image_add_atLeastAtMost[where k="Suc 0"] by simp
    11.9  
   11.10  corollary image_Suc_atLeastLessThan[simp]:
   11.11    "Suc ` {i..<j} = {Suc i..<Suc j}"
   11.12 -using image_add_atLeastLessThan[where k=1] by simp
   11.13 +using image_add_atLeastLessThan[where k="Suc 0"] by simp
   11.14  
   11.15  lemma image_add_int_atLeastLessThan:
   11.16      "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
   11.17 @@ -556,7 +556,7 @@
   11.18  qed
   11.19  
   11.20  lemma card_less_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}"
   11.21 -apply (rule card_bij_eq [of "Suc" _ _ "\<lambda>x. x - 1"])
   11.22 +apply (rule card_bij_eq [of "Suc" _ _ "\<lambda>x. x - Suc 0"])
   11.23  apply simp
   11.24  apply fastsimp
   11.25  apply auto
   11.26 @@ -803,7 +803,7 @@
   11.27  
   11.28  lemma setsum_head_upt_Suc:
   11.29    "m < n \<Longrightarrow> setsum f {m..<n} = f m + setsum f {Suc m..<n}"
   11.30 -apply(insert setsum_head_Suc[of m "n - 1" f])
   11.31 +apply(insert setsum_head_Suc[of m "n - Suc 0" f])
   11.32  apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps)
   11.33  done
   11.34  
   11.35 @@ -835,11 +835,11 @@
   11.36  
   11.37  corollary setsum_shift_bounds_cl_Suc_ivl:
   11.38    "setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}"
   11.39 -by (simp add:setsum_shift_bounds_cl_nat_ivl[where k=1,simplified])
   11.40 +by (simp add:setsum_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
   11.41  
   11.42  corollary setsum_shift_bounds_Suc_ivl:
   11.43    "setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}"
   11.44 -by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified])
   11.45 +by (simp add:setsum_shift_bounds_nat_ivl[where k="Suc 0", simplified])
   11.46  
   11.47  lemma setsum_shift_lb_Suc0_0:
   11.48    "f(0::nat) = (0::nat) \<Longrightarrow> setsum f {Suc 0..k} = setsum f {0..k}"
   11.49 @@ -883,6 +883,7 @@
   11.50      by (rule setsum_addf)
   11.51    also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
   11.52    also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
   11.53 +    unfolding One_nat_def
   11.54      by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt mult_ac)
   11.55    also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)"
   11.56      by (simp add: left_distrib right_distrib)
   11.57 @@ -890,7 +891,7 @@
   11.58      by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
   11.59    also from ngt1
   11.60    have "(1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)"
   11.61 -    by (simp only: mult_ac gauss_sum [of "n - 1"])
   11.62 +    by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def)
   11.63         (simp add:  mult_ac trans [OF add_commute of_nat_Suc [symmetric]])
   11.64    finally show ?thesis by (simp add: algebra_simps)
   11.65  next
   11.66 @@ -906,7 +907,8 @@
   11.67      "((1::nat) + 1) * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) =
   11.68      of_nat(n) * (a + (a + of_nat(n - 1)*d))"
   11.69      by (rule arith_series_general)
   11.70 -  thus ?thesis by (auto simp add: of_nat_id)
   11.71 +  thus ?thesis
   11.72 +    unfolding One_nat_def by (auto simp add: of_nat_id)
   11.73  qed
   11.74  
   11.75  lemma arith_series_int: