eliminiated neg_numeral in favour of - (numeral _)
authorhaftmann
Tue Nov 19 10:05:53 2013 +0100 (2013-11-19)
changeset 5448903ff4d1e6784
parent 54488 b60f1fab408c
child 54490 930409d43211
eliminiated neg_numeral in favour of - (numeral _)
NEWS
src/HOL/Archimedean_Field.thy
src/HOL/BNF/More_BNFs.thy
src/HOL/Code_Numeral.thy
src/HOL/Complex.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Divides.thy
src/HOL/GCD.thy
src/HOL/IMP/Hoare_Examples.thy
src/HOL/Int.thy
src/HOL/Library/Binomial.thy
src/HOL/Library/Bit.thy
src/HOL/Library/Code_Prolog.thy
src/HOL/Library/Code_Real_Approx_By_Float.thy
src/HOL/Library/Code_Target_Int.thy
src/HOL/Library/Extended.thy
src/HOL/Library/Float.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
src/HOL/List.thy
src/HOL/Matrix_LP/ComputeFloat.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NSA/HTranscendental.thy
src/HOL/NSA/HyperDef.thy
src/HOL/NSA/NSA.thy
src/HOL/NSA/NSComplex.thy
src/HOL/NSA/StarDef.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Num.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Numeral_Simprocs.thy
src/HOL/Parity.thy
src/HOL/Power.thy
src/HOL/Rat.thy
src/HOL/Real.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Rings.thy
src/HOL/SMT_Examples/SMT_Tests.thy
src/HOL/SMT_Examples/SMT_Word_Examples.certs
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/SMT/smt_builtin.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smt_utils.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/numeral.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Transcendental.thy
src/HOL/Word/Bit_Int.thy
src/HOL/Word/Bit_Representation.thy
src/HOL/Word/Word.thy
src/HOL/Word/WordBitwise.thy
     1.1 --- a/NEWS	Tue Nov 19 01:30:14 2013 +0100
     1.2 +++ b/NEWS	Tue Nov 19 10:05:53 2013 +0100
     1.3 @@ -18,6 +18,14 @@
     1.4      even_zero_(nat|int) ~> even_zero
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Abolished neg_numeral.
     1.8 +  * Canonical representation for minus one is "- 1".
     1.9 +  * Canonical representation for other negative numbers is "- (numeral _)".
    1.10 +  * When devising rules set for number calculation, consider the
    1.11 +    following cases: 0, 1, numeral _, - 1, - numeral _.
    1.12 +  * Syntax for negative numerals is mere input syntax.
    1.13 +INCOMPATBILITY.
    1.14 +
    1.15  * Elimination of fact duplicates:
    1.16      equals_zero_I ~> minus_unique
    1.17      diff_eq_0_iff_eq ~> right_minus_eq
     2.1 --- a/src/HOL/Archimedean_Field.thy	Tue Nov 19 01:30:14 2013 +0100
     2.2 +++ b/src/HOL/Archimedean_Field.thy	Tue Nov 19 10:05:53 2013 +0100
     2.3 @@ -204,8 +204,8 @@
     2.4  lemma floor_numeral [simp]: "floor (numeral v) = numeral v"
     2.5    using floor_of_int [of "numeral v"] by simp
     2.6  
     2.7 -lemma floor_neg_numeral [simp]: "floor (neg_numeral v) = neg_numeral v"
     2.8 -  using floor_of_int [of "neg_numeral v"] by simp
     2.9 +lemma floor_neg_numeral [simp]: "floor (- numeral v) = - numeral v"
    2.10 +  using floor_of_int [of "- numeral v"] by simp
    2.11  
    2.12  lemma zero_le_floor [simp]: "0 \<le> floor x \<longleftrightarrow> 0 \<le> x"
    2.13    by (simp add: le_floor_iff)
    2.14 @@ -218,7 +218,7 @@
    2.15    by (simp add: le_floor_iff)
    2.16  
    2.17  lemma neg_numeral_le_floor [simp]:
    2.18 -  "neg_numeral v \<le> floor x \<longleftrightarrow> neg_numeral v \<le> x"
    2.19 +  "- numeral v \<le> floor x \<longleftrightarrow> - numeral v \<le> x"
    2.20    by (simp add: le_floor_iff)
    2.21  
    2.22  lemma zero_less_floor [simp]: "0 < floor x \<longleftrightarrow> 1 \<le> x"
    2.23 @@ -232,7 +232,7 @@
    2.24    by (simp add: less_floor_iff)
    2.25  
    2.26  lemma neg_numeral_less_floor [simp]:
    2.27 -  "neg_numeral v < floor x \<longleftrightarrow> neg_numeral v + 1 \<le> x"
    2.28 +  "- numeral v < floor x \<longleftrightarrow> - numeral v + 1 \<le> x"
    2.29    by (simp add: less_floor_iff)
    2.30  
    2.31  lemma floor_le_zero [simp]: "floor x \<le> 0 \<longleftrightarrow> x < 1"
    2.32 @@ -246,7 +246,7 @@
    2.33    by (simp add: floor_le_iff)
    2.34  
    2.35  lemma floor_le_neg_numeral [simp]:
    2.36 -  "floor x \<le> neg_numeral v \<longleftrightarrow> x < neg_numeral v + 1"
    2.37 +  "floor x \<le> - numeral v \<longleftrightarrow> x < - numeral v + 1"
    2.38    by (simp add: floor_le_iff)
    2.39  
    2.40  lemma floor_less_zero [simp]: "floor x < 0 \<longleftrightarrow> x < 0"
    2.41 @@ -260,7 +260,7 @@
    2.42    by (simp add: floor_less_iff)
    2.43  
    2.44  lemma floor_less_neg_numeral [simp]:
    2.45 -  "floor x < neg_numeral v \<longleftrightarrow> x < neg_numeral v"
    2.46 +  "floor x < - numeral v \<longleftrightarrow> x < - numeral v"
    2.47    by (simp add: floor_less_iff)
    2.48  
    2.49  text {* Addition and subtraction of integers *}
    2.50 @@ -272,10 +272,6 @@
    2.51      "floor (x + numeral v) = floor x + numeral v"
    2.52    using floor_add_of_int [of x "numeral v"] by simp
    2.53  
    2.54 -lemma floor_add_neg_numeral [simp]:
    2.55 -    "floor (x + neg_numeral v) = floor x + neg_numeral v"
    2.56 -  using floor_add_of_int [of x "neg_numeral v"] by simp
    2.57 -
    2.58  lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1"
    2.59    using floor_add_of_int [of x 1] by simp
    2.60  
    2.61 @@ -286,10 +282,6 @@
    2.62    "floor (x - numeral v) = floor x - numeral v"
    2.63    using floor_diff_of_int [of x "numeral v"] by simp
    2.64  
    2.65 -lemma floor_diff_neg_numeral [simp]:
    2.66 -  "floor (x - neg_numeral v) = floor x - neg_numeral v"
    2.67 -  using floor_diff_of_int [of x "neg_numeral v"] by simp
    2.68 -
    2.69  lemma floor_diff_one [simp]: "floor (x - 1) = floor x - 1"
    2.70    using floor_diff_of_int [of x 1] by simp
    2.71  
    2.72 @@ -353,8 +345,8 @@
    2.73  lemma ceiling_numeral [simp]: "ceiling (numeral v) = numeral v"
    2.74    using ceiling_of_int [of "numeral v"] by simp
    2.75  
    2.76 -lemma ceiling_neg_numeral [simp]: "ceiling (neg_numeral v) = neg_numeral v"
    2.77 -  using ceiling_of_int [of "neg_numeral v"] by simp
    2.78 +lemma ceiling_neg_numeral [simp]: "ceiling (- numeral v) = - numeral v"
    2.79 +  using ceiling_of_int [of "- numeral v"] by simp
    2.80  
    2.81  lemma ceiling_le_zero [simp]: "ceiling x \<le> 0 \<longleftrightarrow> x \<le> 0"
    2.82    by (simp add: ceiling_le_iff)
    2.83 @@ -367,7 +359,7 @@
    2.84    by (simp add: ceiling_le_iff)
    2.85  
    2.86  lemma ceiling_le_neg_numeral [simp]:
    2.87 -  "ceiling x \<le> neg_numeral v \<longleftrightarrow> x \<le> neg_numeral v"
    2.88 +  "ceiling x \<le> - numeral v \<longleftrightarrow> x \<le> - numeral v"
    2.89    by (simp add: ceiling_le_iff)
    2.90  
    2.91  lemma ceiling_less_zero [simp]: "ceiling x < 0 \<longleftrightarrow> x \<le> -1"
    2.92 @@ -381,7 +373,7 @@
    2.93    by (simp add: ceiling_less_iff)
    2.94  
    2.95  lemma ceiling_less_neg_numeral [simp]:
    2.96 -  "ceiling x < neg_numeral v \<longleftrightarrow> x \<le> neg_numeral v - 1"
    2.97 +  "ceiling x < - numeral v \<longleftrightarrow> x \<le> - numeral v - 1"
    2.98    by (simp add: ceiling_less_iff)
    2.99  
   2.100  lemma zero_le_ceiling [simp]: "0 \<le> ceiling x \<longleftrightarrow> -1 < x"
   2.101 @@ -395,7 +387,7 @@
   2.102    by (simp add: le_ceiling_iff)
   2.103  
   2.104  lemma neg_numeral_le_ceiling [simp]:
   2.105 -  "neg_numeral v \<le> ceiling x \<longleftrightarrow> neg_numeral v - 1 < x"
   2.106 +  "- numeral v \<le> ceiling x \<longleftrightarrow> - numeral v - 1 < x"
   2.107    by (simp add: le_ceiling_iff)
   2.108  
   2.109  lemma zero_less_ceiling [simp]: "0 < ceiling x \<longleftrightarrow> 0 < x"
   2.110 @@ -409,7 +401,7 @@
   2.111    by (simp add: less_ceiling_iff)
   2.112  
   2.113  lemma neg_numeral_less_ceiling [simp]:
   2.114 -  "neg_numeral v < ceiling x \<longleftrightarrow> neg_numeral v < x"
   2.115 +  "- numeral v < ceiling x \<longleftrightarrow> - numeral v < x"
   2.116    by (simp add: less_ceiling_iff)
   2.117  
   2.118  text {* Addition and subtraction of integers *}
   2.119 @@ -421,10 +413,6 @@
   2.120      "ceiling (x + numeral v) = ceiling x + numeral v"
   2.121    using ceiling_add_of_int [of x "numeral v"] by simp
   2.122  
   2.123 -lemma ceiling_add_neg_numeral [simp]:
   2.124 -    "ceiling (x + neg_numeral v) = ceiling x + neg_numeral v"
   2.125 -  using ceiling_add_of_int [of x "neg_numeral v"] by simp
   2.126 -
   2.127  lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1"
   2.128    using ceiling_add_of_int [of x 1] by simp
   2.129  
   2.130 @@ -435,10 +423,6 @@
   2.131    "ceiling (x - numeral v) = ceiling x - numeral v"
   2.132    using ceiling_diff_of_int [of x "numeral v"] by simp
   2.133  
   2.134 -lemma ceiling_diff_neg_numeral [simp]:
   2.135 -  "ceiling (x - neg_numeral v) = ceiling x - neg_numeral v"
   2.136 -  using ceiling_diff_of_int [of x "neg_numeral v"] by simp
   2.137 -
   2.138  lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1"
   2.139    using ceiling_diff_of_int [of x 1] by simp
   2.140  
     3.1 --- a/src/HOL/BNF/More_BNFs.thy	Tue Nov 19 01:30:14 2013 +0100
     3.2 +++ b/src/HOL/BNF/More_BNFs.thy	Tue Nov 19 10:05:53 2013 +0100
     3.3 @@ -973,8 +973,7 @@
     3.4    using finite_Collect_mem .
     3.5    ultimately have fin: "finite {b. \<exists>a. f a = b \<and> a \<in># M}" by(rule finite_subset)
     3.6    have i: "inj_on A ?B" unfolding inj_on_def A_def apply clarsimp
     3.7 -  by (metis (lifting, mono_tags) mem_Collect_eq rel_simps(54)
     3.8 -                                 setsum_gt_0_iff setsum_infinite)
     3.9 +    by (metis (lifting, full_types) mem_Collect_eq neq0_conv setsum.neutral)
    3.10    have 0: "\<And> b. 0 < setsum (count M) (A b) \<longleftrightarrow> (\<exists> a \<in> A b. count M a > 0)"
    3.11    apply safe
    3.12      apply (metis less_not_refl setsum_gt_0_iff setsum_infinite)
     4.1 --- a/src/HOL/Code_Numeral.thy	Tue Nov 19 01:30:14 2013 +0100
     4.2 +++ b/src/HOL/Code_Numeral.thy	Tue Nov 19 10:05:53 2013 +0100
     4.3 @@ -96,10 +96,6 @@
     4.4  qed
     4.5  
     4.6  lemma [transfer_rule]:
     4.7 -  "fun_rel HOL.eq pcr_integer (neg_numeral :: num \<Rightarrow> int) (neg_numeral :: num \<Rightarrow> integer)"
     4.8 -  by (unfold neg_numeral_def [abs_def]) transfer_prover
     4.9 -
    4.10 -lemma [transfer_rule]:
    4.11    "fun_rel HOL.eq (fun_rel HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
    4.12    by (unfold Num.sub_def [abs_def]) transfer_prover
    4.13  
    4.14 @@ -147,10 +143,6 @@
    4.15    "int_of_integer (numeral k) = numeral k"
    4.16    by transfer rule
    4.17  
    4.18 -lemma int_of_integer_neg_numeral [simp]:
    4.19 -  "int_of_integer (neg_numeral k) = neg_numeral k"
    4.20 -  by transfer rule
    4.21 -
    4.22  lemma int_of_integer_sub [simp]:
    4.23    "int_of_integer (Num.sub k l) = Num.sub k l"
    4.24    by transfer rule
    4.25 @@ -253,11 +245,11 @@
    4.26  
    4.27  definition Neg :: "num \<Rightarrow> integer"
    4.28  where
    4.29 -  [simp, code_abbrev]: "Neg = neg_numeral"
    4.30 +  [simp, code_abbrev]: "Neg n = - Pos n"
    4.31  
    4.32  lemma [transfer_rule]:
    4.33 -  "fun_rel HOL.eq pcr_integer neg_numeral Neg"
    4.34 -  by simp transfer_prover
    4.35 +  "fun_rel HOL.eq pcr_integer (\<lambda>n. - numeral n) Neg"
    4.36 +  by (simp add: Neg_def [abs_def]) transfer_prover
    4.37  
    4.38  code_datatype "0::integer" Pos Neg
    4.39  
    4.40 @@ -272,7 +264,7 @@
    4.41    "dup 0 = 0"
    4.42    "dup (Pos n) = Pos (Num.Bit0 n)"
    4.43    "dup (Neg n) = Neg (Num.Bit0 n)"
    4.44 -  by (transfer, simp only: neg_numeral_def numeral_Bit0 minus_add_distrib)+
    4.45 +  by (transfer, simp only: numeral_Bit0 minus_add_distrib)+
    4.46  
    4.47  lift_definition sub :: "num \<Rightarrow> num \<Rightarrow> integer"
    4.48    is "\<lambda>m n. numeral m - numeral n :: int"
     5.1 --- a/src/HOL/Complex.thy	Tue Nov 19 01:30:14 2013 +0100
     5.2 +++ b/src/HOL/Complex.thy	Tue Nov 19 10:05:53 2013 +0100
     5.3 @@ -108,7 +108,12 @@
     5.4  definition complex_divide_def:
     5.5    "x / (y\<Colon>complex) = x * inverse y"
     5.6  
     5.7 -lemma Complex_eq_1 [simp]: "(Complex a b = 1) = (a = 1 \<and> b = 0)"
     5.8 +lemma Complex_eq_1 [simp]:
     5.9 +  "Complex a b = 1 \<longleftrightarrow> a = 1 \<and> b = 0"
    5.10 +  by (simp add: complex_one_def)
    5.11 +
    5.12 +lemma Complex_eq_neg_1 [simp]:
    5.13 +  "Complex a b = - 1 \<longleftrightarrow> a = - 1 \<and> b = 0"
    5.14    by (simp add: complex_one_def)
    5.15  
    5.16  lemma complex_Re_one [simp]: "Re 1 = 1"
    5.17 @@ -166,21 +171,21 @@
    5.18  lemma complex_Re_numeral [simp]: "Re (numeral v) = numeral v"
    5.19    using complex_Re_of_int [of "numeral v"] by simp
    5.20  
    5.21 -lemma complex_Re_neg_numeral [simp]: "Re (neg_numeral v) = neg_numeral v"
    5.22 -  using complex_Re_of_int [of "neg_numeral v"] by simp
    5.23 +lemma complex_Re_neg_numeral [simp]: "Re (- numeral v) = - numeral v"
    5.24 +  using complex_Re_of_int [of "- numeral v"] by simp
    5.25  
    5.26  lemma complex_Im_numeral [simp]: "Im (numeral v) = 0"
    5.27    using complex_Im_of_int [of "numeral v"] by simp
    5.28  
    5.29 -lemma complex_Im_neg_numeral [simp]: "Im (neg_numeral v) = 0"
    5.30 -  using complex_Im_of_int [of "neg_numeral v"] by simp
    5.31 +lemma complex_Im_neg_numeral [simp]: "Im (- numeral v) = 0"
    5.32 +  using complex_Im_of_int [of "- numeral v"] by simp
    5.33  
    5.34  lemma Complex_eq_numeral [simp]:
    5.35 -  "(Complex a b = numeral w) = (a = numeral w \<and> b = 0)"
    5.36 +  "Complex a b = numeral w \<longleftrightarrow> a = numeral w \<and> b = 0"
    5.37    by (simp add: complex_eq_iff)
    5.38  
    5.39  lemma Complex_eq_neg_numeral [simp]:
    5.40 -  "(Complex a b = neg_numeral w) = (a = neg_numeral w \<and> b = 0)"
    5.41 +  "Complex a b = - numeral w \<longleftrightarrow> a = - numeral w \<and> b = 0"
    5.42    by (simp add: complex_eq_iff)
    5.43  
    5.44  
    5.45 @@ -421,7 +426,7 @@
    5.46  lemma complex_i_not_numeral [simp]: "ii \<noteq> numeral w"
    5.47    by (simp add: complex_eq_iff)
    5.48  
    5.49 -lemma complex_i_not_neg_numeral [simp]: "ii \<noteq> neg_numeral w"
    5.50 +lemma complex_i_not_neg_numeral [simp]: "ii \<noteq> - numeral w"
    5.51    by (simp add: complex_eq_iff)
    5.52  
    5.53  lemma i_mult_Complex [simp]: "ii * Complex a b = Complex (- b) a"
    5.54 @@ -508,7 +513,7 @@
    5.55  lemma complex_cnj_numeral [simp]: "cnj (numeral w) = numeral w"
    5.56    by (simp add: complex_eq_iff)
    5.57  
    5.58 -lemma complex_cnj_neg_numeral [simp]: "cnj (neg_numeral w) = neg_numeral w"
    5.59 +lemma complex_cnj_neg_numeral [simp]: "cnj (- numeral w) = - numeral w"
    5.60    by (simp add: complex_eq_iff)
    5.61  
    5.62  lemma complex_cnj_scaleR: "cnj (scaleR r x) = scaleR r (cnj x)"
     6.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Tue Nov 19 01:30:14 2013 +0100
     6.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Nov 19 10:05:53 2013 +0100
     6.3 @@ -11,8 +11,10 @@
     6.4    "~~/src/HOL/Library/Code_Target_Numeral"
     6.5  begin
     6.6  
     6.7 -declare powr_numeral[simp]
     6.8 -declare powr_neg_numeral[simp]
     6.9 +declare powr_one [simp]
    6.10 +declare powr_numeral [simp]
    6.11 +declare powr_neg_one [simp]
    6.12 +declare powr_neg_numeral [simp]
    6.13  
    6.14  section "Horner Scheme"
    6.15  
    6.16 @@ -1261,8 +1263,8 @@
    6.17          unfolding cos_periodic_int ..
    6.18        also have "\<dots> \<le> cos ((?ux - 2 * ?lpi))"
    6.19          using cos_monotone_minus_pi_0'[OF pi_x x_le_ux ux_0]
    6.20 -        by (simp only: minus_float.rep_eq real_of_int_minus real_of_one minus_one[symmetric]
    6.21 -            mult_minus_left mult_1_left) simp
    6.22 +        by (simp only: minus_float.rep_eq real_of_int_minus real_of_one
    6.23 +          mult_minus_left mult_1_left) simp
    6.24        also have "\<dots> = cos ((- (?ux - 2 * ?lpi)))"
    6.25          unfolding uminus_float.rep_eq cos_minus ..
    6.26        also have "\<dots> \<le> (ub_cos prec (- (?ux - 2 * ?lpi)))"
    6.27 @@ -1306,7 +1308,7 @@
    6.28        also have "\<dots> \<le> cos ((?lx + 2 * ?lpi))"
    6.29          using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
    6.30          by (simp only: minus_float.rep_eq real_of_int_minus real_of_one
    6.31 -          minus_one[symmetric] mult_minus_left mult_1_left) simp
    6.32 +          mult_minus_left mult_1_left) simp
    6.33        also have "\<dots> \<le> (ub_cos prec (?lx + 2 * ?lpi))"
    6.34          using lb_cos[OF lx_0 pi_lx] by simp
    6.35        finally show ?thesis unfolding u by (simp add: real_of_float_max)
    6.36 @@ -2104,8 +2106,9 @@
    6.37  lemma interpret_floatarith_num:
    6.38    shows "interpret_floatarith (Num (Float 0 0)) vs = 0"
    6.39    and "interpret_floatarith (Num (Float 1 0)) vs = 1"
    6.40 +  and "interpret_floatarith (Num (Float (- 1) 0)) vs = - 1"
    6.41    and "interpret_floatarith (Num (Float (numeral a) 0)) vs = numeral a"
    6.42 -  and "interpret_floatarith (Num (Float (neg_numeral a) 0)) vs = neg_numeral a" by auto
    6.43 +  and "interpret_floatarith (Num (Float (- numeral a) 0)) vs = - numeral a" by auto
    6.44  
    6.45  subsection "Implement approximation function"
    6.46  
     7.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Tue Nov 19 01:30:14 2013 +0100
     7.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Tue Nov 19 10:05:53 2013 +0100
     7.3 @@ -2006,9 +2006,10 @@
     7.4        | SOME n => @{code Bound} (@{code nat_of_integer} n))
     7.5    | num_of_term vs @{term "0::int"} = @{code C} (@{code int_of_integer} 0)
     7.6    | num_of_term vs @{term "1::int"} = @{code C} (@{code int_of_integer} 1)
     7.7 +  | num_of_term vs @{term "- 1::int"} = @{code C} (@{code int_of_integer} (~ 1))
     7.8    | num_of_term vs (@{term "numeral :: _ \<Rightarrow> int"} $ t) =
     7.9        @{code C} (@{code int_of_integer} (HOLogic.dest_num t))
    7.10 -  | num_of_term vs (@{term "neg_numeral :: _ \<Rightarrow> int"} $ t) =
    7.11 +  | num_of_term vs (@{term "- numeral :: _ \<Rightarrow> int"} $ t) =
    7.12        @{code C} (@{code int_of_integer} (~(HOLogic.dest_num t)))
    7.13    | num_of_term vs (Bound i) = @{code Bound} (@{code nat_of_integer} i)
    7.14    | num_of_term vs (@{term "uminus :: int \<Rightarrow> int"} $ t') = @{code Neg} (num_of_term vs t')
     8.1 --- a/src/HOL/Decision_Procs/MIR.thy	Tue Nov 19 01:30:14 2013 +0100
     8.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Tue Nov 19 10:05:53 2013 +0100
     8.3 @@ -3154,7 +3154,7 @@
     8.4      hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = (- ?N i e + real j1) - 1"
     8.5        by (simp only: algebra_simps)
     8.6          hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = - 1 - ?N i e + real j1"
     8.7 -          by (simp add: algebra_simps minus_one [symmetric] del: minus_one)
     8.8 +          by (simp add: algebra_simps)
     8.9      with nob  have ?case by blast }
    8.10    ultimately show ?case by blast
    8.11  next
    8.12 @@ -5549,6 +5549,7 @@
    8.13    | num_of_term vs @{term "real (1::int)"} = mk_C 1
    8.14    | num_of_term vs @{term "0::real"} = mk_C 0
    8.15    | num_of_term vs @{term "1::real"} = mk_C 1
    8.16 +  | num_of_term vs @{term "- 1::real"} = mk_C (~ 1)
    8.17    | num_of_term vs (Bound i) = mk_Bound i
    8.18    | num_of_term vs (@{term "uminus :: real \<Rightarrow> real"} $ t') = @{code Neg} (num_of_term vs t')
    8.19    | num_of_term vs (@{term "op + :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
    8.20 @@ -5561,7 +5562,7 @@
    8.21          | _ => error "num_of_term: unsupported Multiplication")
    8.22    | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "numeral :: _ \<Rightarrow> int"} $ t')) =
    8.23        mk_C (HOLogic.dest_num t')
    8.24 -  | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "neg_numeral :: _ \<Rightarrow> int"} $ t')) =
    8.25 +  | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "- numeral :: _ \<Rightarrow> int"} $ t')) =
    8.26        mk_C (~ (HOLogic.dest_num t'))
    8.27    | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "floor :: real \<Rightarrow> int"} $ t')) =
    8.28        @{code Floor} (num_of_term vs t')
    8.29 @@ -5569,7 +5570,7 @@
    8.30        @{code Neg} (@{code Floor} (@{code Neg} (num_of_term vs t')))
    8.31    | num_of_term vs (@{term "numeral :: _ \<Rightarrow> real"} $ t') =
    8.32        mk_C (HOLogic.dest_num t')
    8.33 -  | num_of_term vs (@{term "neg_numeral :: _ \<Rightarrow> real"} $ t') =
    8.34 +  | num_of_term vs (@{term "- numeral :: _ \<Rightarrow> real"} $ t') =
    8.35        mk_C (~ (HOLogic.dest_num t'))
    8.36    | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t);
    8.37  
    8.38 @@ -5583,7 +5584,7 @@
    8.39        @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) 
    8.40    | fm_of_term vs (@{term "op rdvd"} $ (@{term "real :: int \<Rightarrow> real"} $ (@{term "numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
    8.41        mk_Dvd (HOLogic.dest_num t1, num_of_term vs t2)
    8.42 -  | fm_of_term vs (@{term "op rdvd"} $ (@{term "real :: int \<Rightarrow> real"} $ (@{term "neg_numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
    8.43 +  | fm_of_term vs (@{term "op rdvd"} $ (@{term "real :: int \<Rightarrow> real"} $ (@{term "- numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
    8.44        mk_Dvd (~ (HOLogic.dest_num t1), num_of_term vs t2)
    8.45    | fm_of_term vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
    8.46        @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
     9.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Nov 19 01:30:14 2013 +0100
     9.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Nov 19 10:05:53 2013 +0100
     9.3 @@ -1256,12 +1256,10 @@
     9.4    apply (case_tac n', simp, simp)
     9.5    apply (case_tac n, simp, simp)
     9.6    apply (case_tac n, case_tac n', simp add: Let_def)
     9.7 -  apply (case_tac "pa +\<^sub>p p' = 0\<^sub>p")
     9.8 -  apply (auto simp add: polyadd_eq_const_degree)
     9.9 +  apply (auto simp add: polyadd_eq_const_degree)[2]
    9.10    apply (metis head_nz)
    9.11    apply (metis head_nz)
    9.12    apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq)
    9.13 -  apply (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans)
    9.14    done
    9.15  
    9.16  lemma polymul_head_polyeq:
    10.1 --- a/src/HOL/Divides.thy	Tue Nov 19 01:30:14 2013 +0100
    10.2 +++ b/src/HOL/Divides.thy	Tue Nov 19 10:05:53 2013 +0100
    10.3 @@ -1919,10 +1919,9 @@
    10.4    val zero = @{term "0 :: int"}
    10.5    val less = @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"}
    10.6    val le = @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"}
    10.7 -  val simps = @{thms arith_simps} @ @{thms rel_simps} @
    10.8 -    map (fn th => th RS sym) [@{thm numeral_1_eq_1}]
    10.9 -  fun prove ctxt goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
   10.10 -    (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps))));
   10.11 +  val simps = @{thms arith_simps} @ @{thms rel_simps} @ [@{thm numeral_1_eq_1 [symmetric]}]
   10.12 +  fun prove ctxt goal = (writeln "prove"; Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
   10.13 +    (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps)))));
   10.14    fun binary_proc proc ctxt ct =
   10.15      (case Thm.term_of ct of
   10.16        _ $ t $ u =>
   10.17 @@ -1945,23 +1944,23 @@
   10.18  
   10.19  simproc_setup binary_int_div
   10.20    ("numeral m div numeral n :: int" |
   10.21 -   "numeral m div neg_numeral n :: int" |
   10.22 -   "neg_numeral m div numeral n :: int" |
   10.23 -   "neg_numeral m div neg_numeral n :: int") =
   10.24 +   "numeral m div - numeral n :: int" |
   10.25 +   "- numeral m div numeral n :: int" |
   10.26 +   "- numeral m div - numeral n :: int") =
   10.27    {* K (divmod_proc @{thm int_div_pos_eq} @{thm int_div_neg_eq}) *}
   10.28  
   10.29  simproc_setup binary_int_mod
   10.30    ("numeral m mod numeral n :: int" |
   10.31 -   "numeral m mod neg_numeral n :: int" |
   10.32 -   "neg_numeral m mod numeral n :: int" |
   10.33 -   "neg_numeral m mod neg_numeral n :: int") =
   10.34 +   "numeral m mod - numeral n :: int" |
   10.35 +   "- numeral m mod numeral n :: int" |
   10.36 +   "- numeral m mod - numeral n :: int") =
   10.37    {* K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq}) *}
   10.38  
   10.39  lemmas posDivAlg_eqn_numeral [simp] =
   10.40      posDivAlg_eqn [of "numeral v" "numeral w", OF zero_less_numeral] for v w
   10.41  
   10.42  lemmas negDivAlg_eqn_numeral [simp] =
   10.43 -    negDivAlg_eqn [of "numeral v" "neg_numeral w", OF zero_less_numeral] for v w
   10.44 +    negDivAlg_eqn [of "numeral v" "- numeral w", OF zero_less_numeral] for v w
   10.45  
   10.46  
   10.47  text{*Special-case simplification *}
   10.48 @@ -1973,14 +1972,14 @@
   10.49    div_pos_pos [OF zero_less_one, of "numeral w", OF zero_le_numeral] for w
   10.50  
   10.51  lemmas div_pos_neg_1_numeral [simp] =
   10.52 -  div_pos_neg [OF zero_less_one, of "neg_numeral w",
   10.53 +  div_pos_neg [OF zero_less_one, of "- numeral w",
   10.54    OF neg_numeral_less_zero] for w
   10.55  
   10.56  lemmas mod_pos_pos_1_numeral [simp] =
   10.57    mod_pos_pos [OF zero_less_one, of "numeral w", OF zero_le_numeral] for w
   10.58  
   10.59  lemmas mod_pos_neg_1_numeral [simp] =
   10.60 -  mod_pos_neg [OF zero_less_one, of "neg_numeral w",
   10.61 +  mod_pos_neg [OF zero_less_one, of "- numeral w",
   10.62    OF neg_numeral_less_zero] for w
   10.63  
   10.64  lemmas posDivAlg_eqn_1_numeral [simp] =
   10.65 @@ -2290,6 +2289,8 @@
   10.66    shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
   10.67    using assms unfolding divmod_int_rel_def by auto
   10.68  
   10.69 +declaration {* K (Lin_Arith.add_simps @{thms uminus_numeral_One}) *}
   10.70 +
   10.71  lemma neg_divmod_int_rel_mult_2:
   10.72    assumes "b \<le> 0"
   10.73    assumes "divmod_int_rel (a + 1) b (q, r)"
   10.74 @@ -2427,13 +2428,13 @@
   10.75  
   10.76  lemma dvd_neg_numeral_left [simp]:
   10.77    fixes y :: "'a::comm_ring_1"
   10.78 -  shows "(neg_numeral k) dvd y \<longleftrightarrow> (numeral k) dvd y"
   10.79 -  unfolding neg_numeral_def minus_dvd_iff ..
   10.80 +  shows "(- numeral k) dvd y \<longleftrightarrow> (numeral k) dvd y"
   10.81 +  by (fact minus_dvd_iff)
   10.82  
   10.83  lemma dvd_neg_numeral_right [simp]:
   10.84    fixes x :: "'a::comm_ring_1"
   10.85 -  shows "x dvd (neg_numeral k) \<longleftrightarrow> x dvd (numeral k)"
   10.86 -  unfolding neg_numeral_def dvd_minus_iff ..
   10.87 +  shows "x dvd (- numeral k) \<longleftrightarrow> x dvd (numeral k)"
   10.88 +  by (fact dvd_minus_iff)
   10.89  
   10.90  lemmas dvd_eq_mod_eq_0_numeral [simp] =
   10.91    dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y
    11.1 --- a/src/HOL/GCD.thy	Tue Nov 19 01:30:14 2013 +0100
    11.2 +++ b/src/HOL/GCD.thy	Tue Nov 19 10:05:53 2013 +0100
    11.3 @@ -134,6 +134,14 @@
    11.4  lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
    11.5    by (simp add: gcd_int_def)
    11.6  
    11.7 +lemma gcd_neg_numeral_1_int [simp]:
    11.8 +  "gcd (- numeral n :: int) x = gcd (numeral n) x"
    11.9 +  by (fact gcd_neg1_int)
   11.10 +
   11.11 +lemma gcd_neg_numeral_2_int [simp]:
   11.12 +  "gcd x (- numeral n :: int) = gcd x (numeral n)"
   11.13 +  by (fact gcd_neg2_int)
   11.14 +
   11.15  lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"
   11.16  by(simp add: gcd_int_def)
   11.17  
    12.1 --- a/src/HOL/IMP/Hoare_Examples.thy	Tue Nov 19 01:30:14 2013 +0100
    12.2 +++ b/src/HOL/IMP/Hoare_Examples.thy	Tue Nov 19 10:05:53 2013 +0100
    12.3 @@ -2,17 +2,6 @@
    12.4  
    12.5  theory Hoare_Examples imports Hoare begin
    12.6  
    12.7 -text{* Improves proof automation for negative numerals: *}
    12.8 -
    12.9 -lemma add_neg1R[simp]:
   12.10 -  "x + -1 = x - (1 :: int)"
   12.11 -by arith
   12.12 -
   12.13 -lemma add_neg_numeralR[simp]:
   12.14 -  "x + neg_numeral n = (x::'a::neg_numeral) - numeral(n)"
   12.15 -by (simp only: diff_minus_eq_add[symmetric] minus_neg_numeral)
   12.16 -
   12.17 -
   12.18  text{* Summing up the first @{text x} natural numbers in variable @{text y}. *}
   12.19  
   12.20  fun sum :: "int \<Rightarrow> int" where
    13.1 --- a/src/HOL/Int.thy	Tue Nov 19 01:30:14 2013 +0100
    13.2 +++ b/src/HOL/Int.thy	Tue Nov 19 10:05:53 2013 +0100
    13.3 @@ -232,9 +232,8 @@
    13.4  lemma of_int_numeral [simp, code_post]: "of_int (numeral k) = numeral k"
    13.5    by (simp add: of_nat_numeral [symmetric] of_int_of_nat_eq [symmetric])
    13.6  
    13.7 -lemma of_int_neg_numeral [simp, code_post]: "of_int (neg_numeral k) = neg_numeral k"
    13.8 -  unfolding neg_numeral_def neg_numeral_class.neg_numeral_def
    13.9 -  by (simp only: of_int_minus of_int_numeral)
   13.10 +lemma of_int_neg_numeral [code_post]: "of_int (- numeral k) = - numeral k"
   13.11 +  by simp
   13.12  
   13.13  lemma of_int_power:
   13.14    "of_int (z ^ n) = of_int z ^ n"
   13.15 @@ -370,7 +369,7 @@
   13.16    by (simp add: nat_eq_iff)
   13.17  
   13.18  lemma nat_neg_numeral [simp]:
   13.19 -  "nat (neg_numeral k) = 0"
   13.20 +  "nat (- numeral k) = 0"
   13.21    by simp
   13.22  
   13.23  lemma nat_2: "nat 2 = Suc (Suc 0)"
   13.24 @@ -511,13 +510,13 @@
   13.25  
   13.26  lemma nonneg_int_cases:
   13.27    assumes "0 \<le> k" obtains n where "k = int n"
   13.28 -  using assms by (cases k, simp, simp del: of_nat_Suc)
   13.29 +  using assms by (rule nonneg_eq_int)
   13.30  
   13.31  lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
   13.32    -- {* Unfold all @{text let}s involving constants *}
   13.33    unfolding Let_def ..
   13.34  
   13.35 -lemma Let_neg_numeral [simp]: "Let (neg_numeral v) f = f (neg_numeral v)"
   13.36 +lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
   13.37    -- {* Unfold all @{text let}s involving constants *}
   13.38    unfolding Let_def ..
   13.39  
   13.40 @@ -525,15 +524,15 @@
   13.41  
   13.42  lemmas max_number_of [simp] =
   13.43    max_def [of "numeral u" "numeral v"]
   13.44 -  max_def [of "numeral u" "neg_numeral v"]
   13.45 -  max_def [of "neg_numeral u" "numeral v"]
   13.46 -  max_def [of "neg_numeral u" "neg_numeral v"] for u v
   13.47 +  max_def [of "numeral u" "- numeral v"]
   13.48 +  max_def [of "- numeral u" "numeral v"]
   13.49 +  max_def [of "- numeral u" "- numeral v"] for u v
   13.50  
   13.51  lemmas min_number_of [simp] =
   13.52    min_def [of "numeral u" "numeral v"]
   13.53 -  min_def [of "numeral u" "neg_numeral v"]
   13.54 -  min_def [of "neg_numeral u" "numeral v"]
   13.55 -  min_def [of "neg_numeral u" "neg_numeral v"] for u v
   13.56 +  min_def [of "numeral u" "- numeral v"]
   13.57 +  min_def [of "- numeral u" "numeral v"]
   13.58 +  min_def [of "- numeral u" "- numeral v"] for u v
   13.59  
   13.60  
   13.61  subsubsection {* Binary comparisons *}
   13.62 @@ -1070,8 +1069,6 @@
   13.63      by auto
   13.64  qed
   13.65  
   13.66 -ML_val {* @{const_name neg_numeral} *}
   13.67 -
   13.68  lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
   13.69  by (insert abs_zmult_eq_1 [of m n], arith)
   13.70  
   13.71 @@ -1127,62 +1124,30 @@
   13.72    inverse_eq_divide [of "numeral w"] for w
   13.73  
   13.74  lemmas inverse_eq_divide_neg_numeral [simp] =
   13.75 -  inverse_eq_divide [of "neg_numeral w"] for w
   13.76 +  inverse_eq_divide [of "- numeral w"] for w
   13.77  
   13.78  text {*These laws simplify inequalities, moving unary minus from a term
   13.79  into the literal.*}
   13.80  
   13.81 -lemmas le_minus_iff_numeral [simp, no_atp] =
   13.82 -  le_minus_iff [of "numeral v"]
   13.83 -  le_minus_iff [of "neg_numeral v"] for v
   13.84 -
   13.85 -lemmas equation_minus_iff_numeral [simp, no_atp] =
   13.86 -  equation_minus_iff [of "numeral v"]
   13.87 -  equation_minus_iff [of "neg_numeral v"] for v
   13.88 +lemmas equation_minus_iff_numeral [no_atp] =
   13.89 +  equation_minus_iff [of "numeral v"] for v
   13.90  
   13.91 -lemmas minus_less_iff_numeral [simp, no_atp] =
   13.92 -  minus_less_iff [of _ "numeral v"]
   13.93 -  minus_less_iff [of _ "neg_numeral v"] for v
   13.94 +lemmas minus_equation_iff_numeral [no_atp] =
   13.95 +  minus_equation_iff [of _ "numeral v"] for v
   13.96  
   13.97 -lemmas minus_le_iff_numeral [simp, no_atp] =
   13.98 -  minus_le_iff [of _ "numeral v"]
   13.99 -  minus_le_iff [of _ "neg_numeral v"] for v
  13.100 -
  13.101 -lemmas minus_equation_iff_numeral [simp, no_atp] =
  13.102 -  minus_equation_iff [of _ "numeral v"]
  13.103 -  minus_equation_iff [of _ "neg_numeral v"] for v
  13.104 -
  13.105 -text{*To Simplify Inequalities Where One Side is the Constant 1*}
  13.106 +lemmas le_minus_iff_numeral [no_atp] =
  13.107 +  le_minus_iff [of "numeral v"] for v
  13.108  
  13.109 -lemma less_minus_iff_1 [simp]:
  13.110 -  fixes b::"'b::linordered_idom"
  13.111 -  shows "(1 < - b) = (b < -1)"
  13.112 -by auto
  13.113 -
  13.114 -lemma le_minus_iff_1 [simp]:
  13.115 -  fixes b::"'b::linordered_idom"
  13.116 -  shows "(1 \<le> - b) = (b \<le> -1)"
  13.117 -by auto
  13.118 -
  13.119 -lemma equation_minus_iff_1 [simp]:
  13.120 -  fixes b::"'b::ring_1"
  13.121 -  shows "(1 = - b) = (b = -1)"
  13.122 -by (subst equation_minus_iff, auto)
  13.123 +lemmas minus_le_iff_numeral [no_atp] =
  13.124 +  minus_le_iff [of _ "numeral v"] for v
  13.125  
  13.126 -lemma minus_less_iff_1 [simp]:
  13.127 -  fixes a::"'b::linordered_idom"
  13.128 -  shows "(- a < 1) = (-1 < a)"
  13.129 -by auto
  13.130 +lemmas less_minus_iff_numeral [no_atp] =
  13.131 +  less_minus_iff [of "numeral v"] for v
  13.132  
  13.133 -lemma minus_le_iff_1 [simp]:
  13.134 -  fixes a::"'b::linordered_idom"
  13.135 -  shows "(- a \<le> 1) = (-1 \<le> a)"
  13.136 -by auto
  13.137 +lemmas minus_less_iff_numeral [no_atp] =
  13.138 +  minus_less_iff [of _ "numeral v"] for v
  13.139  
  13.140 -lemma minus_equation_iff_1 [simp]:
  13.141 -  fixes a::"'b::ring_1"
  13.142 -  shows "(- a = 1) = (a = -1)"
  13.143 -by (subst minus_equation_iff, auto)
  13.144 +-- {* FIXME maybe simproc *}
  13.145  
  13.146  
  13.147  text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
  13.148 @@ -1197,27 +1162,28 @@
  13.149  
  13.150  lemmas le_divide_eq_numeral1 [simp] =
  13.151    pos_le_divide_eq [of "numeral w", OF zero_less_numeral]
  13.152 -  neg_le_divide_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
  13.153 +  neg_le_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
  13.154  
  13.155  lemmas divide_le_eq_numeral1 [simp] =
  13.156    pos_divide_le_eq [of "numeral w", OF zero_less_numeral]
  13.157 -  neg_divide_le_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
  13.158 +  neg_divide_le_eq [of "- numeral w", OF neg_numeral_less_zero] for w
  13.159  
  13.160  lemmas less_divide_eq_numeral1 [simp] =
  13.161    pos_less_divide_eq [of "numeral w", OF zero_less_numeral]
  13.162 -  neg_less_divide_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
  13.163 +  neg_less_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
  13.164  
  13.165  lemmas divide_less_eq_numeral1 [simp] =
  13.166    pos_divide_less_eq [of "numeral w", OF zero_less_numeral]
  13.167 -  neg_divide_less_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
  13.168 +  neg_divide_less_eq [of "- numeral w", OF neg_numeral_less_zero] for w
  13.169  
  13.170  lemmas eq_divide_eq_numeral1 [simp] =
  13.171    eq_divide_eq [of _ _ "numeral w"]
  13.172 -  eq_divide_eq [of _ _ "neg_numeral w"] for w
  13.173 +  eq_divide_eq [of _ _ "- numeral w"] for w
  13.174  
  13.175  lemmas divide_eq_eq_numeral1 [simp] =
  13.176    divide_eq_eq [of _ "numeral w"]
  13.177 -  divide_eq_eq [of _ "neg_numeral w"] for w
  13.178 +  divide_eq_eq [of _ "- numeral w"] for w
  13.179 +
  13.180  
  13.181  subsubsection{*Optional Simplification Rules Involving Constants*}
  13.182  
  13.183 @@ -1225,27 +1191,27 @@
  13.184  
  13.185  lemmas le_divide_eq_numeral =
  13.186    le_divide_eq [of "numeral w"]
  13.187 -  le_divide_eq [of "neg_numeral w"] for w
  13.188 +  le_divide_eq [of "- numeral w"] for w
  13.189  
  13.190  lemmas divide_le_eq_numeral =
  13.191    divide_le_eq [of _ _ "numeral w"]
  13.192 -  divide_le_eq [of _ _ "neg_numeral w"] for w
  13.193 +  divide_le_eq [of _ _ "- numeral w"] for w
  13.194  
  13.195  lemmas less_divide_eq_numeral =
  13.196    less_divide_eq [of "numeral w"]
  13.197 -  less_divide_eq [of "neg_numeral w"] for w
  13.198 +  less_divide_eq [of "- numeral w"] for w
  13.199  
  13.200  lemmas divide_less_eq_numeral =
  13.201    divide_less_eq [of _ _ "numeral w"]
  13.202 -  divide_less_eq [of _ _ "neg_numeral w"] for w
  13.203 +  divide_less_eq [of _ _ "- numeral w"] for w
  13.204  
  13.205  lemmas eq_divide_eq_numeral =
  13.206    eq_divide_eq [of "numeral w"]
  13.207 -  eq_divide_eq [of "neg_numeral w"] for w
  13.208 +  eq_divide_eq [of "- numeral w"] for w
  13.209  
  13.210  lemmas divide_eq_eq_numeral =
  13.211    divide_eq_eq [of _ _ "numeral w"]
  13.212 -  divide_eq_eq [of _ _ "neg_numeral w"] for w
  13.213 +  divide_eq_eq [of _ _ "- numeral w"] for w
  13.214  
  13.215  
  13.216  text{*Not good as automatic simprules because they cause case splits.*}
  13.217 @@ -1257,21 +1223,20 @@
  13.218  text{*Division By @{text "-1"}*}
  13.219  
  13.220  lemma divide_minus1 [simp]: "(x::'a::field) / -1 = - x"
  13.221 -  unfolding minus_one [symmetric]
  13.222    unfolding nonzero_minus_divide_right [OF one_neq_zero, symmetric]
  13.223    by simp
  13.224  
  13.225  lemma minus1_divide [simp]: "-1 / (x::'a::field) = - (1 / x)"
  13.226 -  unfolding minus_one [symmetric] by (rule divide_minus_left)
  13.227 +  by (fact divide_minus_left)
  13.228  
  13.229  lemma half_gt_zero_iff:
  13.230 -     "(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))"
  13.231 -by auto
  13.232 +  "(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))"
  13.233 +  by auto
  13.234  
  13.235  lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2]
  13.236  
  13.237  lemma divide_Numeral1: "(x::'a::field) / Numeral1 = x"
  13.238 -  by simp
  13.239 +  by (fact divide_numeral_1)
  13.240  
  13.241  
  13.242  subsection {* The divides relation *}
  13.243 @@ -1475,7 +1440,7 @@
  13.244    [simp, code_abbrev]: "Pos = numeral"
  13.245  
  13.246  definition Neg :: "num \<Rightarrow> int" where
  13.247 -  [simp, code_abbrev]: "Neg = neg_numeral"
  13.248 +  [simp, code_abbrev]: "Neg n = - (Pos n)"
  13.249  
  13.250  code_datatype "0::int" Pos Neg
  13.251  
  13.252 @@ -1489,7 +1454,7 @@
  13.253    "dup 0 = 0"
  13.254    "dup (Pos n) = Pos (Num.Bit0 n)"
  13.255    "dup (Neg n) = Neg (Num.Bit0 n)"
  13.256 -  unfolding Pos_def Neg_def neg_numeral_def
  13.257 +  unfolding Pos_def Neg_def
  13.258    by (simp_all add: numeral_Bit0)
  13.259  
  13.260  definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
  13.261 @@ -1505,12 +1470,10 @@
  13.262    "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
  13.263    "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
  13.264    "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
  13.265 -  apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def
  13.266 -    neg_numeral_def numeral_BitM)
  13.267 +  apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM)
  13.268    apply (simp_all only: algebra_simps minus_diff_eq)
  13.269    apply (simp_all only: add.commute [of _ "- (numeral n + numeral n)"])
  13.270    apply (simp_all only: minus_add add.assoc left_minus)
  13.271 -  apply (simp_all only: algebra_simps right_minus)
  13.272    done
  13.273  
  13.274  text {* Implementations *}
  13.275 @@ -1606,10 +1569,10 @@
  13.276    "nat (Int.Neg k) = 0"
  13.277    "nat 0 = 0"
  13.278    "nat (Int.Pos k) = nat_of_num k"
  13.279 -  by (simp_all add: nat_of_num_numeral nat_numeral)
  13.280 +  by (simp_all add: nat_of_num_numeral)
  13.281  
  13.282  lemma (in ring_1) of_int_code [code]:
  13.283 -  "of_int (Int.Neg k) = neg_numeral k"
  13.284 +  "of_int (Int.Neg k) = - numeral k"
  13.285    "of_int 0 = 0"
  13.286    "of_int (Int.Pos k) = numeral k"
  13.287    by simp_all
  13.288 @@ -1653,7 +1616,7 @@
  13.289  
  13.290  lemma int_power:
  13.291    "int (m ^ n) = int m ^ n"
  13.292 -  by (rule of_nat_power)
  13.293 +  by (fact of_nat_power)
  13.294  
  13.295  lemmas zpower_int = int_power [symmetric]
  13.296  
    14.1 --- a/src/HOL/Library/Binomial.thy	Tue Nov 19 01:30:14 2013 +0100
    14.2 +++ b/src/HOL/Library/Binomial.thy	Tue Nov 19 10:05:53 2013 +0100
    14.3 @@ -370,7 +370,7 @@
    14.4      by auto
    14.5    from False show ?thesis
    14.6      by (simp add: pochhammer_def gbinomial_def field_simps
    14.7 -      eq setprod_timesf[symmetric] del: minus_one)
    14.8 +      eq setprod_timesf[symmetric])
    14.9  qed
   14.10  
   14.11  lemma binomial_fact_lemma: "k \<le> n \<Longrightarrow> fact k * fact (n - k) * (n choose k) = fact n"
   14.12 @@ -441,9 +441,9 @@
   14.13      from eq[symmetric]
   14.14      have ?thesis using kn
   14.15        apply (simp add: binomial_fact[OF kn, where ?'a = 'a]
   14.16 -        gbinomial_pochhammer field_simps pochhammer_Suc_setprod del: minus_one)
   14.17 +        gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
   14.18        apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h
   14.19 -        of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc del: minus_one)
   14.20 +        of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
   14.21        unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
   14.22        unfolding mult_assoc[symmetric]
   14.23        unfolding setprod_timesf[symmetric]
    15.1 --- a/src/HOL/Library/Bit.thy	Tue Nov 19 01:30:14 2013 +0100
    15.2 +++ b/src/HOL/Library/Bit.thy	Tue Nov 19 10:05:53 2013 +0100
    15.3 @@ -147,11 +147,11 @@
    15.4  
    15.5  text {* All numerals reduce to either 0 or 1. *}
    15.6  
    15.7 -lemma bit_minus1 [simp]: "-1 = (1 :: bit)"
    15.8 -  by (simp only: minus_one [symmetric] uminus_bit_def)
    15.9 +lemma bit_minus1 [simp]: "- 1 = (1 :: bit)"
   15.10 +  by (simp only: uminus_bit_def)
   15.11  
   15.12 -lemma bit_neg_numeral [simp]: "(neg_numeral w :: bit) = numeral w"
   15.13 -  by (simp only: neg_numeral_def uminus_bit_def)
   15.14 +lemma bit_neg_numeral [simp]: "(- numeral w :: bit) = numeral w"
   15.15 +  by (simp only: uminus_bit_def)
   15.16  
   15.17  lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
   15.18    by (simp only: numeral_Bit0 bit_add_self)
    16.1 --- a/src/HOL/Library/Code_Prolog.thy	Tue Nov 19 01:30:14 2013 +0100
    16.2 +++ b/src/HOL/Library/Code_Prolog.thy	Tue Nov 19 10:05:53 2013 +0100
    16.3 @@ -12,10 +12,8 @@
    16.4  
    16.5  section {* Setup for Numerals *}
    16.6  
    16.7 -setup {* Predicate_Compile_Data.ignore_consts
    16.8 -  [@{const_name numeral}, @{const_name neg_numeral}] *}
    16.9 +setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}] *}
   16.10  
   16.11 -setup {* Predicate_Compile_Data.keep_functions
   16.12 -  [@{const_name numeral}, @{const_name neg_numeral}] *}
   16.13 +setup {* Predicate_Compile_Data.keep_functions [@{const_name numeral}] *}
   16.14  
   16.15  end
    17.1 --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Tue Nov 19 01:30:14 2013 +0100
    17.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Tue Nov 19 10:05:53 2013 +0100
    17.3 @@ -169,7 +169,7 @@
    17.4    by simp
    17.5  
    17.6  lemma [code_unfold del]:
    17.7 -  "neg_numeral k \<equiv> (of_rat (neg_numeral k) :: real)"
    17.8 +  "- numeral k \<equiv> (of_rat (- numeral k) :: real)"
    17.9    by simp
   17.10  
   17.11  hide_const (open) real_of_int
    18.1 --- a/src/HOL/Library/Code_Target_Int.thy	Tue Nov 19 01:30:14 2013 +0100
    18.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Tue Nov 19 10:05:53 2013 +0100
    18.3 @@ -30,7 +30,7 @@
    18.4    by transfer simp
    18.5  
    18.6  lemma [code_abbrev]:
    18.7 -  "int_of_integer (neg_numeral k) = Int.Neg k"
    18.8 +  "int_of_integer (- numeral k) = Int.Neg k"
    18.9    by transfer simp
   18.10    
   18.11  lemma [code, symmetric, code_post]:
    19.1 --- a/src/HOL/Library/Extended.thy	Tue Nov 19 01:30:14 2013 +0100
    19.2 +++ b/src/HOL/Library/Extended.thy	Tue Nov 19 10:05:53 2013 +0100
    19.3 @@ -161,8 +161,8 @@
    19.4    apply (simp only: numeral_inc one_extended_def plus_extended.simps(1)[symmetric])
    19.5    done
    19.6  
    19.7 -lemma Fin_neg_numeral: "Fin(neg_numeral w) = - numeral w"
    19.8 -by (simp only: Fin_numeral minus_numeral[symmetric] uminus_extended.simps[symmetric])
    19.9 +lemma Fin_neg_numeral: "Fin (- numeral w) = - numeral w"
   19.10 +by (simp only: Fin_numeral uminus_extended.simps[symmetric])
   19.11  
   19.12  
   19.13  instantiation extended :: (lattice)bounded_lattice
    20.1 --- a/src/HOL/Library/Float.thy	Tue Nov 19 01:30:14 2013 +0100
    20.2 +++ b/src/HOL/Library/Float.thy	Tue Nov 19 10:05:53 2013 +0100
    20.3 @@ -45,7 +45,7 @@
    20.4  lemma zero_float[simp]: "0 \<in> float" by (auto simp: float_def)
    20.5  lemma one_float[simp]: "1 \<in> float" by (intro floatI[of 1 0]) simp
    20.6  lemma numeral_float[simp]: "numeral i \<in> float" by (intro floatI[of "numeral i" 0]) simp
    20.7 -lemma neg_numeral_float[simp]: "neg_numeral i \<in> float" by (intro floatI[of "neg_numeral i" 0]) simp
    20.8 +lemma neg_numeral_float[simp]: "- numeral i \<in> float" by (intro floatI[of "- numeral i" 0]) simp
    20.9  lemma real_of_int_float[simp]: "real (x :: int) \<in> float" by (intro floatI[of x 0]) simp
   20.10  lemma real_of_nat_float[simp]: "real (x :: nat) \<in> float" by (intro floatI[of x 0]) simp
   20.11  lemma two_powr_int_float[simp]: "2 powr (real (i::int)) \<in> float" by (intro floatI[of 1 i]) simp
   20.12 @@ -53,7 +53,7 @@
   20.13  lemma two_powr_minus_int_float[simp]: "2 powr - (real (i::int)) \<in> float" by (intro floatI[of 1 "-i"]) simp
   20.14  lemma two_powr_minus_nat_float[simp]: "2 powr - (real (i::nat)) \<in> float" by (intro floatI[of 1 "-i"]) simp
   20.15  lemma two_powr_numeral_float[simp]: "2 powr numeral i \<in> float" by (intro floatI[of 1 "numeral i"]) simp
   20.16 -lemma two_powr_neg_numeral_float[simp]: "2 powr neg_numeral i \<in> float" by (intro floatI[of 1 "neg_numeral i"]) simp
   20.17 +lemma two_powr_neg_numeral_float[simp]: "2 powr - numeral i \<in> float" by (intro floatI[of 1 "- numeral i"]) simp
   20.18  lemma two_pow_float[simp]: "2 ^ n \<in> float" by (intro floatI[of 1 "n"]) (simp add: powr_realpow)
   20.19  lemma real_of_float_float[simp]: "real (f::float) \<in> float" by (cases f) simp
   20.20  
   20.21 @@ -121,11 +121,11 @@
   20.22  qed
   20.23  
   20.24  lemma div_neg_numeral_Bit0_float[simp]:
   20.25 -  assumes x: "x / numeral n \<in> float" shows "x / (neg_numeral (Num.Bit0 n)) \<in> float"
   20.26 +  assumes x: "x / numeral n \<in> float" shows "x / (- numeral (Num.Bit0 n)) \<in> float"
   20.27  proof -
   20.28    have "- (x / numeral (Num.Bit0 n)) \<in> float" using x by simp
   20.29 -  also have "- (x / numeral (Num.Bit0 n)) = x / neg_numeral (Num.Bit0 n)"
   20.30 -    unfolding neg_numeral_def by (simp del: minus_numeral)
   20.31 +  also have "- (x / numeral (Num.Bit0 n)) = x / - numeral (Num.Bit0 n)"
   20.32 +    by simp
   20.33    finally show ?thesis .
   20.34  qed
   20.35  
   20.36 @@ -197,7 +197,7 @@
   20.37    then show "\<exists>c. a < c \<and> c < b"
   20.38      apply (intro exI[of _ "(a + b) * Float 1 -1"])
   20.39      apply transfer
   20.40 -    apply (simp add: powr_neg_numeral)
   20.41 +    apply (simp add: powr_minus)
   20.42      done
   20.43  qed
   20.44  
   20.45 @@ -226,16 +226,16 @@
   20.46    "fun_rel (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
   20.47    unfolding fun_rel_def float.pcr_cr_eq  cr_float_def by simp
   20.48  
   20.49 -lemma float_neg_numeral[simp]: "real (neg_numeral x :: float) = neg_numeral x"
   20.50 -  by (simp add: minus_numeral[symmetric] del: minus_numeral)
   20.51 +lemma float_neg_numeral[simp]: "real (- numeral x :: float) = - numeral x"
   20.52 +  by simp
   20.53  
   20.54  lemma transfer_neg_numeral [transfer_rule]:
   20.55 -  "fun_rel (op =) pcr_float (neg_numeral :: _ \<Rightarrow> real) (neg_numeral :: _ \<Rightarrow> float)"
   20.56 +  "fun_rel (op =) pcr_float (- numeral :: _ \<Rightarrow> real) (- numeral :: _ \<Rightarrow> float)"
   20.57    unfolding fun_rel_def float.pcr_cr_eq cr_float_def by simp
   20.58  
   20.59  lemma
   20.60    shows float_of_numeral[simp]: "numeral k = float_of (numeral k)"
   20.61 -    and float_of_neg_numeral[simp]: "neg_numeral k = float_of (neg_numeral k)"
   20.62 +    and float_of_neg_numeral[simp]: "- numeral k = float_of (- numeral k)"
   20.63    unfolding real_of_float_eq by simp_all
   20.64  
   20.65  subsection {* Represent floats as unique mantissa and exponent *}
   20.66 @@ -439,7 +439,7 @@
   20.67    by transfer simp
   20.68  hide_fact (open) compute_float_numeral
   20.69  
   20.70 -lemma compute_float_neg_numeral[code_abbrev]: "Float (neg_numeral k) 0 = neg_numeral k"
   20.71 +lemma compute_float_neg_numeral[code_abbrev]: "Float (- numeral k) 0 = - numeral k"
   20.72    by transfer simp
   20.73  hide_fact (open) compute_float_neg_numeral
   20.74  
   20.75 @@ -960,7 +960,7 @@
   20.76    also have "... < (1 / 2) * 2 powr real (rat_precision n (int x) (int y))"
   20.77      apply (rule mult_strict_right_mono) by (insert assms) auto
   20.78    also have "\<dots> = 2 powr real (rat_precision n (int x) (int y) - 1)"
   20.79 -    using powr_add [of 2 _ "- 1", simplified add_uminus_conv_diff] by (simp add: powr_neg_numeral)
   20.80 +    using powr_add [of 2 _ "- 1", simplified add_uminus_conv_diff] by (simp add: powr_minus)
   20.81    also have "\<dots> = 2 ^ nat (rat_precision n (int x) (int y) - 1)"
   20.82      using rat_precision_pos[of x y n] assms by (simp add: powr_realpow[symmetric])
   20.83    also have "\<dots> \<le> 2 ^ nat (rat_precision n (int x) (int y)) - 1"
    21.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Nov 19 01:30:14 2013 +0100
    21.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Nov 19 10:05:53 2013 +0100
    21.3 @@ -384,8 +384,8 @@
    21.4    by (induct k) (simp_all only: numeral.simps fps_const_1_eq_1
    21.5      fps_const_add [symmetric])
    21.6  
    21.7 -lemma neg_numeral_fps_const: "neg_numeral k = fps_const (neg_numeral k)"
    21.8 -  by (simp only: neg_numeral_def numeral_fps_const fps_const_neg)
    21.9 +lemma neg_numeral_fps_const: "- numeral k = fps_const (- numeral k)"
   21.10 +  by (simp only: numeral_fps_const fps_const_neg)
   21.11  
   21.12  subsection{* The eXtractor series X*}
   21.13  
   21.14 @@ -1202,7 +1202,7 @@
   21.15    have eq: "(1 + X) * ?r = 1"
   21.16      unfolding minus_one_power_iff
   21.17      by (auto simp add: field_simps fps_eq_iff)
   21.18 -  show ?thesis by (auto simp add: eq intro: fps_inverse_unique simp del: minus_one)
   21.19 +  show ?thesis by (auto simp add: eq intro: fps_inverse_unique)
   21.20  qed
   21.21  
   21.22  
   21.23 @@ -1245,7 +1245,7 @@
   21.24  lemma numeral_compose[simp]: "(numeral k::('a::{comm_ring_1}) fps) oo b = numeral k"
   21.25    unfolding numeral_fps_const by simp
   21.26  
   21.27 -lemma neg_numeral_compose[simp]: "(neg_numeral k::('a::{comm_ring_1}) fps) oo b = neg_numeral k"
   21.28 +lemma neg_numeral_compose[simp]: "(- numeral k::('a::{comm_ring_1}) fps) oo b = - numeral k"
   21.29    unfolding neg_numeral_fps_const by simp
   21.30  
   21.31  lemma X_fps_compose_startby0[simp]: "a$0 = 0 \<Longrightarrow> X oo a = (a :: ('a :: comm_ring_1) fps)"
   21.32 @@ -2363,7 +2363,7 @@
   21.33        next
   21.34          case (Suc n1)
   21.35          have "?i $ n = setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} + fps_inv a $ Suc n1 * (a $ 1)^ Suc n1"
   21.36 -          by (simp add: fps_compose_nth Suc startsby_zero_power_nth_same[OF a0] del: power_Suc)
   21.37 +          by (simp only: fps_compose_nth) (simp add: Suc startsby_zero_power_nth_same [OF a0] del: power_Suc)
   21.38          also have "\<dots> = setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} +
   21.39            (X$ Suc n1 - setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1})"
   21.40            using a0 a1 Suc by (simp add: fps_inv_def)
   21.41 @@ -2404,7 +2404,7 @@
   21.42        next
   21.43          case (Suc n1)
   21.44          have "?i $ n = setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1} + fps_ginv b a $ Suc n1 * (a $ 1)^ Suc n1"
   21.45 -          by (simp add: fps_compose_nth Suc startsby_zero_power_nth_same[OF a0] del: power_Suc)
   21.46 +          by (simp only: fps_compose_nth) (simp add: Suc startsby_zero_power_nth_same [OF a0] del: power_Suc)
   21.47          also have "\<dots> = setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1} +
   21.48            (b$ Suc n1 - setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1})"
   21.49            using a0 a1 Suc by (simp add: fps_ginv_def)
   21.50 @@ -2564,9 +2564,9 @@
   21.51  
   21.52  
   21.53  lemma fps_compose_mult_distrib:
   21.54 -  assumes c0: "c$0 = (0::'a::idom)"
   21.55 -  shows "(a * b) oo c = (a oo c) * (b oo c)" (is "?l = ?r")
   21.56 -  apply (simp add: fps_eq_iff fps_compose_mult_distrib_lemma[OF c0])
   21.57 +  assumes c0: "c $ 0 = (0::'a::idom)"
   21.58 +  shows "(a * b) oo c = (a oo c) * (b oo c)"
   21.59 +  apply (simp add: fps_eq_iff fps_compose_mult_distrib_lemma [OF c0])
   21.60    apply (simp add: fps_compose_nth fps_mult_nth setsum_left_distrib)
   21.61    done
   21.62  
   21.63 @@ -2941,7 +2941,7 @@
   21.64    (is "inverse ?l = ?r")
   21.65  proof -
   21.66    have th: "?l * ?r = 1"
   21.67 -    by (auto simp add: field_simps fps_eq_iff minus_one_power_iff simp del: minus_one)
   21.68 +    by (auto simp add: field_simps fps_eq_iff minus_one_power_iff)
   21.69    have th': "?l $ 0 \<noteq> 0" by (simp add: )
   21.70    from fps_inverse_unique[OF th' th] show ?thesis .
   21.71  qed
   21.72 @@ -3165,7 +3165,7 @@
   21.73    have th: "?r$0 \<noteq> 0" by simp
   21.74    have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + X)"
   21.75      by (simp add: fps_inverse_deriv[OF th] fps_divide_def
   21.76 -      power2_eq_square mult_commute fps_const_neg[symmetric] del: fps_const_neg minus_one)
   21.77 +      power2_eq_square mult_commute fps_const_neg[symmetric] del: fps_const_neg)
   21.78    have eq: "inverse ?r $ 0 = 1"
   21.79      by (simp add: fps_inverse_def)
   21.80    from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + X)" "- 1"] th'] eq
   21.81 @@ -3276,7 +3276,7 @@
   21.82          have th1: "(?m1 k * ?p (of_nat n) k) / ?f n = 1 / of_nat(fact (n - k))"
   21.83            unfolding m1nk
   21.84            unfolding m h pochhammer_Suc_setprod
   21.85 -          apply (simp add: field_simps del: fact_Suc minus_one)
   21.86 +          apply (simp add: field_simps del: fact_Suc)
   21.87            unfolding fact_altdef_nat id_def
   21.88            unfolding of_nat_setprod
   21.89            unfolding setprod_timesf[symmetric]
   21.90 @@ -3593,7 +3593,7 @@
   21.91          unfolding even_mult_two_ex by blast
   21.92  
   21.93        have "?l $n = ?r$n"
   21.94 -        by (simp add: m fps_sin_def fps_cos_def power_mult_distrib power_mult power_minus)
   21.95 +        by (simp add: m fps_sin_def fps_cos_def power_mult_distrib power_mult power_minus [of "c ^ 2"])
   21.96      }
   21.97      moreover
   21.98      {
   21.99 @@ -3602,7 +3602,7 @@
  21.100          unfolding odd_nat_equiv_def2 by (auto simp add: mult_2)
  21.101        have "?l $n = ?r$n"
  21.102          by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
  21.103 -          power_mult power_minus)
  21.104 +          power_mult power_minus [of "c ^ 2"])
  21.105      }
  21.106      ultimately have "?l $n = ?r$n"  by blast
  21.107    } then show ?thesis by (simp add: fps_eq_iff)
    22.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Nov 19 01:30:14 2013 +0100
    22.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Nov 19 10:05:53 2013 +0100
    22.3 @@ -207,12 +207,14 @@
    22.4      from unimodular_reduce_norm[OF th0] o
    22.5      have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
    22.6        apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
    22.7 -      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp del: minus_one add: minus_one [symmetric])
    22.8 +      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp)
    22.9        apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
   22.10        apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
   22.11        apply (rule_tac x="- ii" in exI, simp add: m power_mult)
   22.12        apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult)
   22.13 -      apply (rule_tac x="ii" in exI, simp add: m power_mult)
   22.14 +      apply (auto simp add: m power_mult)
   22.15 +      apply (rule_tac x="ii" in exI)
   22.16 +      apply (auto simp add: m power_mult)
   22.17        done
   22.18      then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
   22.19      let ?w = "v / complex_of_real (root n (cmod b))"
    23.1 --- a/src/HOL/Library/Polynomial.thy	Tue Nov 19 01:30:14 2013 +0100
    23.2 +++ b/src/HOL/Library/Polynomial.thy	Tue Nov 19 10:05:53 2013 +0100
    23.3 @@ -1575,12 +1575,12 @@
    23.4  lemma poly_div_minus_left [simp]:
    23.5    fixes x y :: "'a::field poly"
    23.6    shows "(- x) div y = - (x div y)"
    23.7 -  using div_smult_left [of "- 1::'a"] by (simp del: minus_one) (* FIXME *)
    23.8 +  using div_smult_left [of "- 1::'a"] by simp
    23.9  
   23.10  lemma poly_mod_minus_left [simp]:
   23.11    fixes x y :: "'a::field poly"
   23.12    shows "(- x) mod y = - (x mod y)"
   23.13 -  using mod_smult_left [of "- 1::'a"] by (simp del: minus_one) (* FIXME *)
   23.14 +  using mod_smult_left [of "- 1::'a"] by simp
   23.15  
   23.16  lemma pdivmod_rel_smult_right:
   23.17    "\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk>
   23.18 @@ -1597,13 +1597,12 @@
   23.19  lemma poly_div_minus_right [simp]:
   23.20    fixes x y :: "'a::field poly"
   23.21    shows "x div (- y) = - (x div y)"
   23.22 -  using div_smult_right [of "- 1::'a"]
   23.23 -  by (simp add: nonzero_inverse_minus_eq del: minus_one) (* FIXME *)
   23.24 +  using div_smult_right [of "- 1::'a"] by (simp add: nonzero_inverse_minus_eq)
   23.25  
   23.26  lemma poly_mod_minus_right [simp]:
   23.27    fixes x y :: "'a::field poly"
   23.28    shows "x mod (- y) = x mod y"
   23.29 -  using mod_smult_right [of "- 1::'a"] by (simp del: minus_one) (* FIXME *)
   23.30 +  using mod_smult_right [of "- 1::'a"] by simp
   23.31  
   23.32  lemma pdivmod_rel_mult:
   23.33    "\<lbrakk>pdivmod_rel x y q r; pdivmod_rel q z q' r'\<rbrakk>
    24.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Nov 19 01:30:14 2013 +0100
    24.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Nov 19 10:05:53 2013 +0100
    24.3 @@ -45,8 +45,8 @@
    24.4  
    24.5  section {* Setup for Numerals *}
    24.6  
    24.7 -setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}, @{const_name neg_numeral}] *}
    24.8 -setup {* Predicate_Compile_Data.keep_functions [@{const_name numeral}, @{const_name neg_numeral}] *}
    24.9 +setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}] *}
   24.10 +setup {* Predicate_Compile_Data.keep_functions [@{const_name numeral}] *}
   24.11  
   24.12  setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
   24.13  
    25.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Tue Nov 19 01:30:14 2013 +0100
    25.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Tue Nov 19 10:05:53 2013 +0100
    25.3 @@ -875,7 +875,6 @@
    25.4     @{term "0::real"}, @{term "1::real"},
    25.5     @{term "numeral :: num => nat"},
    25.6     @{term "numeral :: num => real"},
    25.7 -   @{term "neg_numeral :: num => real"},
    25.8     @{term "Num.Bit0"}, @{term "Num.Bit1"}, @{term "Num.One"}];
    25.9  
   25.10  fun check_sos kcts ct =
    26.1 --- a/src/HOL/List.thy	Tue Nov 19 01:30:14 2013 +0100
    26.2 +++ b/src/HOL/List.thy	Tue Nov 19 10:05:53 2013 +0100
    26.3 @@ -3072,9 +3072,9 @@
    26.4  
    26.5  lemmas upto_rec_numeral [simp] =
    26.6    upto.simps[of "numeral m" "numeral n"]
    26.7 -  upto.simps[of "numeral m" "neg_numeral n"]
    26.8 -  upto.simps[of "neg_numeral m" "numeral n"]
    26.9 -  upto.simps[of "neg_numeral m" "neg_numeral n"] for m n
   26.10 +  upto.simps[of "numeral m" "- numeral n"]
   26.11 +  upto.simps[of "- numeral m" "numeral n"]
   26.12 +  upto.simps[of "- numeral m" "- numeral n"] for m n
   26.13  
   26.14  lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
   26.15  by(simp add: upto.simps)
    27.1 --- a/src/HOL/Matrix_LP/ComputeFloat.thy	Tue Nov 19 01:30:14 2013 +0100
    27.2 +++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Tue Nov 19 10:05:53 2013 +0100
    27.3 @@ -79,8 +79,8 @@
    27.4  lemma real_is_int_numeral[simp]: "real_is_int (numeral x)"
    27.5    by (auto simp: real_is_int_def intro!: exI[of _ "numeral x"])
    27.6  
    27.7 -lemma real_is_int_neg_numeral[simp]: "real_is_int (neg_numeral x)"
    27.8 -  by (auto simp: real_is_int_def intro!: exI[of _ "neg_numeral x"])
    27.9 +lemma real_is_int_neg_numeral[simp]: "real_is_int (- numeral x)"
   27.10 +  by (auto simp: real_is_int_def intro!: exI[of _ "- numeral x"])
   27.11  
   27.12  lemma int_of_real_0[simp]: "int_of_real (0::real) = (0::int)"
   27.13  by (simp add: int_of_real_def)
   27.14 @@ -96,7 +96,7 @@
   27.15    by (intro some_equality)
   27.16       (auto simp add: real_of_int_inject[symmetric] simp del: real_of_int_inject)
   27.17  
   27.18 -lemma int_of_real_neg_numeral[simp]: "int_of_real (neg_numeral b) = neg_numeral b"
   27.19 +lemma int_of_real_neg_numeral[simp]: "int_of_real (- numeral b) = - numeral b"
   27.20    unfolding int_of_real_def
   27.21    by (intro some_equality)
   27.22       (auto simp add: real_of_int_inject[symmetric] simp del: real_of_int_inject)
    28.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Nov 19 01:30:14 2013 +0100
    28.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Nov 19 10:05:53 2013 +0100
    28.3 @@ -228,7 +228,10 @@
    28.4    then show ?case by vector
    28.5  qed
    28.6  
    28.7 -lemma one_index[simp]: "(1 :: 'a::one ^'n)$i = 1"
    28.8 +lemma one_index [simp]: "(1 :: 'a :: one ^ 'n) $ i = 1"
    28.9 +  by vector
   28.10 +
   28.11 +lemma neg_one_index [simp]: "(- 1 :: 'a :: {one, uminus} ^ 'n) $ i = - 1"
   28.12    by vector
   28.13  
   28.14  instance vec :: (semiring_char_0, finite) semiring_char_0
   28.15 @@ -244,8 +247,8 @@
   28.16  lemma numeral_index [simp]: "numeral w $ i = numeral w"
   28.17    by (induct w) (simp_all only: numeral.simps vector_add_component one_index)
   28.18  
   28.19 -lemma neg_numeral_index [simp]: "neg_numeral w $ i = neg_numeral w"
   28.20 -  by (simp only: neg_numeral_def vector_uminus_component numeral_index)
   28.21 +lemma neg_numeral_index [simp]: "- numeral w $ i = - numeral w"
   28.22 +  by (simp only: vector_uminus_component numeral_index)
   28.23  
   28.24  instance vec :: (comm_ring_1, finite) comm_ring_1 ..
   28.25  instance vec :: (ring_char_0, finite) ring_char_0 ..
    29.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Nov 19 01:30:14 2013 +0100
    29.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Nov 19 10:05:53 2013 +0100
    29.3 @@ -337,10 +337,10 @@
    29.4    by (simp add: bilinear_def linear_iff)
    29.5  
    29.6  lemma bilinear_lneg: "bilinear h \<Longrightarrow> h (- x) y = - h x y"
    29.7 -  by (simp only: scaleR_minus1_left [symmetric] bilinear_lmul)
    29.8 +  by (drule bilinear_lmul [of _ "- 1"]) simp
    29.9  
   29.10  lemma bilinear_rneg: "bilinear h \<Longrightarrow> h x (- y) = - h x y"
   29.11 -  by (simp only: scaleR_minus1_left [symmetric] bilinear_rmul)
   29.12 +  by (drule bilinear_rmul [of _ _ "- 1"]) simp
   29.13  
   29.14  lemma (in ab_group_add) eq_add_iff: "x = x + y \<longleftrightarrow> y = 0"
   29.15    using add_imp_eq[of x y 0] by auto
    30.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 19 01:30:14 2013 +0100
    30.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 19 10:05:53 2013 +0100
    30.3 @@ -5163,9 +5163,8 @@
    30.4  
    30.5  lemma open_negations:
    30.6    fixes s :: "'a::real_normed_vector set"
    30.7 -  shows "open s \<Longrightarrow> open ((\<lambda> x. -x) ` s)"
    30.8 -  unfolding scaleR_minus1_left [symmetric]
    30.9 -  by (rule open_scaling, auto)
   30.10 +  shows "open s \<Longrightarrow> open ((\<lambda>x. - x) ` s)"
   30.11 +  using open_scaling [of "- 1" s] by simp
   30.12  
   30.13  lemma open_translation:
   30.14    fixes s :: "'a::real_normed_vector set"
    31.1 --- a/src/HOL/NSA/HTranscendental.thy	Tue Nov 19 01:30:14 2013 +0100
    31.2 +++ b/src/HOL/NSA/HTranscendental.thy	Tue Nov 19 10:05:53 2013 +0100
    31.3 @@ -258,7 +258,7 @@
    31.4              simp add: mult_assoc)
    31.5  apply (rule approx_add_right_cancel [where d="-1"])
    31.6  apply (rule approx_sym [THEN [2] approx_trans2])
    31.7 -apply (auto simp add: mem_infmal_iff minus_one [symmetric] simp del: minus_one)
    31.8 +apply (auto simp add: mem_infmal_iff)
    31.9  done
   31.10  
   31.11  lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1"
   31.12 @@ -450,7 +450,7 @@
   31.13  apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   31.14              simp add: mult_assoc)
   31.15  apply (rule approx_add_right_cancel [where d = "-1"])
   31.16 -apply (simp add: minus_one [symmetric] del: minus_one)
   31.17 +apply simp
   31.18  done
   31.19  
   31.20  lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
    32.1 --- a/src/HOL/NSA/HyperDef.thy	Tue Nov 19 01:30:14 2013 +0100
    32.2 +++ b/src/HOL/NSA/HyperDef.thy	Tue Nov 19 10:05:53 2013 +0100
    32.3 @@ -425,7 +425,7 @@
    32.4  declare power_hypreal_of_real_numeral [of _ "numeral w", simp] for w
    32.5  
    32.6  lemma power_hypreal_of_real_neg_numeral:
    32.7 -     "(neg_numeral v :: hypreal) ^ n = hypreal_of_real ((neg_numeral v) ^ n)"
    32.8 +     "(- numeral v :: hypreal) ^ n = hypreal_of_real ((- numeral v) ^ n)"
    32.9  by simp
   32.10  declare power_hypreal_of_real_neg_numeral [of _ "numeral w", simp] for w
   32.11  (*
    33.1 --- a/src/HOL/NSA/NSA.thy	Tue Nov 19 01:30:14 2013 +0100
    33.2 +++ b/src/HOL/NSA/NSA.thy	Tue Nov 19 10:05:53 2013 +0100
    33.3 @@ -654,7 +654,7 @@
    33.4  (*reorientation simplification procedure: reorients (polymorphic)
    33.5    0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
    33.6  simproc_setup approx_reorient_simproc
    33.7 -  ("0 @= x" | "1 @= y" | "numeral w @= z" | "neg_numeral w @= r") =
    33.8 +  ("0 @= x" | "1 @= y" | "numeral w @= z" | "- 1 @= y" | "- numeral w @= r") =
    33.9  {*
   33.10    let val rule = @{thm approx_reorient} RS eq_reflection
   33.11        fun proc phi ss ct = case term_of ct of
   33.12 @@ -1849,8 +1849,12 @@
   33.13  lemma st_numeral [simp]: "st (numeral w) = numeral w"
   33.14  by (rule Reals_numeral [THEN st_SReal_eq])
   33.15  
   33.16 -lemma st_neg_numeral [simp]: "st (neg_numeral w) = neg_numeral w"
   33.17 -by (rule Reals_neg_numeral [THEN st_SReal_eq])
   33.18 +lemma st_neg_numeral [simp]: "st (- numeral w) = - numeral w"
   33.19 +proof -
   33.20 +  from Reals_numeral have "numeral w \<in> \<real>" .
   33.21 +  then have "- numeral w \<in> \<real>" by simp
   33.22 +  with st_SReal_eq show ?thesis .
   33.23 +qed
   33.24  
   33.25  lemma st_0 [simp]: "st 0 = 0"
   33.26  by (simp add: st_SReal_eq)
   33.27 @@ -1858,6 +1862,9 @@
   33.28  lemma st_1 [simp]: "st 1 = 1"
   33.29  by (simp add: st_SReal_eq)
   33.30  
   33.31 +lemma st_neg_1 [simp]: "st (- 1) = - 1"
   33.32 +by (simp add: st_SReal_eq)
   33.33 +
   33.34  lemma st_minus: "x \<in> HFinite \<Longrightarrow> st (- x) = - st x"
   33.35  by (simp add: st_unique st_SReal st_approx_self approx_minus)
   33.36  
    34.1 --- a/src/HOL/NSA/NSComplex.thy	Tue Nov 19 01:30:14 2013 +0100
    34.2 +++ b/src/HOL/NSA/NSComplex.thy	Tue Nov 19 10:05:53 2013 +0100
    34.3 @@ -635,7 +635,7 @@
    34.4  by transfer (rule of_real_numeral [symmetric])
    34.5  
    34.6  lemma hcomplex_hypreal_neg_numeral:
    34.7 -  "hcomplex_of_complex (neg_numeral w) = hcomplex_of_hypreal(neg_numeral w)"
    34.8 +  "hcomplex_of_complex (- numeral w) = hcomplex_of_hypreal(- numeral w)"
    34.9  by transfer (rule of_real_neg_numeral [symmetric])
   34.10  
   34.11  lemma hcomplex_numeral_hcnj [simp]:
   34.12 @@ -647,7 +647,7 @@
   34.13  by transfer (rule norm_numeral)
   34.14  
   34.15  lemma hcomplex_neg_numeral_hcmod [simp]: 
   34.16 -      "hcmod(neg_numeral v :: hcomplex) = (numeral v :: hypreal)"
   34.17 +      "hcmod(- numeral v :: hcomplex) = (numeral v :: hypreal)"
   34.18  by transfer (rule norm_neg_numeral)
   34.19  
   34.20  lemma hcomplex_numeral_hRe [simp]: 
    35.1 --- a/src/HOL/NSA/StarDef.thy	Tue Nov 19 01:30:14 2013 +0100
    35.2 +++ b/src/HOL/NSA/StarDef.thy	Tue Nov 19 10:05:53 2013 +0100
    35.3 @@ -968,13 +968,13 @@
    35.4  by transfer (rule refl)
    35.5  
    35.6  lemma star_neg_numeral_def [transfer_unfold]:
    35.7 -  "neg_numeral k = star_of (neg_numeral k)"
    35.8 -by (simp only: neg_numeral_def star_of_minus star_of_numeral)
    35.9 +  "- numeral k = star_of (- numeral k)"
   35.10 +by (simp only: star_of_minus star_of_numeral)
   35.11  
   35.12 -lemma Standard_neg_numeral [simp]: "neg_numeral k \<in> Standard"
   35.13 -by (simp add: star_neg_numeral_def)
   35.14 +lemma Standard_neg_numeral [simp]: "- numeral k \<in> Standard"
   35.15 +  using star_neg_numeral_def [of k] by simp
   35.16  
   35.17 -lemma star_of_neg_numeral [simp]: "star_of (neg_numeral k) = neg_numeral k"
   35.18 +lemma star_of_neg_numeral [simp]: "star_of (- numeral k) = - numeral k"
   35.19  by transfer (rule refl)
   35.20  
   35.21  lemma star_of_nat_def [transfer_unfold]: "of_nat n = star_of (of_nat n)"
   35.22 @@ -987,12 +987,12 @@
   35.23    star_of_less [of _ "numeral k", simplified star_of_numeral]
   35.24    star_of_le   [of _ "numeral k", simplified star_of_numeral]
   35.25    star_of_eq   [of _ "numeral k", simplified star_of_numeral]
   35.26 -  star_of_less [of "neg_numeral k", simplified star_of_numeral]
   35.27 -  star_of_le   [of "neg_numeral k", simplified star_of_numeral]
   35.28 -  star_of_eq   [of "neg_numeral k", simplified star_of_numeral]
   35.29 -  star_of_less [of _ "neg_numeral k", simplified star_of_numeral]
   35.30 -  star_of_le   [of _ "neg_numeral k", simplified star_of_numeral]
   35.31 -  star_of_eq   [of _ "neg_numeral k", simplified star_of_numeral] for k
   35.32 +  star_of_less [of "- numeral k", simplified star_of_numeral]
   35.33 +  star_of_le   [of "- numeral k", simplified star_of_numeral]
   35.34 +  star_of_eq   [of "- numeral k", simplified star_of_numeral]
   35.35 +  star_of_less [of _ "- numeral k", simplified star_of_numeral]
   35.36 +  star_of_le   [of _ "- numeral k", simplified star_of_numeral]
   35.37 +  star_of_eq   [of _ "- numeral k", simplified star_of_numeral] for k
   35.38  
   35.39  lemma Standard_of_nat [simp]: "of_nat n \<in> Standard"
   35.40  by (simp add: star_of_nat_def)
    36.1 --- a/src/HOL/Nominal/Nominal.thy	Tue Nov 19 01:30:14 2013 +0100
    36.2 +++ b/src/HOL/Nominal/Nominal.thy	Tue Nov 19 10:05:53 2013 +0100
    36.3 @@ -3517,7 +3517,7 @@
    36.4  by (simp add: perm_int_def perm_int_def)
    36.5  
    36.6  lemma neg_numeral_int_eqvt:
    36.7 - shows "pi\<bullet>((neg_numeral n)::int) = neg_numeral n"
    36.8 + shows "pi\<bullet>((- numeral n)::int) = - numeral n"
    36.9  by (simp add: perm_int_def perm_int_def)
   36.10  
   36.11  lemma max_int_eqvt:
    37.1 --- a/src/HOL/Num.thy	Tue Nov 19 01:30:14 2013 +0100
    37.2 +++ b/src/HOL/Num.thy	Tue Nov 19 10:05:53 2013 +0100
    37.3 @@ -275,16 +275,6 @@
    37.4  
    37.5  end
    37.6  
    37.7 -text {* Negative numerals. *}
    37.8 -
    37.9 -class neg_numeral = numeral + group_add
   37.10 -begin
   37.11 -
   37.12 -definition neg_numeral :: "num \<Rightarrow> 'a" where
   37.13 -  "neg_numeral k = - numeral k"
   37.14 -
   37.15 -end
   37.16 -
   37.17  text {* Numeral syntax. *}
   37.18  
   37.19  syntax
   37.20 @@ -299,8 +289,8 @@
   37.21          | (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n
   37.22          | (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n)
   37.23        else raise Match
   37.24 -    val pos = Syntax.const @{const_name numeral}
   37.25 -    val neg = Syntax.const @{const_name neg_numeral}
   37.26 +    val numeral = Syntax.const @{const_name numeral}
   37.27 +    val uminus = Syntax.const @{const_name uminus}
   37.28      val one = Syntax.const @{const_name Groups.one}
   37.29      val zero = Syntax.const @{const_name Groups.zero}
   37.30      fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
   37.31 @@ -311,8 +301,9 @@
   37.32            in
   37.33              if value = 0 then zero else
   37.34              if value > 0
   37.35 -            then pos $ num_of_int value
   37.36 -            else neg $ num_of_int (~value)
   37.37 +            then numeral $ num_of_int value
   37.38 +            else if value = ~1 then uminus $ one
   37.39 +            else uminus $ (numeral $ num_of_int (~value))
   37.40            end
   37.41        | numeral_tr ts = raise TERM ("numeral_tr", ts);
   37.42    in [("_Numeral", K numeral_tr)] end
   37.43 @@ -323,12 +314,12 @@
   37.44      fun dest_num (Const (@{const_syntax Bit0}, _) $ n) = 2 * dest_num n
   37.45        | dest_num (Const (@{const_syntax Bit1}, _) $ n) = 2 * dest_num n + 1
   37.46        | dest_num (Const (@{const_syntax One}, _)) = 1;
   37.47 -    fun num_tr' sign ctxt T [n] =
   37.48 +    fun num_tr' ctxt T [n] =
   37.49        let
   37.50          val k = dest_num n;
   37.51          val t' =
   37.52            Syntax.const @{syntax_const "_Numeral"} $
   37.53 -            Syntax.free (sign ^ string_of_int k);
   37.54 +            Syntax.free (string_of_int k);
   37.55        in
   37.56          (case T of
   37.57            Type (@{type_name fun}, [_, T']) =>
   37.58 @@ -339,8 +330,7 @@
   37.59          | _ => if T = dummyT then t' else raise Match)
   37.60        end;
   37.61    in
   37.62 -   [(@{const_syntax numeral}, num_tr' ""),
   37.63 -    (@{const_syntax neg_numeral}, num_tr' "-")]
   37.64 +   [(@{const_syntax numeral}, num_tr')]
   37.65    end
   37.66  *}
   37.67  
   37.68 @@ -383,9 +373,13 @@
   37.69    Structures with negation: class @{text neg_numeral}
   37.70  *}
   37.71  
   37.72 -context neg_numeral
   37.73 +class neg_numeral = numeral + group_add
   37.74  begin
   37.75  
   37.76 +lemma uminus_numeral_One:
   37.77 +  "- Numeral1 = - 1"
   37.78 +  by (simp add: numeral_One)
   37.79 +
   37.80  text {* Numerals form an abelian subgroup. *}
   37.81  
   37.82  inductive is_num :: "'a \<Rightarrow> bool" where
   37.83 @@ -403,7 +397,7 @@
   37.84    apply simp
   37.85    apply (rule_tac a=x in add_left_imp_eq)
   37.86    apply (rule_tac a=x in add_right_imp_eq)
   37.87 -  apply (simp add: add_assoc minus_add_cancel)
   37.88 +  apply (simp add: add_assoc)
   37.89    apply (simp add: add_assoc [symmetric], simp add: add_assoc)
   37.90    apply (rule_tac a=x in add_left_imp_eq)
   37.91    apply (rule_tac a=x in add_right_imp_eq)
   37.92 @@ -431,77 +425,85 @@
   37.93    by (simp only: BitM_plus_one [symmetric] numeral_add numeral_One eq_diff_eq)
   37.94  
   37.95  lemma dbl_simps [simp]:
   37.96 -  "dbl (neg_numeral k) = neg_numeral (Bit0 k)"
   37.97 +  "dbl (- numeral k) = - dbl (numeral k)"
   37.98    "dbl 0 = 0"
   37.99    "dbl 1 = 2"
  37.100 +  "dbl (- 1) = - 2"
  37.101    "dbl (numeral k) = numeral (Bit0 k)"
  37.102 -  by (simp_all add: dbl_def neg_numeral_def numeral.simps minus_add)
  37.103 +  by (simp_all add: dbl_def numeral.simps minus_add)
  37.104  
  37.105  lemma dbl_inc_simps [simp]:
  37.106 -  "dbl_inc (neg_numeral k) = neg_numeral (BitM k)"
  37.107 +  "dbl_inc (- numeral k) = - dbl_dec (numeral k)"
  37.108    "dbl_inc 0 = 1"
  37.109    "dbl_inc 1 = 3"
  37.110 +  "dbl_inc (- 1) = - 1"
  37.111    "dbl_inc (numeral k) = numeral (Bit1 k)"
  37.112 -  by (simp_all add: dbl_inc_def neg_numeral_def numeral.simps numeral_BitM is_num_normalize algebra_simps del: add_uminus_conv_diff)
  37.113 +  by (simp_all add: dbl_inc_def dbl_dec_def numeral.simps numeral_BitM is_num_normalize algebra_simps del: add_uminus_conv_diff)
  37.114  
  37.115  lemma dbl_dec_simps [simp]:
  37.116 -  "dbl_dec (neg_numeral k) = neg_numeral (Bit1 k)"
  37.117 -  "dbl_dec 0 = -1"
  37.118 +  "dbl_dec (- numeral k) = - dbl_inc (numeral k)"
  37.119 +  "dbl_dec 0 = - 1"
  37.120    "dbl_dec 1 = 1"
  37.121 +  "dbl_dec (- 1) = - 3"
  37.122    "dbl_dec (numeral k) = numeral (BitM k)"
  37.123 -  by (simp_all add: dbl_dec_def neg_numeral_def numeral.simps numeral_BitM is_num_normalize)
  37.124 +  by (simp_all add: dbl_dec_def dbl_inc_def numeral.simps numeral_BitM is_num_normalize)
  37.125  
  37.126  lemma sub_num_simps [simp]:
  37.127    "sub One One = 0"
  37.128 -  "sub One (Bit0 l) = neg_numeral (BitM l)"
  37.129 -  "sub One (Bit1 l) = neg_numeral (Bit0 l)"
  37.130 +  "sub One (Bit0 l) = - numeral (BitM l)"
  37.131 +  "sub One (Bit1 l) = - numeral (Bit0 l)"
  37.132    "sub (Bit0 k) One = numeral (BitM k)"
  37.133    "sub (Bit1 k) One = numeral (Bit0 k)"
  37.134    "sub (Bit0 k) (Bit0 l) = dbl (sub k l)"
  37.135    "sub (Bit0 k) (Bit1 l) = dbl_dec (sub k l)"
  37.136    "sub (Bit1 k) (Bit0 l) = dbl_inc (sub k l)"
  37.137    "sub (Bit1 k) (Bit1 l) = dbl (sub k l)"
  37.138 -  by (simp_all add: dbl_def dbl_dec_def dbl_inc_def sub_def neg_numeral_def numeral.simps
  37.139 +  by (simp_all add: dbl_def dbl_dec_def dbl_inc_def sub_def numeral.simps
  37.140      numeral_BitM is_num_normalize del: add_uminus_conv_diff add: diff_conv_add_uminus)
  37.141  
  37.142  lemma add_neg_numeral_simps:
  37.143 -  "numeral m + neg_numeral n = sub m n"
  37.144 -  "neg_numeral m + numeral n = sub n m"
  37.145 -  "neg_numeral m + neg_numeral n = neg_numeral (m + n)"
  37.146 -  by (simp_all add: sub_def neg_numeral_def numeral_add numeral.simps is_num_normalize
  37.147 +  "numeral m + - numeral n = sub m n"
  37.148 +  "- numeral m + numeral n = sub n m"
  37.149 +  "- numeral m + - numeral n = - (numeral m + numeral n)"
  37.150 +  by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize
  37.151      del: add_uminus_conv_diff add: diff_conv_add_uminus)
  37.152  
  37.153  lemma add_neg_numeral_special:
  37.154 -  "1 + neg_numeral m = sub One m"
  37.155 -  "neg_numeral m + 1 = sub One m"
  37.156 -  by (simp_all add: sub_def neg_numeral_def numeral_add numeral.simps is_num_normalize)
  37.157 +  "1 + - numeral m = sub One m"
  37.158 +  "- numeral m + 1 = sub One m"
  37.159 +  "numeral m + - 1 = sub m One"
  37.160 +  "- 1 + numeral n = sub n One"
  37.161 +  "- 1 + - numeral n = - numeral (inc n)"
  37.162 +  "- numeral m + - 1 = - numeral (inc m)"
  37.163 +  "1 + - 1 = 0"
  37.164 +  "- 1 + 1 = 0"
  37.165 +  "- 1 + - 1 = - 2"
  37.166 +  by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize right_minus numeral_inc
  37.167 +    del: add_uminus_conv_diff add: diff_conv_add_uminus)
  37.168  
  37.169  lemma diff_numeral_simps:
  37.170    "numeral m - numeral n = sub m n"
  37.171 -  "numeral m - neg_numeral n = numeral (m + n)"
  37.172 -  "neg_numeral m - numeral n = neg_numeral (m + n)"
  37.173 -  "neg_numeral m - neg_numeral n = sub n m"
  37.174 -  by (simp_all add: neg_numeral_def sub_def numeral_add numeral.simps is_num_normalize
  37.175 +  "numeral m - - numeral n = numeral (m + n)"
  37.176 +  "- numeral m - numeral n = - numeral (m + n)"
  37.177 +  "- numeral m - - numeral n = sub n m"
  37.178 +  by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize
  37.179      del: add_uminus_conv_diff add: diff_conv_add_uminus)
  37.180  
  37.181  lemma diff_numeral_special:
  37.182    "1 - numeral n = sub One n"
  37.183 -  "1 - neg_numeral n = numeral (One + n)"
  37.184    "numeral m - 1 = sub m One"
  37.185 -  "neg_numeral m - 1 = neg_numeral (m + One)"
  37.186 -  by (simp_all add: neg_numeral_def sub_def numeral_add numeral.simps add: is_num_normalize)
  37.187 -
  37.188 -lemma minus_one: "- 1 = -1"
  37.189 -  unfolding neg_numeral_def numeral.simps ..
  37.190 -
  37.191 -lemma minus_numeral: "- numeral n = neg_numeral n"
  37.192 -  unfolding neg_numeral_def ..
  37.193 -
  37.194 -lemma minus_neg_numeral: "- neg_numeral n = numeral n"
  37.195 -  unfolding neg_numeral_def by simp
  37.196 -
  37.197 -lemmas minus_numeral_simps [simp] =
  37.198 -  minus_one minus_numeral minus_neg_numeral
  37.199 +  "1 - - numeral n = numeral (One + n)"
  37.200 +  "- numeral m - 1 = - numeral (m + One)"
  37.201 +  "- 1 - numeral n = - numeral (inc n)"
  37.202 +  "numeral m - - 1 = numeral (inc m)"
  37.203 +  "- 1 - - numeral n = sub n One"
  37.204 +  "- numeral m - - 1 = sub One m"
  37.205 +  "1 - 1 = 0"
  37.206 +  "- 1 - 1 = - 2"
  37.207 +  "1 - - 1 = 2"
  37.208 +  "- 1 - - 1 = 0"
  37.209 +  by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize numeral_inc
  37.210 +    del: add_uminus_conv_diff add: diff_conv_add_uminus)
  37.211  
  37.212  end
  37.213  
  37.214 @@ -675,17 +677,17 @@
  37.215  subclass neg_numeral ..
  37.216  
  37.217  lemma mult_neg_numeral_simps:
  37.218 -  "neg_numeral m * neg_numeral n = numeral (m * n)"
  37.219 -  "neg_numeral m * numeral n = neg_numeral (m * n)"
  37.220 -  "numeral m * neg_numeral n = neg_numeral (m * n)"
  37.221 -  unfolding neg_numeral_def mult_minus_left mult_minus_right
  37.222 +  "- numeral m * - numeral n = numeral (m * n)"
  37.223 +  "- numeral m * numeral n = - numeral (m * n)"
  37.224 +  "numeral m * - numeral n = - numeral (m * n)"
  37.225 +  unfolding mult_minus_left mult_minus_right
  37.226    by (simp_all only: minus_minus numeral_mult)
  37.227  
  37.228 -lemma mult_minus1 [simp]: "-1 * z = - z"
  37.229 -  unfolding neg_numeral_def numeral.simps mult_minus_left by simp
  37.230 +lemma mult_minus1 [simp]: "- 1 * z = - z"
  37.231 +  unfolding numeral.simps mult_minus_left by simp
  37.232  
  37.233 -lemma mult_minus1_right [simp]: "z * -1 = - z"
  37.234 -  unfolding neg_numeral_def numeral.simps mult_minus_right by simp
  37.235 +lemma mult_minus1_right [simp]: "z * - 1 = - z"
  37.236 +  unfolding numeral.simps mult_minus_right by simp
  37.237  
  37.238  end
  37.239  
  37.240 @@ -708,9 +710,15 @@
  37.241  lemma not_iszero_Numeral1: "\<not> iszero Numeral1"
  37.242    by (simp add: numeral_One)
  37.243  
  37.244 +lemma not_iszero_neg_1 [simp]: "\<not> iszero (- 1)"
  37.245 +  by (simp add: iszero_def)
  37.246 +
  37.247 +lemma not_iszero_neg_Numeral1: "\<not> iszero (- Numeral1)"
  37.248 +  by (simp add: numeral_One)
  37.249 +
  37.250  lemma iszero_neg_numeral [simp]:
  37.251 -  "iszero (neg_numeral w) \<longleftrightarrow> iszero (numeral w)"
  37.252 -  unfolding iszero_def neg_numeral_def
  37.253 +  "iszero (- numeral w) \<longleftrightarrow> iszero (numeral w)"
  37.254 +  unfolding iszero_def
  37.255    by (rule neg_equal_0_iff_equal)
  37.256  
  37.257  lemma eq_iff_iszero_diff: "x = y \<longleftrightarrow> iszero (x - y)"
  37.258 @@ -730,17 +738,17 @@
  37.259  
  37.260  lemma eq_numeral_iff_iszero:
  37.261    "numeral x = numeral y \<longleftrightarrow> iszero (sub x y)"
  37.262 -  "numeral x = neg_numeral y \<longleftrightarrow> iszero (numeral (x + y))"
  37.263 -  "neg_numeral x = numeral y \<longleftrightarrow> iszero (numeral (x + y))"
  37.264 -  "neg_numeral x = neg_numeral y \<longleftrightarrow> iszero (sub y x)"
  37.265 +  "numeral x = - numeral y \<longleftrightarrow> iszero (numeral (x + y))"
  37.266 +  "- numeral x = numeral y \<longleftrightarrow> iszero (numeral (x + y))"
  37.267 +  "- numeral x = - numeral y \<longleftrightarrow> iszero (sub y x)"
  37.268    "numeral x = 1 \<longleftrightarrow> iszero (sub x One)"
  37.269    "1 = numeral y \<longleftrightarrow> iszero (sub One y)"
  37.270 -  "neg_numeral x = 1 \<longleftrightarrow> iszero (numeral (x + One))"
  37.271 -  "1 = neg_numeral y \<longleftrightarrow> iszero (numeral (One + y))"
  37.272 +  "- numeral x = 1 \<longleftrightarrow> iszero (numeral (x + One))"
  37.273 +  "1 = - numeral y \<longleftrightarrow> iszero (numeral (One + y))"
  37.274    "numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
  37.275    "0 = numeral y \<longleftrightarrow> iszero (numeral y)"
  37.276 -  "neg_numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
  37.277 -  "0 = neg_numeral y \<longleftrightarrow> iszero (numeral y)"
  37.278 +  "- numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
  37.279 +  "0 = - numeral y \<longleftrightarrow> iszero (numeral y)"
  37.280    unfolding eq_iff_iszero_diff diff_numeral_simps diff_numeral_special
  37.281    by simp_all
  37.282  
  37.283 @@ -756,33 +764,69 @@
  37.284  lemma not_iszero_numeral [simp]: "\<not> iszero (numeral w)"
  37.285    by (simp add: iszero_def)
  37.286  
  37.287 -lemma neg_numeral_eq_iff: "neg_numeral m = neg_numeral n \<longleftrightarrow> m = n"
  37.288 -  by (simp only: neg_numeral_def neg_equal_iff_equal numeral_eq_iff)
  37.289 +lemma neg_numeral_eq_iff: "- numeral m = - numeral n \<longleftrightarrow> m = n"
  37.290 +  by simp
  37.291  
  37.292 -lemma numeral_neq_neg_numeral: "numeral m \<noteq> neg_numeral n"
  37.293 -  unfolding neg_numeral_def eq_neg_iff_add_eq_0
  37.294 +lemma numeral_neq_neg_numeral: "numeral m \<noteq> - numeral n"
  37.295 +  unfolding eq_neg_iff_add_eq_0
  37.296    by (simp add: numeral_plus_numeral)
  37.297  
  37.298 -lemma neg_numeral_neq_numeral: "neg_numeral m \<noteq> numeral n"
  37.299 +lemma neg_numeral_neq_numeral: "- numeral m \<noteq> numeral n"
  37.300    by (rule numeral_neq_neg_numeral [symmetric])
  37.301  
  37.302 -lemma zero_neq_neg_numeral: "0 \<noteq> neg_numeral n"
  37.303 -  unfolding neg_numeral_def neg_0_equal_iff_equal by simp
  37.304 +lemma zero_neq_neg_numeral: "0 \<noteq> - numeral n"
  37.305 +  unfolding neg_0_equal_iff_equal by simp
  37.306  
  37.307 -lemma neg_numeral_neq_zero: "neg_numeral n \<noteq> 0"
  37.308 -  unfolding neg_numeral_def neg_equal_0_iff_equal by simp
  37.309 +lemma neg_numeral_neq_zero: "- numeral n \<noteq> 0"
  37.310 +  unfolding neg_equal_0_iff_equal by simp
  37.311  
  37.312 -lemma one_neq_neg_numeral: "1 \<noteq> neg_numeral n"
  37.313 +lemma one_neq_neg_numeral: "1 \<noteq> - numeral n"
  37.314    using numeral_neq_neg_numeral [of One n] by (simp add: numeral_One)
  37.315  
  37.316 -lemma neg_numeral_neq_one: "neg_numeral n \<noteq> 1"
  37.317 +lemma neg_numeral_neq_one: "- numeral n \<noteq> 1"
  37.318    using neg_numeral_neq_numeral [of n One] by (simp add: numeral_One)
  37.319  
  37.320 +lemma neg_one_neq_numeral:
  37.321 +  "- 1 \<noteq> numeral n"
  37.322 +  using neg_numeral_neq_numeral [of One n] by (simp add: numeral_One)
  37.323 +
  37.324 +lemma numeral_neq_neg_one:
  37.325 +  "numeral n \<noteq> - 1"
  37.326 +  using numeral_neq_neg_numeral [of n One] by (simp add: numeral_One)
  37.327 +
  37.328 +lemma neg_one_eq_numeral_iff:
  37.329 +  "- 1 = - numeral n \<longleftrightarrow> n = One"
  37.330 +  using neg_numeral_eq_iff [of One n] by (auto simp add: numeral_One)
  37.331 +
  37.332 +lemma numeral_eq_neg_one_iff:
  37.333 +  "- numeral n = - 1 \<longleftrightarrow> n = One"
  37.334 +  using neg_numeral_eq_iff [of n One] by (auto simp add: numeral_One)
  37.335 +
  37.336 +lemma neg_one_neq_zero:
  37.337 +  "- 1 \<noteq> 0"
  37.338 +  by simp
  37.339 +
  37.340 +lemma zero_neq_neg_one:
  37.341 +  "0 \<noteq> - 1"
  37.342 +  by simp
  37.343 +
  37.344 +lemma neg_one_neq_one:
  37.345 +  "- 1 \<noteq> 1"
  37.346 +  using neg_numeral_neq_numeral [of One One] by (simp only: numeral_One not_False_eq_True)
  37.347 +
  37.348 +lemma one_neq_neg_one:
  37.349 +  "1 \<noteq> - 1"
  37.350 +  using numeral_neq_neg_numeral [of One One] by (simp only: numeral_One not_False_eq_True)
  37.351 +
  37.352  lemmas eq_neg_numeral_simps [simp] =
  37.353    neg_numeral_eq_iff
  37.354    numeral_neq_neg_numeral neg_numeral_neq_numeral
  37.355    one_neq_neg_numeral neg_numeral_neq_one
  37.356    zero_neq_neg_numeral neg_numeral_neq_zero
  37.357 +  neg_one_neq_numeral numeral_neq_neg_one
  37.358 +  neg_one_eq_numeral_iff numeral_eq_neg_one_iff
  37.359 +  neg_one_neq_zero zero_neq_neg_one
  37.360 +  neg_one_neq_one one_neq_neg_one
  37.361  
  37.362  end
  37.363  
  37.364 @@ -795,48 +839,72 @@
  37.365  
  37.366  subclass ring_char_0 ..
  37.367  
  37.368 -lemma neg_numeral_le_iff: "neg_numeral m \<le> neg_numeral n \<longleftrightarrow> n \<le> m"
  37.369 -  by (simp only: neg_numeral_def neg_le_iff_le numeral_le_iff)
  37.370 +lemma neg_numeral_le_iff: "- numeral m \<le> - numeral n \<longleftrightarrow> n \<le> m"
  37.371 +  by (simp only: neg_le_iff_le numeral_le_iff)
  37.372  
  37.373 -lemma neg_numeral_less_iff: "neg_numeral m < neg_numeral n \<longleftrightarrow> n < m"
  37.374 -  by (simp only: neg_numeral_def neg_less_iff_less numeral_less_iff)
  37.375 +lemma neg_numeral_less_iff: "- numeral m < - numeral n \<longleftrightarrow> n < m"
  37.376 +  by (simp only: neg_less_iff_less numeral_less_iff)
  37.377  
  37.378 -lemma neg_numeral_less_zero: "neg_numeral n < 0"
  37.379 -  by (simp only: neg_numeral_def neg_less_0_iff_less zero_less_numeral)
  37.380 +lemma neg_numeral_less_zero: "- numeral n < 0"
  37.381 +  by (simp only: neg_less_0_iff_less zero_less_numeral)
  37.382  
  37.383 -lemma neg_numeral_le_zero: "neg_numeral n \<le> 0"
  37.384 -  by (simp only: neg_numeral_def neg_le_0_iff_le zero_le_numeral)
  37.385 +lemma neg_numeral_le_zero: "- numeral n \<le> 0"
  37.386 +  by (simp only: neg_le_0_iff_le zero_le_numeral)
  37.387  
  37.388 -lemma not_zero_less_neg_numeral: "\<not> 0 < neg_numeral n"
  37.389 +lemma not_zero_less_neg_numeral: "\<not> 0 < - numeral n"
  37.390    by (simp only: not_less neg_numeral_le_zero)
  37.391  
  37.392 -lemma not_zero_le_neg_numeral: "\<not> 0 \<le> neg_numeral n"
  37.393 +lemma not_zero_le_neg_numeral: "\<not> 0 \<le> - numeral n"
  37.394    by (simp only: not_le neg_numeral_less_zero)
  37.395  
  37.396 -lemma neg_numeral_less_numeral: "neg_numeral m < numeral n"
  37.397 +lemma neg_numeral_less_numeral: "- numeral m < numeral n"
  37.398    using neg_numeral_less_zero zero_less_numeral by (rule less_trans)
  37.399  
  37.400 -lemma neg_numeral_le_numeral: "neg_numeral m \<le> numeral n"
  37.401 +lemma neg_numeral_le_numeral: "- numeral m \<le> numeral n"
  37.402    by (simp only: less_imp_le neg_numeral_less_numeral)
  37.403  
  37.404 -lemma not_numeral_less_neg_numeral: "\<not> numeral m < neg_numeral n"
  37.405 +lemma not_numeral_less_neg_numeral: "\<not> numeral m < - numeral n"
  37.406    by (simp only: not_less neg_numeral_le_numeral)
  37.407  
  37.408 -lemma not_numeral_le_neg_numeral: "\<not> numeral m \<le> neg_numeral n"
  37.409 +lemma not_numeral_le_neg_numeral: "\<not> numeral m \<le> - numeral n"
  37.410    by (simp only: not_le neg_numeral_less_numeral)
  37.411    
  37.412 -lemma neg_numeral_less_one: "neg_numeral m < 1"
  37.413 +lemma neg_numeral_less_one: "- numeral m < 1"
  37.414    by (rule neg_numeral_less_numeral [of m One, unfolded numeral_One])
  37.415  
  37.416 -lemma neg_numeral_le_one: "neg_numeral m \<le> 1"
  37.417 +lemma neg_numeral_le_one: "- numeral m \<le> 1"
  37.418    by (rule neg_numeral_le_numeral [of m One, unfolded numeral_One])
  37.419  
  37.420 -lemma not_one_less_neg_numeral: "\<not> 1 < neg_numeral m"
  37.421 +lemma not_one_less_neg_numeral: "\<not> 1 < - numeral m"
  37.422    by (simp only: not_less neg_numeral_le_one)
  37.423  
  37.424 -lemma not_one_le_neg_numeral: "\<not> 1 \<le> neg_numeral m"
  37.425 +lemma not_one_le_neg_numeral: "\<not> 1 \<le> - numeral m"
  37.426    by (simp only: not_le neg_numeral_less_one)
  37.427  
  37.428 +lemma not_numeral_less_neg_one: "\<not> numeral m < - 1"
  37.429 +  using not_numeral_less_neg_numeral [of m One] by (simp add: numeral_One)
  37.430 +
  37.431 +lemma not_numeral_le_neg_one: "\<not> numeral m \<le> - 1"
  37.432 +  using not_numeral_le_neg_numeral [of m One] by (simp add: numeral_One)
  37.433 +
  37.434 +lemma neg_one_less_numeral: "- 1 < numeral m"
  37.435 +  using neg_numeral_less_numeral [of One m] by (simp add: numeral_One)
  37.436 +
  37.437 +lemma neg_one_le_numeral: "- 1 \<le> numeral m"
  37.438 +  using neg_numeral_le_numeral [of One m] by (simp add: numeral_One)
  37.439 +
  37.440 +lemma neg_numeral_less_neg_one_iff: "- numeral m < - 1 \<longleftrightarrow> m \<noteq> One"
  37.441 +  by (cases m) simp_all
  37.442 +
  37.443 +lemma neg_numeral_le_neg_one: "- numeral m \<le> - 1"
  37.444 +  by simp
  37.445 +
  37.446 +lemma not_neg_one_less_neg_numeral: "\<not> - 1 < - numeral m"
  37.447 +  by simp
  37.448 +
  37.449 +lemma not_neg_one_le_neg_numeral_iff: "\<not> - 1 \<le> - numeral m \<longleftrightarrow> m \<noteq> One"
  37.450 +  by (cases m) simp_all
  37.451 +
  37.452  lemma sub_non_negative:
  37.453    "sub n m \<ge> 0 \<longleftrightarrow> n \<ge> m"
  37.454    by (simp only: sub_def le_diff_eq) simp
  37.455 @@ -858,18 +926,40 @@
  37.456    neg_numeral_le_numeral not_numeral_le_neg_numeral
  37.457    neg_numeral_le_zero not_zero_le_neg_numeral
  37.458    neg_numeral_le_one not_one_le_neg_numeral
  37.459 +  neg_one_le_numeral not_numeral_le_neg_one
  37.460 +  neg_numeral_le_neg_one not_neg_one_le_neg_numeral_iff
  37.461 +
  37.462 +lemma le_minus_one_simps [simp]:
  37.463 +  "- 1 \<le> 0"
  37.464 +  "- 1 \<le> 1"
  37.465 +  "\<not> 0 \<le> - 1"
  37.466 +  "\<not> 1 \<le> - 1"
  37.467 +  by simp_all
  37.468  
  37.469  lemmas less_neg_numeral_simps [simp] =
  37.470    neg_numeral_less_iff
  37.471    neg_numeral_less_numeral not_numeral_less_neg_numeral
  37.472    neg_numeral_less_zero not_zero_less_neg_numeral
  37.473    neg_numeral_less_one not_one_less_neg_numeral
  37.474 +  neg_one_less_numeral not_numeral_less_neg_one
  37.475 +  neg_numeral_less_neg_one_iff not_neg_one_less_neg_numeral
  37.476 +
  37.477 +lemma less_minus_one_simps [simp]:
  37.478 +  "- 1 < 0"
  37.479 +  "- 1 < 1"
  37.480 +  "\<not> 0 < - 1"
  37.481 +  "\<not> 1 < - 1"
  37.482 +  by (simp_all add: less_le)
  37.483  
  37.484  lemma abs_numeral [simp]: "abs (numeral n) = numeral n"
  37.485    by simp
  37.486  
  37.487 -lemma abs_neg_numeral [simp]: "abs (neg_numeral n) = numeral n"
  37.488 -  by (simp only: neg_numeral_def abs_minus_cancel abs_numeral)
  37.489 +lemma abs_neg_numeral [simp]: "abs (- numeral n) = numeral n"
  37.490 +  by (simp only: abs_minus_cancel abs_numeral)
  37.491 +
  37.492 +lemma abs_neg_one [simp]:
  37.493 +  "abs (- 1) = 1"
  37.494 +  by simp
  37.495  
  37.496  end
  37.497  
  37.498 @@ -1032,31 +1122,36 @@
  37.499  text{*Theorem lists for the cancellation simprocs. The use of a binary
  37.500  numeral for 1 reduces the number of special cases.*}
  37.501  
  37.502 -lemmas mult_1s =
  37.503 -  mult_numeral_1 mult_numeral_1_right 
  37.504 -  mult_minus1 mult_minus1_right
  37.505 +lemma mult_1s:
  37.506 +  fixes a :: "'a::semiring_numeral"
  37.507 +    and b :: "'b::ring_1"
  37.508 +  shows "Numeral1 * a = a"
  37.509 +    "a * Numeral1 = a"
  37.510 +    "- Numeral1 * b = - b"
  37.511 +    "b * - Numeral1 = - b"
  37.512 +  by simp_all
  37.513  
  37.514  setup {*
  37.515    Reorient_Proc.add
  37.516      (fn Const (@{const_name numeral}, _) $ _ => true
  37.517 -    | Const (@{const_name neg_numeral}, _) $ _ => true
  37.518 +    | Const (@{const_name uminus}, _) $ (Const (@{const_name numeral}, _) $ _) => true
  37.519      | _ => false)
  37.520  *}
  37.521  
  37.522  simproc_setup reorient_numeral
  37.523 -  ("numeral w = x" | "neg_numeral w = y") = Reorient_Proc.proc
  37.524 +  ("numeral w = x" | "- numeral w = y") = Reorient_Proc.proc
  37.525  
  37.526  
  37.527  subsubsection {* Simplification of arithmetic operations on integer constants. *}
  37.528  
  37.529  lemmas arith_special = (* already declared simp above *)
  37.530    add_numeral_special add_neg_numeral_special
  37.531 -  diff_numeral_special minus_one
  37.532 +  diff_numeral_special
  37.533  
  37.534  (* rules already in simpset *)
  37.535  lemmas arith_extra_simps =
  37.536    numeral_plus_numeral add_neg_numeral_simps add_0_left add_0_right
  37.537 -  minus_numeral minus_neg_numeral minus_zero minus_one
  37.538 +  minus_zero
  37.539    diff_numeral_simps diff_0 diff_0_right
  37.540    numeral_times_numeral mult_neg_numeral_simps
  37.541    mult_zero_left mult_zero_right
  37.542 @@ -1089,15 +1184,15 @@
  37.543  
  37.544  lemmas rel_simps =
  37.545    le_num_simps less_num_simps eq_num_simps
  37.546 -  le_numeral_simps le_neg_numeral_simps le_numeral_extra
  37.547 -  less_numeral_simps less_neg_numeral_simps less_numeral_extra
  37.548 +  le_numeral_simps le_neg_numeral_simps le_minus_one_simps le_numeral_extra
  37.549 +  less_numeral_simps less_neg_numeral_simps less_minus_one_simps less_numeral_extra
  37.550    eq_numeral_simps eq_neg_numeral_simps eq_numeral_extra
  37.551  
  37.552  lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
  37.553    -- {* Unfold all @{text let}s involving constants *}
  37.554    unfolding Let_def ..
  37.555  
  37.556 -lemma Let_neg_numeral [simp]: "Let (neg_numeral v) f = f (neg_numeral v)"
  37.557 +lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
  37.558    -- {* Unfold all @{text let}s involving constants *}
  37.559    unfolding Let_def ..
  37.560  
  37.561 @@ -1133,16 +1228,16 @@
  37.562    by (simp_all add: add_assoc [symmetric])
  37.563  
  37.564  lemma add_neg_numeral_left [simp]:
  37.565 -  "numeral v + (neg_numeral w + y) = (sub v w + y)"
  37.566 -  "neg_numeral v + (numeral w + y) = (sub w v + y)"
  37.567 -  "neg_numeral v + (neg_numeral w + y) = (neg_numeral(v + w) + y)"
  37.568 +  "numeral v + (- numeral w + y) = (sub v w + y)"
  37.569 +  "- numeral v + (numeral w + y) = (sub w v + y)"
  37.570 +  "- numeral v + (- numeral w + y) = (- numeral(v + w) + y)"
  37.571    by (simp_all add: add_assoc [symmetric])
  37.572  
  37.573  lemma mult_numeral_left [simp]:
  37.574    "numeral v * (numeral w * z) = (numeral(v * w) * z :: 'a::semiring_numeral)"
  37.575 -  "neg_numeral v * (numeral w * y) = (neg_numeral(v * w) * y :: 'b::ring_1)"
  37.576 -  "numeral v * (neg_numeral w * y) = (neg_numeral(v * w) * y :: 'b::ring_1)"
  37.577 -  "neg_numeral v * (neg_numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)"
  37.578 +  "- numeral v * (numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
  37.579 +  "numeral v * (- numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
  37.580 +  "- numeral v * (- numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)"
  37.581    by (simp_all add: mult_assoc [symmetric])
  37.582  
  37.583  hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_dec
    38.1 --- a/src/HOL/Number_Theory/Cong.thy	Tue Nov 19 01:30:14 2013 +0100
    38.2 +++ b/src/HOL/Number_Theory/Cong.thy	Tue Nov 19 10:05:53 2013 +0100
    38.3 @@ -323,8 +323,6 @@
    38.4      \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
    38.5    apply (simp only: cong_altdef_int)
    38.6    apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
    38.7 -  (* any way around this? *)
    38.8 -  apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
    38.9    apply (auto simp add: field_simps)
   38.10    done
   38.11  
   38.12 @@ -665,7 +663,6 @@
   38.13    apply auto
   38.14    apply (cases "n \<ge> 0")
   38.15    apply auto
   38.16 -  apply (subst cong_int_def, auto)
   38.17    apply (frule cong_solve_int [of a n])
   38.18    apply auto
   38.19    done
    39.1 --- a/src/HOL/Number_Theory/Residues.thy	Tue Nov 19 01:30:14 2013 +0100
    39.2 +++ b/src/HOL/Number_Theory/Residues.thy	Tue Nov 19 10:05:53 2013 +0100
    39.3 @@ -455,6 +455,7 @@
    39.4    apply (subst fact_altdef_int, simp)
    39.5    apply (subst cong_int_def)
    39.6    apply simp
    39.7 +  apply arith
    39.8    apply (rule residues_prime.wilson_theorem1)
    39.9    apply (rule residues_prime.intro)
   39.10    apply auto
    40.1 --- a/src/HOL/Numeral_Simprocs.thy	Tue Nov 19 01:30:14 2013 +0100
    40.2 +++ b/src/HOL/Numeral_Simprocs.thy	Tue Nov 19 10:05:53 2013 +0100
    40.3 @@ -17,7 +17,7 @@
    40.4    if_False if_True
    40.5    add_0 add_Suc add_numeral_left
    40.6    add_neg_numeral_left mult_numeral_left
    40.7 -  numeral_1_eq_1 [symmetric] Suc_eq_plus1
    40.8 +  numeral_One [symmetric] uminus_numeral_One [symmetric] Suc_eq_plus1
    40.9    eq_numeral_iff_iszero not_iszero_Numeral1
   40.10  
   40.11  declare split_div [of _ _ "numeral k", arith_split] for k
   40.12 @@ -85,18 +85,19 @@
   40.13  
   40.14  text {* For @{text cancel_factor} *}
   40.15  
   40.16 -lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
   40.17 -by auto
   40.18 +lemmas nat_mult_le_cancel_disj = mult_le_cancel1
   40.19  
   40.20 -lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
   40.21 -by auto
   40.22 +lemmas nat_mult_less_cancel_disj = mult_less_cancel1
   40.23  
   40.24 -lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
   40.25 -by auto
   40.26 +lemma nat_mult_eq_cancel_disj:
   40.27 +  fixes k m n :: nat
   40.28 +  shows "k * m = k * n \<longleftrightarrow> k = 0 \<or> m = n"
   40.29 +  by auto
   40.30  
   40.31 -lemma nat_mult_div_cancel_disj[simp]:
   40.32 -     "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
   40.33 -by (simp add: nat_mult_div_cancel1)
   40.34 +lemma nat_mult_div_cancel_disj [simp]:
   40.35 +  fixes k m n :: nat
   40.36 +  shows "(k * m) div (k * n) = (if k = 0 then 0 else m div n)"
   40.37 +  by (fact div_mult_mult1_if)
   40.38  
   40.39  ML_file "Tools/numeral_simprocs.ML"
   40.40  
    41.1 --- a/src/HOL/Parity.thy	Tue Nov 19 01:30:14 2013 +0100
    41.2 +++ b/src/HOL/Parity.thy	Tue Nov 19 10:05:53 2013 +0100
    41.3 @@ -78,7 +78,7 @@
    41.4    unfolding even_def by simp
    41.5  
    41.6  (* TODO: proper simp rules for Num.Bit0, Num.Bit1 *)
    41.7 -declare even_def [of "neg_numeral v", simp] for v
    41.8 +declare even_def [of "- numeral v", simp] for v
    41.9  
   41.10  lemma even_numeral_nat [simp]: "even (numeral (Num.Bit0 k) :: nat)"
   41.11    unfolding even_nat_def by simp
   41.12 @@ -190,14 +190,9 @@
   41.13    by (induct n) simp_all
   41.14  
   41.15  lemma (in comm_ring_1)
   41.16 -  shows minus_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1"
   41.17 -  and minus_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1"
   41.18 -  by (simp_all add: neg_power_if del: minus_one)
   41.19 -
   41.20 -lemma (in comm_ring_1)
   41.21 -  shows neg_one_even_power [simp]: "even n \<Longrightarrow> (-1) ^ n = 1"
   41.22 -  and neg_one_odd_power [simp]: "odd n \<Longrightarrow> (-1) ^ n = - 1"
   41.23 -  by (simp_all add: minus_one [symmetric] del: minus_one)
   41.24 +  shows neg_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1"
   41.25 +  and neg_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1"
   41.26 +  by (simp_all add: neg_power_if)
   41.27  
   41.28  lemma zero_le_even_power: "even n ==>
   41.29      0 <= (x::'a::{linordered_ring,monoid_mult}) ^ n"
    42.1 --- a/src/HOL/Power.thy	Tue Nov 19 01:30:14 2013 +0100
    42.2 +++ b/src/HOL/Power.thy	Tue Nov 19 10:05:53 2013 +0100
    42.3 @@ -209,14 +209,6 @@
    42.4    "(- x) ^ numeral (Num.Bit1 k) = - (x ^ numeral (Num.Bit1 k))"
    42.5    by (simp only: eval_nat_numeral(3) power_Suc power_minus_Bit0 mult_minus_left)
    42.6  
    42.7 -lemma power_neg_numeral_Bit0 [simp]:
    42.8 -  "neg_numeral k ^ numeral (Num.Bit0 l) = numeral (Num.pow k (Num.Bit0 l))"
    42.9 -  by (simp only: neg_numeral_def power_minus_Bit0 power_numeral)
   42.10 -
   42.11 -lemma power_neg_numeral_Bit1 [simp]:
   42.12 -  "neg_numeral k ^ numeral (Num.Bit1 l) = neg_numeral (Num.pow k (Num.Bit1 l))"
   42.13 -  by (simp only: neg_numeral_def power_minus_Bit1 power_numeral pow.simps)
   42.14 -
   42.15  lemma power2_minus [simp]:
   42.16    "(- a)\<^sup>2 = a\<^sup>2"
   42.17    by (rule power_minus_Bit0)
    43.1 --- a/src/HOL/Rat.thy	Tue Nov 19 01:30:14 2013 +0100
    43.2 +++ b/src/HOL/Rat.thy	Tue Nov 19 10:05:53 2013 +0100
    43.3 @@ -215,17 +215,19 @@
    43.4    "Fract 0 k = 0"
    43.5    "Fract 1 1 = 1"
    43.6    "Fract (numeral w) 1 = numeral w"
    43.7 -  "Fract (neg_numeral w) 1 = neg_numeral w"
    43.8 +  "Fract (- numeral w) 1 = - numeral w"
    43.9 +  "Fract (- 1) 1 = - 1"
   43.10    "Fract k 0 = 0"
   43.11    using Fract_of_int_eq [of "numeral w"]
   43.12 -  using Fract_of_int_eq [of "neg_numeral w"]
   43.13 +  using Fract_of_int_eq [of "- numeral w"]
   43.14    by (simp_all add: Zero_rat_def One_rat_def eq_rat)
   43.15  
   43.16  lemma rat_number_expand:
   43.17    "0 = Fract 0 1"
   43.18    "1 = Fract 1 1"
   43.19    "numeral k = Fract (numeral k) 1"
   43.20 -  "neg_numeral k = Fract (neg_numeral k) 1"
   43.21 +  "- 1 = Fract (- 1) 1"
   43.22 +  "- numeral k = Fract (- numeral k) 1"
   43.23    by (simp_all add: rat_number_collapse)
   43.24  
   43.25  lemma Rat_cases_nonzero [case_names Fract 0]:
   43.26 @@ -356,7 +358,8 @@
   43.27    "quotient_of 0 = (0, 1)"
   43.28    "quotient_of 1 = (1, 1)"
   43.29    "quotient_of (numeral k) = (numeral k, 1)"
   43.30 -  "quotient_of (neg_numeral k) = (neg_numeral k, 1)"
   43.31 +  "quotient_of (- 1) = (- 1, 1)"
   43.32 +  "quotient_of (- numeral k) = (- numeral k, 1)"
   43.33    by (simp_all add: rat_number_expand quotient_of_Fract)
   43.34  
   43.35  lemma quotient_of_eq: "quotient_of (Fract a b) = (p, q) \<Longrightarrow> Fract p q = Fract a b"
   43.36 @@ -620,7 +623,7 @@
   43.37    #> Lin_Arith.add_simps [@{thm neg_less_iff_less},
   43.38        @{thm True_implies_equals},
   43.39        read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm distrib_left},
   43.40 -      read_instantiate @{context} [(("a", 0), "(neg_numeral ?v)")] @{thm distrib_left},
   43.41 +      read_instantiate @{context} [(("a", 0), "(- numeral ?v)")] @{thm distrib_left},
   43.42        @{thm divide_1}, @{thm divide_zero_left},
   43.43        @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
   43.44        @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
   43.45 @@ -664,6 +667,10 @@
   43.46  lemma of_rat_minus: "of_rat (- a) = - of_rat a"
   43.47    by transfer simp
   43.48  
   43.49 +lemma of_rat_neg_one [simp]:
   43.50 +  "of_rat (- 1) = - 1"
   43.51 +  by (simp add: of_rat_minus)
   43.52 +
   43.53  lemma of_rat_diff: "of_rat (a - b) = of_rat a - of_rat b"
   43.54    using of_rat_add [of a "- b"] by (simp add: of_rat_minus)
   43.55  
   43.56 @@ -778,8 +785,8 @@
   43.57  using of_rat_of_int_eq [of "numeral w"] by simp
   43.58  
   43.59  lemma of_rat_neg_numeral_eq [simp]:
   43.60 -  "of_rat (neg_numeral w) = neg_numeral w"
   43.61 -using of_rat_of_int_eq [of "neg_numeral w"] by simp
   43.62 +  "of_rat (- numeral w) = - numeral w"
   43.63 +using of_rat_of_int_eq [of "- numeral w"] by simp
   43.64  
   43.65  lemmas zero_rat = Zero_rat_def
   43.66  lemmas one_rat = One_rat_def
   43.67 @@ -820,9 +827,6 @@
   43.68  lemma Rats_number_of [simp]: "numeral w \<in> Rats"
   43.69  by (subst of_rat_numeral_eq [symmetric], rule Rats_of_rat)
   43.70  
   43.71 -lemma Rats_neg_number_of [simp]: "neg_numeral w \<in> Rats"
   43.72 -by (subst of_rat_neg_numeral_eq [symmetric], rule Rats_of_rat)
   43.73 -
   43.74  lemma Rats_0 [simp]: "0 \<in> Rats"
   43.75  apply (unfold Rats_def)
   43.76  apply (rule range_eqI)
   43.77 @@ -943,7 +947,7 @@
   43.78    by (simp add: Rat.of_int_def)
   43.79  
   43.80  lemma [code_unfold]:
   43.81 -  "neg_numeral k = Rat.of_int (neg_numeral k)"
   43.82 +  "- numeral k = Rat.of_int (- numeral k)"
   43.83    by (simp add: Rat.of_int_def)
   43.84  
   43.85  lemma Frct_code_post [code_post]:
   43.86 @@ -951,13 +955,13 @@
   43.87    "Frct (a, 0) = 0"
   43.88    "Frct (1, 1) = 1"
   43.89    "Frct (numeral k, 1) = numeral k"
   43.90 -  "Frct (neg_numeral k, 1) = neg_numeral k"
   43.91 +  "Frct (- numeral k, 1) = - numeral k"
   43.92    "Frct (1, numeral k) = 1 / numeral k"
   43.93 -  "Frct (1, neg_numeral k) = 1 / neg_numeral k"
   43.94 +  "Frct (1, - numeral k) = 1 / - numeral k"
   43.95    "Frct (numeral k, numeral l) = numeral k / numeral l"
   43.96 -  "Frct (numeral k, neg_numeral l) = numeral k / neg_numeral l"
   43.97 -  "Frct (neg_numeral k, numeral l) = neg_numeral k / numeral l"
   43.98 -  "Frct (neg_numeral k, neg_numeral l) = neg_numeral k / neg_numeral l"
   43.99 +  "Frct (numeral k, - numeral l) = numeral k / - numeral l"
  43.100 +  "Frct (- numeral k, numeral l) = - numeral k / numeral l"
  43.101 +  "Frct (- numeral k, - numeral l) = - numeral k / - numeral l"
  43.102    by (simp_all add: Fract_of_int_quotient)
  43.103  
  43.104  
  43.105 @@ -1156,7 +1160,7 @@
  43.106        in
  43.107          if i = 0 then Syntax.const @{const_syntax Groups.zero}
  43.108          else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i
  43.109 -        else Syntax.const @{const_syntax Num.neg_numeral} $ mk (~i)
  43.110 +        else Syntax.const @{const_syntax Groups.uminus} $ (Syntax.const @{const_syntax Num.numeral} $ mk (~i))
  43.111        end;
  43.112  
  43.113      fun mk_frac str =
    44.1 --- a/src/HOL/Real.thy	Tue Nov 19 01:30:14 2013 +0100
    44.2 +++ b/src/HOL/Real.thy	Tue Nov 19 10:05:53 2013 +0100
    44.3 @@ -1447,13 +1447,13 @@
    44.4  
    44.5  lemma [code_abbrev]:
    44.6    "real_of_int (numeral k) = numeral k"
    44.7 -  "real_of_int (neg_numeral k) = neg_numeral k"
    44.8 +  "real_of_int (- numeral k) = - numeral k"
    44.9    by simp_all
   44.10  
   44.11 -text{*Collapse applications of @{term real} to @{term number_of}*}
   44.12 +text{*Collapse applications of @{const real} to @{const numeral}*}
   44.13  lemma real_numeral [simp]:
   44.14    "real (numeral v :: int) = numeral v"
   44.15 -  "real (neg_numeral v :: int) = neg_numeral v"
   44.16 +  "real (- numeral v :: int) = - numeral v"
   44.17  by (simp_all add: real_of_int_def)
   44.18  
   44.19  lemma real_of_nat_numeral [simp]:
   44.20 @@ -1559,11 +1559,11 @@
   44.21    unfolding real_of_int_le_iff[symmetric] by simp
   44.22  
   44.23  lemma neg_numeral_power_le_real_of_int_cancel_iff[simp]:
   44.24 -  "(neg_numeral x::real) ^ n \<le> real a \<longleftrightarrow> (neg_numeral x::int) ^ n \<le> a"
   44.25 +  "(- numeral x::real) ^ n \<le> real a \<longleftrightarrow> (- numeral x::int) ^ n \<le> a"
   44.26    unfolding real_of_int_le_iff[symmetric] by simp
   44.27  
   44.28  lemma real_of_int_le_neg_numeral_power_cancel_iff[simp]:
   44.29 -  "real a \<le> (neg_numeral x::real) ^ n \<longleftrightarrow> a \<le> (neg_numeral x::int) ^ n"
   44.30 +  "real a \<le> (- numeral x::real) ^ n \<longleftrightarrow> a \<le> (- numeral x::int) ^ n"
   44.31    unfolding real_of_int_le_iff[symmetric] by simp
   44.32  
   44.33  subsection{*Density of the Reals*}
   44.34 @@ -2051,7 +2051,7 @@
   44.35    by simp
   44.36  
   44.37  lemma [code_abbrev]:
   44.38 -  "(of_rat (neg_numeral k) :: real) = neg_numeral k"
   44.39 +  "(of_rat (- numeral k) :: real) = - numeral k"
   44.40    by simp
   44.41  
   44.42  lemma [code_post]:
   44.43 @@ -2059,14 +2059,14 @@
   44.44    "(of_rat (r / 0)  :: real) = 0"
   44.45    "(of_rat (1 / 1)  :: real) = 1"
   44.46    "(of_rat (numeral k / 1) :: real) = numeral k"
   44.47 -  "(of_rat (neg_numeral k / 1) :: real) = neg_numeral k"
   44.48 +  "(of_rat (- numeral k / 1) :: real) = - numeral k"
   44.49    "(of_rat (1 / numeral k) :: real) = 1 / numeral k"
   44.50 -  "(of_rat (1 / neg_numeral k) :: real) = 1 / neg_numeral k"
   44.51 +  "(of_rat (1 / - numeral k) :: real) = 1 / - numeral k"
   44.52    "(of_rat (numeral k / numeral l)  :: real) = numeral k / numeral l"
   44.53 -  "(of_rat (numeral k / neg_numeral l)  :: real) = numeral k / neg_numeral l"
   44.54 -  "(of_rat (neg_numeral k / numeral l)  :: real) = neg_numeral k / numeral l"
   44.55 -  "(of_rat (neg_numeral k / neg_numeral l)  :: real) = neg_numeral k / neg_numeral l"
   44.56 -  by (simp_all add: of_rat_divide)
   44.57 +  "(of_rat (numeral k / - numeral l)  :: real) = numeral k / - numeral l"
   44.58 +  "(of_rat (- numeral k / numeral l)  :: real) = - numeral k / numeral l"
   44.59 +  "(of_rat (- numeral k / - numeral l)  :: real) = - numeral k / - numeral l"
   44.60 +  by (simp_all add: of_rat_divide of_rat_minus)
   44.61  
   44.62  
   44.63  text {* Operations *}
    45.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Nov 19 01:30:14 2013 +0100
    45.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Nov 19 10:05:53 2013 +0100
    45.3 @@ -307,8 +307,8 @@
    45.4  lemma of_real_numeral: "of_real (numeral w) = numeral w"
    45.5  using of_real_of_int_eq [of "numeral w"] by simp
    45.6  
    45.7 -lemma of_real_neg_numeral: "of_real (neg_numeral w) = neg_numeral w"
    45.8 -using of_real_of_int_eq [of "neg_numeral w"] by simp
    45.9 +lemma of_real_neg_numeral: "of_real (- numeral w) = - numeral w"
   45.10 +using of_real_of_int_eq [of "- numeral w"] by simp
   45.11  
   45.12  text{*Every real algebra has characteristic zero*}
   45.13  
   45.14 @@ -341,9 +341,6 @@
   45.15  lemma Reals_numeral [simp]: "numeral w \<in> Reals"
   45.16  by (subst of_real_numeral [symmetric], rule Reals_of_real)
   45.17  
   45.18 -lemma Reals_neg_numeral [simp]: "neg_numeral w \<in> Reals"
   45.19 -by (subst of_real_neg_numeral [symmetric], rule Reals_of_real)
   45.20 -
   45.21  lemma Reals_0 [simp]: "0 \<in> Reals"
   45.22  apply (unfold Reals_def)
   45.23  apply (rule range_eqI)
   45.24 @@ -602,7 +599,7 @@
   45.25  by (subst of_real_numeral [symmetric], subst norm_of_real, simp)
   45.26  
   45.27  lemma norm_neg_numeral [simp]:
   45.28 -  "norm (neg_numeral w::'a::real_normed_algebra_1) = numeral w"
   45.29 +  "norm (- numeral w::'a::real_normed_algebra_1) = numeral w"
   45.30  by (subst of_real_neg_numeral [symmetric], subst norm_of_real, simp)
   45.31  
   45.32  lemma norm_of_int [simp]:
    46.1 --- a/src/HOL/Rings.thy	Tue Nov 19 01:30:14 2013 +0100
    46.2 +++ b/src/HOL/Rings.thy	Tue Nov 19 10:05:53 2013 +0100
    46.3 @@ -1058,6 +1058,34 @@
    46.4    "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
    46.5  by(subst abs_dvd_iff[symmetric]) simp
    46.6  
    46.7 +text {* The following lemmas can be proven in more generale structures, but
    46.8 +are dangerous as simp rules in absence of @{thm neg_equal_zero}, 
    46.9 +@{thm neg_less_pos}, @{thm neg_less_eq_nonneg}. *}
   46.10 +
   46.11 +lemma equation_minus_iff_1 [simp, no_atp]:
   46.12 +  "1 = - a \<longleftrightarrow> a = - 1"
   46.13 +  by (fact equation_minus_iff)
   46.14 +
   46.15 +lemma minus_equation_iff_1 [simp, no_atp]:
   46.16 +  "- a = 1 \<longleftrightarrow> a = - 1"
   46.17 +  by (subst minus_equation_iff, auto)
   46.18 +
   46.19 +lemma le_minus_iff_1 [simp, no_atp]:
   46.20 +  "1 \<le> - b \<longleftrightarrow> b \<le> - 1"
   46.21 +  by (fact le_minus_iff)
   46.22 +
   46.23 +lemma minus_le_iff_1 [simp, no_atp]:
   46.24 +  "- a \<le> 1 \<longleftrightarrow> - 1 \<le> a"
   46.25 +  by (fact minus_le_iff)
   46.26 +
   46.27 +lemma less_minus_iff_1 [simp, no_atp]:
   46.28 +  "1 < - b \<longleftrightarrow> b < - 1"
   46.29 +  by (fact less_minus_iff)
   46.30 +
   46.31 +lemma minus_less_iff_1 [simp, no_atp]:
   46.32 +  "- a < 1 \<longleftrightarrow> - 1 < a"
   46.33 +  by (fact minus_less_iff)
   46.34 +
   46.35  end
   46.36  
   46.37  text {* Simprules for comparisons where common factors can be cancelled. *}
    47.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Nov 19 01:30:14 2013 +0100
    47.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Nov 19 10:05:53 2013 +0100
    47.3 @@ -374,7 +374,6 @@
    47.4  
    47.5  lemma
    47.6    "(0::int) = 0"
    47.7 -  "(0::int) = -0"
    47.8    "(0::int) = (- 0)"
    47.9    "(1::int) = 1"
   47.10    "\<not>(-1 = (1::int))"
    48.1 --- a/src/HOL/SMT_Examples/SMT_Word_Examples.certs	Tue Nov 19 01:30:14 2013 +0100
    48.2 +++ b/src/HOL/SMT_Examples/SMT_Word_Examples.certs	Tue Nov 19 10:05:53 2013 +0100
    48.3 @@ -54,3 +54,5 @@
    48.4  unsat
    48.5  e5c27ae0a583eeafeaa4ef3c59b1b4ec53e06b0f 1 0
    48.6  unsat
    48.7 +7d3ef49480d3ed3a7e5f2d7a12e7108cf7fc7819 1 0
    48.8 +unsat
    49.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 19 01:30:14 2013 +0100
    49.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 19 10:05:53 2013 +0100
    49.3 @@ -1645,10 +1645,10 @@
    49.4          (hol_ctxt as {thy, ctxt, stds, whacks, total_consts, case_names,
    49.5                        def_tables, ground_thm_table, ersatz_table, ...}) =
    49.6    let
    49.7 -    fun do_numeral depth Ts mult T t0 t1 =
    49.8 +    fun do_numeral depth Ts mult T some_t0 t1 t2 =
    49.9        (if is_number_type ctxt T then
   49.10           let
   49.11 -           val j = mult * HOLogic.dest_num t1
   49.12 +           val j = mult * HOLogic.dest_num t2
   49.13           in
   49.14             if j = 1 then
   49.15               raise SAME ()
   49.16 @@ -1667,15 +1667,16 @@
   49.17           handle TERM _ => raise SAME ()
   49.18         else
   49.19           raise SAME ())
   49.20 -      handle SAME () => s_betapply [] (do_term depth Ts t0, do_term depth Ts t1)
   49.21 +      handle SAME () => (case some_t0 of NONE => s_betapply [] (do_term depth Ts t1, do_term depth Ts t2)
   49.22 +         | SOME t0 => s_betapply [] (do_term depth Ts t0, s_betapply [] (do_term depth Ts t1, do_term depth Ts t2)))
   49.23      and do_term depth Ts t =
   49.24        case t of
   49.25 -        (t0 as Const (@{const_name Num.neg_numeral_class.neg_numeral},
   49.26 -                      Type (@{type_name fun}, [_, ran_T]))) $ t1 =>
   49.27 -        do_numeral depth Ts ~1 ran_T t0 t1
   49.28 -      | (t0 as Const (@{const_name Num.numeral_class.numeral},
   49.29 -                      Type (@{type_name fun}, [_, ran_T]))) $ t1 =>
   49.30 -        do_numeral depth Ts 1 ran_T t0 t1
   49.31 +        (t0 as Const (@{const_name uminus}, _) $ ((t1 as Const (@{const_name numeral},
   49.32 +                      Type (@{type_name fun}, [_, ran_T]))) $ t2)) =>
   49.33 +        do_numeral depth Ts ~1 ran_T (SOME t0) t1 t2
   49.34 +      | (t1 as Const (@{const_name numeral},
   49.35 +                      Type (@{type_name fun}, [_, ran_T]))) $ t2 =>
   49.36 +        do_numeral depth Ts 1 ran_T NONE t1 t2
   49.37        | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
   49.38          do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
   49.39        | (t0 as Const (@{const_name Sigma}, Type (_, [T1, Type (_, [T2, T3])])))
    50.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Tue Nov 19 01:30:14 2013 +0100
    50.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Nov 19 10:05:53 2013 +0100
    50.3 @@ -42,7 +42,6 @@
    50.4     @{term "nat"}, @{term "int"},
    50.5     @{term "Num.One"}, @{term "Num.Bit0"}, @{term "Num.Bit1"},
    50.6     @{term "Num.numeral :: num => int"}, @{term "Num.numeral :: num => nat"},
    50.7 -   @{term "Num.neg_numeral :: num => int"},
    50.8     @{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"},
    50.9     @{term "True"}, @{term "False"}];
   50.10  
   50.11 @@ -610,8 +609,6 @@
   50.12    | num_of_term vs @{term "1::int"} = Proc.C (Proc.Int_of_integer 1)
   50.13    | num_of_term vs (t as Const (@{const_name numeral}, _) $ _) =
   50.14        Proc.C (Proc.Int_of_integer (dest_number t))
   50.15 -  | num_of_term vs (t as Const (@{const_name neg_numeral}, _) $ _) =
   50.16 -      Proc.Neg (Proc.C (Proc.Int_of_integer (dest_number t)))
   50.17    | num_of_term vs (Const (@{const_name Groups.uminus}, _) $ t') =
   50.18        Proc.Neg (num_of_term vs t')
   50.19    | num_of_term vs (Const (@{const_name Groups.plus}, _) $ t1 $ t2) =
    51.1 --- a/src/HOL/Tools/SMT/smt_builtin.ML	Tue Nov 19 01:30:14 2013 +0100
    51.2 +++ b/src/HOL/Tools/SMT/smt_builtin.ML	Tue Nov 19 10:05:53 2013 +0100
    51.3 @@ -144,9 +144,10 @@
    51.4    (case try HOLogic.dest_number t of
    51.5      NONE => NONE
    51.6    | SOME (T, i) =>
    51.7 -      (case lookup_builtin_typ ctxt T of
    51.8 -        SOME (_, Int (_, g)) => g T i |> Option.map (rpair T)
    51.9 -      | _ => NONE))
   51.10 +      if i < 0 then NONE else
   51.11 +        (case lookup_builtin_typ ctxt T of
   51.12 +          SOME (_, Int (_, g)) => g T i |> Option.map (rpair T)
   51.13 +        | _ => NONE))
   51.14  
   51.15  val is_builtin_num = is_some oo dest_builtin_num
   51.16  
    52.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Nov 19 01:30:14 2013 +0100
    52.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Nov 19 10:05:53 2013 +0100
    52.3 @@ -526,23 +526,26 @@
    52.4  
    52.5  local
    52.6    (*
    52.7 -    rewrite negative numerals into positive numerals,
    52.8 -    rewrite Numeral0 into 0
    52.9      rewrite Numeral1 into 1
   52.10 +    rewrite - 0 into 0
   52.11    *)
   52.12  
   52.13 -  fun is_strange_number ctxt (t as Const (@{const_name neg_numeral}, _) $ _) =
   52.14 -        SMT_Builtin.is_builtin_num ctxt t
   52.15 -    | is_strange_number _ _ = false
   52.16 +  fun is_irregular_number (Const (@{const_name numeral}, _) $ Const (@{const_name num.One}, _)) =
   52.17 +        true
   52.18 +    | is_irregular_number (Const (@{const_name uminus}, _) $ Const (@{const_name Groups.zero}, _)) =
   52.19 +        true
   52.20 +    | is_irregular_number _ =
   52.21 +        false;
   52.22  
   52.23 -  val pos_num_ss =
   52.24 +  fun is_strange_number ctxt t = is_irregular_number t andalso SMT_Builtin.is_builtin_num ctxt t;
   52.25 +
   52.26 +  val proper_num_ss =
   52.27      simpset_of (put_simpset HOL_ss @{context}
   52.28 -      addsimps [@{thm Num.numeral_One}]
   52.29 -      addsimps [@{thm Num.neg_numeral_def}])
   52.30 +      addsimps @{thms Num.numeral_One minus_zero})
   52.31  
   52.32    fun norm_num_conv ctxt =
   52.33      SMT_Utils.if_conv (is_strange_number ctxt)
   52.34 -      (Simplifier.rewrite (put_simpset pos_num_ss ctxt)) Conv.no_conv
   52.35 +      (Simplifier.rewrite (put_simpset proper_num_ss ctxt)) Conv.no_conv
   52.36  in
   52.37  
   52.38  fun normalize_numerals_conv ctxt =
    53.1 --- a/src/HOL/Tools/SMT/smt_utils.ML	Tue Nov 19 01:30:14 2013 +0100
    53.2 +++ b/src/HOL/Tools/SMT/smt_utils.ML	Tue Nov 19 10:05:53 2013 +0100
    53.3 @@ -140,7 +140,6 @@
    53.4            is_num env t andalso is_num env u
    53.5        | is_num env (Const (@{const_name Let}, _) $ t $ Abs (_, _, u)) =
    53.6            is_num (t :: env) u
    53.7 -      | is_num env (Const (@{const_name uminus}, _) $ t) = is_num env t
    53.8        | is_num env (Bound i) = i < length env andalso is_num env (nth env i)
    53.9        | is_num _ t = can HOLogic.dest_number t
   53.10    in is_num [] end
    54.1 --- a/src/HOL/Tools/hologic.ML	Tue Nov 19 01:30:14 2013 +0100
    54.2 +++ b/src/HOL/Tools/hologic.ML	Tue Nov 19 10:05:53 2013 +0100
    54.3 @@ -104,7 +104,6 @@
    54.4    val mk_numeral: int -> term
    54.5    val dest_num: term -> int
    54.6    val numeral_const: typ -> term
    54.7 -  val neg_numeral_const: typ -> term
    54.8    val add_numerals: term -> (term * typ) list -> (term * typ) list
    54.9    val mk_number: typ -> int -> term
   54.10    val dest_number: term -> typ * int
   54.11 @@ -548,7 +547,6 @@
   54.12    | dest_num t = raise TERM ("dest_num", [t]);
   54.13  
   54.14  fun numeral_const T = Const ("Num.numeral_class.numeral", numT --> T);
   54.15 -fun neg_numeral_const T = Const ("Num.neg_numeral_class.neg_numeral", numT --> T);
   54.16  
   54.17  fun add_numerals (Const ("Num.numeral_class.numeral", Type (_, [_, T])) $ t) = cons (t, T)
   54.18    | add_numerals (t $ u) = add_numerals t #> add_numerals u
   54.19 @@ -559,14 +557,14 @@
   54.20    | mk_number T 1 = Const ("Groups.one_class.one", T)
   54.21    | mk_number T i =
   54.22      if i > 0 then numeral_const T $ mk_numeral i
   54.23 -    else neg_numeral_const T $ mk_numeral (~ i);
   54.24 +    else Const ("Groups.uminus_class.uminus", T --> T) $ mk_number T (~ i);
   54.25  
   54.26  fun dest_number (Const ("Groups.zero_class.zero", T)) = (T, 0)
   54.27    | dest_number (Const ("Groups.one_class.one", T)) = (T, 1)
   54.28    | dest_number (Const ("Num.numeral_class.numeral", Type ("fun", [_, T])) $ t) =
   54.29        (T, dest_num t)
   54.30 -  | dest_number (Const ("Num.neg_numeral_class.neg_numeral", Type ("fun", [_, T])) $ t) =
   54.31 -      (T, ~ (dest_num t))
   54.32 +  | dest_number (Const ("Groups.uminus_class.uminus", Type ("fun", [_, T])) $ t) =
   54.33 +      apsnd (op ~) (dest_number t)
   54.34    | dest_number t = raise TERM ("dest_number", [t]);
   54.35  
   54.36  
    55.1 --- a/src/HOL/Tools/lin_arith.ML	Tue Nov 19 01:30:14 2013 +0100
    55.2 +++ b/src/HOL/Tools/lin_arith.ML	Tue Nov 19 10:05:53 2013 +0100
    55.3 @@ -183,9 +183,6 @@
    55.4      | demult (t as Const ("Num.numeral_class.numeral", _) $ n, m) =
    55.5        ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_num n)))
    55.6          handle TERM _ => (SOME t, m))
    55.7 -    | demult (t as Const ("Num.neg_numeral_class.neg_numeral", _) $ n, m) =
    55.8 -      ((NONE, Rat.mult m (Rat.rat_of_int (~ (HOLogic.dest_num n))))
    55.9 -        handle TERM _ => (SOME t, m))
   55.10      | demult (t as Const (@{const_name Suc}, _) $ _, m) =
   55.11        ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_nat t)))
   55.12          handle TERM _ => (SOME t, m))
   55.13 @@ -212,6 +209,10 @@
   55.14          pi
   55.15      | poly (Const (@{const_name Groups.one}, _), m, (p, i)) =
   55.16          (p, Rat.add i m)
   55.17 +    | poly (all as Const ("Num.numeral_class.numeral", Type(_,[_,_])) $ t, m, pi as (p, i)) =
   55.18 +        (let val k = HOLogic.dest_num t
   55.19 +        in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k))) end
   55.20 +        handle TERM _ => add_atom all m pi)
   55.21      | poly (Const (@{const_name Suc}, _) $ t, m, (p, i)) =
   55.22          poly (t, m, (p, Rat.add i m))
   55.23      | poly (all as Const (@{const_name Groups.times}, _) $ _ $ _, m, pi as (p, i)) =
   55.24 @@ -222,14 +223,6 @@
   55.25          (case demult inj_consts (all, m) of
   55.26             (NONE,   m') => (p, Rat.add i m')
   55.27           | (SOME u, m') => add_atom u m' pi)
   55.28 -    | poly (all as Const ("Num.numeral_class.numeral", Type(_,[_,_])) $ t, m, pi as (p, i)) =
   55.29 -        (let val k = HOLogic.dest_num t
   55.30 -        in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k))) end
   55.31 -        handle TERM _ => add_atom all m pi)
   55.32 -    | poly (all as Const ("Num.neg_numeral_class.neg_numeral", Type(_,[_,_])) $ t, m, pi as (p, i)) =
   55.33 -        (let val k = HOLogic.dest_num t
   55.34 -        in (p, Rat.add i (Rat.mult m (Rat.rat_of_int (~ k)))) end
   55.35 -        handle TERM _ => add_atom all m pi)
   55.36      | poly (all as Const f $ x, m, pi) =
   55.37          if member (op =) inj_consts f then poly (x, m, pi) else add_atom all m pi
   55.38      | poly (all, m, pi) =
    56.1 --- a/src/HOL/Tools/numeral.ML	Tue Nov 19 01:30:14 2013 +0100
    56.2 +++ b/src/HOL/Tools/numeral.ML	Tue Nov 19 10:05:53 2013 +0100
    56.3 @@ -45,8 +45,8 @@
    56.4  val numeral = @{cpat "numeral"};
    56.5  val numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term numeral)));
    56.6  
    56.7 -val neg_numeral = @{cpat "neg_numeral"};
    56.8 -val neg_numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term neg_numeral)));
    56.9 +val uminus = @{cpat "uminus"};
   56.10 +val uminusT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term uminus)));
   56.11  
   56.12  fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
   56.13  
   56.14 @@ -56,7 +56,7 @@
   56.15    | mk_cnumber T 1 = instT T oneT one
   56.16    | mk_cnumber T i =
   56.17      if i > 0 then Thm.apply (instT T numeralT numeral) (mk_cnumeral i)
   56.18 -    else Thm.apply (instT T neg_numeralT neg_numeral) (mk_cnumeral (~i));
   56.19 +    else Thm.apply (instT T uminusT uminus) (Thm.apply (instT T numeralT numeral) (mk_cnumeral (~i)));
   56.20  
   56.21  end;
   56.22  
    57.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Tue Nov 19 01:30:14 2013 +0100
    57.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Tue Nov 19 10:05:53 2013 +0100
    57.3 @@ -56,9 +56,6 @@
    57.4  val long_mk_sum = Arith_Data.long_mk_sum;
    57.5  val dest_sum = Arith_Data.dest_sum;
    57.6  
    57.7 -val mk_diff = HOLogic.mk_binop @{const_name Groups.minus};
    57.8 -val dest_diff = HOLogic.dest_bin @{const_name Groups.minus} dummyT;
    57.9 -
   57.10  val mk_times = HOLogic.mk_binop @{const_name Groups.times};
   57.11  
   57.12  fun one_of T = Const(@{const_name Groups.one}, T);
   57.13 @@ -181,7 +178,7 @@
   57.14  
   57.15  (*Simplify 0+n, n+0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
   57.16  val add_0s =  @{thms add_0s};
   57.17 -val mult_1s = @{thms mult_1s mult_1_left mult_1_right divide_1};
   57.18 +val mult_1s = @{thms mult_1s divide_numeral_1 mult_1_left mult_1_right mult_minus1 mult_minus1_right divide_1};
   57.19  
   57.20  (* For post-simplification of the rhs of simproc-generated rules *)
   57.21  val post_simps =
   57.22 @@ -194,9 +191,8 @@
   57.23  val field_post_simps =
   57.24      post_simps @ [@{thm divide_zero_left}, @{thm divide_1}]
   57.25                        
   57.26 -(*Simplify inverse Numeral1, a/Numeral1*)
   57.27 +(*Simplify inverse Numeral1*)
   57.28  val inverse_1s = [@{thm inverse_numeral_1}];
   57.29 -val divide_1s = [@{thm divide_numeral_1}];
   57.30  
   57.31  (*To perform binary arithmetic.  The "left" rewriting handles patterns
   57.32    created by the Numeral_Simprocs, such as 3 * (5 * x). *)
   57.33 @@ -217,7 +213,7 @@
   57.34       @{thms add_neg_numeral_simps}) simps;
   57.35  
   57.36  (*To evaluate binary negations of coefficients*)
   57.37 -val minus_simps = [@{thm minus_zero}, @{thm minus_one}, @{thm minus_numeral}, @{thm minus_neg_numeral}];
   57.38 +val minus_simps = [@{thm minus_zero}, @{thm minus_minus}];
   57.39  
   57.40  (*To let us treat subtraction as addition*)
   57.41  val diff_simps = [@{thm diff_conv_add_uminus}, @{thm minus_add_distrib}, @{thm minus_minus}];
   57.42 @@ -225,16 +221,13 @@
   57.43  (*To let us treat division as multiplication*)
   57.44  val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}];
   57.45  
   57.46 -(*push the unary minus down*)
   57.47 -val minus_mult_eq_1_to_2 = @{lemma "- (a::'a::ring) * b = a * - b" by simp};
   57.48 -
   57.49  (*to extract again any uncancelled minuses*)
   57.50  val minus_from_mult_simps =
   57.51      [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}];
   57.52  
   57.53  (*combine unary minus with numeric literals, however nested within a product*)
   57.54  val mult_minus_simps =
   57.55 -    [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2];
   57.56 +    [@{thm mult_assoc}, @{thm minus_mult_right}, @{thm minus_mult_commute}];
   57.57  
   57.58  val norm_ss1 =
   57.59    simpset_of (put_simpset num_ss @{context}
   57.60 @@ -247,7 +240,7 @@
   57.61  
   57.62  val norm_ss3 =
   57.63    simpset_of (put_simpset num_ss @{context}
   57.64 -    addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac})
   57.65 +    addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac minus_mult_commute})
   57.66  
   57.67  structure CancelNumeralsCommon =
   57.68  struct
   57.69 @@ -330,7 +323,7 @@
   57.70  structure FieldCombineNumeralsData =
   57.71  struct
   57.72    type coeff = int * int
   57.73 -  val iszero = (fn (p, q) => p = 0)
   57.74 +  val iszero = (fn (p, _) => p = 0)
   57.75    val add = add_frac
   57.76    val mk_sum = long_mk_sum
   57.77    val dest_sum = dest_sum
   57.78 @@ -368,7 +361,7 @@
   57.79  
   57.80  structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
   57.81  struct
   57.82 -  val assoc_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac})
   57.83 +  val assoc_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac minus_mult_commute})
   57.84    val eq_reflection = eq_reflection
   57.85    val is_numeral = can HOLogic.dest_number
   57.86  end;
   57.87 @@ -388,7 +381,7 @@
   57.88    val norm_ss2 =
   57.89      simpset_of (put_simpset HOL_basic_ss @{context} addsimps simps @ mult_minus_simps)
   57.90    val norm_ss3 =
   57.91 -    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac})
   57.92 +    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac minus_mult_commute})
   57.93    fun norm_tac ctxt =
   57.94      ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
   57.95      THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
   57.96 @@ -463,9 +456,9 @@
   57.97       ["((l::'a::field_inverse_zero) * m) / n",
   57.98        "(l::'a::field_inverse_zero) / (m * n)",
   57.99        "((numeral v)::'a::field_inverse_zero) / (numeral w)",
  57.100 -      "((numeral v)::'a::field_inverse_zero) / (neg_numeral w)",
  57.101 -      "((neg_numeral v)::'a::field_inverse_zero) / (numeral w)",
  57.102 -      "((neg_numeral v)::'a::field_inverse_zero) / (neg_numeral w)"],
  57.103 +      "((numeral v)::'a::field_inverse_zero) / (- numeral w)",
  57.104 +      "((- numeral v)::'a::field_inverse_zero) / (numeral w)",
  57.105 +      "((- numeral v)::'a::field_inverse_zero) / (- numeral w)"],
  57.106       DivideCancelNumeralFactor.proc)]
  57.107  
  57.108  
  57.109 @@ -516,7 +509,7 @@
  57.110    val find_first = find_first_t []
  57.111    val trans_tac = trans_tac
  57.112    val norm_ss =
  57.113 -    simpset_of (put_simpset HOL_basic_ss @{context} addsimps mult_1s @ @{thms mult_ac})
  57.114 +    simpset_of (put_simpset HOL_basic_ss @{context} addsimps mult_1s @ @{thms mult_ac minus_mult_commute})
  57.115    fun norm_tac ctxt =
  57.116      ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
  57.117    val simplify_meta_eq  = cancel_simplify_meta_eq 
    58.1 --- a/src/HOL/Transcendental.thy	Tue Nov 19 01:30:14 2013 +0100
    58.2 +++ b/src/HOL/Transcendental.thy	Tue Nov 19 10:05:53 2013 +0100
    58.3 @@ -2000,8 +2000,8 @@
    58.4    apply (subst powr_add, simp, simp)
    58.5    done
    58.6  
    58.7 -lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x^(numeral n)"
    58.8 -  unfolding real_of_nat_numeral[symmetric] by (rule powr_realpow)
    58.9 +lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
   58.10 +  unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow)
   58.11  
   58.12  lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))"
   58.13    apply (case_tac "x = 0", simp, simp)
   58.14 @@ -2020,11 +2020,17 @@
   58.15    then show ?thesis by (simp add: assms powr_realpow[symmetric])
   58.16  qed
   58.17  
   58.18 -lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x^numeral n"
   58.19 -  using powr_realpow[of x "numeral n"] by simp
   58.20 -
   58.21 -lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr neg_numeral n = 1 / x^numeral n"
   58.22 -  using powr_int[of x "neg_numeral n"] by simp
   58.23 +lemma powr_one: "0 < x \<Longrightarrow> x powr 1 = x"
   58.24 +  using powr_realpow [of x 1] by simp
   58.25 +
   58.26 +lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x ^ numeral n"
   58.27 +  by (fact powr_realpow_numeral)
   58.28 +
   58.29 +lemma powr_neg_one: "0 < x \<Longrightarrow> x powr - 1 = 1 / x"
   58.30 +  using powr_int [of x "- 1"] by simp
   58.31 +
   58.32 +lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr - numeral n = 1 / x ^ numeral n"
   58.33 +  using powr_int [of x "- numeral n"] by simp
   58.34  
   58.35  lemma root_powr_inverse: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
   58.36    by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
   58.37 @@ -4047,7 +4053,7 @@
   58.38    show "sgn x * pi / 2 - arctan x < pi / 2"
   58.39      using arctan_bounded [of "- x"] assms
   58.40      unfolding sgn_real_def arctan_minus
   58.41 -    by auto
   58.42 +    by (auto simp add: algebra_simps)
   58.43    show "tan (sgn x * pi / 2 - arctan x) = 1 / x"
   58.44      unfolding tan_inverse [of "arctan x", unfolded tan_arctan]
   58.45      unfolding sgn_real_def
    59.1 --- a/src/HOL/Word/Bit_Int.thy	Tue Nov 19 01:30:14 2013 +0100
    59.2 +++ b/src/HOL/Word/Bit_Int.thy	Tue Nov 19 10:05:53 2013 +0100
    59.3 @@ -52,10 +52,10 @@
    59.4  lemma int_not_simps [simp]:
    59.5    "NOT (0::int) = -1"
    59.6    "NOT (1::int) = -2"
    59.7 -  "NOT (-1::int) = 0"
    59.8 -  "NOT (numeral w::int) = neg_numeral (w + Num.One)"
    59.9 -  "NOT (neg_numeral (Num.Bit0 w)::int) = numeral (Num.BitM w)"
   59.10 -  "NOT (neg_numeral (Num.Bit1 w)::int) = numeral (Num.Bit0 w)"
   59.11 +  "NOT (- 1::int) = 0"
   59.12 +  "NOT (numeral w::int) = - numeral (w + Num.One)"
   59.13 +  "NOT (- numeral (Num.Bit0 w)::int) = numeral (Num.BitM w)"
   59.14 +  "NOT (- numeral (Num.Bit1 w)::int) = numeral (Num.Bit0 w)"
   59.15    unfolding int_not_def by simp_all
   59.16  
   59.17  lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
   59.18 @@ -228,11 +228,11 @@
   59.19    by (metis bin_rl_simp)
   59.20  
   59.21  lemma bin_rest_neg_numeral_BitM [simp]:
   59.22 -  "bin_rest (neg_numeral (Num.BitM w)) = neg_numeral w"
   59.23 +  "bin_rest (- numeral (Num.BitM w)) = - numeral w"
   59.24    by (simp only: BIT_bin_simps [symmetric] bin_rest_BIT)
   59.25  
   59.26  lemma bin_last_neg_numeral_BitM [simp]:
   59.27 -  "bin_last (neg_numeral (Num.BitM w)) = 1"
   59.28 +  "bin_last (-  numeral (Num.BitM w)) = 1"
   59.29    by (simp only: BIT_bin_simps [symmetric] bin_last_BIT)
   59.30  
   59.31  text {* FIXME: The rule sets below are very large (24 rules for each
   59.32 @@ -243,26 +243,26 @@
   59.33    "numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT 0"
   59.34    "numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT 0"
   59.35    "numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT 1"
   59.36 -  "numeral (Num.Bit0 x) AND neg_numeral (Num.Bit0 y) = (numeral x AND neg_numeral y) BIT 0"
   59.37 -  "numeral (Num.Bit0 x) AND neg_numeral (Num.Bit1 y) = (numeral x AND neg_numeral (y + Num.One)) BIT 0"
   59.38 -  "numeral (Num.Bit1 x) AND neg_numeral (Num.Bit0 y) = (numeral x AND neg_numeral y) BIT 0"
   59.39 -  "numeral (Num.Bit1 x) AND neg_numeral (Num.Bit1 y) = (numeral x AND neg_numeral (y + Num.One)) BIT 1"
   59.40 -  "neg_numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (neg_numeral x AND numeral y) BIT 0"
   59.41 -  "neg_numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (neg_numeral x AND numeral y) BIT 0"
   59.42 -  "neg_numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) AND numeral y) BIT 0"
   59.43 -  "neg_numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) AND numeral y) BIT 1"
   59.44 -  "neg_numeral (Num.Bit0 x) AND neg_numeral (Num.Bit0 y) = (neg_numeral x AND neg_numeral y) BIT 0"
   59.45 -  "neg_numeral (Num.Bit0 x) AND neg_numeral (Num.Bit1 y) = (neg_numeral x AND neg_numeral (y + Num.One)) BIT 0"
   59.46 -  "neg_numeral (Num.Bit1 x) AND neg_numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) AND neg_numeral y) BIT 0"
   59.47 -  "neg_numeral (Num.Bit1 x) AND neg_numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) AND neg_numeral (y + Num.One)) BIT 1"
   59.48 +  "numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT 0"
   59.49 +  "numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT 0"
   59.50 +  "numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT 0"
   59.51 +  "numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT 1"
   59.52 +  "- numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (- numeral x AND numeral y) BIT 0"
   59.53 +  "- numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (- numeral x AND numeral y) BIT 0"
   59.54 +  "- numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND numeral y) BIT 0"
   59.55 +  "- numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND numeral y) BIT 1"
   59.56 +  "- numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (- numeral x AND - numeral y) BIT 0"
   59.57 +  "- numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (- numeral x AND - numeral (y + Num.One)) BIT 0"
   59.58 +  "- numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND - numeral y) BIT 0"
   59.59 +  "- numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND - numeral (y + Num.One)) BIT 1"
   59.60    "(1::int) AND numeral (Num.Bit0 y) = 0"
   59.61    "(1::int) AND numeral (Num.Bit1 y) = 1"
   59.62 -  "(1::int) AND neg_numeral (Num.Bit0 y) = 0"
   59.63 -  "(1::int) AND neg_numeral (Num.Bit1 y) = 1"
   59.64 +  "(1::int) AND - numeral (Num.Bit0 y) = 0"
   59.65 +  "(1::int) AND - numeral (Num.Bit1 y) = 1"
   59.66    "numeral (Num.Bit0 x) AND (1::int) = 0"
   59.67    "numeral (Num.Bit1 x) AND (1::int) = 1"
   59.68 -  "neg_numeral (Num.Bit0 x) AND (1::int) = 0"
   59.69 -  "neg_numeral (Num.Bit1 x) AND (1::int) = 1"
   59.70 +  "- numeral (Num.Bit0 x) AND (1::int) = 0"
   59.71 +  "- numeral (Num.Bit1 x) AND (1::int) = 1"
   59.72    by (rule bin_rl_eqI, simp, simp)+
   59.73  
   59.74  lemma int_or_numerals [simp]:
   59.75 @@ -270,26 +270,26 @@
   59.76    "numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT 1"
   59.77    "numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT 1"
   59.78    "numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT 1"
   59.79 -  "numeral (Num.Bit0 x) OR neg_numeral (Num.Bit0 y) = (numeral x OR neg_numeral y) BIT 0"
   59.80 -  "numeral (Num.Bit0 x) OR neg_numeral (Num.Bit1 y) = (numeral x OR neg_numeral (y + Num.One)) BIT 1"
   59.81 -  "numeral (Num.Bit1 x) OR neg_numeral (Num.Bit0 y) = (numeral x OR neg_numeral y) BIT 1"
   59.82 -  "numeral (Num.Bit1 x) OR neg_numeral (Num.Bit1 y) = (numeral x OR neg_numeral (y + Num.One)) BIT 1"
   59.83 -  "neg_numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (neg_numeral x OR numeral y) BIT 0"
   59.84 -  "neg_numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (neg_numeral x OR numeral y) BIT 1"
   59.85 -  "neg_numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) OR numeral y) BIT 1"
   59.86 -  "neg_numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) OR numeral y) BIT 1"
   59.87 -  "neg_numeral (Num.Bit0 x) OR neg_numeral (Num.Bit0 y) = (neg_numeral x OR neg_numeral y) BIT 0"
   59.88 -  "neg_numeral (Num.Bit0 x) OR neg_numeral (Num.Bit1 y) = (neg_numeral x OR neg_numeral (y + Num.One)) BIT 1"
   59.89 -  "neg_numeral (Num.Bit1 x) OR neg_numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) OR neg_numeral y) BIT 1"
   59.90 -  "neg_numeral (Num.Bit1 x) OR neg_numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) OR neg_numeral (y + Num.One)) BIT 1"
   59.91 +  "numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT 0"
   59.92 +  "numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT 1"
   59.93 +  "numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT 1"
   59.94 +  "numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT 1"
   59.95 +  "- numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (- numeral x OR numeral y) BIT 0"
   59.96 +  "- numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (- numeral x OR numeral y) BIT 1"
   59.97 +  "- numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR numeral y) BIT 1"
   59.98 +  "- numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR numeral y) BIT 1"
   59.99 +  "- numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (- numeral x OR - numeral y) BIT 0"
  59.100 +  "- numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (- numeral x OR - numeral (y + Num.One)) BIT 1"
  59.101 +  "- numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR - numeral y) BIT 1"
  59.102 +  "- numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR - numeral (y + Num.One)) BIT 1"
  59.103    "(1::int) OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
  59.104    "(1::int) OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)"
  59.105 -  "(1::int) OR neg_numeral (Num.Bit0 y) = neg_numeral (Num.BitM y)"
  59.106 -  "(1::int) OR neg_numeral (Num.Bit1 y) = neg_numeral (Num.Bit1 y)"
  59.107 +  "(1::int) OR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
  59.108 +  "(1::int) OR - numeral (Num.Bit1 y) = - numeral (Num.Bit1 y)"
  59.109    "numeral (Num.Bit0 x) OR (1::int) = numeral (Num.Bit1 x)"
  59.110    "numeral (Num.Bit1 x) OR (1::int) = numeral (Num.Bit1 x)"
  59.111 -  "neg_numeral (Num.Bit0 x) OR (1::int) = neg_numeral (Num.BitM x)"
  59.112 -  "neg_numeral (Num.Bit1 x) OR (1::int) = neg_numeral (Num.Bit1 x)"
  59.113 +  "- numeral (Num.Bit0 x) OR (1::int) = - numeral (Num.BitM x)"
  59.114 +  "- numeral (Num.Bit1 x) OR (1::int) = - numeral (Num.Bit1 x)"
  59.115    by (rule bin_rl_eqI, simp, simp)+
  59.116  
  59.117  lemma int_xor_numerals [simp]:
  59.118 @@ -297,26 +297,26 @@
  59.119    "numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT 1"
  59.120    "numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT 1"
  59.121    "numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT 0"
  59.122 -  "numeral (Num.Bit0 x) XOR neg_numeral (Num.Bit0 y) = (numeral x XOR neg_numeral y) BIT 0"
  59.123 -  "numeral (Num.Bit0 x) XOR neg_numeral (Num.Bit1 y) = (numeral x XOR neg_numeral (y + Num.One)) BIT 1"
  59.124 -  "numeral (Num.Bit1 x) XOR neg_numeral (Num.Bit0 y) = (numeral x XOR neg_numeral y) BIT 1"
  59.125 -  "numeral (Num.Bit1 x) XOR neg_numeral (Num.Bit1 y) = (numeral x XOR neg_numeral (y + Num.One)) BIT 0"
  59.126 -  "neg_numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (neg_numeral x XOR numeral y) BIT 0"
  59.127 -  "neg_numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (neg_numeral x XOR numeral y) BIT 1"
  59.128 -  "neg_numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) XOR numeral y) BIT 1"
  59.129 -  "neg_numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) XOR numeral y) BIT 0"
  59.130 -  "neg_numeral (Num.Bit0 x) XOR neg_numeral (Num.Bit0 y) = (neg_numeral x XOR neg_numeral y) BIT 0"
  59.131 -  "neg_numeral (Num.Bit0 x) XOR neg_numeral (Num.Bit1 y) = (neg_numeral x XOR neg_numeral (y + Num.One)) BIT 1"
  59.132 -  "neg_numeral (Num.Bit1 x) XOR neg_numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) XOR neg_numeral y) BIT 1"
  59.133 -  "neg_numeral (Num.Bit1 x) XOR neg_numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) XOR neg_numeral (y + Num.One)) BIT 0"
  59.134 +  "numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT 0"
  59.135 +  "numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT 1"
  59.136 +  "numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT 1"
  59.137 +  "numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT 0"
  59.138 +  "- numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (- numeral x XOR numeral y) BIT 0"
  59.139 +  "- numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (- numeral x XOR numeral y) BIT 1"
  59.140 +  "- numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR numeral y) BIT 1"
  59.141 +  "- numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR numeral y) BIT 0"
  59.142 +  "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (- numeral x XOR - numeral y) BIT 0"
  59.143 +  "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (- numeral x XOR - numeral (y + Num.One)) BIT 1"
  59.144 +  "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR - numeral y) BIT 1"
  59.145 +  "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR - numeral (y + Num.One)) BIT 0"
  59.146    "(1::int) XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
  59.147    "(1::int) XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)"
  59.148 -  "(1::int) XOR neg_numeral (Num.Bit0 y) = neg_numeral (Num.BitM y)"
  59.149 -  "(1::int) XOR neg_numeral (Num.Bit1 y) = neg_numeral (Num.Bit0 (y + Num.One))"
  59.150 +  "(1::int) XOR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
  59.151 +  "(1::int) XOR - numeral (Num.Bit1 y) = - numeral (Num.Bit0 (y + Num.One))"
  59.152    "numeral (Num.Bit0 x) XOR (1::int) = numeral (Num.Bit1 x)"
  59.153    "numeral (Num.Bit1 x) XOR (1::int) = numeral (Num.Bit0 x)"
  59.154 -  "neg_numeral (Num.Bit0 x) XOR (1::int) = neg_numeral (Num.BitM x)"
  59.155 -  "neg_numeral (Num.Bit1 x) XOR (1::int) = neg_numeral (Num.Bit0 (x + Num.One))"
  59.156 +  "- numeral (Num.Bit0 x) XOR (1::int) = - numeral (Num.BitM x)"
  59.157 +  "- numeral (Num.Bit1 x) XOR (1::int) = - numeral (Num.Bit0 (x + Num.One))"
  59.158    by (rule bin_rl_eqI, simp, simp)+
  59.159  
  59.160  subsubsection {* Interactions with arithmetic *}
    60.1 --- a/src/HOL/Word/Bit_Representation.thy	Tue Nov 19 01:30:14 2013 +0100
    60.2 +++ b/src/HOL/Word/Bit_Representation.thy	Tue Nov 19 10:05:53 2013 +0100
    60.3 @@ -61,21 +61,23 @@
    60.4  lemma BIT_bin_simps [simp]:
    60.5    "numeral k BIT 0 = numeral (Num.Bit0 k)"
    60.6    "numeral k BIT 1 = numeral (Num.Bit1 k)"
    60.7 -  "neg_numeral k BIT 0 = neg_numeral (Num.Bit0 k)"
    60.8 -  "neg_numeral k BIT 1 = neg_numeral (Num.BitM k)"
    60.9 -  unfolding neg_numeral_def numeral.simps numeral_BitM
   60.10 +  "(- numeral k) BIT 0 = - numeral (Num.Bit0 k)"
   60.11 +  "(- numeral k) BIT 1 = - numeral (Num.BitM k)"
   60.12 +  unfolding numeral.simps numeral_BitM
   60.13    unfolding Bit_def bitval_simps
   60.14    by (simp_all del: arith_simps add_numeral_special diff_numeral_special)
   60.15  
   60.16  lemma BIT_special_simps [simp]:
   60.17 -  shows "0 BIT 0 = 0" and "0 BIT 1 = 1" and "1 BIT 0 = 2" and "1 BIT 1 = 3"
   60.18 +  shows "0 BIT 0 = 0" and "0 BIT 1 = 1"
   60.19 +  and "1 BIT 0 = 2" and "1 BIT 1 = 3"
   60.20 +  and "(- 1) BIT 0 = - 2" and "(- 1) BIT 1 = - 1"
   60.21    unfolding Bit_def by simp_all
   60.22  
   60.23  lemma Bit_eq_0_iff: "w BIT b = 0 \<longleftrightarrow> w = 0 \<and> b = 0"
   60.24    by (subst BIT_eq_iff [symmetric], simp)
   60.25  
   60.26 -lemma Bit_eq_m1_iff: "w BIT b = -1 \<longleftrightarrow> w = -1 \<and> b = 1"
   60.27 -  by (subst BIT_eq_iff [symmetric], simp)
   60.28 +lemma Bit_eq_m1_iff: "w BIT b = - 1 \<longleftrightarrow> w = - 1 \<and> b = 1"
   60.29 +  by (cases b) (auto simp add: Bit_def, arith)
   60.30  
   60.31  lemma BitM_inc: "Num.BitM (Num.inc w) = Num.Bit1 w"
   60.32    by (induct w, simp_all)
   60.33 @@ -83,8 +85,8 @@
   60.34  lemma expand_BIT:
   60.35    "numeral (Num.Bit0 w) = numeral w BIT 0"
   60.36    "numeral (Num.Bit1 w) = numeral w BIT 1"
   60.37 -  "neg_numeral (Num.Bit0 w) = neg_numeral w BIT 0"
   60.38 -  "neg_numeral (Num.Bit1 w) = neg_numeral (w + Num.One) BIT 1"
   60.39 +  "- numeral (Num.Bit0 w) = - numeral w BIT 0"
   60.40 +  "- numeral (Num.Bit1 w) = (- numeral (w + Num.One)) BIT 1"
   60.41    unfolding add_One by (simp_all add: BitM_inc)
   60.42  
   60.43  lemma bin_last_numeral_simps [simp]:
   60.44 @@ -94,9 +96,9 @@
   60.45    "bin_last Numeral1 = 1"
   60.46    "bin_last (numeral (Num.Bit0 w)) = 0"
   60.47    "bin_last (numeral (Num.Bit1 w)) = 1"
   60.48 -  "bin_last (neg_numeral (Num.Bit0 w)) = 0"
   60.49 -  "bin_last (neg_numeral (Num.Bit1 w)) = 1"
   60.50 -  unfolding expand_BIT bin_last_BIT by (simp_all add: bin_last_def)
   60.51 +  "bin_last (- numeral (Num.Bit0 w)) = 0"
   60.52 +  "bin_last (- numeral (Num.Bit1 w)) = 1"
   60.53 +  unfolding expand_BIT bin_last_BIT by (simp_all add: bin_last_def zmod_zminus1_eq_if)
   60.54  
   60.55  lemma bin_rest_numeral_simps [simp]:
   60.56    "bin_rest 0 = 0"
   60.57 @@ -105,9 +107,9 @@
   60.58    "bin_rest Numeral1 = 0"
   60.59    "bin_rest (numeral (Num.Bit0 w)) = numeral w"
   60.60    "bin_rest (numeral (Num.Bit1 w)) = numeral w"
   60.61 -  "bin_rest (neg_numeral (Num.Bit0 w)) = neg_numeral w"
   60.62 -  "bin_rest (neg_numeral (Num.Bit1 w)) = neg_numeral (w + Num.One)"
   60.63 -  unfolding expand_BIT bin_rest_BIT by (simp_all add: bin_rest_def)
   60.64 +  "bin_rest (- numeral (Num.Bit0 w)) = - numeral w"
   60.65 +  "bin_rest (- numeral (Num.Bit1 w)) = - numeral (w + Num.One)"
   60.66 +  unfolding expand_BIT bin_rest_BIT by (simp_all add: bin_rest_def zdiv_zminus1_eq_if)
   60.67  
   60.68  lemma less_Bits: 
   60.69    "(v BIT b < w BIT c) = (v < w | v <= w & b = (0::bit) & c = (1::bit))"
   60.70 @@ -197,42 +199,45 @@
   60.71  lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
   60.72    unfolding bin_rest_def [symmetric] by (rule bin_rest_BIT)
   60.73  
   60.74 -lemma bin_nth_lem [rule_format]:
   60.75 -  "ALL y. bin_nth x = bin_nth y --> x = y"
   60.76 -  apply (induct x rule: bin_induct)
   60.77 -    apply safe
   60.78 -    apply (erule rev_mp)
   60.79 -    apply (induct_tac y rule: bin_induct)
   60.80 +lemma bin_nth_eq_iff:
   60.81 +  "bin_nth x = bin_nth y \<longleftrightarrow> x = y"
   60.82 +proof -
   60.83 +  have bin_nth_lem [rule_format]: "ALL y. bin_nth x = bin_nth y --> x = y"
   60.84 +    apply (induct x rule: bin_induct)
   60.85        apply safe
   60.86 -      apply (drule_tac x=0 in fun_cong, force)
   60.87 -     apply (erule notE, rule ext, 
   60.88 +      apply (erule rev_mp)
   60.89 +      apply (induct_tac y rule: bin_induct)
   60.90 +        apply safe
   60.91 +        apply (drule_tac x=0 in fun_cong, force)
   60.92 +       apply (erule notE, rule ext, 
   60.93              drule_tac x="Suc x" in fun_cong, force)
   60.94 -    apply (drule_tac x=0 in fun_cong, force)
   60.95 -   apply (erule rev_mp)
   60.96 -   apply (induct_tac y rule: bin_induct)
   60.97 -     apply safe
   60.98 +      apply (drule_tac x=0 in fun_cong, force)
   60.99 +     apply (erule rev_mp)
  60.100 +     apply (induct_tac y rule: bin_induct)
  60.101 +       apply safe
  60.102 +       apply (drule_tac x=0 in fun_cong, force)
  60.103 +      apply (erule notE, rule ext, 
  60.104 +           drule_tac x="Suc x" in fun_cong, force)
  60.105 +      apply (metis Bit_eq_m1_iff Z bin_last_BIT)
  60.106 +    apply (case_tac y rule: bin_exhaust)
  60.107 +    apply clarify
  60.108 +    apply (erule allE)
  60.109 +    apply (erule impE)
  60.110 +     prefer 2
  60.111 +     apply (erule conjI)
  60.112       apply (drule_tac x=0 in fun_cong, force)
  60.113 -    apply (erule notE, rule ext, 
  60.114 -           drule_tac x="Suc x" in fun_cong, force)
  60.115 -   apply (drule_tac x=0 in fun_cong, force)
  60.116 -  apply (case_tac y rule: bin_exhaust)
  60.117 -  apply clarify
  60.118 -  apply (erule allE)
  60.119 -  apply (erule impE)
  60.120 -   prefer 2
  60.121 -   apply (erule conjI)
  60.122 -   apply (drule_tac x=0 in fun_cong, force)
  60.123 -  apply (rule ext)
  60.124 -  apply (drule_tac x="Suc ?x" in fun_cong, force)
  60.125 -  done
  60.126 -
  60.127 -lemma bin_nth_eq_iff: "(bin_nth x = bin_nth y) = (x = y)"
  60.128 +    apply (rule ext)
  60.129 +    apply (drule_tac x="Suc ?x" in fun_cong, force)
  60.130 +    done
  60.131 +  show ?thesis
  60.132    by (auto elim: bin_nth_lem)
  60.133 +qed
  60.134  
  60.135  lemmas bin_eqI = ext [THEN bin_nth_eq_iff [THEN iffD1]]
  60.136  
  60.137 -lemma bin_eq_iff: "x = y \<longleftrightarrow> (\<forall>n. bin_nth x n = bin_nth y n)"
  60.138 -  by (auto intro!: bin_nth_lem del: equalityI)
  60.139 +lemma bin_eq_iff:
  60.140 +  "x = y \<longleftrightarrow> (\<forall>n. bin_nth x n = bin_nth y n)"
  60.141 +  using bin_nth_eq_iff by auto
  60.142  
  60.143  lemma bin_nth_zero [simp]: "\<not> bin_nth 0 n"
  60.144    by (induct n) auto
  60.145 @@ -276,8 +281,9 @@
  60.146  lemma bin_sign_simps [simp]:
  60.147    "bin_sign 0 = 0"
  60.148    "bin_sign 1 = 0"
  60.149 +  "bin_sign (- 1) = - 1"
  60.150    "bin_sign (numeral k) = 0"
  60.151 -  "bin_sign (neg_numeral k) = -1"
  60.152 +  "bin_sign (- numeral k) = -1"
  60.153    "bin_sign (w BIT b) = bin_sign w"
  60.154    unfolding bin_sign_def Bit_def bitval_def
  60.155    by (simp_all split: bit.split)
  60.156 @@ -331,18 +337,18 @@
  60.157    "bintrunc (Suc n) -1 = bintrunc n -1 BIT 1"
  60.158    "bintrunc (Suc n) (numeral (Num.Bit0 w)) = bintrunc n (numeral w) BIT 0"
  60.159    "bintrunc (Suc n) (numeral (Num.Bit1 w)) = bintrunc n (numeral w) BIT 1"
  60.160 -  "bintrunc (Suc n) (neg_numeral (Num.Bit0 w)) =
  60.161 -    bintrunc n (neg_numeral w) BIT 0"
  60.162 -  "bintrunc (Suc n) (neg_numeral (Num.Bit1 w)) =
  60.163 -    bintrunc n (neg_numeral (w + Num.One)) BIT 1"
  60.164 +  "bintrunc (Suc n) (- numeral (Num.Bit0 w)) =
  60.165 +    bintrunc n (- numeral w) BIT 0"
  60.166 +  "bintrunc (Suc n) (- numeral (Num.Bit1 w)) =
  60.167 +    bintrunc n (- numeral (w + Num.One)) BIT 1"
  60.168    by simp_all
  60.169  
  60.170  lemma sbintrunc_0_numeral [simp]:
  60.171    "sbintrunc 0 1 = -1"
  60.172    "sbintrunc 0 (numeral (Num.Bit0 w)) = 0"
  60.173    "sbintrunc 0 (numeral (Num.Bit1 w)) = -1"
  60.174 -  "sbintrunc 0 (neg_numeral (Num.Bit0 w)) = 0"
  60.175 -  "sbintrunc 0 (neg_numeral (Num.Bit1 w)) = -1"
  60.176 +  "sbintrunc 0 (- numeral (Num.Bit0 w)) = 0"
  60.177 +  "sbintrunc 0 (- numeral (Num.Bit1 w)) = -1"
  60.178    by simp_all
  60.179  
  60.180  lemma sbintrunc_Suc_numeral:
  60.181 @@ -351,10 +357,10 @@
  60.182      sbintrunc n (numeral w) BIT 0"
  60.183    "sbintrunc (Suc n) (numeral (Num.Bit1 w)) =
  60.184      sbintrunc n (numeral w) BIT 1"
  60.185 -  "sbintrunc (Suc n) (neg_numeral (Num.Bit0 w)) =
  60.186 -    sbintrunc n (neg_numeral w) BIT 0"
  60.187 -  "sbintrunc (Suc n) (neg_numeral (Num.Bit1 w)) =
  60.188 -    sbintrunc n (neg_numeral (w + Num.One)) BIT 1"
  60.189 +  "sbintrunc (Suc n) (- numeral (Num.Bit0 w)) =
  60.190 +    sbintrunc n (- numeral w) BIT 0"
  60.191 +  "sbintrunc (Suc n) (- numeral (Num.Bit1 w)) =
  60.192 +    sbintrunc n (- numeral (w + Num.One)) BIT 1"
  60.193    by simp_all
  60.194  
  60.195  lemma bit_bool:
  60.196 @@ -580,10 +586,10 @@
  60.197      bintrunc (pred_numeral k) (numeral w) BIT 0"
  60.198    "bintrunc (numeral k) (numeral (Num.Bit1 w)) =
  60.199      bintrunc (pred_numeral k) (numeral w) BIT 1"
  60.200 -  "bintrunc (numeral k) (neg_numeral (Num.Bit0 w)) =
  60.201 -    bintrunc (pred_numeral k) (neg_numeral w) BIT 0"
  60.202 -  "bintrunc (numeral k) (neg_numeral (Num.Bit1 w)) =
  60.203 -    bintrunc (pred_numeral k) (neg_numeral (w + Num.One)) BIT 1"
  60.204 +  "bintrunc (numeral k) (- numeral (Num.Bit0 w)) =
  60.205 +    bintrunc (pred_numeral k) (- numeral w) BIT 0"
  60.206 +  "bintrunc (numeral k) (- numeral (Num.Bit1 w)) =
  60.207 +    bintrunc (pred_numeral k) (- numeral (w + Num.One)) BIT 1"
  60.208    "bintrunc (numeral k) 1 = 1"
  60.209    by (simp_all add: bintrunc_numeral)
  60.210  
  60.211 @@ -592,10 +598,10 @@
  60.212      sbintrunc (pred_numeral k) (numeral w) BIT 0"
  60.213    "sbintrunc (numeral k) (numeral (Num.Bit1 w)) =
  60.214      sbintrunc (pred_numeral k) (numeral w) BIT 1"
  60.215 -  "sbintrunc (numeral k) (neg_numeral (Num.Bit0 w)) =
  60.216 -    sbintrunc (pred_numeral k) (neg_numeral w) BIT 0"
  60.217 -  "sbintrunc (numeral k) (neg_numeral (Num.Bit1 w)) =
  60.218 -    sbintrunc (pred_numeral k) (neg_numeral (w + Num.One)) BIT 1"
  60.219 +  "sbintrunc (numeral k) (- numeral (Num.Bit0 w)) =
  60.220 +    sbintrunc (pred_numeral k) (- numeral w) BIT 0"
  60.221 +  "sbintrunc (numeral k) (- numeral (Num.Bit1 w)) =
  60.222 +    sbintrunc (pred_numeral k) (- numeral (w + Num.One)) BIT 1"
  60.223    "sbintrunc (numeral k) 1 = 1"
  60.224    by (simp_all add: sbintrunc_numeral)
  60.225  
    61.1 --- a/src/HOL/Word/Word.thy	Tue Nov 19 01:30:14 2013 +0100
    61.2 +++ b/src/HOL/Word/Word.thy	Tue Nov 19 10:05:53 2013 +0100
    61.3 @@ -591,24 +591,24 @@
    61.4  declare word_numeral_alt [symmetric, code_abbrev]
    61.5  
    61.6  lemma word_neg_numeral_alt:
    61.7 -  "neg_numeral b = word_of_int (neg_numeral b)"
    61.8 -  by (simp only: neg_numeral_def word_numeral_alt wi_hom_neg)
    61.9 +  "- numeral b = word_of_int (- numeral b)"
   61.10 +  by (simp only: word_numeral_alt wi_hom_neg)
   61.11  
   61.12  declare word_neg_numeral_alt [symmetric, code_abbrev]
   61.13  
   61.14  lemma word_numeral_transfer [transfer_rule]:
   61.15    "(fun_rel op = pcr_word) numeral numeral"
   61.16 -  "(fun_rel op = pcr_word) neg_numeral neg_numeral"
   61.17 -  unfolding fun_rel_def word.pcr_cr_eq cr_word_def word_numeral_alt word_neg_numeral_alt
   61.18 -  by simp_all
   61.19 +  "(fun_rel op = pcr_word) (- numeral) (- numeral)"
   61.20 +  apply (simp_all add: fun_rel_def word.pcr_cr_eq cr_word_def)
   61.21 +  using word_numeral_alt [symmetric] word_neg_numeral_alt [symmetric] by blast+
   61.22  
   61.23  lemma uint_bintrunc [simp]:
   61.24    "uint (numeral bin :: 'a word) = 
   61.25      bintrunc (len_of TYPE ('a :: len0)) (numeral bin)"
   61.26    unfolding word_numeral_alt by (rule word_ubin.eq_norm)
   61.27  
   61.28 -lemma uint_bintrunc_neg [simp]: "uint (neg_numeral bin :: 'a word) = 
   61.29 -    bintrunc (len_of TYPE ('a :: len0)) (neg_numeral bin)"
   61.30 +lemma uint_bintrunc_neg [simp]: "uint (- numeral bin :: 'a word) = 
   61.31 +    bintrunc (len_of TYPE ('a :: len0)) (- numeral bin)"
   61.32    by (simp only: word_neg_numeral_alt word_ubin.eq_norm)
   61.33  
   61.34  lemma sint_sbintrunc [simp]:
   61.35 @@ -616,8 +616,8 @@
   61.36      sbintrunc (len_of TYPE ('a :: len) - 1) (numeral bin)"
   61.37    by (simp only: word_numeral_alt word_sbin.eq_norm)
   61.38  
   61.39 -lemma sint_sbintrunc_neg [simp]: "sint (neg_numeral bin :: 'a word) = 
   61.40 -    sbintrunc (len_of TYPE ('a :: len) - 1) (neg_numeral bin)"
   61.41 +lemma sint_sbintrunc_neg [simp]: "sint (- numeral bin :: 'a word) = 
   61.42 +    sbintrunc (len_of TYPE ('a :: len) - 1) (- numeral bin)"
   61.43    by (simp only: word_neg_numeral_alt word_sbin.eq_norm)
   61.44  
   61.45  lemma unat_bintrunc [simp]:
   61.46 @@ -626,8 +626,8 @@
   61.47    by (simp only: unat_def uint_bintrunc)
   61.48  
   61.49  lemma unat_bintrunc_neg [simp]:
   61.50 -  "unat (neg_numeral bin :: 'a :: len0 word) =
   61.51 -    nat (bintrunc (len_of TYPE('a)) (neg_numeral bin))"
   61.52 +  "unat (- numeral bin :: 'a :: len0 word) =
   61.53 +    nat (bintrunc (len_of TYPE('a)) (- numeral bin))"
   61.54    by (simp only: unat_def uint_bintrunc_neg)
   61.55  
   61.56  lemma size_0_eq: "size (w :: 'a :: len0 word) = 0 \<Longrightarrow> v = w"
   61.57 @@ -678,7 +678,7 @@
   61.58    by (simp only: int_word_uint)
   61.59  
   61.60  lemma uint_neg_numeral:
   61.61 -  "uint (neg_numeral b :: 'a :: len0 word) = neg_numeral b mod 2 ^ len_of TYPE('a)"
   61.62 +  "uint (- numeral b :: 'a :: len0 word) = - numeral b mod 2 ^ len_of TYPE('a)"
   61.63    unfolding word_neg_numeral_alt
   61.64    by (simp only: int_word_uint)
   61.65  
   61.66 @@ -702,13 +702,16 @@
   61.67  lemma word_of_int_1 [simp, code_post]: "word_of_int 1 = 1"
   61.68    unfolding word_1_wi ..
   61.69  
   61.70 +lemma word_of_int_neg_1 [simp]: "word_of_int (- 1) = - 1"
   61.71 +  by (simp add: wi_hom_syms)
   61.72 +
   61.73  lemma word_of_int_numeral [simp] : 
   61.74    "(word_of_int (numeral bin) :: 'a :: len0 word) = (numeral bin)"
   61.75    unfolding word_numeral_alt ..
   61.76  
   61.77  lemma word_of_int_neg_numeral [simp]:
   61.78 -  "(word_of_int (neg_numeral bin) :: 'a :: len0 word) = (neg_numeral bin)"
   61.79 -  unfolding neg_numeral_def word_numeral_alt wi_hom_syms ..
   61.80 +  "(word_of_int (- numeral bin) :: 'a :: len0 word) = (- numeral bin)"
   61.81 +  unfolding word_numeral_alt wi_hom_syms ..
   61.82  
   61.83  lemma word_int_case_wi: 
   61.84    "word_int_case f (word_of_int i :: 'b word) = 
   61.85 @@ -880,8 +883,8 @@
   61.86    unfolding word_numeral_alt by (rule to_bl_of_bin)
   61.87  
   61.88  lemma to_bl_neg_numeral [simp]:
   61.89 -  "to_bl (neg_numeral bin::'a::len0 word) =
   61.90 -    bin_to_bl (len_of TYPE('a)) (neg_numeral bin)"
   61.91 +  "to_bl (- numeral bin::'a::len0 word) =
   61.92 +    bin_to_bl (len_of TYPE('a)) (- numeral bin)"
   61.93    unfolding word_neg_numeral_alt by (rule to_bl_of_bin)
   61.94  
   61.95  lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"
   61.96 @@ -1156,11 +1159,8 @@
   61.97  
   61.98  lemmas word_sle_no [simp] = word_sle_def [of "numeral a" "numeral b"] for a b
   61.99  
  61.100 -lemma word_1_no: "(1::'a::len0 word) = Numeral1"
  61.101 -  by (simp add: word_numeral_alt)
  61.102 -
  61.103 -lemma word_m1_wi: "-1 = word_of_int -1" 
  61.104 -  by (rule word_neg_numeral_alt)
  61.105 +lemma word_m1_wi: "- 1 = word_of_int (- 1)" 
  61.106 +  using word_neg_numeral_alt [of Num.One] by simp
  61.107  
  61.108  lemma word_0_bl [simp]: "of_bl [] = 0"
  61.109    unfolding of_bl_def by simp
  61.110 @@ -1215,9 +1215,9 @@
  61.111    unfolding scast_def by simp
  61.112  
  61.113  lemma sint_n1 [simp] : "sint -1 = -1"
  61.114 -  unfolding word_m1_wi by (simp add: word_sbin.eq_norm)
  61.115 -
  61.116 -lemma scast_n1 [simp]: "scast -1 = -1"
  61.117 +  unfolding word_m1_wi word_sbin.eq_norm by simp
  61.118 +
  61.119 +lemma scast_n1 [simp]: "scast (- 1) = - 1"
  61.120    unfolding scast_def by simp
  61.121  
  61.122  lemma uint_1 [simp]: "uint (1::'a::len word) = 1"
  61.123 @@ -1270,8 +1270,8 @@
  61.124  lemma succ_pred_no [simp]:
  61.125    "word_succ (numeral w) = numeral w + 1"
  61.126    "word_pred (numeral w) = numeral w - 1"
  61.127 -  "word_succ (neg_numeral w) = neg_numeral w + 1"
  61.128 -  "word_pred (neg_numeral w) = neg_numeral w - 1"
  61.129 +  "word_succ (- numeral w) = - numeral w + 1"
  61.130 +  "word_pred (- numeral w) = - numeral w - 1"
  61.131    unfolding word_succ_p1 word_pred_m1 by simp_all
  61.132  
  61.133  lemma word_sp_01 [simp] : 
  61.134 @@ -2151,19 +2151,19 @@
  61.135  
  61.136  lemma word_no_log_defs [simp]:
  61.137    "NOT (numeral a) = word_of_int (NOT (numeral a))"
  61.138 -  "NOT (neg_numeral a) = word_of_int (NOT (neg_numeral a))"
  61.139 +  "NOT (- numeral a) = word_of_int (NOT (- numeral a))"
  61.140    "numeral a AND numeral b = word_of_int (numeral a AND numeral b)"
  61.141 -  "numeral a AND neg_numeral b = word_of_int (numeral a AND neg_numeral b)"
  61.142 -  "neg_numeral a AND numeral b = word_of_int (neg_numeral a AND numeral b)"
  61.143 -  "neg_numeral a AND neg_numeral b = word_of_int (neg_numeral a AND neg_numeral b)"
  61.144 +  "numeral a AND - numeral b = word_of_int (numeral a AND - numeral b)"
  61.145 +  "- numeral a AND numeral b = word_of_int (- numeral a AND numeral b)"
  61.146 +  "- numeral a AND - numeral b = word_of_int (- numeral a AND - numeral b)"
  61.147    "numeral a OR numeral b = word_of_int (numeral a OR numeral b)"
  61.148 -  "numeral a OR neg_numeral b = word_of_int (numeral a OR neg_numeral b)"
  61.149 -  "neg_numeral a OR numeral b = word_of_int (neg_numeral a OR numeral b)"
  61.150 -  "neg_numeral a OR neg_numeral b = word_of_int (neg_numeral a OR neg_numeral b)"
  61.151 +  "numeral a OR - numeral b = word_of_int (numeral a OR - numeral b)"
  61.152 +  "- numeral a OR numeral b = word_of_int (- numeral a OR numeral b)"
  61.153 +  "- numeral a OR - numeral b = word_of_int (- numeral a OR - numeral b)"
  61.154    "numeral a XOR numeral b = word_of_int (numeral a XOR numeral b)"
  61.155 -  "numeral a XOR neg_numeral b = word_of_int (numeral a XOR neg_numeral b)"
  61.156 -  "neg_numeral a XOR numeral b = word_of_int (neg_numeral a XOR numeral b)"
  61.157 -  "neg_numeral a XOR neg_numeral b = word_of_int (neg_numeral a XOR neg_numeral b)"
  61.158 +  "numeral a XOR - numeral b = word_of_int (numeral a XOR - numeral b)"
  61.159 +  "- numeral a XOR numeral b = word_of_int (- numeral a XOR numeral b)"
  61.160 +  "- numeral a XOR - numeral b = word_of_int (- numeral a XOR - numeral b)"
  61.161    by (transfer, rule refl)+
  61.162  
  61.163  text {* Special cases for when one of the arguments equals 1. *}
  61.164 @@ -2171,17 +2171,17 @@
  61.165  lemma word_bitwise_1_simps [simp]:
  61.166    "NOT (1::'a::len0 word) = -2"
  61.167    "1 AND numeral b = word_of_int (1 AND numeral b)"
  61.168 -  "1 AND neg_numeral b = word_of_int (1 AND neg_numeral b)"
  61.169 +  "1 AND - numeral b = word_of_int (1 AND - numeral b)"
  61.170    "numeral a AND 1 = word_of_int (numeral a AND 1)"
  61.171 -  "neg_numeral a AND 1 = word_of_int (neg_numeral a AND 1)"
  61.172 +  "- numeral a AND 1 = word_of_int (- numeral a AND 1)"
  61.173    "1 OR numeral b = word_of_int (1 OR numeral b)"
  61.174 -  "1 OR neg_numeral b = word_of_int (1 OR neg_numeral b)"
  61.175 +  "1 OR - numeral b = word_of_int (1 OR - numeral b)"
  61.176    "numeral a OR 1 = word_of_int (numeral a OR 1)"
  61.177 -  "neg_numeral a OR 1 = word_of_int (neg_numeral a OR 1)"
  61.178 +  "- numeral a OR 1 = word_of_int (- numeral a OR 1)"
  61.179    "1 XOR numeral b = word_of_int (1 XOR numeral b)"
  61.180 -  "1 XOR neg_numeral b = word_of_int (1 XOR neg_numeral b)"
  61.181 +  "1 XOR - numeral b = word_of_int (1 XOR - numeral b)"
  61.182    "numeral a XOR 1 = word_of_int (numeral a XOR 1)"
  61.183 -  "neg_numeral a XOR 1 = word_of_int (neg_numeral a XOR 1)"
  61.184 +  "- numeral a XOR 1 = word_of_int (- numeral a XOR 1)"
  61.185    by (transfer, simp)+
  61.186  
  61.187  lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
  61.188 @@ -2220,8 +2220,8 @@
  61.189    by transfer (rule refl)
  61.190  
  61.191  lemma test_bit_neg_numeral [simp]:
  61.192 -  "(neg_numeral w :: 'a::len0 word) !! n \<longleftrightarrow>
  61.193 -    n < len_of TYPE('a) \<and> bin_nth (neg_numeral w) n"
  61.194 +  "(- numeral w :: 'a::len0 word) !! n \<longleftrightarrow>
  61.195 +    n < len_of TYPE('a) \<and> bin_nth (- numeral w) n"
  61.196    by transfer (rule refl)
  61.197  
  61.198  lemma test_bit_1 [simp]: "(1::'a::len word) !! n \<longleftrightarrow> n = 0"
  61.199 @@ -2398,7 +2398,7 @@
  61.200    unfolding word_numeral_alt by (rule msb_word_of_int)
  61.201  
  61.202  lemma word_msb_neg_numeral [simp]:
  61.203 -  "msb (neg_numeral w::'a::len word) = bin_nth (neg_numeral w) (len_of TYPE('a) - 1)"
  61.204 +  "msb (- numeral w::'a::len word) = bin_nth (- numeral w) (len_of TYPE('a) - 1)"
  61.205    unfolding word_neg_numeral_alt by (rule msb_word_of_int)
  61.206  
  61.207  lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)"
  61.208 @@ -2528,7 +2528,7 @@
  61.209    unfolding word_lsb_alt test_bit_numeral by simp
  61.210  
  61.211  lemma word_lsb_neg_numeral [simp]:
  61.212 -  "lsb (neg_numeral bin :: 'a :: len word) = (bin_last (neg_numeral bin) = 1)"
  61.213 +  "lsb (- numeral bin :: 'a :: len word) = (bin_last (- numeral bin) = 1)"
  61.214    unfolding word_lsb_alt test_bit_neg_numeral by simp
  61.215  
  61.216  lemma set_bit_word_of_int:
  61.217 @@ -2544,8 +2544,8 @@
  61.218    unfolding word_numeral_alt by (rule set_bit_word_of_int)
  61.219  
  61.220  lemma word_set_neg_numeral [simp]:
  61.221 -  "set_bit (neg_numeral bin::'a::len0 word) n b = 
  61.222 -    word_of_int (bin_sc n (if b then 1 else 0) (neg_numeral bin))"
  61.223 +  "set_bit (- numeral bin::'a::len0 word) n b = 
  61.224 +    word_of_int (bin_sc n (if b then 1 else 0) (- numeral bin))"
  61.225    unfolding word_neg_numeral_alt by (rule set_bit_word_of_int)
  61.226  
  61.227  lemma word_set_bit_0 [simp]:
  61.228 @@ -2612,8 +2612,14 @@
  61.229      apply clarsimp
  61.230     apply clarsimp
  61.231    apply (drule word_gt_0 [THEN iffD1])
  61.232 -  apply (safe intro!: word_eqI bin_nth_lem)
  61.233 -     apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric])
  61.234 +  apply (safe intro!: word_eqI)
  61.235 +  apply (auto simp add: nth_2p_bin)
  61.236 +  apply (erule notE)
  61.237 +  apply (simp (no_asm_use) add: uint_word_of_int word_size)
  61.238 +  apply (subst mod_pos_pos_trivial)
  61.239 +  apply simp
  61.240 +  apply (rule power_strict_increasing)
  61.241 +  apply simp_all
  61.242    done
  61.243  
  61.244  lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n" 
  61.245 @@ -2670,7 +2676,7 @@
  61.246    unfolding word_numeral_alt shiftl1_wi by simp
  61.247  
  61.248  lemma shiftl1_neg_numeral [simp]:
  61.249 -  "shiftl1 (neg_numeral w) = neg_numeral (Num.Bit0 w)"
  61.250 +  "shiftl1 (- numeral w) = - numeral (Num.Bit0 w)"
  61.251    unfolding word_neg_numeral_alt shiftl1_wi by simp
  61.252  
  61.253  lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
  61.254 @@ -4638,9 +4644,6 @@
  61.255    "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
  61.256    by unat_arith
  61.257  
  61.258 -lemma word_no_1 [simp]: "(Numeral1::'a::len0 word) = 1"
  61.259 -  by (fact word_1_no [symmetric])
  61.260 -
  61.261  declare bin_to_bl_def [simp]
  61.262  
  61.263  ML_file "Tools/word_lib.ML"
    62.1 --- a/src/HOL/Word/WordBitwise.thy	Tue Nov 19 01:30:14 2013 +0100
    62.2 +++ b/src/HOL/Word/WordBitwise.thy	Tue Nov 19 10:05:53 2013 +0100
    62.3 @@ -461,18 +461,18 @@
    62.4      = True # rev (bin_to_bl n (numeral nm))"
    62.5    "rev (bin_to_bl (Suc n) (numeral (num.One)))
    62.6      = True # replicate n False"
    62.7 -  "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit0 nm)))
    62.8 -    = False # rev (bin_to_bl n (neg_numeral nm))"
    62.9 -  "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit1 nm)))
   62.10 -    = True # rev (bin_to_bl n (neg_numeral (nm + num.One)))"
   62.11 -  "rev (bin_to_bl (Suc n) (neg_numeral (num.One)))
   62.12 +  "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm)))
   62.13 +    = False # rev (bin_to_bl n (- numeral nm))"
   62.14 +  "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm)))
   62.15 +    = True # rev (bin_to_bl n (- numeral (nm + num.One)))"
   62.16 +  "rev (bin_to_bl (Suc n) (- numeral (num.One)))
   62.17      = True # replicate n True"
   62.18 -  "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit0 nm + num.One)))
   62.19 -    = True # rev (bin_to_bl n (neg_numeral (nm + num.One)))"
   62.20 -  "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit1 nm + num.One)))
   62.21 -    = False # rev (bin_to_bl n (neg_numeral (nm + num.One)))"
   62.22 -  "rev (bin_to_bl (Suc n) (neg_numeral (num.One + num.One)))
   62.23 -    = False # rev (bin_to_bl n (neg_numeral num.One))"
   62.24 +  "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm + num.One)))
   62.25 +    = True # rev (bin_to_bl n (- numeral (nm + num.One)))"
   62.26 +  "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm + num.One)))
   62.27 +    = False # rev (bin_to_bl n (- numeral (nm + num.One)))"
   62.28 +  "rev (bin_to_bl (Suc n) (- numeral (num.One + num.One)))
   62.29 +    = False # rev (bin_to_bl n (- numeral num.One))"
   62.30    apply (simp_all add: bin_to_bl_def)
   62.31    apply (simp_all only: bin_to_bl_aux_alt)
   62.32    apply (simp_all)