src/HOL/Num.thy
changeset 54489 03ff4d1e6784
parent 54249 ce00f2fef556
child 55415 05f5fdb8d093
     1.1 --- a/src/HOL/Num.thy	Tue Nov 19 01:30:14 2013 +0100
     1.2 +++ b/src/HOL/Num.thy	Tue Nov 19 10:05:53 2013 +0100
     1.3 @@ -275,16 +275,6 @@
     1.4  
     1.5  end
     1.6  
     1.7 -text {* Negative numerals. *}
     1.8 -
     1.9 -class neg_numeral = numeral + group_add
    1.10 -begin
    1.11 -
    1.12 -definition neg_numeral :: "num \<Rightarrow> 'a" where
    1.13 -  "neg_numeral k = - numeral k"
    1.14 -
    1.15 -end
    1.16 -
    1.17  text {* Numeral syntax. *}
    1.18  
    1.19  syntax
    1.20 @@ -299,8 +289,8 @@
    1.21          | (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n
    1.22          | (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n)
    1.23        else raise Match
    1.24 -    val pos = Syntax.const @{const_name numeral}
    1.25 -    val neg = Syntax.const @{const_name neg_numeral}
    1.26 +    val numeral = Syntax.const @{const_name numeral}
    1.27 +    val uminus = Syntax.const @{const_name uminus}
    1.28      val one = Syntax.const @{const_name Groups.one}
    1.29      val zero = Syntax.const @{const_name Groups.zero}
    1.30      fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
    1.31 @@ -311,8 +301,9 @@
    1.32            in
    1.33              if value = 0 then zero else
    1.34              if value > 0
    1.35 -            then pos $ num_of_int value
    1.36 -            else neg $ num_of_int (~value)
    1.37 +            then numeral $ num_of_int value
    1.38 +            else if value = ~1 then uminus $ one
    1.39 +            else uminus $ (numeral $ num_of_int (~value))
    1.40            end
    1.41        | numeral_tr ts = raise TERM ("numeral_tr", ts);
    1.42    in [("_Numeral", K numeral_tr)] end
    1.43 @@ -323,12 +314,12 @@
    1.44      fun dest_num (Const (@{const_syntax Bit0}, _) $ n) = 2 * dest_num n
    1.45        | dest_num (Const (@{const_syntax Bit1}, _) $ n) = 2 * dest_num n + 1
    1.46        | dest_num (Const (@{const_syntax One}, _)) = 1;
    1.47 -    fun num_tr' sign ctxt T [n] =
    1.48 +    fun num_tr' ctxt T [n] =
    1.49        let
    1.50          val k = dest_num n;
    1.51          val t' =
    1.52            Syntax.const @{syntax_const "_Numeral"} $
    1.53 -            Syntax.free (sign ^ string_of_int k);
    1.54 +            Syntax.free (string_of_int k);
    1.55        in
    1.56          (case T of
    1.57            Type (@{type_name fun}, [_, T']) =>
    1.58 @@ -339,8 +330,7 @@
    1.59          | _ => if T = dummyT then t' else raise Match)
    1.60        end;
    1.61    in
    1.62 -   [(@{const_syntax numeral}, num_tr' ""),
    1.63 -    (@{const_syntax neg_numeral}, num_tr' "-")]
    1.64 +   [(@{const_syntax numeral}, num_tr')]
    1.65    end
    1.66  *}
    1.67  
    1.68 @@ -383,9 +373,13 @@
    1.69    Structures with negation: class @{text neg_numeral}
    1.70  *}
    1.71  
    1.72 -context neg_numeral
    1.73 +class neg_numeral = numeral + group_add
    1.74  begin
    1.75  
    1.76 +lemma uminus_numeral_One:
    1.77 +  "- Numeral1 = - 1"
    1.78 +  by (simp add: numeral_One)
    1.79 +
    1.80  text {* Numerals form an abelian subgroup. *}
    1.81  
    1.82  inductive is_num :: "'a \<Rightarrow> bool" where
    1.83 @@ -403,7 +397,7 @@
    1.84    apply simp
    1.85    apply (rule_tac a=x in add_left_imp_eq)
    1.86    apply (rule_tac a=x in add_right_imp_eq)
    1.87 -  apply (simp add: add_assoc minus_add_cancel)
    1.88 +  apply (simp add: add_assoc)
    1.89    apply (simp add: add_assoc [symmetric], simp add: add_assoc)
    1.90    apply (rule_tac a=x in add_left_imp_eq)
    1.91    apply (rule_tac a=x in add_right_imp_eq)
    1.92 @@ -431,77 +425,85 @@
    1.93    by (simp only: BitM_plus_one [symmetric] numeral_add numeral_One eq_diff_eq)
    1.94  
    1.95  lemma dbl_simps [simp]:
    1.96 -  "dbl (neg_numeral k) = neg_numeral (Bit0 k)"
    1.97 +  "dbl (- numeral k) = - dbl (numeral k)"
    1.98    "dbl 0 = 0"
    1.99    "dbl 1 = 2"
   1.100 +  "dbl (- 1) = - 2"
   1.101    "dbl (numeral k) = numeral (Bit0 k)"
   1.102 -  by (simp_all add: dbl_def neg_numeral_def numeral.simps minus_add)
   1.103 +  by (simp_all add: dbl_def numeral.simps minus_add)
   1.104  
   1.105  lemma dbl_inc_simps [simp]:
   1.106 -  "dbl_inc (neg_numeral k) = neg_numeral (BitM k)"
   1.107 +  "dbl_inc (- numeral k) = - dbl_dec (numeral k)"
   1.108    "dbl_inc 0 = 1"
   1.109    "dbl_inc 1 = 3"
   1.110 +  "dbl_inc (- 1) = - 1"
   1.111    "dbl_inc (numeral k) = numeral (Bit1 k)"
   1.112 -  by (simp_all add: dbl_inc_def neg_numeral_def numeral.simps numeral_BitM is_num_normalize algebra_simps del: add_uminus_conv_diff)
   1.113 +  by (simp_all add: dbl_inc_def dbl_dec_def numeral.simps numeral_BitM is_num_normalize algebra_simps del: add_uminus_conv_diff)
   1.114  
   1.115  lemma dbl_dec_simps [simp]:
   1.116 -  "dbl_dec (neg_numeral k) = neg_numeral (Bit1 k)"
   1.117 -  "dbl_dec 0 = -1"
   1.118 +  "dbl_dec (- numeral k) = - dbl_inc (numeral k)"
   1.119 +  "dbl_dec 0 = - 1"
   1.120    "dbl_dec 1 = 1"
   1.121 +  "dbl_dec (- 1) = - 3"
   1.122    "dbl_dec (numeral k) = numeral (BitM k)"
   1.123 -  by (simp_all add: dbl_dec_def neg_numeral_def numeral.simps numeral_BitM is_num_normalize)
   1.124 +  by (simp_all add: dbl_dec_def dbl_inc_def numeral.simps numeral_BitM is_num_normalize)
   1.125  
   1.126  lemma sub_num_simps [simp]:
   1.127    "sub One One = 0"
   1.128 -  "sub One (Bit0 l) = neg_numeral (BitM l)"
   1.129 -  "sub One (Bit1 l) = neg_numeral (Bit0 l)"
   1.130 +  "sub One (Bit0 l) = - numeral (BitM l)"
   1.131 +  "sub One (Bit1 l) = - numeral (Bit0 l)"
   1.132    "sub (Bit0 k) One = numeral (BitM k)"
   1.133    "sub (Bit1 k) One = numeral (Bit0 k)"
   1.134    "sub (Bit0 k) (Bit0 l) = dbl (sub k l)"
   1.135    "sub (Bit0 k) (Bit1 l) = dbl_dec (sub k l)"
   1.136    "sub (Bit1 k) (Bit0 l) = dbl_inc (sub k l)"
   1.137    "sub (Bit1 k) (Bit1 l) = dbl (sub k l)"
   1.138 -  by (simp_all add: dbl_def dbl_dec_def dbl_inc_def sub_def neg_numeral_def numeral.simps
   1.139 +  by (simp_all add: dbl_def dbl_dec_def dbl_inc_def sub_def numeral.simps
   1.140      numeral_BitM is_num_normalize del: add_uminus_conv_diff add: diff_conv_add_uminus)
   1.141  
   1.142  lemma add_neg_numeral_simps:
   1.143 -  "numeral m + neg_numeral n = sub m n"
   1.144 -  "neg_numeral m + numeral n = sub n m"
   1.145 -  "neg_numeral m + neg_numeral n = neg_numeral (m + n)"
   1.146 -  by (simp_all add: sub_def neg_numeral_def numeral_add numeral.simps is_num_normalize
   1.147 +  "numeral m + - numeral n = sub m n"
   1.148 +  "- numeral m + numeral n = sub n m"
   1.149 +  "- numeral m + - numeral n = - (numeral m + numeral n)"
   1.150 +  by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize
   1.151      del: add_uminus_conv_diff add: diff_conv_add_uminus)
   1.152  
   1.153  lemma add_neg_numeral_special:
   1.154 -  "1 + neg_numeral m = sub One m"
   1.155 -  "neg_numeral m + 1 = sub One m"
   1.156 -  by (simp_all add: sub_def neg_numeral_def numeral_add numeral.simps is_num_normalize)
   1.157 +  "1 + - numeral m = sub One m"
   1.158 +  "- numeral m + 1 = sub One m"
   1.159 +  "numeral m + - 1 = sub m One"
   1.160 +  "- 1 + numeral n = sub n One"
   1.161 +  "- 1 + - numeral n = - numeral (inc n)"
   1.162 +  "- numeral m + - 1 = - numeral (inc m)"
   1.163 +  "1 + - 1 = 0"
   1.164 +  "- 1 + 1 = 0"
   1.165 +  "- 1 + - 1 = - 2"
   1.166 +  by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize right_minus numeral_inc
   1.167 +    del: add_uminus_conv_diff add: diff_conv_add_uminus)
   1.168  
   1.169  lemma diff_numeral_simps:
   1.170    "numeral m - numeral n = sub m n"
   1.171 -  "numeral m - neg_numeral n = numeral (m + n)"
   1.172 -  "neg_numeral m - numeral n = neg_numeral (m + n)"
   1.173 -  "neg_numeral m - neg_numeral n = sub n m"
   1.174 -  by (simp_all add: neg_numeral_def sub_def numeral_add numeral.simps is_num_normalize
   1.175 +  "numeral m - - numeral n = numeral (m + n)"
   1.176 +  "- numeral m - numeral n = - numeral (m + n)"
   1.177 +  "- numeral m - - numeral n = sub n m"
   1.178 +  by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize
   1.179      del: add_uminus_conv_diff add: diff_conv_add_uminus)
   1.180  
   1.181  lemma diff_numeral_special:
   1.182    "1 - numeral n = sub One n"
   1.183 -  "1 - neg_numeral n = numeral (One + n)"
   1.184    "numeral m - 1 = sub m One"
   1.185 -  "neg_numeral m - 1 = neg_numeral (m + One)"
   1.186 -  by (simp_all add: neg_numeral_def sub_def numeral_add numeral.simps add: is_num_normalize)
   1.187 -
   1.188 -lemma minus_one: "- 1 = -1"
   1.189 -  unfolding neg_numeral_def numeral.simps ..
   1.190 -
   1.191 -lemma minus_numeral: "- numeral n = neg_numeral n"
   1.192 -  unfolding neg_numeral_def ..
   1.193 -
   1.194 -lemma minus_neg_numeral: "- neg_numeral n = numeral n"
   1.195 -  unfolding neg_numeral_def by simp
   1.196 -
   1.197 -lemmas minus_numeral_simps [simp] =
   1.198 -  minus_one minus_numeral minus_neg_numeral
   1.199 +  "1 - - numeral n = numeral (One + n)"
   1.200 +  "- numeral m - 1 = - numeral (m + One)"
   1.201 +  "- 1 - numeral n = - numeral (inc n)"
   1.202 +  "numeral m - - 1 = numeral (inc m)"
   1.203 +  "- 1 - - numeral n = sub n One"
   1.204 +  "- numeral m - - 1 = sub One m"
   1.205 +  "1 - 1 = 0"
   1.206 +  "- 1 - 1 = - 2"
   1.207 +  "1 - - 1 = 2"
   1.208 +  "- 1 - - 1 = 0"
   1.209 +  by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize numeral_inc
   1.210 +    del: add_uminus_conv_diff add: diff_conv_add_uminus)
   1.211  
   1.212  end
   1.213  
   1.214 @@ -675,17 +677,17 @@
   1.215  subclass neg_numeral ..
   1.216  
   1.217  lemma mult_neg_numeral_simps:
   1.218 -  "neg_numeral m * neg_numeral n = numeral (m * n)"
   1.219 -  "neg_numeral m * numeral n = neg_numeral (m * n)"
   1.220 -  "numeral m * neg_numeral n = neg_numeral (m * n)"
   1.221 -  unfolding neg_numeral_def mult_minus_left mult_minus_right
   1.222 +  "- numeral m * - numeral n = numeral (m * n)"
   1.223 +  "- numeral m * numeral n = - numeral (m * n)"
   1.224 +  "numeral m * - numeral n = - numeral (m * n)"
   1.225 +  unfolding mult_minus_left mult_minus_right
   1.226    by (simp_all only: minus_minus numeral_mult)
   1.227  
   1.228 -lemma mult_minus1 [simp]: "-1 * z = - z"
   1.229 -  unfolding neg_numeral_def numeral.simps mult_minus_left by simp
   1.230 +lemma mult_minus1 [simp]: "- 1 * z = - z"
   1.231 +  unfolding numeral.simps mult_minus_left by simp
   1.232  
   1.233 -lemma mult_minus1_right [simp]: "z * -1 = - z"
   1.234 -  unfolding neg_numeral_def numeral.simps mult_minus_right by simp
   1.235 +lemma mult_minus1_right [simp]: "z * - 1 = - z"
   1.236 +  unfolding numeral.simps mult_minus_right by simp
   1.237  
   1.238  end
   1.239  
   1.240 @@ -708,9 +710,15 @@
   1.241  lemma not_iszero_Numeral1: "\<not> iszero Numeral1"
   1.242    by (simp add: numeral_One)
   1.243  
   1.244 +lemma not_iszero_neg_1 [simp]: "\<not> iszero (- 1)"
   1.245 +  by (simp add: iszero_def)
   1.246 +
   1.247 +lemma not_iszero_neg_Numeral1: "\<not> iszero (- Numeral1)"
   1.248 +  by (simp add: numeral_One)
   1.249 +
   1.250  lemma iszero_neg_numeral [simp]:
   1.251 -  "iszero (neg_numeral w) \<longleftrightarrow> iszero (numeral w)"
   1.252 -  unfolding iszero_def neg_numeral_def
   1.253 +  "iszero (- numeral w) \<longleftrightarrow> iszero (numeral w)"
   1.254 +  unfolding iszero_def
   1.255    by (rule neg_equal_0_iff_equal)
   1.256  
   1.257  lemma eq_iff_iszero_diff: "x = y \<longleftrightarrow> iszero (x - y)"
   1.258 @@ -730,17 +738,17 @@
   1.259  
   1.260  lemma eq_numeral_iff_iszero:
   1.261    "numeral x = numeral y \<longleftrightarrow> iszero (sub x y)"
   1.262 -  "numeral x = neg_numeral y \<longleftrightarrow> iszero (numeral (x + y))"
   1.263 -  "neg_numeral x = numeral y \<longleftrightarrow> iszero (numeral (x + y))"
   1.264 -  "neg_numeral x = neg_numeral y \<longleftrightarrow> iszero (sub y x)"
   1.265 +  "numeral x = - numeral y \<longleftrightarrow> iszero (numeral (x + y))"
   1.266 +  "- numeral x = numeral y \<longleftrightarrow> iszero (numeral (x + y))"
   1.267 +  "- numeral x = - numeral y \<longleftrightarrow> iszero (sub y x)"
   1.268    "numeral x = 1 \<longleftrightarrow> iszero (sub x One)"
   1.269    "1 = numeral y \<longleftrightarrow> iszero (sub One y)"
   1.270 -  "neg_numeral x = 1 \<longleftrightarrow> iszero (numeral (x + One))"
   1.271 -  "1 = neg_numeral y \<longleftrightarrow> iszero (numeral (One + y))"
   1.272 +  "- numeral x = 1 \<longleftrightarrow> iszero (numeral (x + One))"
   1.273 +  "1 = - numeral y \<longleftrightarrow> iszero (numeral (One + y))"
   1.274    "numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
   1.275    "0 = numeral y \<longleftrightarrow> iszero (numeral y)"
   1.276 -  "neg_numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
   1.277 -  "0 = neg_numeral y \<longleftrightarrow> iszero (numeral y)"
   1.278 +  "- numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
   1.279 +  "0 = - numeral y \<longleftrightarrow> iszero (numeral y)"
   1.280    unfolding eq_iff_iszero_diff diff_numeral_simps diff_numeral_special
   1.281    by simp_all
   1.282  
   1.283 @@ -756,33 +764,69 @@
   1.284  lemma not_iszero_numeral [simp]: "\<not> iszero (numeral w)"
   1.285    by (simp add: iszero_def)
   1.286  
   1.287 -lemma neg_numeral_eq_iff: "neg_numeral m = neg_numeral n \<longleftrightarrow> m = n"
   1.288 -  by (simp only: neg_numeral_def neg_equal_iff_equal numeral_eq_iff)
   1.289 +lemma neg_numeral_eq_iff: "- numeral m = - numeral n \<longleftrightarrow> m = n"
   1.290 +  by simp
   1.291  
   1.292 -lemma numeral_neq_neg_numeral: "numeral m \<noteq> neg_numeral n"
   1.293 -  unfolding neg_numeral_def eq_neg_iff_add_eq_0
   1.294 +lemma numeral_neq_neg_numeral: "numeral m \<noteq> - numeral n"
   1.295 +  unfolding eq_neg_iff_add_eq_0
   1.296    by (simp add: numeral_plus_numeral)
   1.297  
   1.298 -lemma neg_numeral_neq_numeral: "neg_numeral m \<noteq> numeral n"
   1.299 +lemma neg_numeral_neq_numeral: "- numeral m \<noteq> numeral n"
   1.300    by (rule numeral_neq_neg_numeral [symmetric])
   1.301  
   1.302 -lemma zero_neq_neg_numeral: "0 \<noteq> neg_numeral n"
   1.303 -  unfolding neg_numeral_def neg_0_equal_iff_equal by simp
   1.304 +lemma zero_neq_neg_numeral: "0 \<noteq> - numeral n"
   1.305 +  unfolding neg_0_equal_iff_equal by simp
   1.306  
   1.307 -lemma neg_numeral_neq_zero: "neg_numeral n \<noteq> 0"
   1.308 -  unfolding neg_numeral_def neg_equal_0_iff_equal by simp
   1.309 +lemma neg_numeral_neq_zero: "- numeral n \<noteq> 0"
   1.310 +  unfolding neg_equal_0_iff_equal by simp
   1.311  
   1.312 -lemma one_neq_neg_numeral: "1 \<noteq> neg_numeral n"
   1.313 +lemma one_neq_neg_numeral: "1 \<noteq> - numeral n"
   1.314    using numeral_neq_neg_numeral [of One n] by (simp add: numeral_One)
   1.315  
   1.316 -lemma neg_numeral_neq_one: "neg_numeral n \<noteq> 1"
   1.317 +lemma neg_numeral_neq_one: "- numeral n \<noteq> 1"
   1.318    using neg_numeral_neq_numeral [of n One] by (simp add: numeral_One)
   1.319  
   1.320 +lemma neg_one_neq_numeral:
   1.321 +  "- 1 \<noteq> numeral n"
   1.322 +  using neg_numeral_neq_numeral [of One n] by (simp add: numeral_One)
   1.323 +
   1.324 +lemma numeral_neq_neg_one:
   1.325 +  "numeral n \<noteq> - 1"
   1.326 +  using numeral_neq_neg_numeral [of n One] by (simp add: numeral_One)
   1.327 +
   1.328 +lemma neg_one_eq_numeral_iff:
   1.329 +  "- 1 = - numeral n \<longleftrightarrow> n = One"
   1.330 +  using neg_numeral_eq_iff [of One n] by (auto simp add: numeral_One)
   1.331 +
   1.332 +lemma numeral_eq_neg_one_iff:
   1.333 +  "- numeral n = - 1 \<longleftrightarrow> n = One"
   1.334 +  using neg_numeral_eq_iff [of n One] by (auto simp add: numeral_One)
   1.335 +
   1.336 +lemma neg_one_neq_zero:
   1.337 +  "- 1 \<noteq> 0"
   1.338 +  by simp
   1.339 +
   1.340 +lemma zero_neq_neg_one:
   1.341 +  "0 \<noteq> - 1"
   1.342 +  by simp
   1.343 +
   1.344 +lemma neg_one_neq_one:
   1.345 +  "- 1 \<noteq> 1"
   1.346 +  using neg_numeral_neq_numeral [of One One] by (simp only: numeral_One not_False_eq_True)
   1.347 +
   1.348 +lemma one_neq_neg_one:
   1.349 +  "1 \<noteq> - 1"
   1.350 +  using numeral_neq_neg_numeral [of One One] by (simp only: numeral_One not_False_eq_True)
   1.351 +
   1.352  lemmas eq_neg_numeral_simps [simp] =
   1.353    neg_numeral_eq_iff
   1.354    numeral_neq_neg_numeral neg_numeral_neq_numeral
   1.355    one_neq_neg_numeral neg_numeral_neq_one
   1.356    zero_neq_neg_numeral neg_numeral_neq_zero
   1.357 +  neg_one_neq_numeral numeral_neq_neg_one
   1.358 +  neg_one_eq_numeral_iff numeral_eq_neg_one_iff
   1.359 +  neg_one_neq_zero zero_neq_neg_one
   1.360 +  neg_one_neq_one one_neq_neg_one
   1.361  
   1.362  end
   1.363  
   1.364 @@ -795,48 +839,72 @@
   1.365  
   1.366  subclass ring_char_0 ..
   1.367  
   1.368 -lemma neg_numeral_le_iff: "neg_numeral m \<le> neg_numeral n \<longleftrightarrow> n \<le> m"
   1.369 -  by (simp only: neg_numeral_def neg_le_iff_le numeral_le_iff)
   1.370 +lemma neg_numeral_le_iff: "- numeral m \<le> - numeral n \<longleftrightarrow> n \<le> m"
   1.371 +  by (simp only: neg_le_iff_le numeral_le_iff)
   1.372  
   1.373 -lemma neg_numeral_less_iff: "neg_numeral m < neg_numeral n \<longleftrightarrow> n < m"
   1.374 -  by (simp only: neg_numeral_def neg_less_iff_less numeral_less_iff)
   1.375 +lemma neg_numeral_less_iff: "- numeral m < - numeral n \<longleftrightarrow> n < m"
   1.376 +  by (simp only: neg_less_iff_less numeral_less_iff)
   1.377  
   1.378 -lemma neg_numeral_less_zero: "neg_numeral n < 0"
   1.379 -  by (simp only: neg_numeral_def neg_less_0_iff_less zero_less_numeral)
   1.380 +lemma neg_numeral_less_zero: "- numeral n < 0"
   1.381 +  by (simp only: neg_less_0_iff_less zero_less_numeral)
   1.382  
   1.383 -lemma neg_numeral_le_zero: "neg_numeral n \<le> 0"
   1.384 -  by (simp only: neg_numeral_def neg_le_0_iff_le zero_le_numeral)
   1.385 +lemma neg_numeral_le_zero: "- numeral n \<le> 0"
   1.386 +  by (simp only: neg_le_0_iff_le zero_le_numeral)
   1.387  
   1.388 -lemma not_zero_less_neg_numeral: "\<not> 0 < neg_numeral n"
   1.389 +lemma not_zero_less_neg_numeral: "\<not> 0 < - numeral n"
   1.390    by (simp only: not_less neg_numeral_le_zero)
   1.391  
   1.392 -lemma not_zero_le_neg_numeral: "\<not> 0 \<le> neg_numeral n"
   1.393 +lemma not_zero_le_neg_numeral: "\<not> 0 \<le> - numeral n"
   1.394    by (simp only: not_le neg_numeral_less_zero)
   1.395  
   1.396 -lemma neg_numeral_less_numeral: "neg_numeral m < numeral n"
   1.397 +lemma neg_numeral_less_numeral: "- numeral m < numeral n"
   1.398    using neg_numeral_less_zero zero_less_numeral by (rule less_trans)
   1.399  
   1.400 -lemma neg_numeral_le_numeral: "neg_numeral m \<le> numeral n"
   1.401 +lemma neg_numeral_le_numeral: "- numeral m \<le> numeral n"
   1.402    by (simp only: less_imp_le neg_numeral_less_numeral)
   1.403  
   1.404 -lemma not_numeral_less_neg_numeral: "\<not> numeral m < neg_numeral n"
   1.405 +lemma not_numeral_less_neg_numeral: "\<not> numeral m < - numeral n"
   1.406    by (simp only: not_less neg_numeral_le_numeral)
   1.407  
   1.408 -lemma not_numeral_le_neg_numeral: "\<not> numeral m \<le> neg_numeral n"
   1.409 +lemma not_numeral_le_neg_numeral: "\<not> numeral m \<le> - numeral n"
   1.410    by (simp only: not_le neg_numeral_less_numeral)
   1.411    
   1.412 -lemma neg_numeral_less_one: "neg_numeral m < 1"
   1.413 +lemma neg_numeral_less_one: "- numeral m < 1"
   1.414    by (rule neg_numeral_less_numeral [of m One, unfolded numeral_One])
   1.415  
   1.416 -lemma neg_numeral_le_one: "neg_numeral m \<le> 1"
   1.417 +lemma neg_numeral_le_one: "- numeral m \<le> 1"
   1.418    by (rule neg_numeral_le_numeral [of m One, unfolded numeral_One])
   1.419  
   1.420 -lemma not_one_less_neg_numeral: "\<not> 1 < neg_numeral m"
   1.421 +lemma not_one_less_neg_numeral: "\<not> 1 < - numeral m"
   1.422    by (simp only: not_less neg_numeral_le_one)
   1.423  
   1.424 -lemma not_one_le_neg_numeral: "\<not> 1 \<le> neg_numeral m"
   1.425 +lemma not_one_le_neg_numeral: "\<not> 1 \<le> - numeral m"
   1.426    by (simp only: not_le neg_numeral_less_one)
   1.427  
   1.428 +lemma not_numeral_less_neg_one: "\<not> numeral m < - 1"
   1.429 +  using not_numeral_less_neg_numeral [of m One] by (simp add: numeral_One)
   1.430 +
   1.431 +lemma not_numeral_le_neg_one: "\<not> numeral m \<le> - 1"
   1.432 +  using not_numeral_le_neg_numeral [of m One] by (simp add: numeral_One)
   1.433 +
   1.434 +lemma neg_one_less_numeral: "- 1 < numeral m"
   1.435 +  using neg_numeral_less_numeral [of One m] by (simp add: numeral_One)
   1.436 +
   1.437 +lemma neg_one_le_numeral: "- 1 \<le> numeral m"
   1.438 +  using neg_numeral_le_numeral [of One m] by (simp add: numeral_One)
   1.439 +
   1.440 +lemma neg_numeral_less_neg_one_iff: "- numeral m < - 1 \<longleftrightarrow> m \<noteq> One"
   1.441 +  by (cases m) simp_all
   1.442 +
   1.443 +lemma neg_numeral_le_neg_one: "- numeral m \<le> - 1"
   1.444 +  by simp
   1.445 +
   1.446 +lemma not_neg_one_less_neg_numeral: "\<not> - 1 < - numeral m"
   1.447 +  by simp
   1.448 +
   1.449 +lemma not_neg_one_le_neg_numeral_iff: "\<not> - 1 \<le> - numeral m \<longleftrightarrow> m \<noteq> One"
   1.450 +  by (cases m) simp_all
   1.451 +
   1.452  lemma sub_non_negative:
   1.453    "sub n m \<ge> 0 \<longleftrightarrow> n \<ge> m"
   1.454    by (simp only: sub_def le_diff_eq) simp
   1.455 @@ -858,18 +926,40 @@
   1.456    neg_numeral_le_numeral not_numeral_le_neg_numeral
   1.457    neg_numeral_le_zero not_zero_le_neg_numeral
   1.458    neg_numeral_le_one not_one_le_neg_numeral
   1.459 +  neg_one_le_numeral not_numeral_le_neg_one
   1.460 +  neg_numeral_le_neg_one not_neg_one_le_neg_numeral_iff
   1.461 +
   1.462 +lemma le_minus_one_simps [simp]:
   1.463 +  "- 1 \<le> 0"
   1.464 +  "- 1 \<le> 1"
   1.465 +  "\<not> 0 \<le> - 1"
   1.466 +  "\<not> 1 \<le> - 1"
   1.467 +  by simp_all
   1.468  
   1.469  lemmas less_neg_numeral_simps [simp] =
   1.470    neg_numeral_less_iff
   1.471    neg_numeral_less_numeral not_numeral_less_neg_numeral
   1.472    neg_numeral_less_zero not_zero_less_neg_numeral
   1.473    neg_numeral_less_one not_one_less_neg_numeral
   1.474 +  neg_one_less_numeral not_numeral_less_neg_one
   1.475 +  neg_numeral_less_neg_one_iff not_neg_one_less_neg_numeral
   1.476 +
   1.477 +lemma less_minus_one_simps [simp]:
   1.478 +  "- 1 < 0"
   1.479 +  "- 1 < 1"
   1.480 +  "\<not> 0 < - 1"
   1.481 +  "\<not> 1 < - 1"
   1.482 +  by (simp_all add: less_le)
   1.483  
   1.484  lemma abs_numeral [simp]: "abs (numeral n) = numeral n"
   1.485    by simp
   1.486  
   1.487 -lemma abs_neg_numeral [simp]: "abs (neg_numeral n) = numeral n"
   1.488 -  by (simp only: neg_numeral_def abs_minus_cancel abs_numeral)
   1.489 +lemma abs_neg_numeral [simp]: "abs (- numeral n) = numeral n"
   1.490 +  by (simp only: abs_minus_cancel abs_numeral)
   1.491 +
   1.492 +lemma abs_neg_one [simp]:
   1.493 +  "abs (- 1) = 1"
   1.494 +  by simp
   1.495  
   1.496  end
   1.497  
   1.498 @@ -1032,31 +1122,36 @@
   1.499  text{*Theorem lists for the cancellation simprocs. The use of a binary
   1.500  numeral for 1 reduces the number of special cases.*}
   1.501  
   1.502 -lemmas mult_1s =
   1.503 -  mult_numeral_1 mult_numeral_1_right 
   1.504 -  mult_minus1 mult_minus1_right
   1.505 +lemma mult_1s:
   1.506 +  fixes a :: "'a::semiring_numeral"
   1.507 +    and b :: "'b::ring_1"
   1.508 +  shows "Numeral1 * a = a"
   1.509 +    "a * Numeral1 = a"
   1.510 +    "- Numeral1 * b = - b"
   1.511 +    "b * - Numeral1 = - b"
   1.512 +  by simp_all
   1.513  
   1.514  setup {*
   1.515    Reorient_Proc.add
   1.516      (fn Const (@{const_name numeral}, _) $ _ => true
   1.517 -    | Const (@{const_name neg_numeral}, _) $ _ => true
   1.518 +    | Const (@{const_name uminus}, _) $ (Const (@{const_name numeral}, _) $ _) => true
   1.519      | _ => false)
   1.520  *}
   1.521  
   1.522  simproc_setup reorient_numeral
   1.523 -  ("numeral w = x" | "neg_numeral w = y") = Reorient_Proc.proc
   1.524 +  ("numeral w = x" | "- numeral w = y") = Reorient_Proc.proc
   1.525  
   1.526  
   1.527  subsubsection {* Simplification of arithmetic operations on integer constants. *}
   1.528  
   1.529  lemmas arith_special = (* already declared simp above *)
   1.530    add_numeral_special add_neg_numeral_special
   1.531 -  diff_numeral_special minus_one
   1.532 +  diff_numeral_special
   1.533  
   1.534  (* rules already in simpset *)
   1.535  lemmas arith_extra_simps =
   1.536    numeral_plus_numeral add_neg_numeral_simps add_0_left add_0_right
   1.537 -  minus_numeral minus_neg_numeral minus_zero minus_one
   1.538 +  minus_zero
   1.539    diff_numeral_simps diff_0 diff_0_right
   1.540    numeral_times_numeral mult_neg_numeral_simps
   1.541    mult_zero_left mult_zero_right
   1.542 @@ -1089,15 +1184,15 @@
   1.543  
   1.544  lemmas rel_simps =
   1.545    le_num_simps less_num_simps eq_num_simps
   1.546 -  le_numeral_simps le_neg_numeral_simps le_numeral_extra
   1.547 -  less_numeral_simps less_neg_numeral_simps less_numeral_extra
   1.548 +  le_numeral_simps le_neg_numeral_simps le_minus_one_simps le_numeral_extra
   1.549 +  less_numeral_simps less_neg_numeral_simps less_minus_one_simps less_numeral_extra
   1.550    eq_numeral_simps eq_neg_numeral_simps eq_numeral_extra
   1.551  
   1.552  lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
   1.553    -- {* Unfold all @{text let}s involving constants *}
   1.554    unfolding Let_def ..
   1.555  
   1.556 -lemma Let_neg_numeral [simp]: "Let (neg_numeral v) f = f (neg_numeral v)"
   1.557 +lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
   1.558    -- {* Unfold all @{text let}s involving constants *}
   1.559    unfolding Let_def ..
   1.560  
   1.561 @@ -1133,16 +1228,16 @@
   1.562    by (simp_all add: add_assoc [symmetric])
   1.563  
   1.564  lemma add_neg_numeral_left [simp]:
   1.565 -  "numeral v + (neg_numeral w + y) = (sub v w + y)"
   1.566 -  "neg_numeral v + (numeral w + y) = (sub w v + y)"
   1.567 -  "neg_numeral v + (neg_numeral w + y) = (neg_numeral(v + w) + y)"
   1.568 +  "numeral v + (- numeral w + y) = (sub v w + y)"
   1.569 +  "- numeral v + (numeral w + y) = (sub w v + y)"
   1.570 +  "- numeral v + (- numeral w + y) = (- numeral(v + w) + y)"
   1.571    by (simp_all add: add_assoc [symmetric])
   1.572  
   1.573  lemma mult_numeral_left [simp]:
   1.574    "numeral v * (numeral w * z) = (numeral(v * w) * z :: 'a::semiring_numeral)"
   1.575 -  "neg_numeral v * (numeral w * y) = (neg_numeral(v * w) * y :: 'b::ring_1)"
   1.576 -  "numeral v * (neg_numeral w * y) = (neg_numeral(v * w) * y :: 'b::ring_1)"
   1.577 -  "neg_numeral v * (neg_numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)"
   1.578 +  "- numeral v * (numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
   1.579 +  "numeral v * (- numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
   1.580 +  "- numeral v * (- numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)"
   1.581    by (simp_all add: mult_assoc [symmetric])
   1.582  
   1.583  hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_dec