merged
authorhuffman
Fri, 30 Mar 2012 17:21:36 +0200
changeset 47229 ba37aaead155
parent 47228 4f4d85c3516f (diff)
parent 47215 ca516aa5b6ce (current diff)
child 47231 3ff8c79a9e2f
merged
--- a/NEWS	Fri Mar 30 15:25:47 2012 +0200
+++ b/NEWS	Fri Mar 30 17:21:36 2012 +0200
@@ -162,6 +162,9 @@
   mod_mult_distrib ~> mult_mod_left
   mod_mult_distrib2 ~> mult_mod_right
 
+* Removed redundant theorems nat_mult_2 and nat_mult_2_right; use
+generic mult_2 and mult_2_right instead. INCOMPATIBILITY.
+
 * More default pred/set conversions on a couple of relation operations
 and predicates.  Added powers of predicate relations.
 Consolidation of some relation theorems:
--- a/src/HOL/Divides.thy	Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/Divides.thy	Fri Mar 30 17:21:36 2012 +0200
@@ -1086,7 +1086,7 @@
   by (simp add: numeral_2_eq_2 le_mod_geq)
 
 lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
-by (simp add: nat_mult_2 [symmetric])
+by (simp add: mult_2 [symmetric])
 
 lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
 proof -
--- a/src/HOL/Enum.thy	Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/Enum.thy	Fri Mar 30 17:21:36 2012 +0200
@@ -465,7 +465,7 @@
   | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
 
 lemma length_sublists:
-  "length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs"
+  "length (sublists xs) = 2 ^ length xs"
   by (induct xs) (simp_all add: Let_def)
 
 lemma sublists_powset:
@@ -484,9 +484,9 @@
   shows "distinct (map set (sublists xs))"
 proof (rule card_distinct)
   have "finite (set xs)" by rule
-  then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow)
+  then have "card (Pow (set xs)) = 2 ^ card (set xs)" by (rule card_Pow)
   with assms distinct_card [of xs]
-    have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp
+    have "card (Pow (set xs)) = 2 ^ length xs" by simp
   then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
     by (simp add: sublists_powset length_sublists)
 qed
--- a/src/HOL/Finite_Set.thy	Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Mar 30 17:21:36 2012 +0200
@@ -2212,12 +2212,13 @@
 
 subsubsection {* Cardinality of the Powerset *}
 
-lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
+lemma card_Pow: "finite A ==> card (Pow A) = 2 ^ card A"
 apply (induct rule: finite_induct)
  apply (simp_all add: Pow_insert)
 apply (subst card_Un_disjoint, blast)
   apply (blast, blast)
 apply (subgoal_tac "inj_on (insert x) (Pow F)")
+ apply (subst mult_2)
  apply (simp add: card_image Pow_insert)
 apply (unfold inj_on_def)
 apply (blast elim!: equalityE)
--- a/src/HOL/Int.thy	Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/Int.thy	Fri Mar 30 17:21:36 2012 +0200
@@ -8,7 +8,6 @@
 theory Int
 imports Equiv_Relations Wellfounded
 uses
-  ("Tools/numeral.ML")
   ("Tools/int_arith.ML")
 begin
 
@@ -835,7 +834,6 @@
   of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
   of_int_0 of_int_1 of_int_add of_int_mult
 
-use "Tools/numeral.ML"
 use "Tools/int_arith.ML"
 declaration {* K Int_Arith.setup *}
 
@@ -844,16 +842,6 @@
   "(m::'a::linordered_idom) = n") =
   {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
 
-setup {*
-  Reorient_Proc.add
-    (fn Const (@{const_name numeral}, _) $ _ => true
-    | Const (@{const_name neg_numeral}, _) $ _ => true
-    | _ => false)
-*}
-
-simproc_setup reorient_numeral
-  ("numeral w = x" | "neg_numeral w = y") = Reorient_Proc.proc
-
 
 subsection{*Lemmas About Small Numerals*}
 
--- a/src/HOL/IsaMakefile	Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/IsaMakefile	Fri Mar 30 17:21:36 2012 +0200
@@ -1128,7 +1128,7 @@
   Library/Code_Integer.thy Library/Code_Nat.thy				\
   Library/Code_Natural.thy Library/Efficient_Nat.thy			\
   Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy		\
-  ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy	\
+  ex/Arith_Examples.thy ex/BT.thy					\
   ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy ex/CTL.thy		\
   ex/Case_Product.thy ex/Chinese.thy ex/Classical.thy			\
   ex/Code_Nat_examples.thy						\
--- a/src/HOL/Library/Cardinality.thy	Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/Library/Cardinality.thy	Fri Mar 30 17:21:36 2012 +0200
@@ -59,7 +59,7 @@
 
 lemma card_set [simp]: "CARD('a set) = 2 ^ CARD('a::finite)"
   unfolding Pow_UNIV [symmetric]
-  by (simp only: card_Pow finite numeral_2_eq_2)
+  by (simp only: card_Pow finite)
 
 lemma card_nat [simp]: "CARD(nat) = 0"
   by (simp add: card_eq_0_iff)
--- a/src/HOL/Library/Code_Integer.thy	Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/Library/Code_Integer.thy	Fri Mar 30 17:21:36 2012 +0200
@@ -22,7 +22,7 @@
 proof -
   have "2 = nat 2" by simp
   show ?thesis
-    apply (subst nat_mult_2 [symmetric])
+    apply (subst mult_2 [symmetric])
     apply (auto simp add: Let_def divmod_int_mod_div not_le
      nat_div_distrib nat_mult_distrib mult_div_cancel mod_2_not_eq_zero_eq_one_int)
     apply (unfold `2 = nat 2`)
--- a/src/HOL/Library/Formal_Power_Series.thy	Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Mar 30 17:21:36 2012 +0200
@@ -2781,7 +2781,7 @@
   
 lemma binomial_Vandermonde_same: "setsum (\<lambda>k. (n choose k)^2) {0..n} = (2*n) choose n"
   using binomial_Vandermonde[of n n n,symmetric]
-  unfolding nat_mult_2 apply (simp add: power2_eq_square)
+  unfolding mult_2 apply (simp add: power2_eq_square)
   apply (rule setsum_cong2)
   by (auto intro:  binomial_symmetric)
 
@@ -3139,7 +3139,7 @@
     moreover
     {assume on: "odd n"
       from on obtain m where m: "n = 2*m + 1" 
-        unfolding odd_nat_equiv_def2 by (auto simp add: nat_mult_2)  
+        unfolding odd_nat_equiv_def2 by (auto simp add: mult_2)  
       have "?l $n = ?r$n" 
         by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
           power_mult power_minus)}
--- a/src/HOL/Library/Target_Numeral.thy	Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/Library/Target_Numeral.thy	Fri Mar 30 17:21:36 2012 +0200
@@ -385,7 +385,7 @@
       by simp
     then have "num_of_nat (nat (int_of k)) =
       num_of_nat (nat (int_of k) div 2 + nat (int_of k) div 2 + nat (int_of k) mod 2)"
-      by (simp add: nat_mult_2)
+      by (simp add: mult_2)
     with ** have "num_of_nat (nat (int_of k)) =
       num_of_nat (nat (int_of k) div 2 + nat (int_of k) div 2 + 1)"
       by simp
@@ -395,7 +395,7 @@
     by (auto simp add: num_of_int_def nat_of_def Let_def prod_case_beta
       not_le Target_Numeral.int_eq_iff less_eq_int_def
       nat_mult_distrib nat_div_distrib num_of_nat_One num_of_nat_plus_distrib
-       nat_mult_2 aux add_One)
+       mult_2 [where 'a=nat] aux add_One)
 qed
 
 hide_const (open) int_of nat_of Pos Neg sub dup divmod_abs num_of_int
--- a/src/HOL/NSA/HSeries.thy	Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/NSA/HSeries.thy	Fri Mar 30 17:21:36 2012 +0200
@@ -114,7 +114,7 @@
 lemma sumhr_minus_one_realpow_zero [simp]: 
      "!!N. sumhr(0, N + N, %i. (-1) ^ (i+1)) = 0"
 unfolding sumhr_app
-by transfer (simp del: power_Suc add: nat_mult_2 [symmetric])
+by transfer (simp del: power_Suc add: mult_2 [symmetric])
 
 lemma sumhr_interval_const:
      "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na  
--- a/src/HOL/Nat_Numeral.thy	Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/Nat_Numeral.thy	Fri Mar 30 17:21:36 2012 +0200
@@ -61,17 +61,6 @@
 lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
 lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
 
-lemma nat_numeral_Bit0:
-  "numeral (Num.Bit0 w) = (let n::nat = numeral w in n + n)"
-  unfolding numeral_Bit0 Let_def ..
-
-lemma nat_numeral_Bit1:
-  "numeral (Num.Bit1 w) = (let n = numeral w in Suc (n + n))"
-  unfolding numeral_Bit1 Let_def by simp
-
-lemmas eval_nat_numeral =
-  nat_numeral_Bit0 nat_numeral_Bit1
-
 lemmas nat_arith =
   diff_nat_numeral
 
@@ -101,46 +90,14 @@
 lemma Suc_diff_eq_diff_pred: "0 < n ==> Suc m - n = m - (n - Numeral1)"
 by (simp split: nat_diff_split)
 
-text{*No longer required as a simprule because of the @{text inverse_fold}
-   simproc*}
-lemma Suc_diff_numeral: "Suc m - (numeral v) = m - (numeral v - 1)"
-  by (subst expand_Suc, simp only: diff_Suc_Suc)
-
 lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
 by (simp split: nat_diff_split)
 
 
-subsubsection{*For @{term nat_case} and @{term nat_rec}*}
-
-lemma nat_case_numeral [simp]:
-  "nat_case a f (numeral v) = (let pv = nat (numeral v - 1) in f pv)"
-  by (subst expand_Suc, simp only: nat.cases nat_numeral_diff_1 Let_def)
-
-lemma nat_case_add_eq_if [simp]:
-  "nat_case a f ((numeral v) + n) = (let pv = nat (numeral v - 1) in f (pv + n))"
-  by (subst expand_Suc, simp only: nat.cases nat_numeral_diff_1 Let_def add_Suc)
-
-lemma nat_rec_numeral [simp]:
-  "nat_rec a f (numeral v) = (let pv = nat (numeral v - 1) in f pv (nat_rec a f pv))"
-  by (subst expand_Suc, simp only: nat_rec_Suc nat_numeral_diff_1 Let_def)
-
-lemma nat_rec_add_eq_if [simp]:
-  "nat_rec a f (numeral v + n) =
-    (let pv = nat (numeral v - 1) in f (pv + n) (nat_rec a f (pv + n)))"
-  by (subst expand_Suc, simp only: nat_rec_Suc nat_numeral_diff_1 Let_def add_Suc)
-
-
 subsubsection{*Various Other Lemmas*}
 
 text {*Evens and Odds, for Mutilated Chess Board*}
 
-text{*Lemmas for specialist use, NOT as default simprules*}
-lemma nat_mult_2: "2 * z = (z+z::nat)"
-by (rule mult_2) (* FIXME: duplicate *)
-
-lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
-by (rule mult_2_right) (* FIXME: duplicate *)
-
 text{*Case analysis on @{term "n<2"}*}
 lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
 by (auto simp add: numeral_2_eq_2)
--- a/src/HOL/Num.thy	Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/Num.thy	Fri Mar 30 17:21:36 2012 +0200
@@ -7,6 +7,8 @@
 
 theory Num
 imports Datatype
+uses
+  ("Tools/numeral.ML")
 begin
 
 subsection {* The @{text num} type *}
@@ -331,6 +333,9 @@
     (@{const_syntax neg_numeral}, num_tr' "-")] end
 *}
 
+use "Tools/numeral.ML"
+
+
 subsection {* Class-specific numeral rules *}
 
 text {*
@@ -507,7 +512,7 @@
 lemma numeral_mult: "numeral (m * n) = numeral m * numeral n"
   apply (induct n rule: num_induct)
   apply (simp add: numeral_One)
-  apply (simp add: mult_inc numeral_inc numeral_add numeral_inc right_distrib)
+  apply (simp add: mult_inc numeral_inc numeral_add right_distrib)
   done
 
 lemma numeral_times_numeral: "numeral m * numeral n = numeral (m * n)"
@@ -869,8 +874,7 @@
 lemma numeral_eq_Suc: "numeral k = Suc (pred_numeral k)"
   unfolding pred_numeral_def by simp
 
-lemma nat_number:
-  "1 = Suc 0"
+lemma eval_nat_numeral:
   "numeral One = Suc 0"
   "numeral (Bit0 n) = Suc (numeral (BitM n))"
   "numeral (Bit1 n) = Suc (numeral (Bit0 n))"
@@ -880,14 +884,14 @@
   "pred_numeral Num.One = 0"
   "pred_numeral (Num.Bit0 k) = numeral (Num.BitM k)"
   "pred_numeral (Num.Bit1 k) = numeral (Num.Bit0 k)"
-  unfolding pred_numeral_def nat_number
+  unfolding pred_numeral_def eval_nat_numeral
   by (simp_all only: diff_Suc_Suc diff_0)
 
 lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
-  by (simp add: nat_number(2-4))
+  by (simp add: eval_nat_numeral)
 
 lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
-  by (simp add: nat_number(2-4))
+  by (simp add: eval_nat_numeral)
 
 lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
   by (simp only: numeral_One One_nat_def)
@@ -919,6 +923,12 @@
 lemma le_Suc_numeral [simp]: "Suc n \<le> numeral k \<longleftrightarrow> n \<le> pred_numeral k"
   by (simp add: numeral_eq_Suc)
 
+lemma diff_Suc_numeral [simp]: "Suc n - numeral k = n - pred_numeral k"
+  by (simp add: numeral_eq_Suc)
+
+lemma diff_numeral_Suc [simp]: "numeral k - Suc n = pred_numeral k - n"
+  by (simp add: numeral_eq_Suc)
+
 lemma max_Suc_numeral [simp]:
   "max (Suc n) (numeral k) = Suc (max n (pred_numeral k))"
   by (simp add: numeral_eq_Suc)
@@ -935,6 +945,26 @@
   "min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)"
   by (simp add: numeral_eq_Suc)
 
+text {* For @{term nat_case} and @{term nat_rec}. *}
+
+lemma nat_case_numeral [simp]:
+  "nat_case a f (numeral v) = (let pv = pred_numeral v in f pv)"
+  by (simp add: numeral_eq_Suc)
+
+lemma nat_case_add_eq_if [simp]:
+  "nat_case a f ((numeral v) + n) = (let pv = pred_numeral v in f (pv + n))"
+  by (simp add: numeral_eq_Suc)
+
+lemma nat_rec_numeral [simp]:
+  "nat_rec a f (numeral v) =
+    (let pv = pred_numeral v in f pv (nat_rec a f pv))"
+  by (simp add: numeral_eq_Suc Let_def)
+
+lemma nat_rec_add_eq_if [simp]:
+  "nat_rec a f (numeral v + n) =
+    (let pv = pred_numeral v in f (pv + n) (nat_rec a f (pv + n)))"
+  by (simp add: numeral_eq_Suc Let_def)
+
 
 subsection {* Numeral equations as default simplification rules *}
 
@@ -950,10 +980,6 @@
 
 subsection {* Setting up simprocs *}
 
-lemma numeral_reorient:
-  "(numeral w = x) = (x = numeral w)"
-  by auto
-
 lemma mult_numeral_1: "Numeral1 * a = (a::'a::semiring_numeral)"
   by simp
 
@@ -974,6 +1000,16 @@
   mult_numeral_1 mult_numeral_1_right 
   mult_minus1 mult_minus1_right
 
+setup {*
+  Reorient_Proc.add
+    (fn Const (@{const_name numeral}, _) $ _ => true
+    | Const (@{const_name neg_numeral}, _) $ _ => true
+    | _ => false)
+*}
+
+simproc_setup reorient_numeral
+  ("numeral w = x" | "neg_numeral w = y") = Reorient_Proc.proc
+
 
 subsubsection {* Simplification of arithmetic operations on integer constants. *}
 
--- a/src/HOL/Parity.thy	Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/Parity.thy	Fri Mar 30 17:21:36 2012 +0200
@@ -45,11 +45,20 @@
 
 lemma odd_1_nat [simp]: "odd (1::nat)" by presburger
 
+lemma even_numeral_int [simp]: "even (numeral (Num.Bit0 k) :: int)"
+  unfolding even_def by simp
+
+lemma odd_numeral_int [simp]: "odd (numeral (Num.Bit1 k) :: int)"
+  unfolding even_def by simp
+
 (* TODO: proper simp rules for Num.Bit0, Num.Bit1 *)
-declare even_def[of "numeral v", simp] for v
 declare even_def[of "neg_numeral v", simp] for v
 
-declare even_nat_def[of "numeral v", simp] for v
+lemma even_numeral_nat [simp]: "even (numeral (Num.Bit0 k) :: nat)"
+  unfolding even_nat_def by simp
+
+lemma odd_numeral_nat [simp]: "odd (numeral (Num.Bit1 k) :: nat)"
+  unfolding even_nat_def by simp
 
 subsection {* Even and odd are mutually exclusive *}
 
@@ -349,10 +358,6 @@
 
 text {* Simplify, when the exponent is a numeral *}
 
-lemma power_0_left_numeral [simp]:
-  "0 ^ numeral w = (0::'a::{power,semiring_0})"
-by (simp add: power_0_left)
-
 lemmas zero_le_power_eq_numeral [simp] =
     zero_le_power_eq [of _ "numeral w"] for w
 
--- a/src/HOL/Power.thy	Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/Power.thy	Fri Mar 30 17:21:36 2012 +0200
@@ -185,7 +185,7 @@
 
 lemma power_minus_Bit1:
   "(- x) ^ numeral (Num.Bit1 k) = - (x ^ numeral (Num.Bit1 k))"
-  by (simp only: nat_number(4) power_Suc power_minus_Bit0 mult_minus_left)
+  by (simp only: eval_nat_numeral(3) power_Suc power_minus_Bit0 mult_minus_left)
 
 lemma power_neg_numeral_Bit0 [simp]:
   "neg_numeral k ^ numeral (Num.Bit0 l) = numeral (Num.pow k (Num.Bit0 l))"
--- a/src/HOL/SetInterval.thy	Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/SetInterval.thy	Fri Mar 30 17:21:36 2012 +0200
@@ -1282,19 +1282,21 @@
 
 subsection {* The formula for arithmetic sums *}
 
-lemma gauss_sum: (* FIXME: rephrase in terms of "2" *)
-  "((1::'a::comm_semiring_1) + 1)*(\<Sum>i\<in>{1..n}. of_nat i) =
+lemma gauss_sum:
+  "(2::'a::comm_semiring_1)*(\<Sum>i\<in>{1..n}. of_nat i) =
    of_nat n*((of_nat n)+1)"
 proof (induct n)
   case 0
   show ?case by simp
 next
   case (Suc n)
-  then show ?case by (simp add: algebra_simps del: one_add_one) (* FIXME *)
+  then show ?case
+    by (simp add: algebra_simps add: one_add_one [symmetric] del: one_add_one)
+      (* FIXME: make numeral cancellation simprocs work for semirings *)
 qed
 
 theorem arith_series_general:
-  "((1::'a::comm_semiring_1) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
+  "(2::'a::comm_semiring_1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
   of_nat n * (a + (a + of_nat(n - 1)*d))"
 proof cases
   assume ngt1: "n > 1"
@@ -1307,26 +1309,27 @@
   also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
     unfolding One_nat_def
     by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt mult_ac)
-  also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)"
-    by (simp add: left_distrib right_distrib del: one_add_one)
+  also have "2*\<dots> = 2*?n*a + d*2*(\<Sum>i\<in>{1..<n}. ?I i)"
+    by (simp add: algebra_simps)
   also from ngt1 have "{1..<n} = {1..n - 1}"
     by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
   also from ngt1
-  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)"
+  have "2*?n*a + d*2*(\<Sum>i\<in>{1..n - 1}. ?I i) = (2*?n*a + d*?I (n - 1)*?I n)"
     by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def)
        (simp add:  mult_ac trans [OF add_commute of_nat_Suc [symmetric]])
-  finally show ?thesis by (simp add: algebra_simps del: one_add_one)
+  finally show ?thesis
+    unfolding mult_2 by (simp add: algebra_simps)
 next
   assume "\<not>(n > 1)"
   hence "n = 1 \<or> n = 0" by auto
-  thus ?thesis by (auto simp: algebra_simps mult_2_right)
+  thus ?thesis by (auto simp: mult_2)
 qed
 
 lemma arith_series_nat:
-  "Suc (Suc 0) * (\<Sum>i\<in>{..<n}. a+i*d) = n * (a + (a+(n - 1)*d))"
+  "(2::nat) * (\<Sum>i\<in>{..<n}. a+i*d) = n * (a + (a+(n - 1)*d))"
 proof -
   have
-    "((1::nat) + 1) * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) =
+    "2 * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) =
     of_nat(n) * (a + (a + of_nat(n - 1)*d))"
     by (rule arith_series_general)
   thus ?thesis
@@ -1334,15 +1337,8 @@
 qed
 
 lemma arith_series_int:
-  "(2::int) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
-  of_nat n * (a + (a + of_nat(n - 1)*d))"
-proof -
-  have
-    "((1::int) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
-    of_nat(n) * (a + (a + of_nat(n - 1)*d))"
-    by (rule arith_series_general)
-  thus ?thesis by simp
-qed
+  "2 * (\<Sum>i\<in>{..<n}. a + int i * d) = int n * (a + (a + int(n - 1)*d))"
+  by (fact arith_series_general) (* FIXME: duplicate *)
 
 lemma sum_diff_distrib:
   fixes P::"nat\<Rightarrow>nat"
--- a/src/HOL/Word/Bit_Int.thy	Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/Word/Bit_Int.thy	Fri Mar 30 17:21:36 2012 +0200
@@ -501,8 +501,8 @@
 
 lemma bin_sc_numeral [simp]:
   "bin_sc (numeral k) b w =
-    bin_sc (numeral k - 1) b (bin_rest w) BIT bin_last w"
-  by (subst expand_Suc, rule bin_sc.Suc)
+    bin_sc (pred_numeral k) b (bin_rest w) BIT bin_last w"
+  by (simp add: numeral_eq_Suc)
 
 
 subsection {* Splitting and concatenation *}
--- a/src/HOL/Word/Bit_Representation.thy	Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/Word/Bit_Representation.thy	Fri Mar 30 17:21:36 2012 +0200
@@ -229,8 +229,8 @@
   by (cases n) auto
 
 lemma bin_nth_numeral:
-  "bin_rest x = y \<Longrightarrow> bin_nth x (numeral n) = bin_nth y (numeral n - 1)"
-  by (subst expand_Suc, simp only: bin_nth.simps)
+  "bin_rest x = y \<Longrightarrow> bin_nth x (numeral n) = bin_nth y (pred_numeral n)"
+  by (simp add: numeral_eq_Suc)
 
 lemmas bin_nth_numeral_simps [simp] =
   bin_nth_numeral [OF bin_rest_numeral_simps(2)]
@@ -543,35 +543,35 @@
 
 lemma bintrunc_numeral:
   "bintrunc (numeral k) x =
-    bintrunc (numeral k - 1) (bin_rest x) BIT bin_last x"
-  by (subst expand_Suc, rule bintrunc.simps)
+    bintrunc (pred_numeral k) (bin_rest x) BIT bin_last x"
+  by (simp add: numeral_eq_Suc)
 
 lemma sbintrunc_numeral:
   "sbintrunc (numeral k) x =
-    sbintrunc (numeral k - 1) (bin_rest x) BIT bin_last x"
-  by (subst expand_Suc, rule sbintrunc.simps)
+    sbintrunc (pred_numeral k) (bin_rest x) BIT bin_last x"
+  by (simp add: numeral_eq_Suc)
 
 lemma bintrunc_numeral_simps [simp]:
   "bintrunc (numeral k) (numeral (Num.Bit0 w)) =
-    bintrunc (numeral k - 1) (numeral w) BIT 0"
+    bintrunc (pred_numeral k) (numeral w) BIT 0"
   "bintrunc (numeral k) (numeral (Num.Bit1 w)) =
-    bintrunc (numeral k - 1) (numeral w) BIT 1"
+    bintrunc (pred_numeral k) (numeral w) BIT 1"
   "bintrunc (numeral k) (neg_numeral (Num.Bit0 w)) =
-    bintrunc (numeral k - 1) (neg_numeral w) BIT 0"
+    bintrunc (pred_numeral k) (neg_numeral w) BIT 0"
   "bintrunc (numeral k) (neg_numeral (Num.Bit1 w)) =
-    bintrunc (numeral k - 1) (neg_numeral (w + Num.One)) BIT 1"
+    bintrunc (pred_numeral k) (neg_numeral (w + Num.One)) BIT 1"
   "bintrunc (numeral k) 1 = 1"
   by (simp_all add: bintrunc_numeral)
 
 lemma sbintrunc_numeral_simps [simp]:
   "sbintrunc (numeral k) (numeral (Num.Bit0 w)) =
-    sbintrunc (numeral k - 1) (numeral w) BIT 0"
+    sbintrunc (pred_numeral k) (numeral w) BIT 0"
   "sbintrunc (numeral k) (numeral (Num.Bit1 w)) =
-    sbintrunc (numeral k - 1) (numeral w) BIT 1"
+    sbintrunc (pred_numeral k) (numeral w) BIT 1"
   "sbintrunc (numeral k) (neg_numeral (Num.Bit0 w)) =
-    sbintrunc (numeral k - 1) (neg_numeral w) BIT 0"
+    sbintrunc (pred_numeral k) (neg_numeral w) BIT 0"
   "sbintrunc (numeral k) (neg_numeral (Num.Bit1 w)) =
-    sbintrunc (numeral k - 1) (neg_numeral (w + Num.One)) BIT 1"
+    sbintrunc (pred_numeral k) (neg_numeral (w + Num.One)) BIT 1"
   "sbintrunc (numeral k) 1 = 1"
   by (simp_all add: sbintrunc_numeral)
 
@@ -754,12 +754,12 @@
   by (cases n) simp_all
 
 lemma funpow_numeral [simp]:
-  "f ^^ numeral k = f \<circ> f ^^ (numeral k - 1)"
-  by (subst expand_Suc, rule funpow.simps)
+  "f ^^ numeral k = f \<circ> f ^^ (pred_numeral k)"
+  by (simp add: numeral_eq_Suc)
 
 lemma replicate_numeral [simp]: (* TODO: move to List.thy *)
-  "replicate (numeral k) x = x # replicate (numeral k - 1) x"
-  by (subst expand_Suc, rule replicate_Suc)
+  "replicate (numeral k) x = x # replicate (pred_numeral k) x"
+  by (simp add: numeral_eq_Suc)
 
 lemmas power_minus_simp = 
   trans [OF gen_minus [where f = "power f"] power_Suc] for f
--- a/src/HOL/Word/Bool_List_Representation.thy	Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy	Fri Mar 30 17:21:36 2012 +0200
@@ -633,12 +633,12 @@
   takefill_minus [symmetric, THEN trans]]
 
 lemma takefill_numeral_Nil [simp]:
-  "takefill fill (numeral k) [] = fill # takefill fill (numeral k - 1) []"
-  by (subst expand_Suc, rule takefill_Suc_Nil)
+  "takefill fill (numeral k) [] = fill # takefill fill (pred_numeral k) []"
+  by (simp add: numeral_eq_Suc)
 
 lemma takefill_numeral_Cons [simp]:
-  "takefill fill (numeral k) (x # xs) = x # takefill fill (numeral k - 1) xs"
-  by (subst expand_Suc, rule takefill_Suc_Cons)
+  "takefill fill (numeral k) (x # xs) = x # takefill fill (pred_numeral k) xs"
+  by (simp add: numeral_eq_Suc)
 
 (* links with function bl_to_bin *)
 
--- a/src/HOL/ex/Arithmetic_Series_Complex.thy	Fri Mar 30 15:25:47 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(*  Title:      HOL/ex/Arithmetic_Series_Complex.thy
-    Author:     Benjamin Porter, 2006
-*)
-
-
-header {* Arithmetic Series for Reals *}
-
-theory Arithmetic_Series_Complex
-imports Complex_Main 
-begin
-
-lemma arith_series_real:
-  "(2::real) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
-  of_nat n * (a + (a + of_nat(n - 1)*d))"
-proof -
-  have
-    "((1::real) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat(i)*d) =
-    of_nat(n) * (a + (a + of_nat(n - 1)*d))"
-    by (rule arith_series_general)
-  thus ?thesis by simp
-qed
-
-end
--- a/src/HOL/ex/ROOT.ML	Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Mar 30 17:21:36 2012 +0200
@@ -57,7 +57,6 @@
   "Sqrt",
   "Sqrt_Script",
   "Transfer_Ex",
-  "Arithmetic_Series_Complex",
   "HarmonicSeries",
   "Refute_Examples",
   "Landau",