# HG changeset patch
# User haftmann
# Date 1384851953 -3600
# Node ID 03ff4d1e6784108a12513b344a628c1f6fc5b131
# Parent  b60f1fab408c57daf97bfeb4b252b9f6a15ec296
eliminiated neg_numeral in favour of - (numeral _)

diff -r b60f1fab408c -r 03ff4d1e6784 NEWS
--- a/NEWS	Tue Nov 19 01:30:14 2013 +0100
+++ b/NEWS	Tue Nov 19 10:05:53 2013 +0100
@@ -18,6 +18,14 @@
     even_zero_(nat|int) ~> even_zero
 INCOMPATIBILITY.
 
+* Abolished neg_numeral.
+  * Canonical representation for minus one is "- 1".
+  * Canonical representation for other negative numbers is "- (numeral _)".
+  * When devising rules set for number calculation, consider the
+    following cases: 0, 1, numeral _, - 1, - numeral _.
+  * Syntax for negative numerals is mere input syntax.
+INCOMPATBILITY.
+
 * Elimination of fact duplicates:
     equals_zero_I ~> minus_unique
     diff_eq_0_iff_eq ~> right_minus_eq
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Archimedean_Field.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -204,8 +204,8 @@
 lemma floor_numeral [simp]: "floor (numeral v) = numeral v"
   using floor_of_int [of "numeral v"] by simp
 
-lemma floor_neg_numeral [simp]: "floor (neg_numeral v) = neg_numeral v"
-  using floor_of_int [of "neg_numeral v"] by simp
+lemma floor_neg_numeral [simp]: "floor (- numeral v) = - numeral v"
+  using floor_of_int [of "- numeral v"] by simp
 
 lemma zero_le_floor [simp]: "0 \<le> floor x \<longleftrightarrow> 0 \<le> x"
   by (simp add: le_floor_iff)
@@ -218,7 +218,7 @@
   by (simp add: le_floor_iff)
 
 lemma neg_numeral_le_floor [simp]:
-  "neg_numeral v \<le> floor x \<longleftrightarrow> neg_numeral v \<le> x"
+  "- numeral v \<le> floor x \<longleftrightarrow> - numeral v \<le> x"
   by (simp add: le_floor_iff)
 
 lemma zero_less_floor [simp]: "0 < floor x \<longleftrightarrow> 1 \<le> x"
@@ -232,7 +232,7 @@
   by (simp add: less_floor_iff)
 
 lemma neg_numeral_less_floor [simp]:
-  "neg_numeral v < floor x \<longleftrightarrow> neg_numeral v + 1 \<le> x"
+  "- numeral v < floor x \<longleftrightarrow> - numeral v + 1 \<le> x"
   by (simp add: less_floor_iff)
 
 lemma floor_le_zero [simp]: "floor x \<le> 0 \<longleftrightarrow> x < 1"
@@ -246,7 +246,7 @@
   by (simp add: floor_le_iff)
 
 lemma floor_le_neg_numeral [simp]:
-  "floor x \<le> neg_numeral v \<longleftrightarrow> x < neg_numeral v + 1"
+  "floor x \<le> - numeral v \<longleftrightarrow> x < - numeral v + 1"
   by (simp add: floor_le_iff)
 
 lemma floor_less_zero [simp]: "floor x < 0 \<longleftrightarrow> x < 0"
@@ -260,7 +260,7 @@
   by (simp add: floor_less_iff)
 
 lemma floor_less_neg_numeral [simp]:
-  "floor x < neg_numeral v \<longleftrightarrow> x < neg_numeral v"
+  "floor x < - numeral v \<longleftrightarrow> x < - numeral v"
   by (simp add: floor_less_iff)
 
 text {* Addition and subtraction of integers *}
@@ -272,10 +272,6 @@
     "floor (x + numeral v) = floor x + numeral v"
   using floor_add_of_int [of x "numeral v"] by simp
 
-lemma floor_add_neg_numeral [simp]:
-    "floor (x + neg_numeral v) = floor x + neg_numeral v"
-  using floor_add_of_int [of x "neg_numeral v"] by simp
-
 lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1"
   using floor_add_of_int [of x 1] by simp
 
@@ -286,10 +282,6 @@
   "floor (x - numeral v) = floor x - numeral v"
   using floor_diff_of_int [of x "numeral v"] by simp
 
-lemma floor_diff_neg_numeral [simp]:
-  "floor (x - neg_numeral v) = floor x - neg_numeral v"
-  using floor_diff_of_int [of x "neg_numeral v"] by simp
-
 lemma floor_diff_one [simp]: "floor (x - 1) = floor x - 1"
   using floor_diff_of_int [of x 1] by simp
 
@@ -353,8 +345,8 @@
 lemma ceiling_numeral [simp]: "ceiling (numeral v) = numeral v"
   using ceiling_of_int [of "numeral v"] by simp
 
-lemma ceiling_neg_numeral [simp]: "ceiling (neg_numeral v) = neg_numeral v"
-  using ceiling_of_int [of "neg_numeral v"] by simp
+lemma ceiling_neg_numeral [simp]: "ceiling (- numeral v) = - numeral v"
+  using ceiling_of_int [of "- numeral v"] by simp
 
 lemma ceiling_le_zero [simp]: "ceiling x \<le> 0 \<longleftrightarrow> x \<le> 0"
   by (simp add: ceiling_le_iff)
@@ -367,7 +359,7 @@
   by (simp add: ceiling_le_iff)
 
 lemma ceiling_le_neg_numeral [simp]:
-  "ceiling x \<le> neg_numeral v \<longleftrightarrow> x \<le> neg_numeral v"
+  "ceiling x \<le> - numeral v \<longleftrightarrow> x \<le> - numeral v"
   by (simp add: ceiling_le_iff)
 
 lemma ceiling_less_zero [simp]: "ceiling x < 0 \<longleftrightarrow> x \<le> -1"
@@ -381,7 +373,7 @@
   by (simp add: ceiling_less_iff)
 
 lemma ceiling_less_neg_numeral [simp]:
-  "ceiling x < neg_numeral v \<longleftrightarrow> x \<le> neg_numeral v - 1"
+  "ceiling x < - numeral v \<longleftrightarrow> x \<le> - numeral v - 1"
   by (simp add: ceiling_less_iff)
 
 lemma zero_le_ceiling [simp]: "0 \<le> ceiling x \<longleftrightarrow> -1 < x"
@@ -395,7 +387,7 @@
   by (simp add: le_ceiling_iff)
 
 lemma neg_numeral_le_ceiling [simp]:
-  "neg_numeral v \<le> ceiling x \<longleftrightarrow> neg_numeral v - 1 < x"
+  "- numeral v \<le> ceiling x \<longleftrightarrow> - numeral v - 1 < x"
   by (simp add: le_ceiling_iff)
 
 lemma zero_less_ceiling [simp]: "0 < ceiling x \<longleftrightarrow> 0 < x"
@@ -409,7 +401,7 @@
   by (simp add: less_ceiling_iff)
 
 lemma neg_numeral_less_ceiling [simp]:
-  "neg_numeral v < ceiling x \<longleftrightarrow> neg_numeral v < x"
+  "- numeral v < ceiling x \<longleftrightarrow> - numeral v < x"
   by (simp add: less_ceiling_iff)
 
 text {* Addition and subtraction of integers *}
@@ -421,10 +413,6 @@
     "ceiling (x + numeral v) = ceiling x + numeral v"
   using ceiling_add_of_int [of x "numeral v"] by simp
 
-lemma ceiling_add_neg_numeral [simp]:
-    "ceiling (x + neg_numeral v) = ceiling x + neg_numeral v"
-  using ceiling_add_of_int [of x "neg_numeral v"] by simp
-
 lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1"
   using ceiling_add_of_int [of x 1] by simp
 
@@ -435,10 +423,6 @@
   "ceiling (x - numeral v) = ceiling x - numeral v"
   using ceiling_diff_of_int [of x "numeral v"] by simp
 
-lemma ceiling_diff_neg_numeral [simp]:
-  "ceiling (x - neg_numeral v) = ceiling x - neg_numeral v"
-  using ceiling_diff_of_int [of x "neg_numeral v"] by simp
-
 lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1"
   using ceiling_diff_of_int [of x 1] by simp
 
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/BNF/More_BNFs.thy
--- a/src/HOL/BNF/More_BNFs.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/BNF/More_BNFs.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -973,8 +973,7 @@
   using finite_Collect_mem .
   ultimately have fin: "finite {b. \<exists>a. f a = b \<and> a \<in># M}" by(rule finite_subset)
   have i: "inj_on A ?B" unfolding inj_on_def A_def apply clarsimp
-  by (metis (lifting, mono_tags) mem_Collect_eq rel_simps(54)
-                                 setsum_gt_0_iff setsum_infinite)
+    by (metis (lifting, full_types) mem_Collect_eq neq0_conv setsum.neutral)
   have 0: "\<And> b. 0 < setsum (count M) (A b) \<longleftrightarrow> (\<exists> a \<in> A b. count M a > 0)"
   apply safe
     apply (metis less_not_refl setsum_gt_0_iff setsum_infinite)
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Code_Numeral.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -96,10 +96,6 @@
 qed
 
 lemma [transfer_rule]:
-  "fun_rel HOL.eq pcr_integer (neg_numeral :: num \<Rightarrow> int) (neg_numeral :: num \<Rightarrow> integer)"
-  by (unfold neg_numeral_def [abs_def]) transfer_prover
-
-lemma [transfer_rule]:
   "fun_rel HOL.eq (fun_rel HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
   by (unfold Num.sub_def [abs_def]) transfer_prover
 
@@ -147,10 +143,6 @@
   "int_of_integer (numeral k) = numeral k"
   by transfer rule
 
-lemma int_of_integer_neg_numeral [simp]:
-  "int_of_integer (neg_numeral k) = neg_numeral k"
-  by transfer rule
-
 lemma int_of_integer_sub [simp]:
   "int_of_integer (Num.sub k l) = Num.sub k l"
   by transfer rule
@@ -253,11 +245,11 @@
 
 definition Neg :: "num \<Rightarrow> integer"
 where
-  [simp, code_abbrev]: "Neg = neg_numeral"
+  [simp, code_abbrev]: "Neg n = - Pos n"
 
 lemma [transfer_rule]:
-  "fun_rel HOL.eq pcr_integer neg_numeral Neg"
-  by simp transfer_prover
+  "fun_rel HOL.eq pcr_integer (\<lambda>n. - numeral n) Neg"
+  by (simp add: Neg_def [abs_def]) transfer_prover
 
 code_datatype "0::integer" Pos Neg
 
@@ -272,7 +264,7 @@
   "dup 0 = 0"
   "dup (Pos n) = Pos (Num.Bit0 n)"
   "dup (Neg n) = Neg (Num.Bit0 n)"
-  by (transfer, simp only: neg_numeral_def numeral_Bit0 minus_add_distrib)+
+  by (transfer, simp only: numeral_Bit0 minus_add_distrib)+
 
 lift_definition sub :: "num \<Rightarrow> num \<Rightarrow> integer"
   is "\<lambda>m n. numeral m - numeral n :: int"
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Complex.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -108,7 +108,12 @@
 definition complex_divide_def:
   "x / (y\<Colon>complex) = x * inverse y"
 
-lemma Complex_eq_1 [simp]: "(Complex a b = 1) = (a = 1 \<and> b = 0)"
+lemma Complex_eq_1 [simp]:
+  "Complex a b = 1 \<longleftrightarrow> a = 1 \<and> b = 0"
+  by (simp add: complex_one_def)
+
+lemma Complex_eq_neg_1 [simp]:
+  "Complex a b = - 1 \<longleftrightarrow> a = - 1 \<and> b = 0"
   by (simp add: complex_one_def)
 
 lemma complex_Re_one [simp]: "Re 1 = 1"
@@ -166,21 +171,21 @@
 lemma complex_Re_numeral [simp]: "Re (numeral v) = numeral v"
   using complex_Re_of_int [of "numeral v"] by simp
 
-lemma complex_Re_neg_numeral [simp]: "Re (neg_numeral v) = neg_numeral v"
-  using complex_Re_of_int [of "neg_numeral v"] by simp
+lemma complex_Re_neg_numeral [simp]: "Re (- numeral v) = - numeral v"
+  using complex_Re_of_int [of "- numeral v"] by simp
 
 lemma complex_Im_numeral [simp]: "Im (numeral v) = 0"
   using complex_Im_of_int [of "numeral v"] by simp
 
-lemma complex_Im_neg_numeral [simp]: "Im (neg_numeral v) = 0"
-  using complex_Im_of_int [of "neg_numeral v"] by simp
+lemma complex_Im_neg_numeral [simp]: "Im (- numeral v) = 0"
+  using complex_Im_of_int [of "- numeral v"] by simp
 
 lemma Complex_eq_numeral [simp]:
-  "(Complex a b = numeral w) = (a = numeral w \<and> b = 0)"
+  "Complex a b = numeral w \<longleftrightarrow> a = numeral w \<and> b = 0"
   by (simp add: complex_eq_iff)
 
 lemma Complex_eq_neg_numeral [simp]:
-  "(Complex a b = neg_numeral w) = (a = neg_numeral w \<and> b = 0)"
+  "Complex a b = - numeral w \<longleftrightarrow> a = - numeral w \<and> b = 0"
   by (simp add: complex_eq_iff)
 
 
@@ -421,7 +426,7 @@
 lemma complex_i_not_numeral [simp]: "ii \<noteq> numeral w"
   by (simp add: complex_eq_iff)
 
-lemma complex_i_not_neg_numeral [simp]: "ii \<noteq> neg_numeral w"
+lemma complex_i_not_neg_numeral [simp]: "ii \<noteq> - numeral w"
   by (simp add: complex_eq_iff)
 
 lemma i_mult_Complex [simp]: "ii * Complex a b = Complex (- b) a"
@@ -508,7 +513,7 @@
 lemma complex_cnj_numeral [simp]: "cnj (numeral w) = numeral w"
   by (simp add: complex_eq_iff)
 
-lemma complex_cnj_neg_numeral [simp]: "cnj (neg_numeral w) = neg_numeral w"
+lemma complex_cnj_neg_numeral [simp]: "cnj (- numeral w) = - numeral w"
   by (simp add: complex_eq_iff)
 
 lemma complex_cnj_scaleR: "cnj (scaleR r x) = scaleR r (cnj x)"
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -11,8 +11,10 @@
   "~~/src/HOL/Library/Code_Target_Numeral"
 begin
 
-declare powr_numeral[simp]
-declare powr_neg_numeral[simp]
+declare powr_one [simp]
+declare powr_numeral [simp]
+declare powr_neg_one [simp]
+declare powr_neg_numeral [simp]
 
 section "Horner Scheme"
 
@@ -1261,8 +1263,8 @@
         unfolding cos_periodic_int ..
       also have "\<dots> \<le> cos ((?ux - 2 * ?lpi))"
         using cos_monotone_minus_pi_0'[OF pi_x x_le_ux ux_0]
-        by (simp only: minus_float.rep_eq real_of_int_minus real_of_one minus_one[symmetric]
-            mult_minus_left mult_1_left) simp
+        by (simp only: minus_float.rep_eq real_of_int_minus real_of_one
+          mult_minus_left mult_1_left) simp
       also have "\<dots> = cos ((- (?ux - 2 * ?lpi)))"
         unfolding uminus_float.rep_eq cos_minus ..
       also have "\<dots> \<le> (ub_cos prec (- (?ux - 2 * ?lpi)))"
@@ -1306,7 +1308,7 @@
       also have "\<dots> \<le> cos ((?lx + 2 * ?lpi))"
         using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
         by (simp only: minus_float.rep_eq real_of_int_minus real_of_one
-          minus_one[symmetric] mult_minus_left mult_1_left) simp
+          mult_minus_left mult_1_left) simp
       also have "\<dots> \<le> (ub_cos prec (?lx + 2 * ?lpi))"
         using lb_cos[OF lx_0 pi_lx] by simp
       finally show ?thesis unfolding u by (simp add: real_of_float_max)
@@ -2104,8 +2106,9 @@
 lemma interpret_floatarith_num:
   shows "interpret_floatarith (Num (Float 0 0)) vs = 0"
   and "interpret_floatarith (Num (Float 1 0)) vs = 1"
+  and "interpret_floatarith (Num (Float (- 1) 0)) vs = - 1"
   and "interpret_floatarith (Num (Float (numeral a) 0)) vs = numeral a"
-  and "interpret_floatarith (Num (Float (neg_numeral a) 0)) vs = neg_numeral a" by auto
+  and "interpret_floatarith (Num (Float (- numeral a) 0)) vs = - numeral a" by auto
 
 subsection "Implement approximation function"
 
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -2006,9 +2006,10 @@
       | SOME n => @{code Bound} (@{code nat_of_integer} n))
   | num_of_term vs @{term "0::int"} = @{code C} (@{code int_of_integer} 0)
   | num_of_term vs @{term "1::int"} = @{code C} (@{code int_of_integer} 1)
+  | num_of_term vs @{term "- 1::int"} = @{code C} (@{code int_of_integer} (~ 1))
   | num_of_term vs (@{term "numeral :: _ \<Rightarrow> int"} $ t) =
       @{code C} (@{code int_of_integer} (HOLogic.dest_num t))
-  | num_of_term vs (@{term "neg_numeral :: _ \<Rightarrow> int"} $ t) =
+  | num_of_term vs (@{term "- numeral :: _ \<Rightarrow> int"} $ t) =
       @{code C} (@{code int_of_integer} (~(HOLogic.dest_num t)))
   | num_of_term vs (Bound i) = @{code Bound} (@{code nat_of_integer} i)
   | num_of_term vs (@{term "uminus :: int \<Rightarrow> int"} $ t') = @{code Neg} (num_of_term vs t')
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -3154,7 +3154,7 @@
     hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = (- ?N i e + real j1) - 1"
       by (simp only: algebra_simps)
         hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = - 1 - ?N i e + real j1"
-          by (simp add: algebra_simps minus_one [symmetric] del: minus_one)
+          by (simp add: algebra_simps)
     with nob  have ?case by blast }
   ultimately show ?case by blast
 next
@@ -5549,6 +5549,7 @@
   | num_of_term vs @{term "real (1::int)"} = mk_C 1
   | num_of_term vs @{term "0::real"} = mk_C 0
   | num_of_term vs @{term "1::real"} = mk_C 1
+  | num_of_term vs @{term "- 1::real"} = mk_C (~ 1)
   | num_of_term vs (Bound i) = mk_Bound i
   | num_of_term vs (@{term "uminus :: real \<Rightarrow> real"} $ t') = @{code Neg} (num_of_term vs t')
   | num_of_term vs (@{term "op + :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
@@ -5561,7 +5562,7 @@
         | _ => error "num_of_term: unsupported Multiplication")
   | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "numeral :: _ \<Rightarrow> int"} $ t')) =
       mk_C (HOLogic.dest_num t')
-  | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "neg_numeral :: _ \<Rightarrow> int"} $ t')) =
+  | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "- numeral :: _ \<Rightarrow> int"} $ t')) =
       mk_C (~ (HOLogic.dest_num t'))
   | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "floor :: real \<Rightarrow> int"} $ t')) =
       @{code Floor} (num_of_term vs t')
@@ -5569,7 +5570,7 @@
       @{code Neg} (@{code Floor} (@{code Neg} (num_of_term vs t')))
   | num_of_term vs (@{term "numeral :: _ \<Rightarrow> real"} $ t') =
       mk_C (HOLogic.dest_num t')
-  | num_of_term vs (@{term "neg_numeral :: _ \<Rightarrow> real"} $ t') =
+  | num_of_term vs (@{term "- numeral :: _ \<Rightarrow> real"} $ t') =
       mk_C (~ (HOLogic.dest_num t'))
   | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t);
 
@@ -5583,7 +5584,7 @@
       @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) 
   | fm_of_term vs (@{term "op rdvd"} $ (@{term "real :: int \<Rightarrow> real"} $ (@{term "numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
       mk_Dvd (HOLogic.dest_num t1, num_of_term vs t2)
-  | fm_of_term vs (@{term "op rdvd"} $ (@{term "real :: int \<Rightarrow> real"} $ (@{term "neg_numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
+  | fm_of_term vs (@{term "op rdvd"} $ (@{term "real :: int \<Rightarrow> real"} $ (@{term "- numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
       mk_Dvd (~ (HOLogic.dest_num t1), num_of_term vs t2)
   | fm_of_term vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
       @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -1256,12 +1256,10 @@
   apply (case_tac n', simp, simp)
   apply (case_tac n, simp, simp)
   apply (case_tac n, case_tac n', simp add: Let_def)
-  apply (case_tac "pa +\<^sub>p p' = 0\<^sub>p")
-  apply (auto simp add: polyadd_eq_const_degree)
+  apply (auto simp add: polyadd_eq_const_degree)[2]
   apply (metis head_nz)
   apply (metis head_nz)
   apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq)
-  apply (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans)
   done
 
 lemma polymul_head_polyeq:
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Divides.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -1919,10 +1919,9 @@
   val zero = @{term "0 :: int"}
   val less = @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"}
   val le = @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"}
-  val simps = @{thms arith_simps} @ @{thms rel_simps} @
-    map (fn th => th RS sym) [@{thm numeral_1_eq_1}]
-  fun prove ctxt goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
-    (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps))));
+  val simps = @{thms arith_simps} @ @{thms rel_simps} @ [@{thm numeral_1_eq_1 [symmetric]}]
+  fun prove ctxt goal = (writeln "prove"; Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
+    (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps)))));
   fun binary_proc proc ctxt ct =
     (case Thm.term_of ct of
       _ $ t $ u =>
@@ -1945,23 +1944,23 @@
 
 simproc_setup binary_int_div
   ("numeral m div numeral n :: int" |
-   "numeral m div neg_numeral n :: int" |
-   "neg_numeral m div numeral n :: int" |
-   "neg_numeral m div neg_numeral n :: int") =
+   "numeral m div - numeral n :: int" |
+   "- numeral m div numeral n :: int" |
+   "- numeral m div - numeral n :: int") =
   {* K (divmod_proc @{thm int_div_pos_eq} @{thm int_div_neg_eq}) *}
 
 simproc_setup binary_int_mod
   ("numeral m mod numeral n :: int" |
-   "numeral m mod neg_numeral n :: int" |
-   "neg_numeral m mod numeral n :: int" |
-   "neg_numeral m mod neg_numeral n :: int") =
+   "numeral m mod - numeral n :: int" |
+   "- numeral m mod numeral n :: int" |
+   "- numeral m mod - numeral n :: int") =
   {* K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq}) *}
 
 lemmas posDivAlg_eqn_numeral [simp] =
     posDivAlg_eqn [of "numeral v" "numeral w", OF zero_less_numeral] for v w
 
 lemmas negDivAlg_eqn_numeral [simp] =
-    negDivAlg_eqn [of "numeral v" "neg_numeral w", OF zero_less_numeral] for v w
+    negDivAlg_eqn [of "numeral v" "- numeral w", OF zero_less_numeral] for v w
 
 
 text{*Special-case simplification *}
@@ -1973,14 +1972,14 @@
   div_pos_pos [OF zero_less_one, of "numeral w", OF zero_le_numeral] for w
 
 lemmas div_pos_neg_1_numeral [simp] =
-  div_pos_neg [OF zero_less_one, of "neg_numeral w",
+  div_pos_neg [OF zero_less_one, of "- numeral w",
   OF neg_numeral_less_zero] for w
 
 lemmas mod_pos_pos_1_numeral [simp] =
   mod_pos_pos [OF zero_less_one, of "numeral w", OF zero_le_numeral] for w
 
 lemmas mod_pos_neg_1_numeral [simp] =
-  mod_pos_neg [OF zero_less_one, of "neg_numeral w",
+  mod_pos_neg [OF zero_less_one, of "- numeral w",
   OF neg_numeral_less_zero] for w
 
 lemmas posDivAlg_eqn_1_numeral [simp] =
@@ -2290,6 +2289,8 @@
   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
   using assms unfolding divmod_int_rel_def by auto
 
+declaration {* K (Lin_Arith.add_simps @{thms uminus_numeral_One}) *}
+
 lemma neg_divmod_int_rel_mult_2:
   assumes "b \<le> 0"
   assumes "divmod_int_rel (a + 1) b (q, r)"
@@ -2427,13 +2428,13 @@
 
 lemma dvd_neg_numeral_left [simp]:
   fixes y :: "'a::comm_ring_1"
-  shows "(neg_numeral k) dvd y \<longleftrightarrow> (numeral k) dvd y"
-  unfolding neg_numeral_def minus_dvd_iff ..
+  shows "(- numeral k) dvd y \<longleftrightarrow> (numeral k) dvd y"
+  by (fact minus_dvd_iff)
 
 lemma dvd_neg_numeral_right [simp]:
   fixes x :: "'a::comm_ring_1"
-  shows "x dvd (neg_numeral k) \<longleftrightarrow> x dvd (numeral k)"
-  unfolding neg_numeral_def dvd_minus_iff ..
+  shows "x dvd (- numeral k) \<longleftrightarrow> x dvd (numeral k)"
+  by (fact dvd_minus_iff)
 
 lemmas dvd_eq_mod_eq_0_numeral [simp] =
   dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/GCD.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -134,6 +134,14 @@
 lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
   by (simp add: gcd_int_def)
 
+lemma gcd_neg_numeral_1_int [simp]:
+  "gcd (- numeral n :: int) x = gcd (numeral n) x"
+  by (fact gcd_neg1_int)
+
+lemma gcd_neg_numeral_2_int [simp]:
+  "gcd x (- numeral n :: int) = gcd x (numeral n)"
+  by (fact gcd_neg2_int)
+
 lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"
 by(simp add: gcd_int_def)
 
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/IMP/Hoare_Examples.thy
--- a/src/HOL/IMP/Hoare_Examples.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/IMP/Hoare_Examples.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -2,17 +2,6 @@
 
 theory Hoare_Examples imports Hoare begin
 
-text{* Improves proof automation for negative numerals: *}
-
-lemma add_neg1R[simp]:
-  "x + -1 = x - (1 :: int)"
-by arith
-
-lemma add_neg_numeralR[simp]:
-  "x + neg_numeral n = (x::'a::neg_numeral) - numeral(n)"
-by (simp only: diff_minus_eq_add[symmetric] minus_neg_numeral)
-
-
 text{* Summing up the first @{text x} natural numbers in variable @{text y}. *}
 
 fun sum :: "int \<Rightarrow> int" where
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Int.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -232,9 +232,8 @@
 lemma of_int_numeral [simp, code_post]: "of_int (numeral k) = numeral k"
   by (simp add: of_nat_numeral [symmetric] of_int_of_nat_eq [symmetric])
 
-lemma of_int_neg_numeral [simp, code_post]: "of_int (neg_numeral k) = neg_numeral k"
-  unfolding neg_numeral_def neg_numeral_class.neg_numeral_def
-  by (simp only: of_int_minus of_int_numeral)
+lemma of_int_neg_numeral [code_post]: "of_int (- numeral k) = - numeral k"
+  by simp
 
 lemma of_int_power:
   "of_int (z ^ n) = of_int z ^ n"
@@ -370,7 +369,7 @@
   by (simp add: nat_eq_iff)
 
 lemma nat_neg_numeral [simp]:
-  "nat (neg_numeral k) = 0"
+  "nat (- numeral k) = 0"
   by simp
 
 lemma nat_2: "nat 2 = Suc (Suc 0)"
@@ -511,13 +510,13 @@
 
 lemma nonneg_int_cases:
   assumes "0 \<le> k" obtains n where "k = int n"
-  using assms by (cases k, simp, simp del: of_nat_Suc)
+  using assms by (rule nonneg_eq_int)
 
 lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
   -- {* Unfold all @{text let}s involving constants *}
   unfolding Let_def ..
 
-lemma Let_neg_numeral [simp]: "Let (neg_numeral v) f = f (neg_numeral v)"
+lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
   -- {* Unfold all @{text let}s involving constants *}
   unfolding Let_def ..
 
@@ -525,15 +524,15 @@
 
 lemmas max_number_of [simp] =
   max_def [of "numeral u" "numeral v"]
-  max_def [of "numeral u" "neg_numeral v"]
-  max_def [of "neg_numeral u" "numeral v"]
-  max_def [of "neg_numeral u" "neg_numeral v"] for u v
+  max_def [of "numeral u" "- numeral v"]
+  max_def [of "- numeral u" "numeral v"]
+  max_def [of "- numeral u" "- numeral v"] for u v
 
 lemmas min_number_of [simp] =
   min_def [of "numeral u" "numeral v"]
-  min_def [of "numeral u" "neg_numeral v"]
-  min_def [of "neg_numeral u" "numeral v"]
-  min_def [of "neg_numeral u" "neg_numeral v"] for u v
+  min_def [of "numeral u" "- numeral v"]
+  min_def [of "- numeral u" "numeral v"]
+  min_def [of "- numeral u" "- numeral v"] for u v
 
 
 subsubsection {* Binary comparisons *}
@@ -1070,8 +1069,6 @@
     by auto
 qed
 
-ML_val {* @{const_name neg_numeral} *}
-
 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
 by (insert abs_zmult_eq_1 [of m n], arith)
 
@@ -1127,62 +1124,30 @@
   inverse_eq_divide [of "numeral w"] for w
 
 lemmas inverse_eq_divide_neg_numeral [simp] =
-  inverse_eq_divide [of "neg_numeral w"] for w
+  inverse_eq_divide [of "- numeral w"] for w
 
 text {*These laws simplify inequalities, moving unary minus from a term
 into the literal.*}
 
-lemmas le_minus_iff_numeral [simp, no_atp] =
-  le_minus_iff [of "numeral v"]
-  le_minus_iff [of "neg_numeral v"] for v
-
-lemmas equation_minus_iff_numeral [simp, no_atp] =
-  equation_minus_iff [of "numeral v"]
-  equation_minus_iff [of "neg_numeral v"] for v
+lemmas equation_minus_iff_numeral [no_atp] =
+  equation_minus_iff [of "numeral v"] for v
 
-lemmas minus_less_iff_numeral [simp, no_atp] =
-  minus_less_iff [of _ "numeral v"]
-  minus_less_iff [of _ "neg_numeral v"] for v
+lemmas minus_equation_iff_numeral [no_atp] =
+  minus_equation_iff [of _ "numeral v"] for v
 
-lemmas minus_le_iff_numeral [simp, no_atp] =
-  minus_le_iff [of _ "numeral v"]
-  minus_le_iff [of _ "neg_numeral v"] for v
-
-lemmas minus_equation_iff_numeral [simp, no_atp] =
-  minus_equation_iff [of _ "numeral v"]
-  minus_equation_iff [of _ "neg_numeral v"] for v
-
-text{*To Simplify Inequalities Where One Side is the Constant 1*}
+lemmas le_minus_iff_numeral [no_atp] =
+  le_minus_iff [of "numeral v"] for v
 
-lemma less_minus_iff_1 [simp]:
-  fixes b::"'b::linordered_idom"
-  shows "(1 < - b) = (b < -1)"
-by auto
-
-lemma le_minus_iff_1 [simp]:
-  fixes b::"'b::linordered_idom"
-  shows "(1 \<le> - b) = (b \<le> -1)"
-by auto
-
-lemma equation_minus_iff_1 [simp]:
-  fixes b::"'b::ring_1"
-  shows "(1 = - b) = (b = -1)"
-by (subst equation_minus_iff, auto)
+lemmas minus_le_iff_numeral [no_atp] =
+  minus_le_iff [of _ "numeral v"] for v
 
-lemma minus_less_iff_1 [simp]:
-  fixes a::"'b::linordered_idom"
-  shows "(- a < 1) = (-1 < a)"
-by auto
+lemmas less_minus_iff_numeral [no_atp] =
+  less_minus_iff [of "numeral v"] for v
 
-lemma minus_le_iff_1 [simp]:
-  fixes a::"'b::linordered_idom"
-  shows "(- a \<le> 1) = (-1 \<le> a)"
-by auto
+lemmas minus_less_iff_numeral [no_atp] =
+  minus_less_iff [of _ "numeral v"] for v
 
-lemma minus_equation_iff_1 [simp]:
-  fixes a::"'b::ring_1"
-  shows "(- a = 1) = (a = -1)"
-by (subst minus_equation_iff, auto)
+-- {* FIXME maybe simproc *}
 
 
 text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
@@ -1197,27 +1162,28 @@
 
 lemmas le_divide_eq_numeral1 [simp] =
   pos_le_divide_eq [of "numeral w", OF zero_less_numeral]
-  neg_le_divide_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
+  neg_le_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
 
 lemmas divide_le_eq_numeral1 [simp] =
   pos_divide_le_eq [of "numeral w", OF zero_less_numeral]
-  neg_divide_le_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
+  neg_divide_le_eq [of "- numeral w", OF neg_numeral_less_zero] for w
 
 lemmas less_divide_eq_numeral1 [simp] =
   pos_less_divide_eq [of "numeral w", OF zero_less_numeral]
-  neg_less_divide_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
+  neg_less_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
 
 lemmas divide_less_eq_numeral1 [simp] =
   pos_divide_less_eq [of "numeral w", OF zero_less_numeral]
-  neg_divide_less_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
+  neg_divide_less_eq [of "- numeral w", OF neg_numeral_less_zero] for w
 
 lemmas eq_divide_eq_numeral1 [simp] =
   eq_divide_eq [of _ _ "numeral w"]
-  eq_divide_eq [of _ _ "neg_numeral w"] for w
+  eq_divide_eq [of _ _ "- numeral w"] for w
 
 lemmas divide_eq_eq_numeral1 [simp] =
   divide_eq_eq [of _ "numeral w"]
-  divide_eq_eq [of _ "neg_numeral w"] for w
+  divide_eq_eq [of _ "- numeral w"] for w
+
 
 subsubsection{*Optional Simplification Rules Involving Constants*}
 
@@ -1225,27 +1191,27 @@
 
 lemmas le_divide_eq_numeral =
   le_divide_eq [of "numeral w"]
-  le_divide_eq [of "neg_numeral w"] for w
+  le_divide_eq [of "- numeral w"] for w
 
 lemmas divide_le_eq_numeral =
   divide_le_eq [of _ _ "numeral w"]
-  divide_le_eq [of _ _ "neg_numeral w"] for w
+  divide_le_eq [of _ _ "- numeral w"] for w
 
 lemmas less_divide_eq_numeral =
   less_divide_eq [of "numeral w"]
-  less_divide_eq [of "neg_numeral w"] for w
+  less_divide_eq [of "- numeral w"] for w
 
 lemmas divide_less_eq_numeral =
   divide_less_eq [of _ _ "numeral w"]
-  divide_less_eq [of _ _ "neg_numeral w"] for w
+  divide_less_eq [of _ _ "- numeral w"] for w
 
 lemmas eq_divide_eq_numeral =
   eq_divide_eq [of "numeral w"]
-  eq_divide_eq [of "neg_numeral w"] for w
+  eq_divide_eq [of "- numeral w"] for w
 
 lemmas divide_eq_eq_numeral =
   divide_eq_eq [of _ _ "numeral w"]
-  divide_eq_eq [of _ _ "neg_numeral w"] for w
+  divide_eq_eq [of _ _ "- numeral w"] for w
 
 
 text{*Not good as automatic simprules because they cause case splits.*}
@@ -1257,21 +1223,20 @@
 text{*Division By @{text "-1"}*}
 
 lemma divide_minus1 [simp]: "(x::'a::field) / -1 = - x"
-  unfolding minus_one [symmetric]
   unfolding nonzero_minus_divide_right [OF one_neq_zero, symmetric]
   by simp
 
 lemma minus1_divide [simp]: "-1 / (x::'a::field) = - (1 / x)"
-  unfolding minus_one [symmetric] by (rule divide_minus_left)
+  by (fact divide_minus_left)
 
 lemma half_gt_zero_iff:
-     "(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))"
-by auto
+  "(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))"
+  by auto
 
 lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2]
 
 lemma divide_Numeral1: "(x::'a::field) / Numeral1 = x"
-  by simp
+  by (fact divide_numeral_1)
 
 
 subsection {* The divides relation *}
@@ -1475,7 +1440,7 @@
   [simp, code_abbrev]: "Pos = numeral"
 
 definition Neg :: "num \<Rightarrow> int" where
-  [simp, code_abbrev]: "Neg = neg_numeral"
+  [simp, code_abbrev]: "Neg n = - (Pos n)"
 
 code_datatype "0::int" Pos Neg
 
@@ -1489,7 +1454,7 @@
   "dup 0 = 0"
   "dup (Pos n) = Pos (Num.Bit0 n)"
   "dup (Neg n) = Neg (Num.Bit0 n)"
-  unfolding Pos_def Neg_def neg_numeral_def
+  unfolding Pos_def Neg_def
   by (simp_all add: numeral_Bit0)
 
 definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
@@ -1505,12 +1470,10 @@
   "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
   "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
   "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
-  apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def
-    neg_numeral_def numeral_BitM)
+  apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM)
   apply (simp_all only: algebra_simps minus_diff_eq)
   apply (simp_all only: add.commute [of _ "- (numeral n + numeral n)"])
   apply (simp_all only: minus_add add.assoc left_minus)
-  apply (simp_all only: algebra_simps right_minus)
   done
 
 text {* Implementations *}
@@ -1606,10 +1569,10 @@
   "nat (Int.Neg k) = 0"
   "nat 0 = 0"
   "nat (Int.Pos k) = nat_of_num k"
-  by (simp_all add: nat_of_num_numeral nat_numeral)
+  by (simp_all add: nat_of_num_numeral)
 
 lemma (in ring_1) of_int_code [code]:
-  "of_int (Int.Neg k) = neg_numeral k"
+  "of_int (Int.Neg k) = - numeral k"
   "of_int 0 = 0"
   "of_int (Int.Pos k) = numeral k"
   by simp_all
@@ -1653,7 +1616,7 @@
 
 lemma int_power:
   "int (m ^ n) = int m ^ n"
-  by (rule of_nat_power)
+  by (fact of_nat_power)
 
 lemmas zpower_int = int_power [symmetric]
 
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Binomial.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -370,7 +370,7 @@
     by auto
   from False show ?thesis
     by (simp add: pochhammer_def gbinomial_def field_simps
-      eq setprod_timesf[symmetric] del: minus_one)
+      eq setprod_timesf[symmetric])
 qed
 
 lemma binomial_fact_lemma: "k \<le> n \<Longrightarrow> fact k * fact (n - k) * (n choose k) = fact n"
@@ -441,9 +441,9 @@
     from eq[symmetric]
     have ?thesis using kn
       apply (simp add: binomial_fact[OF kn, where ?'a = 'a]
-        gbinomial_pochhammer field_simps pochhammer_Suc_setprod del: minus_one)
+        gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
       apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h
-        of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc del: minus_one)
+        of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
       unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
       unfolding mult_assoc[symmetric]
       unfolding setprod_timesf[symmetric]
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Library/Bit.thy
--- a/src/HOL/Library/Bit.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Bit.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -147,11 +147,11 @@
 
 text {* All numerals reduce to either 0 or 1. *}
 
-lemma bit_minus1 [simp]: "-1 = (1 :: bit)"
-  by (simp only: minus_one [symmetric] uminus_bit_def)
+lemma bit_minus1 [simp]: "- 1 = (1 :: bit)"
+  by (simp only: uminus_bit_def)
 
-lemma bit_neg_numeral [simp]: "(neg_numeral w :: bit) = numeral w"
-  by (simp only: neg_numeral_def uminus_bit_def)
+lemma bit_neg_numeral [simp]: "(- numeral w :: bit) = numeral w"
+  by (simp only: uminus_bit_def)
 
 lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
   by (simp only: numeral_Bit0 bit_add_self)
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Library/Code_Prolog.thy
--- a/src/HOL/Library/Code_Prolog.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Code_Prolog.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -12,10 +12,8 @@
 
 section {* Setup for Numerals *}
 
-setup {* Predicate_Compile_Data.ignore_consts
-  [@{const_name numeral}, @{const_name neg_numeral}] *}
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}] *}
 
-setup {* Predicate_Compile_Data.keep_functions
-  [@{const_name numeral}, @{const_name neg_numeral}] *}
+setup {* Predicate_Compile_Data.keep_functions [@{const_name numeral}] *}
 
 end
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Library/Code_Real_Approx_By_Float.thy
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -169,7 +169,7 @@
   by simp
 
 lemma [code_unfold del]:
-  "neg_numeral k \<equiv> (of_rat (neg_numeral k) :: real)"
+  "- numeral k \<equiv> (of_rat (- numeral k) :: real)"
   by simp
 
 hide_const (open) real_of_int
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Library/Code_Target_Int.thy
--- a/src/HOL/Library/Code_Target_Int.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Code_Target_Int.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -30,7 +30,7 @@
   by transfer simp
 
 lemma [code_abbrev]:
-  "int_of_integer (neg_numeral k) = Int.Neg k"
+  "int_of_integer (- numeral k) = Int.Neg k"
   by transfer simp
   
 lemma [code, symmetric, code_post]:
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Library/Extended.thy
--- a/src/HOL/Library/Extended.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Extended.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -161,8 +161,8 @@
   apply (simp only: numeral_inc one_extended_def plus_extended.simps(1)[symmetric])
   done
 
-lemma Fin_neg_numeral: "Fin(neg_numeral w) = - numeral w"
-by (simp only: Fin_numeral minus_numeral[symmetric] uminus_extended.simps[symmetric])
+lemma Fin_neg_numeral: "Fin (- numeral w) = - numeral w"
+by (simp only: Fin_numeral uminus_extended.simps[symmetric])
 
 
 instantiation extended :: (lattice)bounded_lattice
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Float.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -45,7 +45,7 @@
 lemma zero_float[simp]: "0 \<in> float" by (auto simp: float_def)
 lemma one_float[simp]: "1 \<in> float" by (intro floatI[of 1 0]) simp
 lemma numeral_float[simp]: "numeral i \<in> float" by (intro floatI[of "numeral i" 0]) simp
-lemma neg_numeral_float[simp]: "neg_numeral i \<in> float" by (intro floatI[of "neg_numeral i" 0]) simp
+lemma neg_numeral_float[simp]: "- numeral i \<in> float" by (intro floatI[of "- numeral i" 0]) simp
 lemma real_of_int_float[simp]: "real (x :: int) \<in> float" by (intro floatI[of x 0]) simp
 lemma real_of_nat_float[simp]: "real (x :: nat) \<in> float" by (intro floatI[of x 0]) simp
 lemma two_powr_int_float[simp]: "2 powr (real (i::int)) \<in> float" by (intro floatI[of 1 i]) simp
@@ -53,7 +53,7 @@
 lemma two_powr_minus_int_float[simp]: "2 powr - (real (i::int)) \<in> float" by (intro floatI[of 1 "-i"]) simp
 lemma two_powr_minus_nat_float[simp]: "2 powr - (real (i::nat)) \<in> float" by (intro floatI[of 1 "-i"]) simp
 lemma two_powr_numeral_float[simp]: "2 powr numeral i \<in> float" by (intro floatI[of 1 "numeral i"]) simp
-lemma two_powr_neg_numeral_float[simp]: "2 powr neg_numeral i \<in> float" by (intro floatI[of 1 "neg_numeral i"]) simp
+lemma two_powr_neg_numeral_float[simp]: "2 powr - numeral i \<in> float" by (intro floatI[of 1 "- numeral i"]) simp
 lemma two_pow_float[simp]: "2 ^ n \<in> float" by (intro floatI[of 1 "n"]) (simp add: powr_realpow)
 lemma real_of_float_float[simp]: "real (f::float) \<in> float" by (cases f) simp
 
@@ -121,11 +121,11 @@
 qed
 
 lemma div_neg_numeral_Bit0_float[simp]:
-  assumes x: "x / numeral n \<in> float" shows "x / (neg_numeral (Num.Bit0 n)) \<in> float"
+  assumes x: "x / numeral n \<in> float" shows "x / (- numeral (Num.Bit0 n)) \<in> float"
 proof -
   have "- (x / numeral (Num.Bit0 n)) \<in> float" using x by simp
-  also have "- (x / numeral (Num.Bit0 n)) = x / neg_numeral (Num.Bit0 n)"
-    unfolding neg_numeral_def by (simp del: minus_numeral)
+  also have "- (x / numeral (Num.Bit0 n)) = x / - numeral (Num.Bit0 n)"
+    by simp
   finally show ?thesis .
 qed
 
@@ -197,7 +197,7 @@
   then show "\<exists>c. a < c \<and> c < b"
     apply (intro exI[of _ "(a + b) * Float 1 -1"])
     apply transfer
-    apply (simp add: powr_neg_numeral)
+    apply (simp add: powr_minus)
     done
 qed
 
@@ -226,16 +226,16 @@
   "fun_rel (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
   unfolding fun_rel_def float.pcr_cr_eq  cr_float_def by simp
 
-lemma float_neg_numeral[simp]: "real (neg_numeral x :: float) = neg_numeral x"
-  by (simp add: minus_numeral[symmetric] del: minus_numeral)
+lemma float_neg_numeral[simp]: "real (- numeral x :: float) = - numeral x"
+  by simp
 
 lemma transfer_neg_numeral [transfer_rule]:
-  "fun_rel (op =) pcr_float (neg_numeral :: _ \<Rightarrow> real) (neg_numeral :: _ \<Rightarrow> float)"
+  "fun_rel (op =) pcr_float (- numeral :: _ \<Rightarrow> real) (- numeral :: _ \<Rightarrow> float)"
   unfolding fun_rel_def float.pcr_cr_eq cr_float_def by simp
 
 lemma
   shows float_of_numeral[simp]: "numeral k = float_of (numeral k)"
-    and float_of_neg_numeral[simp]: "neg_numeral k = float_of (neg_numeral k)"
+    and float_of_neg_numeral[simp]: "- numeral k = float_of (- numeral k)"
   unfolding real_of_float_eq by simp_all
 
 subsection {* Represent floats as unique mantissa and exponent *}
@@ -439,7 +439,7 @@
   by transfer simp
 hide_fact (open) compute_float_numeral
 
-lemma compute_float_neg_numeral[code_abbrev]: "Float (neg_numeral k) 0 = neg_numeral k"
+lemma compute_float_neg_numeral[code_abbrev]: "Float (- numeral k) 0 = - numeral k"
   by transfer simp
 hide_fact (open) compute_float_neg_numeral
 
@@ -960,7 +960,7 @@
   also have "... < (1 / 2) * 2 powr real (rat_precision n (int x) (int y))"
     apply (rule mult_strict_right_mono) by (insert assms) auto
   also have "\<dots> = 2 powr real (rat_precision n (int x) (int y) - 1)"
-    using powr_add [of 2 _ "- 1", simplified add_uminus_conv_diff] by (simp add: powr_neg_numeral)
+    using powr_add [of 2 _ "- 1", simplified add_uminus_conv_diff] by (simp add: powr_minus)
   also have "\<dots> = 2 ^ nat (rat_precision n (int x) (int y) - 1)"
     using rat_precision_pos[of x y n] assms by (simp add: powr_realpow[symmetric])
   also have "\<dots> \<le> 2 ^ nat (rat_precision n (int x) (int y)) - 1"
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -384,8 +384,8 @@
   by (induct k) (simp_all only: numeral.simps fps_const_1_eq_1
     fps_const_add [symmetric])
 
-lemma neg_numeral_fps_const: "neg_numeral k = fps_const (neg_numeral k)"
-  by (simp only: neg_numeral_def numeral_fps_const fps_const_neg)
+lemma neg_numeral_fps_const: "- numeral k = fps_const (- numeral k)"
+  by (simp only: numeral_fps_const fps_const_neg)
 
 subsection{* The eXtractor series X*}
 
@@ -1202,7 +1202,7 @@
   have eq: "(1 + X) * ?r = 1"
     unfolding minus_one_power_iff
     by (auto simp add: field_simps fps_eq_iff)
-  show ?thesis by (auto simp add: eq intro: fps_inverse_unique simp del: minus_one)
+  show ?thesis by (auto simp add: eq intro: fps_inverse_unique)
 qed
 
 
@@ -1245,7 +1245,7 @@
 lemma numeral_compose[simp]: "(numeral k::('a::{comm_ring_1}) fps) oo b = numeral k"
   unfolding numeral_fps_const by simp
 
-lemma neg_numeral_compose[simp]: "(neg_numeral k::('a::{comm_ring_1}) fps) oo b = neg_numeral k"
+lemma neg_numeral_compose[simp]: "(- numeral k::('a::{comm_ring_1}) fps) oo b = - numeral k"
   unfolding neg_numeral_fps_const by simp
 
 lemma X_fps_compose_startby0[simp]: "a$0 = 0 \<Longrightarrow> X oo a = (a :: ('a :: comm_ring_1) fps)"
@@ -2363,7 +2363,7 @@
       next
         case (Suc n1)
         have "?i $ n = setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} + fps_inv a $ Suc n1 * (a $ 1)^ Suc n1"
-          by (simp add: fps_compose_nth Suc startsby_zero_power_nth_same[OF a0] del: power_Suc)
+          by (simp only: fps_compose_nth) (simp add: Suc startsby_zero_power_nth_same [OF a0] del: power_Suc)
         also have "\<dots> = setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} +
           (X$ Suc n1 - setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1})"
           using a0 a1 Suc by (simp add: fps_inv_def)
@@ -2404,7 +2404,7 @@
       next
         case (Suc n1)
         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"
-          by (simp add: fps_compose_nth Suc startsby_zero_power_nth_same[OF a0] del: power_Suc)
+          by (simp only: fps_compose_nth) (simp add: Suc startsby_zero_power_nth_same [OF a0] del: power_Suc)
         also have "\<dots> = setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1} +
           (b$ Suc n1 - setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1})"
           using a0 a1 Suc by (simp add: fps_ginv_def)
@@ -2564,9 +2564,9 @@
 
 
 lemma fps_compose_mult_distrib:
-  assumes c0: "c$0 = (0::'a::idom)"
-  shows "(a * b) oo c = (a oo c) * (b oo c)" (is "?l = ?r")
-  apply (simp add: fps_eq_iff fps_compose_mult_distrib_lemma[OF c0])
+  assumes c0: "c $ 0 = (0::'a::idom)"
+  shows "(a * b) oo c = (a oo c) * (b oo c)"
+  apply (simp add: fps_eq_iff fps_compose_mult_distrib_lemma [OF c0])
   apply (simp add: fps_compose_nth fps_mult_nth setsum_left_distrib)
   done
 
@@ -2941,7 +2941,7 @@
   (is "inverse ?l = ?r")
 proof -
   have th: "?l * ?r = 1"
-    by (auto simp add: field_simps fps_eq_iff minus_one_power_iff simp del: minus_one)
+    by (auto simp add: field_simps fps_eq_iff minus_one_power_iff)
   have th': "?l $ 0 \<noteq> 0" by (simp add: )
   from fps_inverse_unique[OF th' th] show ?thesis .
 qed
@@ -3165,7 +3165,7 @@
   have th: "?r$0 \<noteq> 0" by simp
   have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + X)"
     by (simp add: fps_inverse_deriv[OF th] fps_divide_def
-      power2_eq_square mult_commute fps_const_neg[symmetric] del: fps_const_neg minus_one)
+      power2_eq_square mult_commute fps_const_neg[symmetric] del: fps_const_neg)
   have eq: "inverse ?r $ 0 = 1"
     by (simp add: fps_inverse_def)
   from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + X)" "- 1"] th'] eq
@@ -3276,7 +3276,7 @@
         have th1: "(?m1 k * ?p (of_nat n) k) / ?f n = 1 / of_nat(fact (n - k))"
           unfolding m1nk
           unfolding m h pochhammer_Suc_setprod
-          apply (simp add: field_simps del: fact_Suc minus_one)
+          apply (simp add: field_simps del: fact_Suc)
           unfolding fact_altdef_nat id_def
           unfolding of_nat_setprod
           unfolding setprod_timesf[symmetric]
@@ -3593,7 +3593,7 @@
         unfolding even_mult_two_ex by blast
 
       have "?l $n = ?r$n"
-        by (simp add: m fps_sin_def fps_cos_def power_mult_distrib power_mult power_minus)
+        by (simp add: m fps_sin_def fps_cos_def power_mult_distrib power_mult power_minus [of "c ^ 2"])
     }
     moreover
     {
@@ -3602,7 +3602,7 @@
         unfolding odd_nat_equiv_def2 by (auto simp add: mult_2)
       have "?l $n = ?r$n"
         by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
-          power_mult power_minus)
+          power_mult power_minus [of "c ^ 2"])
     }
     ultimately have "?l $n = ?r$n"  by blast
   } then show ?thesis by (simp add: fps_eq_iff)
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -207,12 +207,14 @@
     from unimodular_reduce_norm[OF th0] o
     have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
       apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
-      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])
+      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp)
       apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
       apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
       apply (rule_tac x="- ii" in exI, simp add: m power_mult)
       apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult)
-      apply (rule_tac x="ii" in exI, simp add: m power_mult)
+      apply (auto simp add: m power_mult)
+      apply (rule_tac x="ii" in exI)
+      apply (auto simp add: m power_mult)
       done
     then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
     let ?w = "v / complex_of_real (root n (cmod b))"
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Polynomial.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -1575,12 +1575,12 @@
 lemma poly_div_minus_left [simp]:
   fixes x y :: "'a::field poly"
   shows "(- x) div y = - (x div y)"
-  using div_smult_left [of "- 1::'a"] by (simp del: minus_one) (* FIXME *)
+  using div_smult_left [of "- 1::'a"] by simp
 
 lemma poly_mod_minus_left [simp]:
   fixes x y :: "'a::field poly"
   shows "(- x) mod y = - (x mod y)"
-  using mod_smult_left [of "- 1::'a"] by (simp del: minus_one) (* FIXME *)
+  using mod_smult_left [of "- 1::'a"] by simp
 
 lemma pdivmod_rel_smult_right:
   "\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk>
@@ -1597,13 +1597,12 @@
 lemma poly_div_minus_right [simp]:
   fixes x y :: "'a::field poly"
   shows "x div (- y) = - (x div y)"
-  using div_smult_right [of "- 1::'a"]
-  by (simp add: nonzero_inverse_minus_eq del: minus_one) (* FIXME *)
+  using div_smult_right [of "- 1::'a"] by (simp add: nonzero_inverse_minus_eq)
 
 lemma poly_mod_minus_right [simp]:
   fixes x y :: "'a::field poly"
   shows "x mod (- y) = x mod y"
-  using mod_smult_right [of "- 1::'a"] by (simp del: minus_one) (* FIXME *)
+  using mod_smult_right [of "- 1::'a"] by simp
 
 lemma pdivmod_rel_mult:
   "\<lbrakk>pdivmod_rel x y q r; pdivmod_rel q z q' r'\<rbrakk>
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -45,8 +45,8 @@
 
 section {* Setup for Numerals *}
 
-setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}, @{const_name neg_numeral}] *}
-setup {* Predicate_Compile_Data.keep_functions [@{const_name numeral}, @{const_name neg_numeral}] *}
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}] *}
+setup {* Predicate_Compile_Data.keep_functions [@{const_name numeral}] *}
 
 setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
 
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Tue Nov 19 10:05:53 2013 +0100
@@ -875,7 +875,6 @@
    @{term "0::real"}, @{term "1::real"},
    @{term "numeral :: num => nat"},
    @{term "numeral :: num => real"},
-   @{term "neg_numeral :: num => real"},
    @{term "Num.Bit0"}, @{term "Num.Bit1"}, @{term "Num.One"}];
 
 fun check_sos kcts ct =
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/List.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -3072,9 +3072,9 @@
 
 lemmas upto_rec_numeral [simp] =
   upto.simps[of "numeral m" "numeral n"]
-  upto.simps[of "numeral m" "neg_numeral n"]
-  upto.simps[of "neg_numeral m" "numeral n"]
-  upto.simps[of "neg_numeral m" "neg_numeral n"] for m n
+  upto.simps[of "numeral m" "- numeral n"]
+  upto.simps[of "- numeral m" "numeral n"]
+  upto.simps[of "- numeral m" "- numeral n"] for m n
 
 lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
 by(simp add: upto.simps)
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Matrix_LP/ComputeFloat.thy
--- a/src/HOL/Matrix_LP/ComputeFloat.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -79,8 +79,8 @@
 lemma real_is_int_numeral[simp]: "real_is_int (numeral x)"
   by (auto simp: real_is_int_def intro!: exI[of _ "numeral x"])
 
-lemma real_is_int_neg_numeral[simp]: "real_is_int (neg_numeral x)"
-  by (auto simp: real_is_int_def intro!: exI[of _ "neg_numeral x"])
+lemma real_is_int_neg_numeral[simp]: "real_is_int (- numeral x)"
+  by (auto simp: real_is_int_def intro!: exI[of _ "- numeral x"])
 
 lemma int_of_real_0[simp]: "int_of_real (0::real) = (0::int)"
 by (simp add: int_of_real_def)
@@ -96,7 +96,7 @@
   by (intro some_equality)
      (auto simp add: real_of_int_inject[symmetric] simp del: real_of_int_inject)
 
-lemma int_of_real_neg_numeral[simp]: "int_of_real (neg_numeral b) = neg_numeral b"
+lemma int_of_real_neg_numeral[simp]: "int_of_real (- numeral b) = - numeral b"
   unfolding int_of_real_def
   by (intro some_equality)
      (auto simp add: real_of_int_inject[symmetric] simp del: real_of_int_inject)
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -228,7 +228,10 @@
   then show ?case by vector
 qed
 
-lemma one_index[simp]: "(1 :: 'a::one ^'n)$i = 1"
+lemma one_index [simp]: "(1 :: 'a :: one ^ 'n) $ i = 1"
+  by vector
+
+lemma neg_one_index [simp]: "(- 1 :: 'a :: {one, uminus} ^ 'n) $ i = - 1"
   by vector
 
 instance vec :: (semiring_char_0, finite) semiring_char_0
@@ -244,8 +247,8 @@
 lemma numeral_index [simp]: "numeral w $ i = numeral w"
   by (induct w) (simp_all only: numeral.simps vector_add_component one_index)
 
-lemma neg_numeral_index [simp]: "neg_numeral w $ i = neg_numeral w"
-  by (simp only: neg_numeral_def vector_uminus_component numeral_index)
+lemma neg_numeral_index [simp]: "- numeral w $ i = - numeral w"
+  by (simp only: vector_uminus_component numeral_index)
 
 instance vec :: (comm_ring_1, finite) comm_ring_1 ..
 instance vec :: (ring_char_0, finite) ring_char_0 ..
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -337,10 +337,10 @@
   by (simp add: bilinear_def linear_iff)
 
 lemma bilinear_lneg: "bilinear h \<Longrightarrow> h (- x) y = - h x y"
-  by (simp only: scaleR_minus1_left [symmetric] bilinear_lmul)
+  by (drule bilinear_lmul [of _ "- 1"]) simp
 
 lemma bilinear_rneg: "bilinear h \<Longrightarrow> h x (- y) = - h x y"
-  by (simp only: scaleR_minus1_left [symmetric] bilinear_rmul)
+  by (drule bilinear_rmul [of _ _ "- 1"]) simp
 
 lemma (in ab_group_add) eq_add_iff: "x = x + y \<longleftrightarrow> y = 0"
   using add_imp_eq[of x y 0] by auto
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -5163,9 +5163,8 @@
 
 lemma open_negations:
   fixes s :: "'a::real_normed_vector set"
-  shows "open s \<Longrightarrow> open ((\<lambda> x. -x) ` s)"
-  unfolding scaleR_minus1_left [symmetric]
-  by (rule open_scaling, auto)
+  shows "open s \<Longrightarrow> open ((\<lambda>x. - x) ` s)"
+  using open_scaling [of "- 1" s] by simp
 
 lemma open_translation:
   fixes s :: "'a::real_normed_vector set"
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/NSA/HTranscendental.thy
--- a/src/HOL/NSA/HTranscendental.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/NSA/HTranscendental.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -258,7 +258,7 @@
             simp add: mult_assoc)
 apply (rule approx_add_right_cancel [where d="-1"])
 apply (rule approx_sym [THEN [2] approx_trans2])
-apply (auto simp add: mem_infmal_iff minus_one [symmetric] simp del: minus_one)
+apply (auto simp add: mem_infmal_iff)
 done
 
 lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1"
@@ -450,7 +450,7 @@
 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
             simp add: mult_assoc)
 apply (rule approx_add_right_cancel [where d = "-1"])
-apply (simp add: minus_one [symmetric] del: minus_one)
+apply simp
 done
 
 lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/NSA/HyperDef.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -425,7 +425,7 @@
 declare power_hypreal_of_real_numeral [of _ "numeral w", simp] for w
 
 lemma power_hypreal_of_real_neg_numeral:
-     "(neg_numeral v :: hypreal) ^ n = hypreal_of_real ((neg_numeral v) ^ n)"
+     "(- numeral v :: hypreal) ^ n = hypreal_of_real ((- numeral v) ^ n)"
 by simp
 declare power_hypreal_of_real_neg_numeral [of _ "numeral w", simp] for w
 (*
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/NSA/NSA.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -654,7 +654,7 @@
 (*reorientation simplification procedure: reorients (polymorphic)
   0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
 simproc_setup approx_reorient_simproc
-  ("0 @= x" | "1 @= y" | "numeral w @= z" | "neg_numeral w @= r") =
+  ("0 @= x" | "1 @= y" | "numeral w @= z" | "- 1 @= y" | "- numeral w @= r") =
 {*
   let val rule = @{thm approx_reorient} RS eq_reflection
       fun proc phi ss ct = case term_of ct of
@@ -1849,8 +1849,12 @@
 lemma st_numeral [simp]: "st (numeral w) = numeral w"
 by (rule Reals_numeral [THEN st_SReal_eq])
 
-lemma st_neg_numeral [simp]: "st (neg_numeral w) = neg_numeral w"
-by (rule Reals_neg_numeral [THEN st_SReal_eq])
+lemma st_neg_numeral [simp]: "st (- numeral w) = - numeral w"
+proof -
+  from Reals_numeral have "numeral w \<in> \<real>" .
+  then have "- numeral w \<in> \<real>" by simp
+  with st_SReal_eq show ?thesis .
+qed
 
 lemma st_0 [simp]: "st 0 = 0"
 by (simp add: st_SReal_eq)
@@ -1858,6 +1862,9 @@
 lemma st_1 [simp]: "st 1 = 1"
 by (simp add: st_SReal_eq)
 
+lemma st_neg_1 [simp]: "st (- 1) = - 1"
+by (simp add: st_SReal_eq)
+
 lemma st_minus: "x \<in> HFinite \<Longrightarrow> st (- x) = - st x"
 by (simp add: st_unique st_SReal st_approx_self approx_minus)
 
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/NSA/NSComplex.thy
--- a/src/HOL/NSA/NSComplex.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/NSA/NSComplex.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -635,7 +635,7 @@
 by transfer (rule of_real_numeral [symmetric])
 
 lemma hcomplex_hypreal_neg_numeral:
-  "hcomplex_of_complex (neg_numeral w) = hcomplex_of_hypreal(neg_numeral w)"
+  "hcomplex_of_complex (- numeral w) = hcomplex_of_hypreal(- numeral w)"
 by transfer (rule of_real_neg_numeral [symmetric])
 
 lemma hcomplex_numeral_hcnj [simp]:
@@ -647,7 +647,7 @@
 by transfer (rule norm_numeral)
 
 lemma hcomplex_neg_numeral_hcmod [simp]: 
-      "hcmod(neg_numeral v :: hcomplex) = (numeral v :: hypreal)"
+      "hcmod(- numeral v :: hcomplex) = (numeral v :: hypreal)"
 by transfer (rule norm_neg_numeral)
 
 lemma hcomplex_numeral_hRe [simp]: 
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/NSA/StarDef.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -968,13 +968,13 @@
 by transfer (rule refl)
 
 lemma star_neg_numeral_def [transfer_unfold]:
-  "neg_numeral k = star_of (neg_numeral k)"
-by (simp only: neg_numeral_def star_of_minus star_of_numeral)
+  "- numeral k = star_of (- numeral k)"
+by (simp only: star_of_minus star_of_numeral)
 
-lemma Standard_neg_numeral [simp]: "neg_numeral k \<in> Standard"
-by (simp add: star_neg_numeral_def)
+lemma Standard_neg_numeral [simp]: "- numeral k \<in> Standard"
+  using star_neg_numeral_def [of k] by simp
 
-lemma star_of_neg_numeral [simp]: "star_of (neg_numeral k) = neg_numeral k"
+lemma star_of_neg_numeral [simp]: "star_of (- numeral k) = - numeral k"
 by transfer (rule refl)
 
 lemma star_of_nat_def [transfer_unfold]: "of_nat n = star_of (of_nat n)"
@@ -987,12 +987,12 @@
   star_of_less [of _ "numeral k", simplified star_of_numeral]
   star_of_le   [of _ "numeral k", simplified star_of_numeral]
   star_of_eq   [of _ "numeral k", simplified star_of_numeral]
-  star_of_less [of "neg_numeral k", simplified star_of_numeral]
-  star_of_le   [of "neg_numeral k", simplified star_of_numeral]
-  star_of_eq   [of "neg_numeral k", simplified star_of_numeral]
-  star_of_less [of _ "neg_numeral k", simplified star_of_numeral]
-  star_of_le   [of _ "neg_numeral k", simplified star_of_numeral]
-  star_of_eq   [of _ "neg_numeral k", simplified star_of_numeral] for k
+  star_of_less [of "- numeral k", simplified star_of_numeral]
+  star_of_le   [of "- numeral k", simplified star_of_numeral]
+  star_of_eq   [of "- numeral k", simplified star_of_numeral]
+  star_of_less [of _ "- numeral k", simplified star_of_numeral]
+  star_of_le   [of _ "- numeral k", simplified star_of_numeral]
+  star_of_eq   [of _ "- numeral k", simplified star_of_numeral] for k
 
 lemma Standard_of_nat [simp]: "of_nat n \<in> Standard"
 by (simp add: star_of_nat_def)
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -3517,7 +3517,7 @@
 by (simp add: perm_int_def perm_int_def)
 
 lemma neg_numeral_int_eqvt:
- shows "pi\<bullet>((neg_numeral n)::int) = neg_numeral n"
+ shows "pi\<bullet>((- numeral n)::int) = - numeral n"
 by (simp add: perm_int_def perm_int_def)
 
 lemma max_int_eqvt:
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Num.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -275,16 +275,6 @@
 
 end
 
-text {* Negative numerals. *}
-
-class neg_numeral = numeral + group_add
-begin
-
-definition neg_numeral :: "num \<Rightarrow> 'a" where
-  "neg_numeral k = - numeral k"
-
-end
-
 text {* Numeral syntax. *}
 
 syntax
@@ -299,8 +289,8 @@
         | (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n
         | (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n)
       else raise Match
-    val pos = Syntax.const @{const_name numeral}
-    val neg = Syntax.const @{const_name neg_numeral}
+    val numeral = Syntax.const @{const_name numeral}
+    val uminus = Syntax.const @{const_name uminus}
     val one = Syntax.const @{const_name Groups.one}
     val zero = Syntax.const @{const_name Groups.zero}
     fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
@@ -311,8 +301,9 @@
           in
             if value = 0 then zero else
             if value > 0
-            then pos $ num_of_int value
-            else neg $ num_of_int (~value)
+            then numeral $ num_of_int value
+            else if value = ~1 then uminus $ one
+            else uminus $ (numeral $ num_of_int (~value))
           end
       | numeral_tr ts = raise TERM ("numeral_tr", ts);
   in [("_Numeral", K numeral_tr)] end
@@ -323,12 +314,12 @@
     fun dest_num (Const (@{const_syntax Bit0}, _) $ n) = 2 * dest_num n
       | dest_num (Const (@{const_syntax Bit1}, _) $ n) = 2 * dest_num n + 1
       | dest_num (Const (@{const_syntax One}, _)) = 1;
-    fun num_tr' sign ctxt T [n] =
+    fun num_tr' ctxt T [n] =
       let
         val k = dest_num n;
         val t' =
           Syntax.const @{syntax_const "_Numeral"} $
-            Syntax.free (sign ^ string_of_int k);
+            Syntax.free (string_of_int k);
       in
         (case T of
           Type (@{type_name fun}, [_, T']) =>
@@ -339,8 +330,7 @@
         | _ => if T = dummyT then t' else raise Match)
       end;
   in
-   [(@{const_syntax numeral}, num_tr' ""),
-    (@{const_syntax neg_numeral}, num_tr' "-")]
+   [(@{const_syntax numeral}, num_tr')]
   end
 *}
 
@@ -383,9 +373,13 @@
   Structures with negation: class @{text neg_numeral}
 *}
 
-context neg_numeral
+class neg_numeral = numeral + group_add
 begin
 
+lemma uminus_numeral_One:
+  "- Numeral1 = - 1"
+  by (simp add: numeral_One)
+
 text {* Numerals form an abelian subgroup. *}
 
 inductive is_num :: "'a \<Rightarrow> bool" where
@@ -403,7 +397,7 @@
   apply simp
   apply (rule_tac a=x in add_left_imp_eq)
   apply (rule_tac a=x in add_right_imp_eq)
-  apply (simp add: add_assoc minus_add_cancel)
+  apply (simp add: add_assoc)
   apply (simp add: add_assoc [symmetric], simp add: add_assoc)
   apply (rule_tac a=x in add_left_imp_eq)
   apply (rule_tac a=x in add_right_imp_eq)
@@ -431,77 +425,85 @@
   by (simp only: BitM_plus_one [symmetric] numeral_add numeral_One eq_diff_eq)
 
 lemma dbl_simps [simp]:
-  "dbl (neg_numeral k) = neg_numeral (Bit0 k)"
+  "dbl (- numeral k) = - dbl (numeral k)"
   "dbl 0 = 0"
   "dbl 1 = 2"
+  "dbl (- 1) = - 2"
   "dbl (numeral k) = numeral (Bit0 k)"
-  by (simp_all add: dbl_def neg_numeral_def numeral.simps minus_add)
+  by (simp_all add: dbl_def numeral.simps minus_add)
 
 lemma dbl_inc_simps [simp]:
-  "dbl_inc (neg_numeral k) = neg_numeral (BitM k)"
+  "dbl_inc (- numeral k) = - dbl_dec (numeral k)"
   "dbl_inc 0 = 1"
   "dbl_inc 1 = 3"
+  "dbl_inc (- 1) = - 1"
   "dbl_inc (numeral k) = numeral (Bit1 k)"
-  by (simp_all add: dbl_inc_def neg_numeral_def numeral.simps numeral_BitM is_num_normalize algebra_simps del: add_uminus_conv_diff)
+  by (simp_all add: dbl_inc_def dbl_dec_def numeral.simps numeral_BitM is_num_normalize algebra_simps del: add_uminus_conv_diff)
 
 lemma dbl_dec_simps [simp]:
-  "dbl_dec (neg_numeral k) = neg_numeral (Bit1 k)"
-  "dbl_dec 0 = -1"
+  "dbl_dec (- numeral k) = - dbl_inc (numeral k)"
+  "dbl_dec 0 = - 1"
   "dbl_dec 1 = 1"
+  "dbl_dec (- 1) = - 3"
   "dbl_dec (numeral k) = numeral (BitM k)"
-  by (simp_all add: dbl_dec_def neg_numeral_def numeral.simps numeral_BitM is_num_normalize)
+  by (simp_all add: dbl_dec_def dbl_inc_def numeral.simps numeral_BitM is_num_normalize)
 
 lemma sub_num_simps [simp]:
   "sub One One = 0"
-  "sub One (Bit0 l) = neg_numeral (BitM l)"
-  "sub One (Bit1 l) = neg_numeral (Bit0 l)"
+  "sub One (Bit0 l) = - numeral (BitM l)"
+  "sub One (Bit1 l) = - numeral (Bit0 l)"
   "sub (Bit0 k) One = numeral (BitM k)"
   "sub (Bit1 k) One = numeral (Bit0 k)"
   "sub (Bit0 k) (Bit0 l) = dbl (sub k l)"
   "sub (Bit0 k) (Bit1 l) = dbl_dec (sub k l)"
   "sub (Bit1 k) (Bit0 l) = dbl_inc (sub k l)"
   "sub (Bit1 k) (Bit1 l) = dbl (sub k l)"
-  by (simp_all add: dbl_def dbl_dec_def dbl_inc_def sub_def neg_numeral_def numeral.simps
+  by (simp_all add: dbl_def dbl_dec_def dbl_inc_def sub_def numeral.simps
     numeral_BitM is_num_normalize del: add_uminus_conv_diff add: diff_conv_add_uminus)
 
 lemma add_neg_numeral_simps:
-  "numeral m + neg_numeral n = sub m n"
-  "neg_numeral m + numeral n = sub n m"
-  "neg_numeral m + neg_numeral n = neg_numeral (m + n)"
-  by (simp_all add: sub_def neg_numeral_def numeral_add numeral.simps is_num_normalize
+  "numeral m + - numeral n = sub m n"
+  "- numeral m + numeral n = sub n m"
+  "- numeral m + - numeral n = - (numeral m + numeral n)"
+  by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize
     del: add_uminus_conv_diff add: diff_conv_add_uminus)
 
 lemma add_neg_numeral_special:
-  "1 + neg_numeral m = sub One m"
-  "neg_numeral m + 1 = sub One m"
-  by (simp_all add: sub_def neg_numeral_def numeral_add numeral.simps is_num_normalize)
+  "1 + - numeral m = sub One m"
+  "- numeral m + 1 = sub One m"
+  "numeral m + - 1 = sub m One"
+  "- 1 + numeral n = sub n One"
+  "- 1 + - numeral n = - numeral (inc n)"
+  "- numeral m + - 1 = - numeral (inc m)"
+  "1 + - 1 = 0"
+  "- 1 + 1 = 0"
+  "- 1 + - 1 = - 2"
+  by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize right_minus numeral_inc
+    del: add_uminus_conv_diff add: diff_conv_add_uminus)
 
 lemma diff_numeral_simps:
   "numeral m - numeral n = sub m n"
-  "numeral m - neg_numeral n = numeral (m + n)"
-  "neg_numeral m - numeral n = neg_numeral (m + n)"
-  "neg_numeral m - neg_numeral n = sub n m"
-  by (simp_all add: neg_numeral_def sub_def numeral_add numeral.simps is_num_normalize
+  "numeral m - - numeral n = numeral (m + n)"
+  "- numeral m - numeral n = - numeral (m + n)"
+  "- numeral m - - numeral n = sub n m"
+  by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize
     del: add_uminus_conv_diff add: diff_conv_add_uminus)
 
 lemma diff_numeral_special:
   "1 - numeral n = sub One n"
-  "1 - neg_numeral n = numeral (One + n)"
   "numeral m - 1 = sub m One"
-  "neg_numeral m - 1 = neg_numeral (m + One)"
-  by (simp_all add: neg_numeral_def sub_def numeral_add numeral.simps add: is_num_normalize)
-
-lemma minus_one: "- 1 = -1"
-  unfolding neg_numeral_def numeral.simps ..
-
-lemma minus_numeral: "- numeral n = neg_numeral n"
-  unfolding neg_numeral_def ..
-
-lemma minus_neg_numeral: "- neg_numeral n = numeral n"
-  unfolding neg_numeral_def by simp
-
-lemmas minus_numeral_simps [simp] =
-  minus_one minus_numeral minus_neg_numeral
+  "1 - - numeral n = numeral (One + n)"
+  "- numeral m - 1 = - numeral (m + One)"
+  "- 1 - numeral n = - numeral (inc n)"
+  "numeral m - - 1 = numeral (inc m)"
+  "- 1 - - numeral n = sub n One"
+  "- numeral m - - 1 = sub One m"
+  "1 - 1 = 0"
+  "- 1 - 1 = - 2"
+  "1 - - 1 = 2"
+  "- 1 - - 1 = 0"
+  by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize numeral_inc
+    del: add_uminus_conv_diff add: diff_conv_add_uminus)
 
 end
 
@@ -675,17 +677,17 @@
 subclass neg_numeral ..
 
 lemma mult_neg_numeral_simps:
-  "neg_numeral m * neg_numeral n = numeral (m * n)"
-  "neg_numeral m * numeral n = neg_numeral (m * n)"
-  "numeral m * neg_numeral n = neg_numeral (m * n)"
-  unfolding neg_numeral_def mult_minus_left mult_minus_right
+  "- numeral m * - numeral n = numeral (m * n)"
+  "- numeral m * numeral n = - numeral (m * n)"
+  "numeral m * - numeral n = - numeral (m * n)"
+  unfolding mult_minus_left mult_minus_right
   by (simp_all only: minus_minus numeral_mult)
 
-lemma mult_minus1 [simp]: "-1 * z = - z"
-  unfolding neg_numeral_def numeral.simps mult_minus_left by simp
+lemma mult_minus1 [simp]: "- 1 * z = - z"
+  unfolding numeral.simps mult_minus_left by simp
 
-lemma mult_minus1_right [simp]: "z * -1 = - z"
-  unfolding neg_numeral_def numeral.simps mult_minus_right by simp
+lemma mult_minus1_right [simp]: "z * - 1 = - z"
+  unfolding numeral.simps mult_minus_right by simp
 
 end
 
@@ -708,9 +710,15 @@
 lemma not_iszero_Numeral1: "\<not> iszero Numeral1"
   by (simp add: numeral_One)
 
+lemma not_iszero_neg_1 [simp]: "\<not> iszero (- 1)"
+  by (simp add: iszero_def)
+
+lemma not_iszero_neg_Numeral1: "\<not> iszero (- Numeral1)"
+  by (simp add: numeral_One)
+
 lemma iszero_neg_numeral [simp]:
-  "iszero (neg_numeral w) \<longleftrightarrow> iszero (numeral w)"
-  unfolding iszero_def neg_numeral_def
+  "iszero (- numeral w) \<longleftrightarrow> iszero (numeral w)"
+  unfolding iszero_def
   by (rule neg_equal_0_iff_equal)
 
 lemma eq_iff_iszero_diff: "x = y \<longleftrightarrow> iszero (x - y)"
@@ -730,17 +738,17 @@
 
 lemma eq_numeral_iff_iszero:
   "numeral x = numeral y \<longleftrightarrow> iszero (sub x y)"
-  "numeral x = neg_numeral y \<longleftrightarrow> iszero (numeral (x + y))"
-  "neg_numeral x = numeral y \<longleftrightarrow> iszero (numeral (x + y))"
-  "neg_numeral x = neg_numeral y \<longleftrightarrow> iszero (sub y x)"
+  "numeral x = - numeral y \<longleftrightarrow> iszero (numeral (x + y))"
+  "- numeral x = numeral y \<longleftrightarrow> iszero (numeral (x + y))"
+  "- numeral x = - numeral y \<longleftrightarrow> iszero (sub y x)"
   "numeral x = 1 \<longleftrightarrow> iszero (sub x One)"
   "1 = numeral y \<longleftrightarrow> iszero (sub One y)"
-  "neg_numeral x = 1 \<longleftrightarrow> iszero (numeral (x + One))"
-  "1 = neg_numeral y \<longleftrightarrow> iszero (numeral (One + y))"
+  "- numeral x = 1 \<longleftrightarrow> iszero (numeral (x + One))"
+  "1 = - numeral y \<longleftrightarrow> iszero (numeral (One + y))"
   "numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
   "0 = numeral y \<longleftrightarrow> iszero (numeral y)"
-  "neg_numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
-  "0 = neg_numeral y \<longleftrightarrow> iszero (numeral y)"
+  "- numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
+  "0 = - numeral y \<longleftrightarrow> iszero (numeral y)"
   unfolding eq_iff_iszero_diff diff_numeral_simps diff_numeral_special
   by simp_all
 
@@ -756,33 +764,69 @@
 lemma not_iszero_numeral [simp]: "\<not> iszero (numeral w)"
   by (simp add: iszero_def)
 
-lemma neg_numeral_eq_iff: "neg_numeral m = neg_numeral n \<longleftrightarrow> m = n"
-  by (simp only: neg_numeral_def neg_equal_iff_equal numeral_eq_iff)
+lemma neg_numeral_eq_iff: "- numeral m = - numeral n \<longleftrightarrow> m = n"
+  by simp
 
-lemma numeral_neq_neg_numeral: "numeral m \<noteq> neg_numeral n"
-  unfolding neg_numeral_def eq_neg_iff_add_eq_0
+lemma numeral_neq_neg_numeral: "numeral m \<noteq> - numeral n"
+  unfolding eq_neg_iff_add_eq_0
   by (simp add: numeral_plus_numeral)
 
-lemma neg_numeral_neq_numeral: "neg_numeral m \<noteq> numeral n"
+lemma neg_numeral_neq_numeral: "- numeral m \<noteq> numeral n"
   by (rule numeral_neq_neg_numeral [symmetric])
 
-lemma zero_neq_neg_numeral: "0 \<noteq> neg_numeral n"
-  unfolding neg_numeral_def neg_0_equal_iff_equal by simp
+lemma zero_neq_neg_numeral: "0 \<noteq> - numeral n"
+  unfolding neg_0_equal_iff_equal by simp
 
-lemma neg_numeral_neq_zero: "neg_numeral n \<noteq> 0"
-  unfolding neg_numeral_def neg_equal_0_iff_equal by simp
+lemma neg_numeral_neq_zero: "- numeral n \<noteq> 0"
+  unfolding neg_equal_0_iff_equal by simp
 
-lemma one_neq_neg_numeral: "1 \<noteq> neg_numeral n"
+lemma one_neq_neg_numeral: "1 \<noteq> - numeral n"
   using numeral_neq_neg_numeral [of One n] by (simp add: numeral_One)
 
-lemma neg_numeral_neq_one: "neg_numeral n \<noteq> 1"
+lemma neg_numeral_neq_one: "- numeral n \<noteq> 1"
   using neg_numeral_neq_numeral [of n One] by (simp add: numeral_One)
 
+lemma neg_one_neq_numeral:
+  "- 1 \<noteq> numeral n"
+  using neg_numeral_neq_numeral [of One n] by (simp add: numeral_One)
+
+lemma numeral_neq_neg_one:
+  "numeral n \<noteq> - 1"
+  using numeral_neq_neg_numeral [of n One] by (simp add: numeral_One)
+
+lemma neg_one_eq_numeral_iff:
+  "- 1 = - numeral n \<longleftrightarrow> n = One"
+  using neg_numeral_eq_iff [of One n] by (auto simp add: numeral_One)
+
+lemma numeral_eq_neg_one_iff:
+  "- numeral n = - 1 \<longleftrightarrow> n = One"
+  using neg_numeral_eq_iff [of n One] by (auto simp add: numeral_One)
+
+lemma neg_one_neq_zero:
+  "- 1 \<noteq> 0"
+  by simp
+
+lemma zero_neq_neg_one:
+  "0 \<noteq> - 1"
+  by simp
+
+lemma neg_one_neq_one:
+  "- 1 \<noteq> 1"
+  using neg_numeral_neq_numeral [of One One] by (simp only: numeral_One not_False_eq_True)
+
+lemma one_neq_neg_one:
+  "1 \<noteq> - 1"
+  using numeral_neq_neg_numeral [of One One] by (simp only: numeral_One not_False_eq_True)
+
 lemmas eq_neg_numeral_simps [simp] =
   neg_numeral_eq_iff
   numeral_neq_neg_numeral neg_numeral_neq_numeral
   one_neq_neg_numeral neg_numeral_neq_one
   zero_neq_neg_numeral neg_numeral_neq_zero
+  neg_one_neq_numeral numeral_neq_neg_one
+  neg_one_eq_numeral_iff numeral_eq_neg_one_iff
+  neg_one_neq_zero zero_neq_neg_one
+  neg_one_neq_one one_neq_neg_one
 
 end
 
@@ -795,48 +839,72 @@
 
 subclass ring_char_0 ..
 
-lemma neg_numeral_le_iff: "neg_numeral m \<le> neg_numeral n \<longleftrightarrow> n \<le> m"
-  by (simp only: neg_numeral_def neg_le_iff_le numeral_le_iff)
+lemma neg_numeral_le_iff: "- numeral m \<le> - numeral n \<longleftrightarrow> n \<le> m"
+  by (simp only: neg_le_iff_le numeral_le_iff)
 
-lemma neg_numeral_less_iff: "neg_numeral m < neg_numeral n \<longleftrightarrow> n < m"
-  by (simp only: neg_numeral_def neg_less_iff_less numeral_less_iff)
+lemma neg_numeral_less_iff: "- numeral m < - numeral n \<longleftrightarrow> n < m"
+  by (simp only: neg_less_iff_less numeral_less_iff)
 
-lemma neg_numeral_less_zero: "neg_numeral n < 0"
-  by (simp only: neg_numeral_def neg_less_0_iff_less zero_less_numeral)
+lemma neg_numeral_less_zero: "- numeral n < 0"
+  by (simp only: neg_less_0_iff_less zero_less_numeral)
 
-lemma neg_numeral_le_zero: "neg_numeral n \<le> 0"
-  by (simp only: neg_numeral_def neg_le_0_iff_le zero_le_numeral)
+lemma neg_numeral_le_zero: "- numeral n \<le> 0"
+  by (simp only: neg_le_0_iff_le zero_le_numeral)
 
-lemma not_zero_less_neg_numeral: "\<not> 0 < neg_numeral n"
+lemma not_zero_less_neg_numeral: "\<not> 0 < - numeral n"
   by (simp only: not_less neg_numeral_le_zero)
 
-lemma not_zero_le_neg_numeral: "\<not> 0 \<le> neg_numeral n"
+lemma not_zero_le_neg_numeral: "\<not> 0 \<le> - numeral n"
   by (simp only: not_le neg_numeral_less_zero)
 
-lemma neg_numeral_less_numeral: "neg_numeral m < numeral n"
+lemma neg_numeral_less_numeral: "- numeral m < numeral n"
   using neg_numeral_less_zero zero_less_numeral by (rule less_trans)
 
-lemma neg_numeral_le_numeral: "neg_numeral m \<le> numeral n"
+lemma neg_numeral_le_numeral: "- numeral m \<le> numeral n"
   by (simp only: less_imp_le neg_numeral_less_numeral)
 
-lemma not_numeral_less_neg_numeral: "\<not> numeral m < neg_numeral n"
+lemma not_numeral_less_neg_numeral: "\<not> numeral m < - numeral n"
   by (simp only: not_less neg_numeral_le_numeral)
 
-lemma not_numeral_le_neg_numeral: "\<not> numeral m \<le> neg_numeral n"
+lemma not_numeral_le_neg_numeral: "\<not> numeral m \<le> - numeral n"
   by (simp only: not_le neg_numeral_less_numeral)
   
-lemma neg_numeral_less_one: "neg_numeral m < 1"
+lemma neg_numeral_less_one: "- numeral m < 1"
   by (rule neg_numeral_less_numeral [of m One, unfolded numeral_One])
 
-lemma neg_numeral_le_one: "neg_numeral m \<le> 1"
+lemma neg_numeral_le_one: "- numeral m \<le> 1"
   by (rule neg_numeral_le_numeral [of m One, unfolded numeral_One])
 
-lemma not_one_less_neg_numeral: "\<not> 1 < neg_numeral m"
+lemma not_one_less_neg_numeral: "\<not> 1 < - numeral m"
   by (simp only: not_less neg_numeral_le_one)
 
-lemma not_one_le_neg_numeral: "\<not> 1 \<le> neg_numeral m"
+lemma not_one_le_neg_numeral: "\<not> 1 \<le> - numeral m"
   by (simp only: not_le neg_numeral_less_one)
 
+lemma not_numeral_less_neg_one: "\<not> numeral m < - 1"
+  using not_numeral_less_neg_numeral [of m One] by (simp add: numeral_One)
+
+lemma not_numeral_le_neg_one: "\<not> numeral m \<le> - 1"
+  using not_numeral_le_neg_numeral [of m One] by (simp add: numeral_One)
+
+lemma neg_one_less_numeral: "- 1 < numeral m"
+  using neg_numeral_less_numeral [of One m] by (simp add: numeral_One)
+
+lemma neg_one_le_numeral: "- 1 \<le> numeral m"
+  using neg_numeral_le_numeral [of One m] by (simp add: numeral_One)
+
+lemma neg_numeral_less_neg_one_iff: "- numeral m < - 1 \<longleftrightarrow> m \<noteq> One"
+  by (cases m) simp_all
+
+lemma neg_numeral_le_neg_one: "- numeral m \<le> - 1"
+  by simp
+
+lemma not_neg_one_less_neg_numeral: "\<not> - 1 < - numeral m"
+  by simp
+
+lemma not_neg_one_le_neg_numeral_iff: "\<not> - 1 \<le> - numeral m \<longleftrightarrow> m \<noteq> One"
+  by (cases m) simp_all
+
 lemma sub_non_negative:
   "sub n m \<ge> 0 \<longleftrightarrow> n \<ge> m"
   by (simp only: sub_def le_diff_eq) simp
@@ -858,18 +926,40 @@
   neg_numeral_le_numeral not_numeral_le_neg_numeral
   neg_numeral_le_zero not_zero_le_neg_numeral
   neg_numeral_le_one not_one_le_neg_numeral
+  neg_one_le_numeral not_numeral_le_neg_one
+  neg_numeral_le_neg_one not_neg_one_le_neg_numeral_iff
+
+lemma le_minus_one_simps [simp]:
+  "- 1 \<le> 0"
+  "- 1 \<le> 1"
+  "\<not> 0 \<le> - 1"
+  "\<not> 1 \<le> - 1"
+  by simp_all
 
 lemmas less_neg_numeral_simps [simp] =
   neg_numeral_less_iff
   neg_numeral_less_numeral not_numeral_less_neg_numeral
   neg_numeral_less_zero not_zero_less_neg_numeral
   neg_numeral_less_one not_one_less_neg_numeral
+  neg_one_less_numeral not_numeral_less_neg_one
+  neg_numeral_less_neg_one_iff not_neg_one_less_neg_numeral
+
+lemma less_minus_one_simps [simp]:
+  "- 1 < 0"
+  "- 1 < 1"
+  "\<not> 0 < - 1"
+  "\<not> 1 < - 1"
+  by (simp_all add: less_le)
 
 lemma abs_numeral [simp]: "abs (numeral n) = numeral n"
   by simp
 
-lemma abs_neg_numeral [simp]: "abs (neg_numeral n) = numeral n"
-  by (simp only: neg_numeral_def abs_minus_cancel abs_numeral)
+lemma abs_neg_numeral [simp]: "abs (- numeral n) = numeral n"
+  by (simp only: abs_minus_cancel abs_numeral)
+
+lemma abs_neg_one [simp]:
+  "abs (- 1) = 1"
+  by simp
 
 end
 
@@ -1032,31 +1122,36 @@
 text{*Theorem lists for the cancellation simprocs. The use of a binary
 numeral for 1 reduces the number of special cases.*}
 
-lemmas mult_1s =
-  mult_numeral_1 mult_numeral_1_right 
-  mult_minus1 mult_minus1_right
+lemma mult_1s:
+  fixes a :: "'a::semiring_numeral"
+    and b :: "'b::ring_1"
+  shows "Numeral1 * a = a"
+    "a * Numeral1 = a"
+    "- Numeral1 * b = - b"
+    "b * - Numeral1 = - b"
+  by simp_all
 
 setup {*
   Reorient_Proc.add
     (fn Const (@{const_name numeral}, _) $ _ => true
-    | Const (@{const_name neg_numeral}, _) $ _ => true
+    | Const (@{const_name uminus}, _) $ (Const (@{const_name numeral}, _) $ _) => true
     | _ => false)
 *}
 
 simproc_setup reorient_numeral
-  ("numeral w = x" | "neg_numeral w = y") = Reorient_Proc.proc
+  ("numeral w = x" | "- numeral w = y") = Reorient_Proc.proc
 
 
 subsubsection {* Simplification of arithmetic operations on integer constants. *}
 
 lemmas arith_special = (* already declared simp above *)
   add_numeral_special add_neg_numeral_special
-  diff_numeral_special minus_one
+  diff_numeral_special
 
 (* rules already in simpset *)
 lemmas arith_extra_simps =
   numeral_plus_numeral add_neg_numeral_simps add_0_left add_0_right
-  minus_numeral minus_neg_numeral minus_zero minus_one
+  minus_zero
   diff_numeral_simps diff_0 diff_0_right
   numeral_times_numeral mult_neg_numeral_simps
   mult_zero_left mult_zero_right
@@ -1089,15 +1184,15 @@
 
 lemmas rel_simps =
   le_num_simps less_num_simps eq_num_simps
-  le_numeral_simps le_neg_numeral_simps le_numeral_extra
-  less_numeral_simps less_neg_numeral_simps less_numeral_extra
+  le_numeral_simps le_neg_numeral_simps le_minus_one_simps le_numeral_extra
+  less_numeral_simps less_neg_numeral_simps less_minus_one_simps less_numeral_extra
   eq_numeral_simps eq_neg_numeral_simps eq_numeral_extra
 
 lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
   -- {* Unfold all @{text let}s involving constants *}
   unfolding Let_def ..
 
-lemma Let_neg_numeral [simp]: "Let (neg_numeral v) f = f (neg_numeral v)"
+lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
   -- {* Unfold all @{text let}s involving constants *}
   unfolding Let_def ..
 
@@ -1133,16 +1228,16 @@
   by (simp_all add: add_assoc [symmetric])
 
 lemma add_neg_numeral_left [simp]:
-  "numeral v + (neg_numeral w + y) = (sub v w + y)"
-  "neg_numeral v + (numeral w + y) = (sub w v + y)"
-  "neg_numeral v + (neg_numeral w + y) = (neg_numeral(v + w) + y)"
+  "numeral v + (- numeral w + y) = (sub v w + y)"
+  "- numeral v + (numeral w + y) = (sub w v + y)"
+  "- numeral v + (- numeral w + y) = (- numeral(v + w) + y)"
   by (simp_all add: add_assoc [symmetric])
 
 lemma mult_numeral_left [simp]:
   "numeral v * (numeral w * z) = (numeral(v * w) * z :: 'a::semiring_numeral)"
-  "neg_numeral v * (numeral w * y) = (neg_numeral(v * w) * y :: 'b::ring_1)"
-  "numeral v * (neg_numeral w * y) = (neg_numeral(v * w) * y :: 'b::ring_1)"
-  "neg_numeral v * (neg_numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)"
+  "- numeral v * (numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
+  "numeral v * (- numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
+  "- numeral v * (- numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)"
   by (simp_all add: mult_assoc [symmetric])
 
 hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_dec
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Number_Theory/Cong.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -323,8 +323,6 @@
     \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
   apply (simp only: cong_altdef_int)
   apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
-  (* any way around this? *)
-  apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
   apply (auto simp add: field_simps)
   done
 
@@ -665,7 +663,6 @@
   apply auto
   apply (cases "n \<ge> 0")
   apply auto
-  apply (subst cong_int_def, auto)
   apply (frule cong_solve_int [of a n])
   apply auto
   done
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Number_Theory/Residues.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -455,6 +455,7 @@
   apply (subst fact_altdef_int, simp)
   apply (subst cong_int_def)
   apply simp
+  apply arith
   apply (rule residues_prime.wilson_theorem1)
   apply (rule residues_prime.intro)
   apply auto
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Numeral_Simprocs.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -17,7 +17,7 @@
   if_False if_True
   add_0 add_Suc add_numeral_left
   add_neg_numeral_left mult_numeral_left
-  numeral_1_eq_1 [symmetric] Suc_eq_plus1
+  numeral_One [symmetric] uminus_numeral_One [symmetric] Suc_eq_plus1
   eq_numeral_iff_iszero not_iszero_Numeral1
 
 declare split_div [of _ _ "numeral k", arith_split] for k
@@ -85,18 +85,19 @@
 
 text {* For @{text cancel_factor} *}
 
-lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
-by auto
+lemmas nat_mult_le_cancel_disj = mult_le_cancel1
 
-lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
-by auto
+lemmas nat_mult_less_cancel_disj = mult_less_cancel1
 
-lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
-by auto
+lemma nat_mult_eq_cancel_disj:
+  fixes k m n :: nat
+  shows "k * m = k * n \<longleftrightarrow> k = 0 \<or> m = n"
+  by auto
 
-lemma nat_mult_div_cancel_disj[simp]:
-     "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
-by (simp add: nat_mult_div_cancel1)
+lemma nat_mult_div_cancel_disj [simp]:
+  fixes k m n :: nat
+  shows "(k * m) div (k * n) = (if k = 0 then 0 else m div n)"
+  by (fact div_mult_mult1_if)
 
 ML_file "Tools/numeral_simprocs.ML"
 
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Parity.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -78,7 +78,7 @@
   unfolding even_def by simp
 
 (* TODO: proper simp rules for Num.Bit0, Num.Bit1 *)
-declare even_def [of "neg_numeral v", simp] for v
+declare even_def [of "- numeral v", simp] for v
 
 lemma even_numeral_nat [simp]: "even (numeral (Num.Bit0 k) :: nat)"
   unfolding even_nat_def by simp
@@ -190,14 +190,9 @@
   by (induct n) simp_all
 
 lemma (in comm_ring_1)
-  shows minus_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1"
-  and minus_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1"
-  by (simp_all add: neg_power_if del: minus_one)
-
-lemma (in comm_ring_1)
-  shows neg_one_even_power [simp]: "even n \<Longrightarrow> (-1) ^ n = 1"
-  and neg_one_odd_power [simp]: "odd n \<Longrightarrow> (-1) ^ n = - 1"
-  by (simp_all add: minus_one [symmetric] del: minus_one)
+  shows neg_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1"
+  and neg_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1"
+  by (simp_all add: neg_power_if)
 
 lemma zero_le_even_power: "even n ==>
     0 <= (x::'a::{linordered_ring,monoid_mult}) ^ n"
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Power.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -209,14 +209,6 @@
   "(- x) ^ numeral (Num.Bit1 k) = - (x ^ numeral (Num.Bit1 k))"
   by (simp only: eval_nat_numeral(3) power_Suc power_minus_Bit0 mult_minus_left)
 
-lemma power_neg_numeral_Bit0 [simp]:
-  "neg_numeral k ^ numeral (Num.Bit0 l) = numeral (Num.pow k (Num.Bit0 l))"
-  by (simp only: neg_numeral_def power_minus_Bit0 power_numeral)
-
-lemma power_neg_numeral_Bit1 [simp]:
-  "neg_numeral k ^ numeral (Num.Bit1 l) = neg_numeral (Num.pow k (Num.Bit1 l))"
-  by (simp only: neg_numeral_def power_minus_Bit1 power_numeral pow.simps)
-
 lemma power2_minus [simp]:
   "(- a)\<^sup>2 = a\<^sup>2"
   by (rule power_minus_Bit0)
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Rat.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -215,17 +215,19 @@
   "Fract 0 k = 0"
   "Fract 1 1 = 1"
   "Fract (numeral w) 1 = numeral w"
-  "Fract (neg_numeral w) 1 = neg_numeral w"
+  "Fract (- numeral w) 1 = - numeral w"
+  "Fract (- 1) 1 = - 1"
   "Fract k 0 = 0"
   using Fract_of_int_eq [of "numeral w"]
-  using Fract_of_int_eq [of "neg_numeral w"]
+  using Fract_of_int_eq [of "- numeral w"]
   by (simp_all add: Zero_rat_def One_rat_def eq_rat)
 
 lemma rat_number_expand:
   "0 = Fract 0 1"
   "1 = Fract 1 1"
   "numeral k = Fract (numeral k) 1"
-  "neg_numeral k = Fract (neg_numeral k) 1"
+  "- 1 = Fract (- 1) 1"
+  "- numeral k = Fract (- numeral k) 1"
   by (simp_all add: rat_number_collapse)
 
 lemma Rat_cases_nonzero [case_names Fract 0]:
@@ -356,7 +358,8 @@
   "quotient_of 0 = (0, 1)"
   "quotient_of 1 = (1, 1)"
   "quotient_of (numeral k) = (numeral k, 1)"
-  "quotient_of (neg_numeral k) = (neg_numeral k, 1)"
+  "quotient_of (- 1) = (- 1, 1)"
+  "quotient_of (- numeral k) = (- numeral k, 1)"
   by (simp_all add: rat_number_expand quotient_of_Fract)
 
 lemma quotient_of_eq: "quotient_of (Fract a b) = (p, q) \<Longrightarrow> Fract p q = Fract a b"
@@ -620,7 +623,7 @@
   #> Lin_Arith.add_simps [@{thm neg_less_iff_less},
       @{thm True_implies_equals},
       read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm distrib_left},
-      read_instantiate @{context} [(("a", 0), "(neg_numeral ?v)")] @{thm distrib_left},
+      read_instantiate @{context} [(("a", 0), "(- numeral ?v)")] @{thm distrib_left},
       @{thm divide_1}, @{thm divide_zero_left},
       @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
       @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
@@ -664,6 +667,10 @@
 lemma of_rat_minus: "of_rat (- a) = - of_rat a"
   by transfer simp
 
+lemma of_rat_neg_one [simp]:
+  "of_rat (- 1) = - 1"
+  by (simp add: of_rat_minus)
+
 lemma of_rat_diff: "of_rat (a - b) = of_rat a - of_rat b"
   using of_rat_add [of a "- b"] by (simp add: of_rat_minus)
 
@@ -778,8 +785,8 @@
 using of_rat_of_int_eq [of "numeral w"] by simp
 
 lemma of_rat_neg_numeral_eq [simp]:
-  "of_rat (neg_numeral w) = neg_numeral w"
-using of_rat_of_int_eq [of "neg_numeral w"] by simp
+  "of_rat (- numeral w) = - numeral w"
+using of_rat_of_int_eq [of "- numeral w"] by simp
 
 lemmas zero_rat = Zero_rat_def
 lemmas one_rat = One_rat_def
@@ -820,9 +827,6 @@
 lemma Rats_number_of [simp]: "numeral w \<in> Rats"
 by (subst of_rat_numeral_eq [symmetric], rule Rats_of_rat)
 
-lemma Rats_neg_number_of [simp]: "neg_numeral w \<in> Rats"
-by (subst of_rat_neg_numeral_eq [symmetric], rule Rats_of_rat)
-
 lemma Rats_0 [simp]: "0 \<in> Rats"
 apply (unfold Rats_def)
 apply (rule range_eqI)
@@ -943,7 +947,7 @@
   by (simp add: Rat.of_int_def)
 
 lemma [code_unfold]:
-  "neg_numeral k = Rat.of_int (neg_numeral k)"
+  "- numeral k = Rat.of_int (- numeral k)"
   by (simp add: Rat.of_int_def)
 
 lemma Frct_code_post [code_post]:
@@ -951,13 +955,13 @@
   "Frct (a, 0) = 0"
   "Frct (1, 1) = 1"
   "Frct (numeral k, 1) = numeral k"
-  "Frct (neg_numeral k, 1) = neg_numeral k"
+  "Frct (- numeral k, 1) = - numeral k"
   "Frct (1, numeral k) = 1 / numeral k"
-  "Frct (1, neg_numeral k) = 1 / neg_numeral k"
+  "Frct (1, - numeral k) = 1 / - numeral k"
   "Frct (numeral k, numeral l) = numeral k / numeral l"
-  "Frct (numeral k, neg_numeral l) = numeral k / neg_numeral l"
-  "Frct (neg_numeral k, numeral l) = neg_numeral k / numeral l"
-  "Frct (neg_numeral k, neg_numeral l) = neg_numeral k / neg_numeral l"
+  "Frct (numeral k, - numeral l) = numeral k / - numeral l"
+  "Frct (- numeral k, numeral l) = - numeral k / numeral l"
+  "Frct (- numeral k, - numeral l) = - numeral k / - numeral l"
   by (simp_all add: Fract_of_int_quotient)
 
 
@@ -1156,7 +1160,7 @@
       in
         if i = 0 then Syntax.const @{const_syntax Groups.zero}
         else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i
-        else Syntax.const @{const_syntax Num.neg_numeral} $ mk (~i)
+        else Syntax.const @{const_syntax Groups.uminus} $ (Syntax.const @{const_syntax Num.numeral} $ mk (~i))
       end;
 
     fun mk_frac str =
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Real.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -1447,13 +1447,13 @@
 
 lemma [code_abbrev]:
   "real_of_int (numeral k) = numeral k"
-  "real_of_int (neg_numeral k) = neg_numeral k"
+  "real_of_int (- numeral k) = - numeral k"
   by simp_all
 
-text{*Collapse applications of @{term real} to @{term number_of}*}
+text{*Collapse applications of @{const real} to @{const numeral}*}
 lemma real_numeral [simp]:
   "real (numeral v :: int) = numeral v"
-  "real (neg_numeral v :: int) = neg_numeral v"
+  "real (- numeral v :: int) = - numeral v"
 by (simp_all add: real_of_int_def)
 
 lemma real_of_nat_numeral [simp]:
@@ -1559,11 +1559,11 @@
   unfolding real_of_int_le_iff[symmetric] by simp
 
 lemma neg_numeral_power_le_real_of_int_cancel_iff[simp]:
-  "(neg_numeral x::real) ^ n \<le> real a \<longleftrightarrow> (neg_numeral x::int) ^ n \<le> a"
+  "(- numeral x::real) ^ n \<le> real a \<longleftrightarrow> (- numeral x::int) ^ n \<le> a"
   unfolding real_of_int_le_iff[symmetric] by simp
 
 lemma real_of_int_le_neg_numeral_power_cancel_iff[simp]:
-  "real a \<le> (neg_numeral x::real) ^ n \<longleftrightarrow> a \<le> (neg_numeral x::int) ^ n"
+  "real a \<le> (- numeral x::real) ^ n \<longleftrightarrow> a \<le> (- numeral x::int) ^ n"
   unfolding real_of_int_le_iff[symmetric] by simp
 
 subsection{*Density of the Reals*}
@@ -2051,7 +2051,7 @@
   by simp
 
 lemma [code_abbrev]:
-  "(of_rat (neg_numeral k) :: real) = neg_numeral k"
+  "(of_rat (- numeral k) :: real) = - numeral k"
   by simp
 
 lemma [code_post]:
@@ -2059,14 +2059,14 @@
   "(of_rat (r / 0)  :: real) = 0"
   "(of_rat (1 / 1)  :: real) = 1"
   "(of_rat (numeral k / 1) :: real) = numeral k"
-  "(of_rat (neg_numeral k / 1) :: real) = neg_numeral k"
+  "(of_rat (- numeral k / 1) :: real) = - numeral k"
   "(of_rat (1 / numeral k) :: real) = 1 / numeral k"
-  "(of_rat (1 / neg_numeral k) :: real) = 1 / neg_numeral k"
+  "(of_rat (1 / - numeral k) :: real) = 1 / - numeral k"
   "(of_rat (numeral k / numeral l)  :: real) = numeral k / numeral l"
-  "(of_rat (numeral k / neg_numeral l)  :: real) = numeral k / neg_numeral l"
-  "(of_rat (neg_numeral k / numeral l)  :: real) = neg_numeral k / numeral l"
-  "(of_rat (neg_numeral k / neg_numeral l)  :: real) = neg_numeral k / neg_numeral l"
-  by (simp_all add: of_rat_divide)
+  "(of_rat (numeral k / - numeral l)  :: real) = numeral k / - numeral l"
+  "(of_rat (- numeral k / numeral l)  :: real) = - numeral k / numeral l"
+  "(of_rat (- numeral k / - numeral l)  :: real) = - numeral k / - numeral l"
+  by (simp_all add: of_rat_divide of_rat_minus)
 
 
 text {* Operations *}
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -307,8 +307,8 @@
 lemma of_real_numeral: "of_real (numeral w) = numeral w"
 using of_real_of_int_eq [of "numeral w"] by simp
 
-lemma of_real_neg_numeral: "of_real (neg_numeral w) = neg_numeral w"
-using of_real_of_int_eq [of "neg_numeral w"] by simp
+lemma of_real_neg_numeral: "of_real (- numeral w) = - numeral w"
+using of_real_of_int_eq [of "- numeral w"] by simp
 
 text{*Every real algebra has characteristic zero*}
 
@@ -341,9 +341,6 @@
 lemma Reals_numeral [simp]: "numeral w \<in> Reals"
 by (subst of_real_numeral [symmetric], rule Reals_of_real)
 
-lemma Reals_neg_numeral [simp]: "neg_numeral w \<in> Reals"
-by (subst of_real_neg_numeral [symmetric], rule Reals_of_real)
-
 lemma Reals_0 [simp]: "0 \<in> Reals"
 apply (unfold Reals_def)
 apply (rule range_eqI)
@@ -602,7 +599,7 @@
 by (subst of_real_numeral [symmetric], subst norm_of_real, simp)
 
 lemma norm_neg_numeral [simp]:
-  "norm (neg_numeral w::'a::real_normed_algebra_1) = numeral w"
+  "norm (- numeral w::'a::real_normed_algebra_1) = numeral w"
 by (subst of_real_neg_numeral [symmetric], subst norm_of_real, simp)
 
 lemma norm_of_int [simp]:
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Rings.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -1058,6 +1058,34 @@
   "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
 by(subst abs_dvd_iff[symmetric]) simp
 
+text {* The following lemmas can be proven in more generale structures, but
+are dangerous as simp rules in absence of @{thm neg_equal_zero}, 
+@{thm neg_less_pos}, @{thm neg_less_eq_nonneg}. *}
+
+lemma equation_minus_iff_1 [simp, no_atp]:
+  "1 = - a \<longleftrightarrow> a = - 1"
+  by (fact equation_minus_iff)
+
+lemma minus_equation_iff_1 [simp, no_atp]:
+  "- a = 1 \<longleftrightarrow> a = - 1"
+  by (subst minus_equation_iff, auto)
+
+lemma le_minus_iff_1 [simp, no_atp]:
+  "1 \<le> - b \<longleftrightarrow> b \<le> - 1"
+  by (fact le_minus_iff)
+
+lemma minus_le_iff_1 [simp, no_atp]:
+  "- a \<le> 1 \<longleftrightarrow> - 1 \<le> a"
+  by (fact minus_le_iff)
+
+lemma less_minus_iff_1 [simp, no_atp]:
+  "1 < - b \<longleftrightarrow> b < - 1"
+  by (fact less_minus_iff)
+
+lemma minus_less_iff_1 [simp, no_atp]:
+  "- a < 1 \<longleftrightarrow> - 1 < a"
+  by (fact minus_less_iff)
+
 end
 
 text {* Simprules for comparisons where common factors can be cancelled. *}
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -374,7 +374,6 @@
 
 lemma
   "(0::int) = 0"
-  "(0::int) = -0"
   "(0::int) = (- 0)"
   "(1::int) = 1"
   "\<not>(-1 = (1::int))"
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/SMT_Examples/SMT_Word_Examples.certs
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.certs	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.certs	Tue Nov 19 10:05:53 2013 +0100
@@ -54,3 +54,5 @@
 unsat
 e5c27ae0a583eeafeaa4ef3c59b1b4ec53e06b0f 1 0
 unsat
+7d3ef49480d3ed3a7e5f2d7a12e7108cf7fc7819 1 0
+unsat
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 19 10:05:53 2013 +0100
@@ -1645,10 +1645,10 @@
         (hol_ctxt as {thy, ctxt, stds, whacks, total_consts, case_names,
                       def_tables, ground_thm_table, ersatz_table, ...}) =
   let
-    fun do_numeral depth Ts mult T t0 t1 =
+    fun do_numeral depth Ts mult T some_t0 t1 t2 =
       (if is_number_type ctxt T then
          let
-           val j = mult * HOLogic.dest_num t1
+           val j = mult * HOLogic.dest_num t2
          in
            if j = 1 then
              raise SAME ()
@@ -1667,15 +1667,16 @@
          handle TERM _ => raise SAME ()
        else
          raise SAME ())
-      handle SAME () => s_betapply [] (do_term depth Ts t0, do_term depth Ts t1)
+      handle SAME () => (case some_t0 of NONE => s_betapply [] (do_term depth Ts t1, do_term depth Ts t2)
+         | SOME t0 => s_betapply [] (do_term depth Ts t0, s_betapply [] (do_term depth Ts t1, do_term depth Ts t2)))
     and do_term depth Ts t =
       case t of
-        (t0 as Const (@{const_name Num.neg_numeral_class.neg_numeral},
-                      Type (@{type_name fun}, [_, ran_T]))) $ t1 =>
-        do_numeral depth Ts ~1 ran_T t0 t1
-      | (t0 as Const (@{const_name Num.numeral_class.numeral},
-                      Type (@{type_name fun}, [_, ran_T]))) $ t1 =>
-        do_numeral depth Ts 1 ran_T t0 t1
+        (t0 as Const (@{const_name uminus}, _) $ ((t1 as Const (@{const_name numeral},
+                      Type (@{type_name fun}, [_, ran_T]))) $ t2)) =>
+        do_numeral depth Ts ~1 ran_T (SOME t0) t1 t2
+      | (t1 as Const (@{const_name numeral},
+                      Type (@{type_name fun}, [_, ran_T]))) $ t2 =>
+        do_numeral depth Ts 1 ran_T NONE t1 t2
       | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
         do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
       | (t0 as Const (@{const_name Sigma}, Type (_, [T1, Type (_, [T2, T3])])))
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Nov 19 10:05:53 2013 +0100
@@ -42,7 +42,6 @@
    @{term "nat"}, @{term "int"},
    @{term "Num.One"}, @{term "Num.Bit0"}, @{term "Num.Bit1"},
    @{term "Num.numeral :: num => int"}, @{term "Num.numeral :: num => nat"},
-   @{term "Num.neg_numeral :: num => int"},
    @{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"},
    @{term "True"}, @{term "False"}];
 
@@ -610,8 +609,6 @@
   | num_of_term vs @{term "1::int"} = Proc.C (Proc.Int_of_integer 1)
   | num_of_term vs (t as Const (@{const_name numeral}, _) $ _) =
       Proc.C (Proc.Int_of_integer (dest_number t))
-  | num_of_term vs (t as Const (@{const_name neg_numeral}, _) $ _) =
-      Proc.Neg (Proc.C (Proc.Int_of_integer (dest_number t)))
   | num_of_term vs (Const (@{const_name Groups.uminus}, _) $ t') =
       Proc.Neg (num_of_term vs t')
   | num_of_term vs (Const (@{const_name Groups.plus}, _) $ t1 $ t2) =
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Tools/SMT/smt_builtin.ML
--- a/src/HOL/Tools/SMT/smt_builtin.ML	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Tue Nov 19 10:05:53 2013 +0100
@@ -144,9 +144,10 @@
   (case try HOLogic.dest_number t of
     NONE => NONE
   | SOME (T, i) =>
-      (case lookup_builtin_typ ctxt T of
-        SOME (_, Int (_, g)) => g T i |> Option.map (rpair T)
-      | _ => NONE))
+      if i < 0 then NONE else
+        (case lookup_builtin_typ ctxt T of
+          SOME (_, Int (_, g)) => g T i |> Option.map (rpair T)
+        | _ => NONE))
 
 val is_builtin_num = is_some oo dest_builtin_num
 
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Nov 19 10:05:53 2013 +0100
@@ -526,23 +526,26 @@
 
 local
   (*
-    rewrite negative numerals into positive numerals,
-    rewrite Numeral0 into 0
     rewrite Numeral1 into 1
+    rewrite - 0 into 0
   *)
 
-  fun is_strange_number ctxt (t as Const (@{const_name neg_numeral}, _) $ _) =
-        SMT_Builtin.is_builtin_num ctxt t
-    | is_strange_number _ _ = false
+  fun is_irregular_number (Const (@{const_name numeral}, _) $ Const (@{const_name num.One}, _)) =
+        true
+    | is_irregular_number (Const (@{const_name uminus}, _) $ Const (@{const_name Groups.zero}, _)) =
+        true
+    | is_irregular_number _ =
+        false;
 
-  val pos_num_ss =
+  fun is_strange_number ctxt t = is_irregular_number t andalso SMT_Builtin.is_builtin_num ctxt t;
+
+  val proper_num_ss =
     simpset_of (put_simpset HOL_ss @{context}
-      addsimps [@{thm Num.numeral_One}]
-      addsimps [@{thm Num.neg_numeral_def}])
+      addsimps @{thms Num.numeral_One minus_zero})
 
   fun norm_num_conv ctxt =
     SMT_Utils.if_conv (is_strange_number ctxt)
-      (Simplifier.rewrite (put_simpset pos_num_ss ctxt)) Conv.no_conv
+      (Simplifier.rewrite (put_simpset proper_num_ss ctxt)) Conv.no_conv
 in
 
 fun normalize_numerals_conv ctxt =
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Tools/SMT/smt_utils.ML
--- a/src/HOL/Tools/SMT/smt_utils.ML	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Tools/SMT/smt_utils.ML	Tue Nov 19 10:05:53 2013 +0100
@@ -140,7 +140,6 @@
           is_num env t andalso is_num env u
       | is_num env (Const (@{const_name Let}, _) $ t $ Abs (_, _, u)) =
           is_num (t :: env) u
-      | is_num env (Const (@{const_name uminus}, _) $ t) = is_num env t
       | is_num env (Bound i) = i < length env andalso is_num env (nth env i)
       | is_num _ t = can HOLogic.dest_number t
   in is_num [] end
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Tools/hologic.ML	Tue Nov 19 10:05:53 2013 +0100
@@ -104,7 +104,6 @@
   val mk_numeral: int -> term
   val dest_num: term -> int
   val numeral_const: typ -> term
-  val neg_numeral_const: typ -> term
   val add_numerals: term -> (term * typ) list -> (term * typ) list
   val mk_number: typ -> int -> term
   val dest_number: term -> typ * int
@@ -548,7 +547,6 @@
   | dest_num t = raise TERM ("dest_num", [t]);
 
 fun numeral_const T = Const ("Num.numeral_class.numeral", numT --> T);
-fun neg_numeral_const T = Const ("Num.neg_numeral_class.neg_numeral", numT --> T);
 
 fun add_numerals (Const ("Num.numeral_class.numeral", Type (_, [_, T])) $ t) = cons (t, T)
   | add_numerals (t $ u) = add_numerals t #> add_numerals u
@@ -559,14 +557,14 @@
   | mk_number T 1 = Const ("Groups.one_class.one", T)
   | mk_number T i =
     if i > 0 then numeral_const T $ mk_numeral i
-    else neg_numeral_const T $ mk_numeral (~ i);
+    else Const ("Groups.uminus_class.uminus", T --> T) $ mk_number T (~ i);
 
 fun dest_number (Const ("Groups.zero_class.zero", T)) = (T, 0)
   | dest_number (Const ("Groups.one_class.one", T)) = (T, 1)
   | dest_number (Const ("Num.numeral_class.numeral", Type ("fun", [_, T])) $ t) =
       (T, dest_num t)
-  | dest_number (Const ("Num.neg_numeral_class.neg_numeral", Type ("fun", [_, T])) $ t) =
-      (T, ~ (dest_num t))
+  | dest_number (Const ("Groups.uminus_class.uminus", Type ("fun", [_, T])) $ t) =
+      apsnd (op ~) (dest_number t)
   | dest_number t = raise TERM ("dest_number", [t]);
 
 
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Tue Nov 19 10:05:53 2013 +0100
@@ -183,9 +183,6 @@
     | demult (t as Const ("Num.numeral_class.numeral", _) $ n, m) =
       ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_num n)))
         handle TERM _ => (SOME t, m))
-    | demult (t as Const ("Num.neg_numeral_class.neg_numeral", _) $ n, m) =
-      ((NONE, Rat.mult m (Rat.rat_of_int (~ (HOLogic.dest_num n))))
-        handle TERM _ => (SOME t, m))
     | demult (t as Const (@{const_name Suc}, _) $ _, m) =
       ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_nat t)))
         handle TERM _ => (SOME t, m))
@@ -212,6 +209,10 @@
         pi
     | poly (Const (@{const_name Groups.one}, _), m, (p, i)) =
         (p, Rat.add i m)
+    | poly (all as Const ("Num.numeral_class.numeral", Type(_,[_,_])) $ t, m, pi as (p, i)) =
+        (let val k = HOLogic.dest_num t
+        in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k))) end
+        handle TERM _ => add_atom all m pi)
     | poly (Const (@{const_name Suc}, _) $ t, m, (p, i)) =
         poly (t, m, (p, Rat.add i m))
     | poly (all as Const (@{const_name Groups.times}, _) $ _ $ _, m, pi as (p, i)) =
@@ -222,14 +223,6 @@
         (case demult inj_consts (all, m) of
            (NONE,   m') => (p, Rat.add i m')
          | (SOME u, m') => add_atom u m' pi)
-    | poly (all as Const ("Num.numeral_class.numeral", Type(_,[_,_])) $ t, m, pi as (p, i)) =
-        (let val k = HOLogic.dest_num t
-        in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k))) end
-        handle TERM _ => add_atom all m pi)
-    | poly (all as Const ("Num.neg_numeral_class.neg_numeral", Type(_,[_,_])) $ t, m, pi as (p, i)) =
-        (let val k = HOLogic.dest_num t
-        in (p, Rat.add i (Rat.mult m (Rat.rat_of_int (~ k)))) end
-        handle TERM _ => add_atom all m pi)
     | poly (all as Const f $ x, m, pi) =
         if member (op =) inj_consts f then poly (x, m, pi) else add_atom all m pi
     | poly (all, m, pi) =
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Tools/numeral.ML
--- a/src/HOL/Tools/numeral.ML	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Tools/numeral.ML	Tue Nov 19 10:05:53 2013 +0100
@@ -45,8 +45,8 @@
 val numeral = @{cpat "numeral"};
 val numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term numeral)));
 
-val neg_numeral = @{cpat "neg_numeral"};
-val neg_numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term neg_numeral)));
+val uminus = @{cpat "uminus"};
+val uminusT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term uminus)));
 
 fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
 
@@ -56,7 +56,7 @@
   | mk_cnumber T 1 = instT T oneT one
   | mk_cnumber T i =
     if i > 0 then Thm.apply (instT T numeralT numeral) (mk_cnumeral i)
-    else Thm.apply (instT T neg_numeralT neg_numeral) (mk_cnumeral (~i));
+    else Thm.apply (instT T uminusT uminus) (Thm.apply (instT T numeralT numeral) (mk_cnumeral (~i)));
 
 end;
 
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Tue Nov 19 10:05:53 2013 +0100
@@ -56,9 +56,6 @@
 val long_mk_sum = Arith_Data.long_mk_sum;
 val dest_sum = Arith_Data.dest_sum;
 
-val mk_diff = HOLogic.mk_binop @{const_name Groups.minus};
-val dest_diff = HOLogic.dest_bin @{const_name Groups.minus} dummyT;
-
 val mk_times = HOLogic.mk_binop @{const_name Groups.times};
 
 fun one_of T = Const(@{const_name Groups.one}, T);
@@ -181,7 +178,7 @@
 
 (*Simplify 0+n, n+0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
 val add_0s =  @{thms add_0s};
-val mult_1s = @{thms mult_1s mult_1_left mult_1_right divide_1};
+val mult_1s = @{thms mult_1s divide_numeral_1 mult_1_left mult_1_right mult_minus1 mult_minus1_right divide_1};
 
 (* For post-simplification of the rhs of simproc-generated rules *)
 val post_simps =
@@ -194,9 +191,8 @@
 val field_post_simps =
     post_simps @ [@{thm divide_zero_left}, @{thm divide_1}]
                       
-(*Simplify inverse Numeral1, a/Numeral1*)
+(*Simplify inverse Numeral1*)
 val inverse_1s = [@{thm inverse_numeral_1}];
-val divide_1s = [@{thm divide_numeral_1}];
 
 (*To perform binary arithmetic.  The "left" rewriting handles patterns
   created by the Numeral_Simprocs, such as 3 * (5 * x). *)
@@ -217,7 +213,7 @@
      @{thms add_neg_numeral_simps}) simps;
 
 (*To evaluate binary negations of coefficients*)
-val minus_simps = [@{thm minus_zero}, @{thm minus_one}, @{thm minus_numeral}, @{thm minus_neg_numeral}];
+val minus_simps = [@{thm minus_zero}, @{thm minus_minus}];
 
 (*To let us treat subtraction as addition*)
 val diff_simps = [@{thm diff_conv_add_uminus}, @{thm minus_add_distrib}, @{thm minus_minus}];
@@ -225,16 +221,13 @@
 (*To let us treat division as multiplication*)
 val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}];
 
-(*push the unary minus down*)
-val minus_mult_eq_1_to_2 = @{lemma "- (a::'a::ring) * b = a * - b" by simp};
-
 (*to extract again any uncancelled minuses*)
 val minus_from_mult_simps =
     [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}];
 
 (*combine unary minus with numeric literals, however nested within a product*)
 val mult_minus_simps =
-    [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2];
+    [@{thm mult_assoc}, @{thm minus_mult_right}, @{thm minus_mult_commute}];
 
 val norm_ss1 =
   simpset_of (put_simpset num_ss @{context}
@@ -247,7 +240,7 @@
 
 val norm_ss3 =
   simpset_of (put_simpset num_ss @{context}
-    addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac})
+    addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac minus_mult_commute})
 
 structure CancelNumeralsCommon =
 struct
@@ -330,7 +323,7 @@
 structure FieldCombineNumeralsData =
 struct
   type coeff = int * int
-  val iszero = (fn (p, q) => p = 0)
+  val iszero = (fn (p, _) => p = 0)
   val add = add_frac
   val mk_sum = long_mk_sum
   val dest_sum = dest_sum
@@ -368,7 +361,7 @@
 
 structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
 struct
-  val assoc_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac})
+  val assoc_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac minus_mult_commute})
   val eq_reflection = eq_reflection
   val is_numeral = can HOLogic.dest_number
 end;
@@ -388,7 +381,7 @@
   val norm_ss2 =
     simpset_of (put_simpset HOL_basic_ss @{context} addsimps simps @ mult_minus_simps)
   val norm_ss3 =
-    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac})
+    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac minus_mult_commute})
   fun norm_tac ctxt =
     ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
     THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
@@ -463,9 +456,9 @@
      ["((l::'a::field_inverse_zero) * m) / n",
       "(l::'a::field_inverse_zero) / (m * n)",
       "((numeral v)::'a::field_inverse_zero) / (numeral w)",
-      "((numeral v)::'a::field_inverse_zero) / (neg_numeral w)",
-      "((neg_numeral v)::'a::field_inverse_zero) / (numeral w)",
-      "((neg_numeral v)::'a::field_inverse_zero) / (neg_numeral w)"],
+      "((numeral v)::'a::field_inverse_zero) / (- numeral w)",
+      "((- numeral v)::'a::field_inverse_zero) / (numeral w)",
+      "((- numeral v)::'a::field_inverse_zero) / (- numeral w)"],
      DivideCancelNumeralFactor.proc)]
 
 
@@ -516,7 +509,7 @@
   val find_first = find_first_t []
   val trans_tac = trans_tac
   val norm_ss =
-    simpset_of (put_simpset HOL_basic_ss @{context} addsimps mult_1s @ @{thms mult_ac})
+    simpset_of (put_simpset HOL_basic_ss @{context} addsimps mult_1s @ @{thms mult_ac minus_mult_commute})
   fun norm_tac ctxt =
     ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
   val simplify_meta_eq  = cancel_simplify_meta_eq 
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Transcendental.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -2000,8 +2000,8 @@
   apply (subst powr_add, simp, simp)
   done
 
-lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x^(numeral n)"
-  unfolding real_of_nat_numeral[symmetric] by (rule powr_realpow)
+lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
+  unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow)
 
 lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))"
   apply (case_tac "x = 0", simp, simp)
@@ -2020,11 +2020,17 @@
   then show ?thesis by (simp add: assms powr_realpow[symmetric])
 qed
 
-lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x^numeral n"
-  using powr_realpow[of x "numeral n"] by simp
-
-lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr neg_numeral n = 1 / x^numeral n"
-  using powr_int[of x "neg_numeral n"] by simp
+lemma powr_one: "0 < x \<Longrightarrow> x powr 1 = x"
+  using powr_realpow [of x 1] by simp
+
+lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x ^ numeral n"
+  by (fact powr_realpow_numeral)
+
+lemma powr_neg_one: "0 < x \<Longrightarrow> x powr - 1 = 1 / x"
+  using powr_int [of x "- 1"] by simp
+
+lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr - numeral n = 1 / x ^ numeral n"
+  using powr_int [of x "- numeral n"] by simp
 
 lemma root_powr_inverse: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
   by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
@@ -4047,7 +4053,7 @@
   show "sgn x * pi / 2 - arctan x < pi / 2"
     using arctan_bounded [of "- x"] assms
     unfolding sgn_real_def arctan_minus
-    by auto
+    by (auto simp add: algebra_simps)
   show "tan (sgn x * pi / 2 - arctan x) = 1 / x"
     unfolding tan_inverse [of "arctan x", unfolded tan_arctan]
     unfolding sgn_real_def
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Word/Bit_Int.thy
--- a/src/HOL/Word/Bit_Int.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Word/Bit_Int.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -52,10 +52,10 @@
 lemma int_not_simps [simp]:
   "NOT (0::int) = -1"
   "NOT (1::int) = -2"
-  "NOT (-1::int) = 0"
-  "NOT (numeral w::int) = neg_numeral (w + Num.One)"
-  "NOT (neg_numeral (Num.Bit0 w)::int) = numeral (Num.BitM w)"
-  "NOT (neg_numeral (Num.Bit1 w)::int) = numeral (Num.Bit0 w)"
+  "NOT (- 1::int) = 0"
+  "NOT (numeral w::int) = - numeral (w + Num.One)"
+  "NOT (- numeral (Num.Bit0 w)::int) = numeral (Num.BitM w)"
+  "NOT (- numeral (Num.Bit1 w)::int) = numeral (Num.Bit0 w)"
   unfolding int_not_def by simp_all
 
 lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
@@ -228,11 +228,11 @@
   by (metis bin_rl_simp)
 
 lemma bin_rest_neg_numeral_BitM [simp]:
-  "bin_rest (neg_numeral (Num.BitM w)) = neg_numeral w"
+  "bin_rest (- numeral (Num.BitM w)) = - numeral w"
   by (simp only: BIT_bin_simps [symmetric] bin_rest_BIT)
 
 lemma bin_last_neg_numeral_BitM [simp]:
-  "bin_last (neg_numeral (Num.BitM w)) = 1"
+  "bin_last (-  numeral (Num.BitM w)) = 1"
   by (simp only: BIT_bin_simps [symmetric] bin_last_BIT)
 
 text {* FIXME: The rule sets below are very large (24 rules for each
@@ -243,26 +243,26 @@
   "numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT 0"
   "numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT 0"
   "numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT 1"
-  "numeral (Num.Bit0 x) AND neg_numeral (Num.Bit0 y) = (numeral x AND neg_numeral y) BIT 0"
-  "numeral (Num.Bit0 x) AND neg_numeral (Num.Bit1 y) = (numeral x AND neg_numeral (y + Num.One)) BIT 0"
-  "numeral (Num.Bit1 x) AND neg_numeral (Num.Bit0 y) = (numeral x AND neg_numeral y) BIT 0"
-  "numeral (Num.Bit1 x) AND neg_numeral (Num.Bit1 y) = (numeral x AND neg_numeral (y + Num.One)) BIT 1"
-  "neg_numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (neg_numeral x AND numeral y) BIT 0"
-  "neg_numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (neg_numeral x AND numeral y) BIT 0"
-  "neg_numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) AND numeral y) BIT 0"
-  "neg_numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) AND numeral y) BIT 1"
-  "neg_numeral (Num.Bit0 x) AND neg_numeral (Num.Bit0 y) = (neg_numeral x AND neg_numeral y) BIT 0"
-  "neg_numeral (Num.Bit0 x) AND neg_numeral (Num.Bit1 y) = (neg_numeral x AND neg_numeral (y + Num.One)) BIT 0"
-  "neg_numeral (Num.Bit1 x) AND neg_numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) AND neg_numeral y) BIT 0"
-  "neg_numeral (Num.Bit1 x) AND neg_numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) AND neg_numeral (y + Num.One)) BIT 1"
+  "numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT 0"
+  "numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT 0"
+  "numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT 0"
+  "numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT 1"
+  "- numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (- numeral x AND numeral y) BIT 0"
+  "- numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (- numeral x AND numeral y) BIT 0"
+  "- numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND numeral y) BIT 0"
+  "- numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND numeral y) BIT 1"
+  "- numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (- numeral x AND - numeral y) BIT 0"
+  "- numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (- numeral x AND - numeral (y + Num.One)) BIT 0"
+  "- numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND - numeral y) BIT 0"
+  "- numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND - numeral (y + Num.One)) BIT 1"
   "(1::int) AND numeral (Num.Bit0 y) = 0"
   "(1::int) AND numeral (Num.Bit1 y) = 1"
-  "(1::int) AND neg_numeral (Num.Bit0 y) = 0"
-  "(1::int) AND neg_numeral (Num.Bit1 y) = 1"
+  "(1::int) AND - numeral (Num.Bit0 y) = 0"
+  "(1::int) AND - numeral (Num.Bit1 y) = 1"
   "numeral (Num.Bit0 x) AND (1::int) = 0"
   "numeral (Num.Bit1 x) AND (1::int) = 1"
-  "neg_numeral (Num.Bit0 x) AND (1::int) = 0"
-  "neg_numeral (Num.Bit1 x) AND (1::int) = 1"
+  "- numeral (Num.Bit0 x) AND (1::int) = 0"
+  "- numeral (Num.Bit1 x) AND (1::int) = 1"
   by (rule bin_rl_eqI, simp, simp)+
 
 lemma int_or_numerals [simp]:
@@ -270,26 +270,26 @@
   "numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT 1"
   "numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT 1"
   "numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT 1"
-  "numeral (Num.Bit0 x) OR neg_numeral (Num.Bit0 y) = (numeral x OR neg_numeral y) BIT 0"
-  "numeral (Num.Bit0 x) OR neg_numeral (Num.Bit1 y) = (numeral x OR neg_numeral (y + Num.One)) BIT 1"
-  "numeral (Num.Bit1 x) OR neg_numeral (Num.Bit0 y) = (numeral x OR neg_numeral y) BIT 1"
-  "numeral (Num.Bit1 x) OR neg_numeral (Num.Bit1 y) = (numeral x OR neg_numeral (y + Num.One)) BIT 1"
-  "neg_numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (neg_numeral x OR numeral y) BIT 0"
-  "neg_numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (neg_numeral x OR numeral y) BIT 1"
-  "neg_numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) OR numeral y) BIT 1"
-  "neg_numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) OR numeral y) BIT 1"
-  "neg_numeral (Num.Bit0 x) OR neg_numeral (Num.Bit0 y) = (neg_numeral x OR neg_numeral y) BIT 0"
-  "neg_numeral (Num.Bit0 x) OR neg_numeral (Num.Bit1 y) = (neg_numeral x OR neg_numeral (y + Num.One)) BIT 1"
-  "neg_numeral (Num.Bit1 x) OR neg_numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) OR neg_numeral y) BIT 1"
-  "neg_numeral (Num.Bit1 x) OR neg_numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) OR neg_numeral (y + Num.One)) BIT 1"
+  "numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT 0"
+  "numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT 1"
+  "numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT 1"
+  "numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT 1"
+  "- numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (- numeral x OR numeral y) BIT 0"
+  "- numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (- numeral x OR numeral y) BIT 1"
+  "- numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR numeral y) BIT 1"
+  "- numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR numeral y) BIT 1"
+  "- numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (- numeral x OR - numeral y) BIT 0"
+  "- numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (- numeral x OR - numeral (y + Num.One)) BIT 1"
+  "- numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR - numeral y) BIT 1"
+  "- numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR - numeral (y + Num.One)) BIT 1"
   "(1::int) OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
   "(1::int) OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)"
-  "(1::int) OR neg_numeral (Num.Bit0 y) = neg_numeral (Num.BitM y)"
-  "(1::int) OR neg_numeral (Num.Bit1 y) = neg_numeral (Num.Bit1 y)"
+  "(1::int) OR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
+  "(1::int) OR - numeral (Num.Bit1 y) = - numeral (Num.Bit1 y)"
   "numeral (Num.Bit0 x) OR (1::int) = numeral (Num.Bit1 x)"
   "numeral (Num.Bit1 x) OR (1::int) = numeral (Num.Bit1 x)"
-  "neg_numeral (Num.Bit0 x) OR (1::int) = neg_numeral (Num.BitM x)"
-  "neg_numeral (Num.Bit1 x) OR (1::int) = neg_numeral (Num.Bit1 x)"
+  "- numeral (Num.Bit0 x) OR (1::int) = - numeral (Num.BitM x)"
+  "- numeral (Num.Bit1 x) OR (1::int) = - numeral (Num.Bit1 x)"
   by (rule bin_rl_eqI, simp, simp)+
 
 lemma int_xor_numerals [simp]:
@@ -297,26 +297,26 @@
   "numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT 1"
   "numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT 1"
   "numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT 0"
-  "numeral (Num.Bit0 x) XOR neg_numeral (Num.Bit0 y) = (numeral x XOR neg_numeral y) BIT 0"
-  "numeral (Num.Bit0 x) XOR neg_numeral (Num.Bit1 y) = (numeral x XOR neg_numeral (y + Num.One)) BIT 1"
-  "numeral (Num.Bit1 x) XOR neg_numeral (Num.Bit0 y) = (numeral x XOR neg_numeral y) BIT 1"
-  "numeral (Num.Bit1 x) XOR neg_numeral (Num.Bit1 y) = (numeral x XOR neg_numeral (y + Num.One)) BIT 0"
-  "neg_numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (neg_numeral x XOR numeral y) BIT 0"
-  "neg_numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (neg_numeral x XOR numeral y) BIT 1"
-  "neg_numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) XOR numeral y) BIT 1"
-  "neg_numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) XOR numeral y) BIT 0"
-  "neg_numeral (Num.Bit0 x) XOR neg_numeral (Num.Bit0 y) = (neg_numeral x XOR neg_numeral y) BIT 0"
-  "neg_numeral (Num.Bit0 x) XOR neg_numeral (Num.Bit1 y) = (neg_numeral x XOR neg_numeral (y + Num.One)) BIT 1"
-  "neg_numeral (Num.Bit1 x) XOR neg_numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) XOR neg_numeral y) BIT 1"
-  "neg_numeral (Num.Bit1 x) XOR neg_numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) XOR neg_numeral (y + Num.One)) BIT 0"
+  "numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT 0"
+  "numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT 1"
+  "numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT 1"
+  "numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT 0"
+  "- numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (- numeral x XOR numeral y) BIT 0"
+  "- numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (- numeral x XOR numeral y) BIT 1"
+  "- numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR numeral y) BIT 1"
+  "- numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR numeral y) BIT 0"
+  "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (- numeral x XOR - numeral y) BIT 0"
+  "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (- numeral x XOR - numeral (y + Num.One)) BIT 1"
+  "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR - numeral y) BIT 1"
+  "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR - numeral (y + Num.One)) BIT 0"
   "(1::int) XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
   "(1::int) XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)"
-  "(1::int) XOR neg_numeral (Num.Bit0 y) = neg_numeral (Num.BitM y)"
-  "(1::int) XOR neg_numeral (Num.Bit1 y) = neg_numeral (Num.Bit0 (y + Num.One))"
+  "(1::int) XOR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
+  "(1::int) XOR - numeral (Num.Bit1 y) = - numeral (Num.Bit0 (y + Num.One))"
   "numeral (Num.Bit0 x) XOR (1::int) = numeral (Num.Bit1 x)"
   "numeral (Num.Bit1 x) XOR (1::int) = numeral (Num.Bit0 x)"
-  "neg_numeral (Num.Bit0 x) XOR (1::int) = neg_numeral (Num.BitM x)"
-  "neg_numeral (Num.Bit1 x) XOR (1::int) = neg_numeral (Num.Bit0 (x + Num.One))"
+  "- numeral (Num.Bit0 x) XOR (1::int) = - numeral (Num.BitM x)"
+  "- numeral (Num.Bit1 x) XOR (1::int) = - numeral (Num.Bit0 (x + Num.One))"
   by (rule bin_rl_eqI, simp, simp)+
 
 subsubsection {* Interactions with arithmetic *}
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -61,21 +61,23 @@
 lemma BIT_bin_simps [simp]:
   "numeral k BIT 0 = numeral (Num.Bit0 k)"
   "numeral k BIT 1 = numeral (Num.Bit1 k)"
-  "neg_numeral k BIT 0 = neg_numeral (Num.Bit0 k)"
-  "neg_numeral k BIT 1 = neg_numeral (Num.BitM k)"
-  unfolding neg_numeral_def numeral.simps numeral_BitM
+  "(- numeral k) BIT 0 = - numeral (Num.Bit0 k)"
+  "(- numeral k) BIT 1 = - numeral (Num.BitM k)"
+  unfolding numeral.simps numeral_BitM
   unfolding Bit_def bitval_simps
   by (simp_all del: arith_simps add_numeral_special diff_numeral_special)
 
 lemma BIT_special_simps [simp]:
-  shows "0 BIT 0 = 0" and "0 BIT 1 = 1" and "1 BIT 0 = 2" and "1 BIT 1 = 3"
+  shows "0 BIT 0 = 0" and "0 BIT 1 = 1"
+  and "1 BIT 0 = 2" and "1 BIT 1 = 3"
+  and "(- 1) BIT 0 = - 2" and "(- 1) BIT 1 = - 1"
   unfolding Bit_def by simp_all
 
 lemma Bit_eq_0_iff: "w BIT b = 0 \<longleftrightarrow> w = 0 \<and> b = 0"
   by (subst BIT_eq_iff [symmetric], simp)
 
-lemma Bit_eq_m1_iff: "w BIT b = -1 \<longleftrightarrow> w = -1 \<and> b = 1"
-  by (subst BIT_eq_iff [symmetric], simp)
+lemma Bit_eq_m1_iff: "w BIT b = - 1 \<longleftrightarrow> w = - 1 \<and> b = 1"
+  by (cases b) (auto simp add: Bit_def, arith)
 
 lemma BitM_inc: "Num.BitM (Num.inc w) = Num.Bit1 w"
   by (induct w, simp_all)
@@ -83,8 +85,8 @@
 lemma expand_BIT:
   "numeral (Num.Bit0 w) = numeral w BIT 0"
   "numeral (Num.Bit1 w) = numeral w BIT 1"
-  "neg_numeral (Num.Bit0 w) = neg_numeral w BIT 0"
-  "neg_numeral (Num.Bit1 w) = neg_numeral (w + Num.One) BIT 1"
+  "- numeral (Num.Bit0 w) = - numeral w BIT 0"
+  "- numeral (Num.Bit1 w) = (- numeral (w + Num.One)) BIT 1"
   unfolding add_One by (simp_all add: BitM_inc)
 
 lemma bin_last_numeral_simps [simp]:
@@ -94,9 +96,9 @@
   "bin_last Numeral1 = 1"
   "bin_last (numeral (Num.Bit0 w)) = 0"
   "bin_last (numeral (Num.Bit1 w)) = 1"
-  "bin_last (neg_numeral (Num.Bit0 w)) = 0"
-  "bin_last (neg_numeral (Num.Bit1 w)) = 1"
-  unfolding expand_BIT bin_last_BIT by (simp_all add: bin_last_def)
+  "bin_last (- numeral (Num.Bit0 w)) = 0"
+  "bin_last (- numeral (Num.Bit1 w)) = 1"
+  unfolding expand_BIT bin_last_BIT by (simp_all add: bin_last_def zmod_zminus1_eq_if)
 
 lemma bin_rest_numeral_simps [simp]:
   "bin_rest 0 = 0"
@@ -105,9 +107,9 @@
   "bin_rest Numeral1 = 0"
   "bin_rest (numeral (Num.Bit0 w)) = numeral w"
   "bin_rest (numeral (Num.Bit1 w)) = numeral w"
-  "bin_rest (neg_numeral (Num.Bit0 w)) = neg_numeral w"
-  "bin_rest (neg_numeral (Num.Bit1 w)) = neg_numeral (w + Num.One)"
-  unfolding expand_BIT bin_rest_BIT by (simp_all add: bin_rest_def)
+  "bin_rest (- numeral (Num.Bit0 w)) = - numeral w"
+  "bin_rest (- numeral (Num.Bit1 w)) = - numeral (w + Num.One)"
+  unfolding expand_BIT bin_rest_BIT by (simp_all add: bin_rest_def zdiv_zminus1_eq_if)
 
 lemma less_Bits: 
   "(v BIT b < w BIT c) = (v < w | v <= w & b = (0::bit) & c = (1::bit))"
@@ -197,42 +199,45 @@
 lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
   unfolding bin_rest_def [symmetric] by (rule bin_rest_BIT)
 
-lemma bin_nth_lem [rule_format]:
-  "ALL y. bin_nth x = bin_nth y --> x = y"
-  apply (induct x rule: bin_induct)
-    apply safe
-    apply (erule rev_mp)
-    apply (induct_tac y rule: bin_induct)
+lemma bin_nth_eq_iff:
+  "bin_nth x = bin_nth y \<longleftrightarrow> x = y"
+proof -
+  have bin_nth_lem [rule_format]: "ALL y. bin_nth x = bin_nth y --> x = y"
+    apply (induct x rule: bin_induct)
       apply safe
-      apply (drule_tac x=0 in fun_cong, force)
-     apply (erule notE, rule ext, 
+      apply (erule rev_mp)
+      apply (induct_tac y rule: bin_induct)
+        apply safe
+        apply (drule_tac x=0 in fun_cong, force)
+       apply (erule notE, rule ext, 
             drule_tac x="Suc x" in fun_cong, force)
-    apply (drule_tac x=0 in fun_cong, force)
-   apply (erule rev_mp)
-   apply (induct_tac y rule: bin_induct)
-     apply safe
+      apply (drule_tac x=0 in fun_cong, force)
+     apply (erule rev_mp)
+     apply (induct_tac y rule: bin_induct)
+       apply safe
+       apply (drule_tac x=0 in fun_cong, force)
+      apply (erule notE, rule ext, 
+           drule_tac x="Suc x" in fun_cong, force)
+      apply (metis Bit_eq_m1_iff Z bin_last_BIT)
+    apply (case_tac y rule: bin_exhaust)
+    apply clarify
+    apply (erule allE)
+    apply (erule impE)
+     prefer 2
+     apply (erule conjI)
      apply (drule_tac x=0 in fun_cong, force)
-    apply (erule notE, rule ext, 
-           drule_tac x="Suc x" in fun_cong, force)
-   apply (drule_tac x=0 in fun_cong, force)
-  apply (case_tac y rule: bin_exhaust)
-  apply clarify
-  apply (erule allE)
-  apply (erule impE)
-   prefer 2
-   apply (erule conjI)
-   apply (drule_tac x=0 in fun_cong, force)
-  apply (rule ext)
-  apply (drule_tac x="Suc ?x" in fun_cong, force)
-  done
-
-lemma bin_nth_eq_iff: "(bin_nth x = bin_nth y) = (x = y)"
+    apply (rule ext)
+    apply (drule_tac x="Suc ?x" in fun_cong, force)
+    done
+  show ?thesis
   by (auto elim: bin_nth_lem)
+qed
 
 lemmas bin_eqI = ext [THEN bin_nth_eq_iff [THEN iffD1]]
 
-lemma bin_eq_iff: "x = y \<longleftrightarrow> (\<forall>n. bin_nth x n = bin_nth y n)"
-  by (auto intro!: bin_nth_lem del: equalityI)
+lemma bin_eq_iff:
+  "x = y \<longleftrightarrow> (\<forall>n. bin_nth x n = bin_nth y n)"
+  using bin_nth_eq_iff by auto
 
 lemma bin_nth_zero [simp]: "\<not> bin_nth 0 n"
   by (induct n) auto
@@ -276,8 +281,9 @@
 lemma bin_sign_simps [simp]:
   "bin_sign 0 = 0"
   "bin_sign 1 = 0"
+  "bin_sign (- 1) = - 1"
   "bin_sign (numeral k) = 0"
-  "bin_sign (neg_numeral k) = -1"
+  "bin_sign (- numeral k) = -1"
   "bin_sign (w BIT b) = bin_sign w"
   unfolding bin_sign_def Bit_def bitval_def
   by (simp_all split: bit.split)
@@ -331,18 +337,18 @@
   "bintrunc (Suc n) -1 = bintrunc n -1 BIT 1"
   "bintrunc (Suc n) (numeral (Num.Bit0 w)) = bintrunc n (numeral w) BIT 0"
   "bintrunc (Suc n) (numeral (Num.Bit1 w)) = bintrunc n (numeral w) BIT 1"
-  "bintrunc (Suc n) (neg_numeral (Num.Bit0 w)) =
-    bintrunc n (neg_numeral w) BIT 0"
-  "bintrunc (Suc n) (neg_numeral (Num.Bit1 w)) =
-    bintrunc n (neg_numeral (w + Num.One)) BIT 1"
+  "bintrunc (Suc n) (- numeral (Num.Bit0 w)) =
+    bintrunc n (- numeral w) BIT 0"
+  "bintrunc (Suc n) (- numeral (Num.Bit1 w)) =
+    bintrunc n (- numeral (w + Num.One)) BIT 1"
   by simp_all
 
 lemma sbintrunc_0_numeral [simp]:
   "sbintrunc 0 1 = -1"
   "sbintrunc 0 (numeral (Num.Bit0 w)) = 0"
   "sbintrunc 0 (numeral (Num.Bit1 w)) = -1"
-  "sbintrunc 0 (neg_numeral (Num.Bit0 w)) = 0"
-  "sbintrunc 0 (neg_numeral (Num.Bit1 w)) = -1"
+  "sbintrunc 0 (- numeral (Num.Bit0 w)) = 0"
+  "sbintrunc 0 (- numeral (Num.Bit1 w)) = -1"
   by simp_all
 
 lemma sbintrunc_Suc_numeral:
@@ -351,10 +357,10 @@
     sbintrunc n (numeral w) BIT 0"
   "sbintrunc (Suc n) (numeral (Num.Bit1 w)) =
     sbintrunc n (numeral w) BIT 1"
-  "sbintrunc (Suc n) (neg_numeral (Num.Bit0 w)) =
-    sbintrunc n (neg_numeral w) BIT 0"
-  "sbintrunc (Suc n) (neg_numeral (Num.Bit1 w)) =
-    sbintrunc n (neg_numeral (w + Num.One)) BIT 1"
+  "sbintrunc (Suc n) (- numeral (Num.Bit0 w)) =
+    sbintrunc n (- numeral w) BIT 0"
+  "sbintrunc (Suc n) (- numeral (Num.Bit1 w)) =
+    sbintrunc n (- numeral (w + Num.One)) BIT 1"
   by simp_all
 
 lemma bit_bool:
@@ -580,10 +586,10 @@
     bintrunc (pred_numeral k) (numeral w) BIT 0"
   "bintrunc (numeral k) (numeral (Num.Bit1 w)) =
     bintrunc (pred_numeral k) (numeral w) BIT 1"
-  "bintrunc (numeral k) (neg_numeral (Num.Bit0 w)) =
-    bintrunc (pred_numeral k) (neg_numeral w) BIT 0"
-  "bintrunc (numeral k) (neg_numeral (Num.Bit1 w)) =
-    bintrunc (pred_numeral k) (neg_numeral (w + Num.One)) BIT 1"
+  "bintrunc (numeral k) (- numeral (Num.Bit0 w)) =
+    bintrunc (pred_numeral k) (- numeral w) BIT 0"
+  "bintrunc (numeral k) (- numeral (Num.Bit1 w)) =
+    bintrunc (pred_numeral k) (- numeral (w + Num.One)) BIT 1"
   "bintrunc (numeral k) 1 = 1"
   by (simp_all add: bintrunc_numeral)
 
@@ -592,10 +598,10 @@
     sbintrunc (pred_numeral k) (numeral w) BIT 0"
   "sbintrunc (numeral k) (numeral (Num.Bit1 w)) =
     sbintrunc (pred_numeral k) (numeral w) BIT 1"
-  "sbintrunc (numeral k) (neg_numeral (Num.Bit0 w)) =
-    sbintrunc (pred_numeral k) (neg_numeral w) BIT 0"
-  "sbintrunc (numeral k) (neg_numeral (Num.Bit1 w)) =
-    sbintrunc (pred_numeral k) (neg_numeral (w + Num.One)) BIT 1"
+  "sbintrunc (numeral k) (- numeral (Num.Bit0 w)) =
+    sbintrunc (pred_numeral k) (- numeral w) BIT 0"
+  "sbintrunc (numeral k) (- numeral (Num.Bit1 w)) =
+    sbintrunc (pred_numeral k) (- numeral (w + Num.One)) BIT 1"
   "sbintrunc (numeral k) 1 = 1"
   by (simp_all add: sbintrunc_numeral)
 
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Word/Word.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -591,24 +591,24 @@
 declare word_numeral_alt [symmetric, code_abbrev]
 
 lemma word_neg_numeral_alt:
-  "neg_numeral b = word_of_int (neg_numeral b)"
-  by (simp only: neg_numeral_def word_numeral_alt wi_hom_neg)
+  "- numeral b = word_of_int (- numeral b)"
+  by (simp only: word_numeral_alt wi_hom_neg)
 
 declare word_neg_numeral_alt [symmetric, code_abbrev]
 
 lemma word_numeral_transfer [transfer_rule]:
   "(fun_rel op = pcr_word) numeral numeral"
-  "(fun_rel op = pcr_word) neg_numeral neg_numeral"
-  unfolding fun_rel_def word.pcr_cr_eq cr_word_def word_numeral_alt word_neg_numeral_alt
-  by simp_all
+  "(fun_rel op = pcr_word) (- numeral) (- numeral)"
+  apply (simp_all add: fun_rel_def word.pcr_cr_eq cr_word_def)
+  using word_numeral_alt [symmetric] word_neg_numeral_alt [symmetric] by blast+
 
 lemma uint_bintrunc [simp]:
   "uint (numeral bin :: 'a word) = 
     bintrunc (len_of TYPE ('a :: len0)) (numeral bin)"
   unfolding word_numeral_alt by (rule word_ubin.eq_norm)
 
-lemma uint_bintrunc_neg [simp]: "uint (neg_numeral bin :: 'a word) = 
-    bintrunc (len_of TYPE ('a :: len0)) (neg_numeral bin)"
+lemma uint_bintrunc_neg [simp]: "uint (- numeral bin :: 'a word) = 
+    bintrunc (len_of TYPE ('a :: len0)) (- numeral bin)"
   by (simp only: word_neg_numeral_alt word_ubin.eq_norm)
 
 lemma sint_sbintrunc [simp]:
@@ -616,8 +616,8 @@
     sbintrunc (len_of TYPE ('a :: len) - 1) (numeral bin)"
   by (simp only: word_numeral_alt word_sbin.eq_norm)
 
-lemma sint_sbintrunc_neg [simp]: "sint (neg_numeral bin :: 'a word) = 
-    sbintrunc (len_of TYPE ('a :: len) - 1) (neg_numeral bin)"
+lemma sint_sbintrunc_neg [simp]: "sint (- numeral bin :: 'a word) = 
+    sbintrunc (len_of TYPE ('a :: len) - 1) (- numeral bin)"
   by (simp only: word_neg_numeral_alt word_sbin.eq_norm)
 
 lemma unat_bintrunc [simp]:
@@ -626,8 +626,8 @@
   by (simp only: unat_def uint_bintrunc)
 
 lemma unat_bintrunc_neg [simp]:
-  "unat (neg_numeral bin :: 'a :: len0 word) =
-    nat (bintrunc (len_of TYPE('a)) (neg_numeral bin))"
+  "unat (- numeral bin :: 'a :: len0 word) =
+    nat (bintrunc (len_of TYPE('a)) (- numeral bin))"
   by (simp only: unat_def uint_bintrunc_neg)
 
 lemma size_0_eq: "size (w :: 'a :: len0 word) = 0 \<Longrightarrow> v = w"
@@ -678,7 +678,7 @@
   by (simp only: int_word_uint)
 
 lemma uint_neg_numeral:
-  "uint (neg_numeral b :: 'a :: len0 word) = neg_numeral b mod 2 ^ len_of TYPE('a)"
+  "uint (- numeral b :: 'a :: len0 word) = - numeral b mod 2 ^ len_of TYPE('a)"
   unfolding word_neg_numeral_alt
   by (simp only: int_word_uint)
 
@@ -702,13 +702,16 @@
 lemma word_of_int_1 [simp, code_post]: "word_of_int 1 = 1"
   unfolding word_1_wi ..
 
+lemma word_of_int_neg_1 [simp]: "word_of_int (- 1) = - 1"
+  by (simp add: wi_hom_syms)
+
 lemma word_of_int_numeral [simp] : 
   "(word_of_int (numeral bin) :: 'a :: len0 word) = (numeral bin)"
   unfolding word_numeral_alt ..
 
 lemma word_of_int_neg_numeral [simp]:
-  "(word_of_int (neg_numeral bin) :: 'a :: len0 word) = (neg_numeral bin)"
-  unfolding neg_numeral_def word_numeral_alt wi_hom_syms ..
+  "(word_of_int (- numeral bin) :: 'a :: len0 word) = (- numeral bin)"
+  unfolding word_numeral_alt wi_hom_syms ..
 
 lemma word_int_case_wi: 
   "word_int_case f (word_of_int i :: 'b word) = 
@@ -880,8 +883,8 @@
   unfolding word_numeral_alt by (rule to_bl_of_bin)
 
 lemma to_bl_neg_numeral [simp]:
-  "to_bl (neg_numeral bin::'a::len0 word) =
-    bin_to_bl (len_of TYPE('a)) (neg_numeral bin)"
+  "to_bl (- numeral bin::'a::len0 word) =
+    bin_to_bl (len_of TYPE('a)) (- numeral bin)"
   unfolding word_neg_numeral_alt by (rule to_bl_of_bin)
 
 lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"
@@ -1156,11 +1159,8 @@
 
 lemmas word_sle_no [simp] = word_sle_def [of "numeral a" "numeral b"] for a b
 
-lemma word_1_no: "(1::'a::len0 word) = Numeral1"
-  by (simp add: word_numeral_alt)
-
-lemma word_m1_wi: "-1 = word_of_int -1" 
-  by (rule word_neg_numeral_alt)
+lemma word_m1_wi: "- 1 = word_of_int (- 1)" 
+  using word_neg_numeral_alt [of Num.One] by simp
 
 lemma word_0_bl [simp]: "of_bl [] = 0"
   unfolding of_bl_def by simp
@@ -1215,9 +1215,9 @@
   unfolding scast_def by simp
 
 lemma sint_n1 [simp] : "sint -1 = -1"
-  unfolding word_m1_wi by (simp add: word_sbin.eq_norm)
-
-lemma scast_n1 [simp]: "scast -1 = -1"
+  unfolding word_m1_wi word_sbin.eq_norm by simp
+
+lemma scast_n1 [simp]: "scast (- 1) = - 1"
   unfolding scast_def by simp
 
 lemma uint_1 [simp]: "uint (1::'a::len word) = 1"
@@ -1270,8 +1270,8 @@
 lemma succ_pred_no [simp]:
   "word_succ (numeral w) = numeral w + 1"
   "word_pred (numeral w) = numeral w - 1"
-  "word_succ (neg_numeral w) = neg_numeral w + 1"
-  "word_pred (neg_numeral w) = neg_numeral w - 1"
+  "word_succ (- numeral w) = - numeral w + 1"
+  "word_pred (- numeral w) = - numeral w - 1"
   unfolding word_succ_p1 word_pred_m1 by simp_all
 
 lemma word_sp_01 [simp] : 
@@ -2151,19 +2151,19 @@
 
 lemma word_no_log_defs [simp]:
   "NOT (numeral a) = word_of_int (NOT (numeral a))"
-  "NOT (neg_numeral a) = word_of_int (NOT (neg_numeral a))"
+  "NOT (- numeral a) = word_of_int (NOT (- numeral a))"
   "numeral a AND numeral b = word_of_int (numeral a AND numeral b)"
-  "numeral a AND neg_numeral b = word_of_int (numeral a AND neg_numeral b)"
-  "neg_numeral a AND numeral b = word_of_int (neg_numeral a AND numeral b)"
-  "neg_numeral a AND neg_numeral b = word_of_int (neg_numeral a AND neg_numeral b)"
+  "numeral a AND - numeral b = word_of_int (numeral a AND - numeral b)"
+  "- numeral a AND numeral b = word_of_int (- numeral a AND numeral b)"
+  "- numeral a AND - numeral b = word_of_int (- numeral a AND - numeral b)"
   "numeral a OR numeral b = word_of_int (numeral a OR numeral b)"
-  "numeral a OR neg_numeral b = word_of_int (numeral a OR neg_numeral b)"
-  "neg_numeral a OR numeral b = word_of_int (neg_numeral a OR numeral b)"
-  "neg_numeral a OR neg_numeral b = word_of_int (neg_numeral a OR neg_numeral b)"
+  "numeral a OR - numeral b = word_of_int (numeral a OR - numeral b)"
+  "- numeral a OR numeral b = word_of_int (- numeral a OR numeral b)"
+  "- numeral a OR - numeral b = word_of_int (- numeral a OR - numeral b)"
   "numeral a XOR numeral b = word_of_int (numeral a XOR numeral b)"
-  "numeral a XOR neg_numeral b = word_of_int (numeral a XOR neg_numeral b)"
-  "neg_numeral a XOR numeral b = word_of_int (neg_numeral a XOR numeral b)"
-  "neg_numeral a XOR neg_numeral b = word_of_int (neg_numeral a XOR neg_numeral b)"
+  "numeral a XOR - numeral b = word_of_int (numeral a XOR - numeral b)"
+  "- numeral a XOR numeral b = word_of_int (- numeral a XOR numeral b)"
+  "- numeral a XOR - numeral b = word_of_int (- numeral a XOR - numeral b)"
   by (transfer, rule refl)+
 
 text {* Special cases for when one of the arguments equals 1. *}
@@ -2171,17 +2171,17 @@
 lemma word_bitwise_1_simps [simp]:
   "NOT (1::'a::len0 word) = -2"
   "1 AND numeral b = word_of_int (1 AND numeral b)"
-  "1 AND neg_numeral b = word_of_int (1 AND neg_numeral b)"
+  "1 AND - numeral b = word_of_int (1 AND - numeral b)"
   "numeral a AND 1 = word_of_int (numeral a AND 1)"
-  "neg_numeral a AND 1 = word_of_int (neg_numeral a AND 1)"
+  "- numeral a AND 1 = word_of_int (- numeral a AND 1)"
   "1 OR numeral b = word_of_int (1 OR numeral b)"
-  "1 OR neg_numeral b = word_of_int (1 OR neg_numeral b)"
+  "1 OR - numeral b = word_of_int (1 OR - numeral b)"
   "numeral a OR 1 = word_of_int (numeral a OR 1)"
-  "neg_numeral a OR 1 = word_of_int (neg_numeral a OR 1)"
+  "- numeral a OR 1 = word_of_int (- numeral a OR 1)"
   "1 XOR numeral b = word_of_int (1 XOR numeral b)"
-  "1 XOR neg_numeral b = word_of_int (1 XOR neg_numeral b)"
+  "1 XOR - numeral b = word_of_int (1 XOR - numeral b)"
   "numeral a XOR 1 = word_of_int (numeral a XOR 1)"
-  "neg_numeral a XOR 1 = word_of_int (neg_numeral a XOR 1)"
+  "- numeral a XOR 1 = word_of_int (- numeral a XOR 1)"
   by (transfer, simp)+
 
 lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
@@ -2220,8 +2220,8 @@
   by transfer (rule refl)
 
 lemma test_bit_neg_numeral [simp]:
-  "(neg_numeral w :: 'a::len0 word) !! n \<longleftrightarrow>
-    n < len_of TYPE('a) \<and> bin_nth (neg_numeral w) n"
+  "(- numeral w :: 'a::len0 word) !! n \<longleftrightarrow>
+    n < len_of TYPE('a) \<and> bin_nth (- numeral w) n"
   by transfer (rule refl)
 
 lemma test_bit_1 [simp]: "(1::'a::len word) !! n \<longleftrightarrow> n = 0"
@@ -2398,7 +2398,7 @@
   unfolding word_numeral_alt by (rule msb_word_of_int)
 
 lemma word_msb_neg_numeral [simp]:
-  "msb (neg_numeral w::'a::len word) = bin_nth (neg_numeral w) (len_of TYPE('a) - 1)"
+  "msb (- numeral w::'a::len word) = bin_nth (- numeral w) (len_of TYPE('a) - 1)"
   unfolding word_neg_numeral_alt by (rule msb_word_of_int)
 
 lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)"
@@ -2528,7 +2528,7 @@
   unfolding word_lsb_alt test_bit_numeral by simp
 
 lemma word_lsb_neg_numeral [simp]:
-  "lsb (neg_numeral bin :: 'a :: len word) = (bin_last (neg_numeral bin) = 1)"
+  "lsb (- numeral bin :: 'a :: len word) = (bin_last (- numeral bin) = 1)"
   unfolding word_lsb_alt test_bit_neg_numeral by simp
 
 lemma set_bit_word_of_int:
@@ -2544,8 +2544,8 @@
   unfolding word_numeral_alt by (rule set_bit_word_of_int)
 
 lemma word_set_neg_numeral [simp]:
-  "set_bit (neg_numeral bin::'a::len0 word) n b = 
-    word_of_int (bin_sc n (if b then 1 else 0) (neg_numeral bin))"
+  "set_bit (- numeral bin::'a::len0 word) n b = 
+    word_of_int (bin_sc n (if b then 1 else 0) (- numeral bin))"
   unfolding word_neg_numeral_alt by (rule set_bit_word_of_int)
 
 lemma word_set_bit_0 [simp]:
@@ -2612,8 +2612,14 @@
     apply clarsimp
    apply clarsimp
   apply (drule word_gt_0 [THEN iffD1])
-  apply (safe intro!: word_eqI bin_nth_lem)
-     apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric])
+  apply (safe intro!: word_eqI)
+  apply (auto simp add: nth_2p_bin)
+  apply (erule notE)
+  apply (simp (no_asm_use) add: uint_word_of_int word_size)
+  apply (subst mod_pos_pos_trivial)
+  apply simp
+  apply (rule power_strict_increasing)
+  apply simp_all
   done
 
 lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n" 
@@ -2670,7 +2676,7 @@
   unfolding word_numeral_alt shiftl1_wi by simp
 
 lemma shiftl1_neg_numeral [simp]:
-  "shiftl1 (neg_numeral w) = neg_numeral (Num.Bit0 w)"
+  "shiftl1 (- numeral w) = - numeral (Num.Bit0 w)"
   unfolding word_neg_numeral_alt shiftl1_wi by simp
 
 lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
@@ -4638,9 +4644,6 @@
   "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
   by unat_arith
 
-lemma word_no_1 [simp]: "(Numeral1::'a::len0 word) = 1"
-  by (fact word_1_no [symmetric])
-
 declare bin_to_bl_def [simp]
 
 ML_file "Tools/word_lib.ML"
diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Word/WordBitwise.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -461,18 +461,18 @@
     = True # rev (bin_to_bl n (numeral nm))"
   "rev (bin_to_bl (Suc n) (numeral (num.One)))
     = True # replicate n False"
-  "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit0 nm)))
-    = False # rev (bin_to_bl n (neg_numeral nm))"
-  "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit1 nm)))
-    = True # rev (bin_to_bl n (neg_numeral (nm + num.One)))"
-  "rev (bin_to_bl (Suc n) (neg_numeral (num.One)))
+  "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm)))
+    = False # rev (bin_to_bl n (- numeral nm))"
+  "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm)))
+    = True # rev (bin_to_bl n (- numeral (nm + num.One)))"
+  "rev (bin_to_bl (Suc n) (- numeral (num.One)))
     = True # replicate n True"
-  "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit0 nm + num.One)))
-    = True # rev (bin_to_bl n (neg_numeral (nm + num.One)))"
-  "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit1 nm + num.One)))
-    = False # rev (bin_to_bl n (neg_numeral (nm + num.One)))"
-  "rev (bin_to_bl (Suc n) (neg_numeral (num.One + num.One)))
-    = False # rev (bin_to_bl n (neg_numeral num.One))"
+  "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm + num.One)))
+    = True # rev (bin_to_bl n (- numeral (nm + num.One)))"
+  "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm + num.One)))
+    = False # rev (bin_to_bl n (- numeral (nm + num.One)))"
+  "rev (bin_to_bl (Suc n) (- numeral (num.One + num.One)))
+    = False # rev (bin_to_bl n (- numeral num.One))"
   apply (simp_all add: bin_to_bl_def)
   apply (simp_all only: bin_to_bl_aux_alt)
   apply (simp_all)