# HG changeset patch # User wenzelm # Date 1333121134 -7200 # Node ID 3ff8c79a9e2f15033d78e242aea1e554bc4f0849 # Parent ba37aaead15556d7f4424ec3bff09b22d5e96e45# Parent 6584098d5378c4acadb740fde74b4db641fb6728 merged diff -r 6584098d5378 -r 3ff8c79a9e2f NEWS --- a/NEWS Fri Mar 30 17:22:17 2012 +0200 +++ b/NEWS Fri Mar 30 17:25:34 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: diff -r 6584098d5378 -r 3ff8c79a9e2f src/HOL/Divides.thy --- a/src/HOL/Divides.thy Fri Mar 30 17:22:17 2012 +0200 +++ b/src/HOL/Divides.thy Fri Mar 30 17:25:34 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\nat) mod 2 \ m mod 2 = 1" proof - diff -r 6584098d5378 -r 3ff8c79a9e2f src/HOL/Enum.thy --- a/src/HOL/Enum.thy Fri Mar 30 17:22:17 2012 +0200 +++ b/src/HOL/Enum.thy Fri Mar 30 17:25:34 2012 +0200 @@ -466,7 +466,7 @@ | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)" lemma length_sublists: - "length (sublists xs) = Suc (Suc (0\nat)) ^ length xs" + "length (sublists xs) = 2 ^ length xs" by (induct xs) (simp_all add: Let_def) lemma sublists_powset: @@ -485,9 +485,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 diff -r 6584098d5378 -r 3ff8c79a9e2f src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Fri Mar 30 17:22:17 2012 +0200 +++ b/src/HOL/Finite_Set.thy Fri Mar 30 17:25:34 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) diff -r 6584098d5378 -r 3ff8c79a9e2f src/HOL/Int.thy --- a/src/HOL/Int.thy Fri Mar 30 17:22:17 2012 +0200 +++ b/src/HOL/Int.thy Fri Mar 30 17:25:34 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*} diff -r 6584098d5378 -r 3ff8c79a9e2f src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Mar 30 17:22:17 2012 +0200 +++ b/src/HOL/IsaMakefile Fri Mar 30 17:25:34 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 \ diff -r 6584098d5378 -r 3ff8c79a9e2f src/HOL/Library/Cardinality.thy --- a/src/HOL/Library/Cardinality.thy Fri Mar 30 17:22:17 2012 +0200 +++ b/src/HOL/Library/Cardinality.thy Fri Mar 30 17:25:34 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) diff -r 6584098d5378 -r 3ff8c79a9e2f src/HOL/Library/Code_Integer.thy --- a/src/HOL/Library/Code_Integer.thy Fri Mar 30 17:22:17 2012 +0200 +++ b/src/HOL/Library/Code_Integer.thy Fri Mar 30 17:25:34 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`) diff -r 6584098d5378 -r 3ff8c79a9e2f src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Fri Mar 30 17:22:17 2012 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Fri Mar 30 17:25:34 2012 +0200 @@ -2781,7 +2781,7 @@ lemma binomial_Vandermonde_same: "setsum (\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)} diff -r 6584098d5378 -r 3ff8c79a9e2f src/HOL/Library/Target_Numeral.thy --- a/src/HOL/Library/Target_Numeral.thy Fri Mar 30 17:22:17 2012 +0200 +++ b/src/HOL/Library/Target_Numeral.thy Fri Mar 30 17:25:34 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 diff -r 6584098d5378 -r 3ff8c79a9e2f src/HOL/NSA/HSeries.thy --- a/src/HOL/NSA/HSeries.thy Fri Mar 30 17:22:17 2012 +0200 +++ b/src/HOL/NSA/HSeries.thy Fri Mar 30 17:25:34 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: "(\n. m \ Suc n --> f n = r) & m \ na diff -r 6584098d5378 -r 3ff8c79a9e2f src/HOL/Nat_Numeral.thy --- a/src/HOL/Nat_Numeral.thy Fri Mar 30 17:22:17 2012 +0200 +++ b/src/HOL/Nat_Numeral.thy Fri Mar 30 17:25:34 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) diff -r 6584098d5378 -r 3ff8c79a9e2f src/HOL/Num.thy --- a/src/HOL/Num.thy Fri Mar 30 17:22:17 2012 +0200 +++ b/src/HOL/Num.thy Fri Mar 30 17:25:34 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 \ numeral k \ n \ 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. *} diff -r 6584098d5378 -r 3ff8c79a9e2f src/HOL/Parity.thy --- a/src/HOL/Parity.thy Fri Mar 30 17:22:17 2012 +0200 +++ b/src/HOL/Parity.thy Fri Mar 30 17:25:34 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 diff -r 6584098d5378 -r 3ff8c79a9e2f src/HOL/Power.thy --- a/src/HOL/Power.thy Fri Mar 30 17:22:17 2012 +0200 +++ b/src/HOL/Power.thy Fri Mar 30 17:25:34 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))" diff -r 6584098d5378 -r 3ff8c79a9e2f src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Fri Mar 30 17:22:17 2012 +0200 +++ b/src/HOL/SetInterval.thy Fri Mar 30 17:25:34 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)*(\i\{1..n}. of_nat i) = +lemma gauss_sum: + "(2::'a::comm_semiring_1)*(\i\{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) * (\i\{..i\{.. 1" @@ -1307,26 +1309,27 @@ also from ngt1 have "\ = (?n*a + d*(\i\{1.. = (1+1)*?n*a + d*(1+1)*(\i\{1.. = 2*?n*a + d*2*(\i\{1..i\{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)" + have "2*?n*a + d*2*(\i\{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 "\(n > 1)" hence "n = 1 \ 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) * (\i\{..i\{..i\{..i\{..i\{..i\{..i\{..nat" diff -r 6584098d5378 -r 3ff8c79a9e2f src/HOL/Word/Bit_Int.thy --- a/src/HOL/Word/Bit_Int.thy Fri Mar 30 17:22:17 2012 +0200 +++ b/src/HOL/Word/Bit_Int.thy Fri Mar 30 17:25:34 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 *} diff -r 6584098d5378 -r 3ff8c79a9e2f src/HOL/Word/Bit_Representation.thy --- a/src/HOL/Word/Bit_Representation.thy Fri Mar 30 17:22:17 2012 +0200 +++ b/src/HOL/Word/Bit_Representation.thy Fri Mar 30 17:25:34 2012 +0200 @@ -229,8 +229,8 @@ by (cases n) auto lemma bin_nth_numeral: - "bin_rest x = y \ bin_nth x (numeral n) = bin_nth y (numeral n - 1)" - by (subst expand_Suc, simp only: bin_nth.simps) + "bin_rest x = y \ 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 \ f ^^ (numeral k - 1)" - by (subst expand_Suc, rule funpow.simps) + "f ^^ numeral k = f \ 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 diff -r 6584098d5378 -r 3ff8c79a9e2f src/HOL/Word/Bool_List_Representation.thy --- a/src/HOL/Word/Bool_List_Representation.thy Fri Mar 30 17:22:17 2012 +0200 +++ b/src/HOL/Word/Bool_List_Representation.thy Fri Mar 30 17:25:34 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 *) diff -r 6584098d5378 -r 3ff8c79a9e2f src/HOL/ex/Arithmetic_Series_Complex.thy --- a/src/HOL/ex/Arithmetic_Series_Complex.thy Fri Mar 30 17:22:17 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) * (\i\{..i\{..