src/HOL/Nat_Numeral.thy
changeset 47108 2a1953f0d20d
parent 46026 83caa4f4bd56
child 47192 0c0501cb6da6
     1.1 --- a/src/HOL/Nat_Numeral.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -15,31 +15,13 @@
     1.4    Arithmetic for naturals is reduced to that for the non-negative integers.
     1.5  *}
     1.6  
     1.7 -instantiation nat :: number_semiring
     1.8 -begin
     1.9 -
    1.10 -definition
    1.11 -  nat_number_of_def [code_unfold, code del]: "number_of v = nat (number_of v)"
    1.12 -
    1.13 -instance proof
    1.14 -  fix n show "number_of (int n) = (of_nat n :: nat)"
    1.15 -    unfolding nat_number_of_def number_of_eq by simp
    1.16 -qed
    1.17 - 
    1.18 -end
    1.19 -
    1.20 -lemma [code_post]:
    1.21 -  "nat (number_of v) = number_of v"
    1.22 -  unfolding nat_number_of_def ..
    1.23 -
    1.24 -
    1.25  subsection {* Special case: squares and cubes *}
    1.26  
    1.27  lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
    1.28 -  by (simp add: nat_number_of_def)
    1.29 +  by (simp add: nat_number(2-4))
    1.30  
    1.31  lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
    1.32 -  by (simp add: nat_number_of_def)
    1.33 +  by (simp add: nat_number(2-4))
    1.34  
    1.35  context power
    1.36  begin
    1.37 @@ -93,26 +75,21 @@
    1.38    "(- a)\<twosuperior> = a\<twosuperior>"
    1.39    by (simp add: power2_eq_square)
    1.40  
    1.41 -text{*
    1.42 -  We cannot prove general results about the numeral @{term "-1"},
    1.43 -  so we have to use @{term "- 1"} instead.
    1.44 -*}
    1.45 -
    1.46  lemma power_minus1_even [simp]:
    1.47 -  "(- 1) ^ (2*n) = 1"
    1.48 +  "-1 ^ (2*n) = 1"
    1.49  proof (induct n)
    1.50    case 0 show ?case by simp
    1.51  next
    1.52 -  case (Suc n) then show ?case by (simp add: power_add)
    1.53 +  case (Suc n) then show ?case by (simp add: power_add power2_eq_square)
    1.54  qed
    1.55  
    1.56  lemma power_minus1_odd:
    1.57 -  "(- 1) ^ Suc (2*n) = - 1"
    1.58 +  "-1 ^ Suc (2*n) = -1"
    1.59    by simp
    1.60  
    1.61  lemma power_minus_even [simp]:
    1.62    "(-a) ^ (2*n) = a ^ (2*n)"
    1.63 -  by (simp add: power_minus [of a]) 
    1.64 +  by (simp add: power_minus [of a])
    1.65  
    1.66  end
    1.67  
    1.68 @@ -261,100 +238,31 @@
    1.69  end
    1.70  
    1.71  lemma power2_sum:
    1.72 -  fixes x y :: "'a::number_semiring"
    1.73 +  fixes x y :: "'a::comm_semiring_1"
    1.74    shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
    1.75 -  by (simp add: algebra_simps power2_eq_square semiring_mult_2_right)
    1.76 +  by (simp add: algebra_simps power2_eq_square mult_2_right)
    1.77  
    1.78  lemma power2_diff:
    1.79 -  fixes x y :: "'a::number_ring"
    1.80 +  fixes x y :: "'a::comm_ring_1"
    1.81    shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
    1.82    by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute)
    1.83  
    1.84  
    1.85 -subsection {* Predicate for negative binary numbers *}
    1.86 -
    1.87 -definition neg  :: "int \<Rightarrow> bool" where
    1.88 -  "neg Z \<longleftrightarrow> Z < 0"
    1.89 -
    1.90 -lemma not_neg_int [simp]: "~ neg (of_nat n)"
    1.91 -by (simp add: neg_def)
    1.92 -
    1.93 -lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
    1.94 -by (simp add: neg_def del: of_nat_Suc)
    1.95 -
    1.96 -lemmas neg_eq_less_0 = neg_def
    1.97 -
    1.98 -lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
    1.99 -by (simp add: neg_def linorder_not_less)
   1.100 -
   1.101 -text{*To simplify inequalities when Numeral1 can get simplified to 1*}
   1.102 -
   1.103 -lemma not_neg_0: "~ neg 0"
   1.104 -by (simp add: One_int_def neg_def)
   1.105 -
   1.106 -lemma not_neg_1: "~ neg 1"
   1.107 -by (simp add: neg_def linorder_not_less)
   1.108 -
   1.109 -lemma neg_nat: "neg z ==> nat z = 0"
   1.110 -by (simp add: neg_def order_less_imp_le) 
   1.111 -
   1.112 -lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
   1.113 -by (simp add: linorder_not_less neg_def)
   1.114 -
   1.115 -text {*
   1.116 -  If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
   1.117 -  @{term Numeral0} IS @{term "number_of Pls"}
   1.118 -*}
   1.119 -
   1.120 -lemma not_neg_number_of_Pls: "~ neg (number_of Int.Pls)"
   1.121 -  by (simp add: neg_def)
   1.122 -
   1.123 -lemma neg_number_of_Min: "neg (number_of Int.Min)"
   1.124 -  by (simp add: neg_def)
   1.125 -
   1.126 -lemma neg_number_of_Bit0:
   1.127 -  "neg (number_of (Int.Bit0 w)) = neg (number_of w)"
   1.128 -  by (simp add: neg_def)
   1.129 -
   1.130 -lemma neg_number_of_Bit1:
   1.131 -  "neg (number_of (Int.Bit1 w)) = neg (number_of w)"
   1.132 -  by (simp add: neg_def)
   1.133 -
   1.134 -lemmas neg_simps [simp] =
   1.135 -  not_neg_0 not_neg_1
   1.136 -  not_neg_number_of_Pls neg_number_of_Min
   1.137 -  neg_number_of_Bit0 neg_number_of_Bit1
   1.138 -
   1.139 -
   1.140  subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
   1.141  
   1.142  declare nat_1 [simp]
   1.143  
   1.144 -lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
   1.145 -  by (simp add: nat_number_of_def)
   1.146 -
   1.147 -lemma nat_numeral_0_eq_0: "Numeral0 = (0::nat)" (* FIXME delete candidate *)
   1.148 -  by (fact semiring_numeral_0_eq_0)
   1.149 -
   1.150 -lemma nat_numeral_1_eq_1: "Numeral1 = (1::nat)" (* FIXME delete candidate *)
   1.151 -  by (fact semiring_numeral_1_eq_1)
   1.152 -
   1.153 -lemma Numeral1_eq1_nat:
   1.154 -  "(1::nat) = Numeral1"
   1.155 +lemma nat_neg_numeral [simp]: "nat (neg_numeral w) = 0"
   1.156    by simp
   1.157  
   1.158  lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
   1.159 -  by (simp only: nat_numeral_1_eq_1 One_nat_def)
   1.160 +  by simp
   1.161  
   1.162  
   1.163  subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
   1.164  
   1.165 -lemma int_nat_number_of [simp]:
   1.166 -     "int (number_of v) =  
   1.167 -         (if neg (number_of v :: int) then 0  
   1.168 -          else (number_of v :: int))"
   1.169 -  unfolding nat_number_of_def number_of_is_id neg_def
   1.170 -  by simp (* FIXME: redundant with of_nat_number_of_eq *)
   1.171 +lemma int_numeral: "int (numeral v) = numeral v"
   1.172 +  by (rule of_nat_numeral) (* already simp *)
   1.173  
   1.174  lemma nonneg_int_cases:
   1.175    fixes k :: int assumes "0 \<le> k" obtains n where "k = of_nat n"
   1.176 @@ -368,149 +276,51 @@
   1.177  done
   1.178  
   1.179  lemma Suc_nat_number_of_add:
   1.180 -     "Suc (number_of v + n) =  
   1.181 -        (if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)"
   1.182 -  unfolding nat_number_of_def number_of_is_id neg_def numeral_simps
   1.183 -  by (simp add: Suc_nat_eq_nat_zadd1 add_ac)
   1.184 -
   1.185 -lemma Suc_nat_number_of [simp]:
   1.186 -     "Suc (number_of v) =  
   1.187 -        (if neg (number_of v :: int) then 1 else number_of (Int.succ v))"
   1.188 -apply (cut_tac n = 0 in Suc_nat_number_of_add)
   1.189 -apply (simp cong del: if_weak_cong)
   1.190 -done
   1.191 -
   1.192 -
   1.193 -subsubsection{*Addition *}
   1.194 -
   1.195 -lemma add_nat_number_of [simp]:
   1.196 -     "(number_of v :: nat) + number_of v' =  
   1.197 -         (if v < Int.Pls then number_of v'  
   1.198 -          else if v' < Int.Pls then number_of v  
   1.199 -          else number_of (v + v'))"
   1.200 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   1.201 -  by (simp add: nat_add_distrib)
   1.202 -
   1.203 -lemma nat_number_of_add_1 [simp]:
   1.204 -  "number_of v + (1::nat) =
   1.205 -    (if v < Int.Pls then 1 else number_of (Int.succ v))"
   1.206 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   1.207 -  by (simp add: nat_add_distrib)
   1.208 +  "Suc (numeral v + n) = numeral (v + Num.One) + n"
   1.209 +  by simp
   1.210  
   1.211 -lemma nat_1_add_number_of [simp]:
   1.212 -  "(1::nat) + number_of v =
   1.213 -    (if v < Int.Pls then 1 else number_of (Int.succ v))"
   1.214 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   1.215 -  by (simp add: nat_add_distrib)
   1.216 -
   1.217 -lemma nat_1_add_1 [simp]: "1 + 1 = (2::nat)"
   1.218 -  by (rule semiring_one_add_one_is_two)
   1.219 -
   1.220 -text {* TODO: replace simp rules above with these generic ones: *}
   1.221 -
   1.222 -lemma semiring_add_number_of:
   1.223 -  "\<lbrakk>Int.Pls \<le> v; Int.Pls \<le> v'\<rbrakk> \<Longrightarrow>
   1.224 -    (number_of v :: 'a::number_semiring) + number_of v' = number_of (v + v')"
   1.225 -  unfolding Int.Pls_def
   1.226 -  by (elim nonneg_int_cases,
   1.227 -    simp only: number_of_int of_nat_add [symmetric])
   1.228 -
   1.229 -lemma semiring_number_of_add_1:
   1.230 -  "Int.Pls \<le> v \<Longrightarrow>
   1.231 -    number_of v + (1::'a::number_semiring) = number_of (Int.succ v)"
   1.232 -  unfolding Int.Pls_def Int.succ_def
   1.233 -  by (elim nonneg_int_cases,
   1.234 -    simp only: number_of_int add_commute [where b=1] of_nat_Suc [symmetric])
   1.235 -
   1.236 -lemma semiring_1_add_number_of:
   1.237 -  "Int.Pls \<le> v \<Longrightarrow>
   1.238 -    (1::'a::number_semiring) + number_of v = number_of (Int.succ v)"
   1.239 -  unfolding Int.Pls_def Int.succ_def
   1.240 -  by (elim nonneg_int_cases,
   1.241 -    simp only: number_of_int add_commute [where b=1] of_nat_Suc [symmetric])
   1.242 +lemma Suc_numeral [simp]:
   1.243 +  "Suc (numeral v) = numeral (v + Num.One)"
   1.244 +  by simp
   1.245  
   1.246  
   1.247  subsubsection{*Subtraction *}
   1.248  
   1.249  lemma diff_nat_eq_if:
   1.250       "nat z - nat z' =  
   1.251 -        (if neg z' then nat z   
   1.252 +        (if z' < 0 then nat z   
   1.253           else let d = z-z' in     
   1.254 -              if neg d then 0 else nat d)"
   1.255 -by (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
   1.256 -
   1.257 -
   1.258 -lemma diff_nat_number_of [simp]: 
   1.259 -     "(number_of v :: nat) - number_of v' =  
   1.260 -        (if v' < Int.Pls then number_of v  
   1.261 -         else let d = number_of (v + uminus v') in     
   1.262 -              if neg d then 0 else nat d)"
   1.263 -  unfolding nat_number_of_def number_of_is_id numeral_simps neg_def
   1.264 -  by auto
   1.265 +              if d < 0 then 0 else nat d)"
   1.266 +by (simp add: Let_def nat_diff_distrib [symmetric])
   1.267  
   1.268 -lemma nat_number_of_diff_1 [simp]:
   1.269 -  "number_of v - (1::nat) =
   1.270 -    (if v \<le> Int.Pls then 0 else number_of (Int.pred v))"
   1.271 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   1.272 -  by auto
   1.273 -
   1.274 -
   1.275 -subsubsection{*Multiplication *}
   1.276 +(* Int.nat_diff_distrib has too-strong premises *)
   1.277 +lemma nat_diff_distrib': "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x - y) = nat x - nat y"
   1.278 +apply (rule int_int_eq [THEN iffD1], clarsimp)
   1.279 +apply (subst zdiff_int [symmetric])
   1.280 +apply (rule nat_mono, simp_all)
   1.281 +done
   1.282  
   1.283 -lemma mult_nat_number_of [simp]:
   1.284 -     "(number_of v :: nat) * number_of v' =  
   1.285 -       (if v < Int.Pls then 0 else number_of (v * v'))"
   1.286 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   1.287 -  by (simp add: nat_mult_distrib)
   1.288 +lemma diff_nat_numeral [simp]: 
   1.289 +  "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
   1.290 +  by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
   1.291  
   1.292 -(* TODO: replace mult_nat_number_of with this next rule *)
   1.293 -lemma semiring_mult_number_of:
   1.294 -  "\<lbrakk>Int.Pls \<le> v; Int.Pls \<le> v'\<rbrakk> \<Longrightarrow>
   1.295 -    (number_of v :: 'a::number_semiring) * number_of v' = number_of (v * v')"
   1.296 -  unfolding Int.Pls_def
   1.297 -  by (elim nonneg_int_cases,
   1.298 -    simp only: number_of_int of_nat_mult [symmetric])
   1.299 +lemma nat_numeral_diff_1 [simp]:
   1.300 +  "numeral v - (1::nat) = nat (numeral v - 1)"
   1.301 +  using diff_nat_numeral [of v Num.One] by simp
   1.302  
   1.303  
   1.304  subsection{*Comparisons*}
   1.305  
   1.306 -subsubsection{*Equals (=) *}
   1.307 -
   1.308 -lemma eq_nat_number_of [simp]:
   1.309 -     "((number_of v :: nat) = number_of v') =  
   1.310 -      (if neg (number_of v :: int) then (number_of v' :: int) \<le> 0
   1.311 -       else if neg (number_of v' :: int) then (number_of v :: int) = 0
   1.312 -       else v = v')"
   1.313 -  unfolding nat_number_of_def number_of_is_id neg_def
   1.314 -  by auto
   1.315 -
   1.316 -
   1.317 -subsubsection{*Less-than (<) *}
   1.318 -
   1.319 -lemma less_nat_number_of [simp]:
   1.320 -  "(number_of v :: nat) < number_of v' \<longleftrightarrow>
   1.321 -    (if v < v' then Int.Pls < v' else False)"
   1.322 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   1.323 -  by auto
   1.324 -
   1.325 -
   1.326 -subsubsection{*Less-than-or-equal *}
   1.327 -
   1.328 -lemma le_nat_number_of [simp]:
   1.329 -  "(number_of v :: nat) \<le> number_of v' \<longleftrightarrow>
   1.330 -    (if v \<le> v' then True else v \<le> Int.Pls)"
   1.331 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   1.332 -  by auto
   1.333 -
   1.334 -(*Maps #n to n for n = 0, 1, 2*)
   1.335 -lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2
   1.336 +(*Maps #n to n for n = 1, 2*)
   1.337 +lemmas numerals = numeral_1_eq_1 [where 'a=nat] numeral_2_eq_2
   1.338  
   1.339  
   1.340  subsection{*Powers with Numeric Exponents*}
   1.341  
   1.342  text{*Squares of literal numerals will be evaluated.*}
   1.343 -lemmas power2_eq_square_number_of [simp] =
   1.344 -  power2_eq_square [of "number_of w"] for w
   1.345 +(* FIXME: replace with more general rules for powers of numerals *)
   1.346 +lemmas power2_eq_square_numeral [simp] =
   1.347 +    power2_eq_square [of "numeral w"] for w
   1.348  
   1.349  
   1.350  text{*Simprules for comparisons where common factors can be cancelled.*}
   1.351 @@ -528,8 +338,8 @@
   1.352  by simp
   1.353  
   1.354  (*Expresses a natural number constant as the Suc of another one.
   1.355 -  NOT suitable for rewriting because n recurs in the condition.*)
   1.356 -lemmas expand_Suc = Suc_pred' [of "number_of v"] for v
   1.357 +  NOT suitable for rewriting because n recurs on the right-hand side.*)
   1.358 +lemmas expand_Suc = Suc_pred' [of "numeral v", OF zero_less_numeral] for v
   1.359  
   1.360  subsubsection{*Arith *}
   1.361  
   1.362 @@ -539,7 +349,7 @@
   1.363  lemma Suc_eq_plus1_left: "Suc n = 1 + n"
   1.364    unfolding One_nat_def by simp
   1.365  
   1.366 -(* These two can be useful when m = number_of... *)
   1.367 +(* These two can be useful when m = numeral... *)
   1.368  
   1.369  lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
   1.370    unfolding One_nat_def by (cases m) simp_all
   1.371 @@ -551,231 +361,108 @@
   1.372    unfolding One_nat_def by (cases m) simp_all
   1.373  
   1.374  
   1.375 -subsection{*Comparisons involving (0::nat) *}
   1.376 -
   1.377 -text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
   1.378 -
   1.379 -lemma eq_number_of_0 [simp]:
   1.380 -  "number_of v = (0::nat) \<longleftrightarrow> v \<le> Int.Pls"
   1.381 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   1.382 -  by auto
   1.383 -
   1.384 -lemma eq_0_number_of [simp]:
   1.385 -  "(0::nat) = number_of v \<longleftrightarrow> v \<le> Int.Pls"
   1.386 -by (rule trans [OF eq_sym_conv eq_number_of_0])
   1.387 -
   1.388 -lemma less_0_number_of [simp]:
   1.389 -   "(0::nat) < number_of v \<longleftrightarrow> Int.Pls < v"
   1.390 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   1.391 -  by simp
   1.392 -
   1.393 -lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
   1.394 -  by (simp del: semiring_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
   1.395 -
   1.396 -
   1.397  subsection{*Comparisons involving  @{term Suc} *}
   1.398  
   1.399 -lemma eq_number_of_Suc [simp]:
   1.400 -     "(number_of v = Suc n) =  
   1.401 -        (let pv = number_of (Int.pred v) in  
   1.402 -         if neg pv then False else nat pv = n)"
   1.403 -apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   1.404 -                  number_of_pred nat_number_of_def 
   1.405 -            split add: split_if)
   1.406 -apply (rule_tac x = "number_of v" in spec)
   1.407 -apply (auto simp add: nat_eq_iff)
   1.408 -done
   1.409 +lemma eq_numeral_Suc [simp]: "numeral v = Suc n \<longleftrightarrow> nat (numeral v - 1) = n"
   1.410 +  by (subst expand_Suc, simp only: nat.inject nat_numeral_diff_1)
   1.411  
   1.412 -lemma Suc_eq_number_of [simp]:
   1.413 -     "(Suc n = number_of v) =  
   1.414 -        (let pv = number_of (Int.pred v) in  
   1.415 -         if neg pv then False else nat pv = n)"
   1.416 -by (rule trans [OF eq_sym_conv eq_number_of_Suc])
   1.417 +lemma Suc_eq_numeral [simp]: "Suc n = numeral v \<longleftrightarrow> n = nat (numeral v - 1)"
   1.418 +  by (subst expand_Suc, simp only: nat.inject nat_numeral_diff_1)
   1.419  
   1.420 -lemma less_number_of_Suc [simp]:
   1.421 -     "(number_of v < Suc n) =  
   1.422 -        (let pv = number_of (Int.pred v) in  
   1.423 -         if neg pv then True else nat pv < n)"
   1.424 -apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   1.425 -                  number_of_pred nat_number_of_def  
   1.426 -            split add: split_if)
   1.427 -apply (rule_tac x = "number_of v" in spec)
   1.428 -apply (auto simp add: nat_less_iff)
   1.429 -done
   1.430 +lemma less_numeral_Suc [simp]: "numeral v < Suc n \<longleftrightarrow> nat (numeral v - 1) < n"
   1.431 +  by (subst expand_Suc, simp only: Suc_less_eq nat_numeral_diff_1)
   1.432  
   1.433 -lemma less_Suc_number_of [simp]:
   1.434 -     "(Suc n < number_of v) =  
   1.435 -        (let pv = number_of (Int.pred v) in  
   1.436 -         if neg pv then False else n < nat pv)"
   1.437 -apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   1.438 -                  number_of_pred nat_number_of_def
   1.439 -            split add: split_if)
   1.440 -apply (rule_tac x = "number_of v" in spec)
   1.441 -apply (auto simp add: zless_nat_eq_int_zless)
   1.442 -done
   1.443 +lemma less_Suc_numeral [simp]: "Suc n < numeral v \<longleftrightarrow> n < nat (numeral v - 1)"
   1.444 +  by (subst expand_Suc, simp only: Suc_less_eq nat_numeral_diff_1)
   1.445  
   1.446 -lemma le_number_of_Suc [simp]:
   1.447 -     "(number_of v <= Suc n) =  
   1.448 -        (let pv = number_of (Int.pred v) in  
   1.449 -         if neg pv then True else nat pv <= n)"
   1.450 -by (simp add: Let_def linorder_not_less [symmetric])
   1.451 +lemma le_numeral_Suc [simp]: "numeral v \<le> Suc n \<longleftrightarrow> nat (numeral v - 1) \<le> n"
   1.452 +  by (subst expand_Suc, simp only: Suc_le_mono nat_numeral_diff_1)
   1.453  
   1.454 -lemma le_Suc_number_of [simp]:
   1.455 -     "(Suc n <= number_of v) =  
   1.456 -        (let pv = number_of (Int.pred v) in  
   1.457 -         if neg pv then False else n <= nat pv)"
   1.458 -by (simp add: Let_def linorder_not_less [symmetric])
   1.459 -
   1.460 -
   1.461 -lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Int.Min"
   1.462 -by auto
   1.463 -
   1.464 +lemma le_Suc_numeral [simp]: "Suc n \<le> numeral v \<longleftrightarrow> n \<le> nat (numeral v - 1)"
   1.465 +  by (subst expand_Suc, simp only: Suc_le_mono nat_numeral_diff_1)
   1.466  
   1.467  
   1.468  subsection{*Max and Min Combined with @{term Suc} *}
   1.469  
   1.470 -lemma max_number_of_Suc [simp]:
   1.471 -     "max (Suc n) (number_of v) =  
   1.472 -        (let pv = number_of (Int.pred v) in  
   1.473 -         if neg pv then Suc n else Suc(max n (nat pv)))"
   1.474 -apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   1.475 -            split add: split_if nat.split)
   1.476 -apply (rule_tac x = "number_of v" in spec) 
   1.477 -apply auto
   1.478 -done
   1.479 - 
   1.480 -lemma max_Suc_number_of [simp]:
   1.481 -     "max (number_of v) (Suc n) =  
   1.482 -        (let pv = number_of (Int.pred v) in  
   1.483 -         if neg pv then Suc n else Suc(max (nat pv) n))"
   1.484 -apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   1.485 -            split add: split_if nat.split)
   1.486 -apply (rule_tac x = "number_of v" in spec) 
   1.487 -apply auto
   1.488 -done
   1.489 - 
   1.490 -lemma min_number_of_Suc [simp]:
   1.491 -     "min (Suc n) (number_of v) =  
   1.492 -        (let pv = number_of (Int.pred v) in  
   1.493 -         if neg pv then 0 else Suc(min n (nat pv)))"
   1.494 -apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   1.495 -            split add: split_if nat.split)
   1.496 -apply (rule_tac x = "number_of v" in spec) 
   1.497 -apply auto
   1.498 -done
   1.499 - 
   1.500 -lemma min_Suc_number_of [simp]:
   1.501 -     "min (number_of v) (Suc n) =  
   1.502 -        (let pv = number_of (Int.pred v) in  
   1.503 -         if neg pv then 0 else Suc(min (nat pv) n))"
   1.504 -apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   1.505 -            split add: split_if nat.split)
   1.506 -apply (rule_tac x = "number_of v" in spec) 
   1.507 -apply auto
   1.508 -done
   1.509 +lemma max_Suc_numeral [simp]:
   1.510 +  "max (Suc n) (numeral v) = Suc (max n (nat (numeral v - 1)))"
   1.511 +  by (subst expand_Suc, simp only: max_Suc_Suc nat_numeral_diff_1)
   1.512 +
   1.513 +lemma max_numeral_Suc [simp]:
   1.514 +  "max (numeral v) (Suc n) = Suc (max (nat (numeral v - 1)) n)"
   1.515 +  by (subst expand_Suc, simp only: max_Suc_Suc nat_numeral_diff_1)
   1.516 +
   1.517 +lemma min_Suc_numeral [simp]:
   1.518 +  "min (Suc n) (numeral v) = Suc (min n (nat (numeral v - 1)))"
   1.519 +  by (subst expand_Suc, simp only: min_Suc_Suc nat_numeral_diff_1)
   1.520 +
   1.521 +lemma min_numeral_Suc [simp]:
   1.522 +  "min (numeral v) (Suc n) = Suc (min (nat (numeral v - 1)) n)"
   1.523 +  by (subst expand_Suc, simp only: min_Suc_Suc nat_numeral_diff_1)
   1.524   
   1.525  subsection{*Literal arithmetic involving powers*}
   1.526  
   1.527 -lemma power_nat_number_of:
   1.528 -     "(number_of v :: nat) ^ n =  
   1.529 -       (if neg (number_of v :: int) then 0^n else nat ((number_of v :: int) ^ n))"
   1.530 -by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq
   1.531 -         split add: split_if cong: imp_cong)
   1.532 +(* TODO: replace with more generic rule for powers of numerals *)
   1.533 +lemma power_nat_numeral:
   1.534 +  "(numeral v :: nat) ^ n = nat ((numeral v :: int) ^ n)"
   1.535 +  by (simp only: nat_power_eq zero_le_numeral nat_numeral)
   1.536  
   1.537 -
   1.538 -lemmas power_nat_number_of_number_of = power_nat_number_of [of _ "number_of w"] for w
   1.539 -declare power_nat_number_of_number_of [simp]
   1.540 -
   1.541 +lemmas power_nat_numeral_numeral = power_nat_numeral [of _ "numeral w"] for w
   1.542 +declare power_nat_numeral_numeral [simp]
   1.543  
   1.544  
   1.545  text{*For arbitrary rings*}
   1.546  
   1.547 -lemma power_number_of_even:
   1.548 +lemma power_numeral_even:
   1.549    fixes z :: "'a::monoid_mult"
   1.550 -  shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
   1.551 -by (cases "w \<ge> 0") (auto simp add: Let_def Bit0_def nat_number_of_def number_of_is_id
   1.552 -  nat_add_distrib power_add simp del: nat_number_of)
   1.553 +  shows "z ^ numeral (Num.Bit0 w) = (let w = z ^ (numeral w) in w * w)"
   1.554 +  unfolding numeral_Bit0 power_add Let_def ..
   1.555  
   1.556 -lemma power_number_of_odd:
   1.557 +lemma power_numeral_odd:
   1.558    fixes z :: "'a::monoid_mult"
   1.559 -  shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
   1.560 -     then (let w = z ^ (number_of w) in z * w * w) else 1)"
   1.561 -unfolding Let_def Bit1_def nat_number_of_def number_of_is_id
   1.562 -apply (cases "0 <= w")
   1.563 -apply (simp only: mult_assoc nat_add_distrib power_add, simp)
   1.564 -apply (simp add: not_le mult_2 [symmetric] add_assoc)
   1.565 -done
   1.566 +  shows "z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)"
   1.567 +  unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right
   1.568 +  unfolding power_Suc power_add Let_def mult_assoc ..
   1.569  
   1.570 -lemmas zpower_number_of_even = power_number_of_even [where 'a=int]
   1.571 -lemmas zpower_number_of_odd = power_number_of_odd [where 'a=int]
   1.572 -
   1.573 -lemmas power_number_of_even_number_of [simp] =
   1.574 -    power_number_of_even [of "number_of v"] for v
   1.575 +lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
   1.576 +lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
   1.577  
   1.578 -lemmas power_number_of_odd_number_of [simp] =
   1.579 -    power_number_of_odd [of "number_of v"] for v
   1.580 +lemmas power_numeral_even_numeral [simp] =
   1.581 +    power_numeral_even [of "numeral v"] for v
   1.582  
   1.583 -lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
   1.584 -  by (simp add: nat_number_of_def)
   1.585 -
   1.586 -lemma nat_number_of_Min [no_atp]: "number_of Int.Min = (0::nat)"
   1.587 -  apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
   1.588 -  done
   1.589 +lemmas power_numeral_odd_numeral [simp] =
   1.590 +    power_numeral_odd [of "numeral v"] for v
   1.591  
   1.592 -lemma nat_number_of_Bit0:
   1.593 -    "number_of (Int.Bit0 w) = (let n::nat = number_of w in n + n)"
   1.594 -by (cases "w \<ge> 0") (auto simp add: Let_def Bit0_def nat_number_of_def number_of_is_id
   1.595 -  nat_add_distrib simp del: nat_number_of)
   1.596 +lemma nat_numeral_Bit0:
   1.597 +  "numeral (Num.Bit0 w) = (let n::nat = numeral w in n + n)"
   1.598 +  unfolding numeral_Bit0 Let_def ..
   1.599  
   1.600 -lemma nat_number_of_Bit1:
   1.601 -  "number_of (Int.Bit1 w) =
   1.602 -    (if neg (number_of w :: int) then 0
   1.603 -     else let n = number_of w in Suc (n + n))"
   1.604 -unfolding Let_def Bit1_def nat_number_of_def number_of_is_id neg_def
   1.605 -apply (cases "w < 0")
   1.606 -apply (simp add: mult_2 [symmetric] add_assoc)
   1.607 -apply (simp only: nat_add_distrib, simp)
   1.608 -done
   1.609 +lemma nat_numeral_Bit1:
   1.610 +  "numeral (Num.Bit1 w) = (let n = numeral w in Suc (n + n))"
   1.611 +  unfolding numeral_Bit1 Let_def by simp
   1.612  
   1.613  lemmas eval_nat_numeral =
   1.614 -  nat_number_of_Bit0 nat_number_of_Bit1
   1.615 +  nat_numeral_Bit0 nat_numeral_Bit1
   1.616  
   1.617  lemmas nat_arith =
   1.618 -  add_nat_number_of
   1.619 -  diff_nat_number_of
   1.620 -  mult_nat_number_of
   1.621 -  eq_nat_number_of
   1.622 -  less_nat_number_of
   1.623 +  diff_nat_numeral
   1.624  
   1.625  lemmas semiring_norm =
   1.626 -  Let_def arith_simps nat_arith rel_simps neg_simps if_False
   1.627 -  if_True add_0 add_Suc add_number_of_left mult_number_of_left
   1.628 +  Let_def arith_simps nat_arith rel_simps
   1.629 +  if_False if_True
   1.630 +  add_0 add_Suc add_numeral_left
   1.631 +  add_neg_numeral_left mult_numeral_left
   1.632    numeral_1_eq_1 [symmetric] Suc_eq_plus1
   1.633 -  numeral_0_eq_0 [symmetric] numerals [symmetric]
   1.634 -  not_iszero_Numeral1
   1.635 +  eq_numeral_iff_iszero not_iszero_Numeral1
   1.636  
   1.637  lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
   1.638    by (fact Let_def)
   1.639  
   1.640 -lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring})"
   1.641 -  by (simp only: number_of_Min power_minus1_even)
   1.642 -
   1.643 -lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring})"
   1.644 -  by (simp only: number_of_Min power_minus1_odd)
   1.645 +lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::ring_1)"
   1.646 +  by (fact power_minus1_even) (* FIXME: duplicate *)
   1.647  
   1.648 -lemma nat_number_of_add_left:
   1.649 -     "number_of v + (number_of v' + (k::nat)) =  
   1.650 -         (if neg (number_of v :: int) then number_of v' + k  
   1.651 -          else if neg (number_of v' :: int) then number_of v + k  
   1.652 -          else number_of (v + v') + k)"
   1.653 -by (auto simp add: neg_def)
   1.654 -
   1.655 -lemma nat_number_of_mult_left:
   1.656 -     "number_of v * (number_of v' * (k::nat)) =  
   1.657 -         (if v < Int.Pls then 0
   1.658 -          else number_of (v * v') * k)"
   1.659 -by (auto simp add: not_less Pls_def nat_number_of_def number_of_is_id
   1.660 -  nat_mult_distrib simp del: nat_number_of)
   1.661 +lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::ring_1)"
   1.662 +  by (fact power_minus1_odd) (* FIXME: duplicate *)
   1.663  
   1.664  
   1.665  subsection{*Literal arithmetic and @{term of_nat}*}
   1.666 @@ -784,52 +471,18 @@
   1.667       "0 \<le> x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)"
   1.668  by (simp only: mult_2 nat_add_distrib of_nat_add) 
   1.669  
   1.670 -lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
   1.671 -by (simp only: nat_number_of_def)
   1.672 -
   1.673 -lemma of_nat_number_of_lemma:
   1.674 -     "of_nat (number_of v :: nat) =  
   1.675 -         (if 0 \<le> (number_of v :: int) 
   1.676 -          then (number_of v :: 'a :: number_semiring)
   1.677 -          else 0)"
   1.678 -  by (auto simp add: int_number_of_def nat_number_of_def number_of_int
   1.679 -    elim!: nonneg_int_cases)
   1.680 -
   1.681 -lemma of_nat_number_of_eq [simp]:
   1.682 -     "of_nat (number_of v :: nat) =  
   1.683 -         (if neg (number_of v :: int) then 0  
   1.684 -          else (number_of v :: 'a :: number_semiring))"
   1.685 -  by (simp only: of_nat_number_of_lemma neg_def, simp)
   1.686 -
   1.687  
   1.688  subsubsection{*For simplifying @{term "Suc m - K"} and  @{term "K - Suc m"}*}
   1.689  
   1.690  text{*Where K above is a literal*}
   1.691  
   1.692 -lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
   1.693 +lemma Suc_diff_eq_diff_pred: "0 < n ==> Suc m - n = m - (n - Numeral1)"
   1.694  by (simp split: nat_diff_split)
   1.695  
   1.696 -text {*Now just instantiating @{text n} to @{text "number_of v"} does
   1.697 -  the right simplification, but with some redundant inequality
   1.698 -  tests.*}
   1.699 -lemma neg_number_of_pred_iff_0:
   1.700 -  "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))"
   1.701 -apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ")
   1.702 -apply (simp only: less_Suc_eq_le le_0_eq)
   1.703 -apply (subst less_number_of_Suc, simp)
   1.704 -done
   1.705 -
   1.706  text{*No longer required as a simprule because of the @{text inverse_fold}
   1.707     simproc*}
   1.708 -lemma Suc_diff_number_of:
   1.709 -     "Int.Pls < v ==>
   1.710 -      Suc m - (number_of v) = m - (number_of (Int.pred v))"
   1.711 -apply (subst Suc_diff_eq_diff_pred)
   1.712 -apply simp
   1.713 -apply (simp del: semiring_numeral_1_eq_1)
   1.714 -apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
   1.715 -                        neg_number_of_pred_iff_0)
   1.716 -done
   1.717 +lemma Suc_diff_numeral: "Suc m - (numeral v) = m - (numeral v - 1)"
   1.718 +  by (subst expand_Suc, simp only: diff_Suc_Suc)
   1.719  
   1.720  lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
   1.721  by (simp split: nat_diff_split)
   1.722 @@ -837,45 +490,22 @@
   1.723  
   1.724  subsubsection{*For @{term nat_case} and @{term nat_rec}*}
   1.725  
   1.726 -lemma nat_case_number_of [simp]:
   1.727 -     "nat_case a f (number_of v) =
   1.728 -        (let pv = number_of (Int.pred v) in
   1.729 -         if neg pv then a else f (nat pv))"
   1.730 -by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
   1.731 +lemma nat_case_numeral [simp]:
   1.732 +  "nat_case a f (numeral v) = (let pv = nat (numeral v - 1) in f pv)"
   1.733 +  by (subst expand_Suc, simp only: nat.cases nat_numeral_diff_1 Let_def)
   1.734  
   1.735  lemma nat_case_add_eq_if [simp]:
   1.736 -     "nat_case a f ((number_of v) + n) =
   1.737 -       (let pv = number_of (Int.pred v) in
   1.738 -         if neg pv then nat_case a f n else f (nat pv + n))"
   1.739 -apply (subst add_eq_if)
   1.740 -apply (simp split add: nat.split
   1.741 -            del: semiring_numeral_1_eq_1
   1.742 -            add: semiring_numeral_1_eq_1 [symmetric]
   1.743 -                 numeral_1_eq_Suc_0 [symmetric]
   1.744 -                 neg_number_of_pred_iff_0)
   1.745 -done
   1.746 +  "nat_case a f ((numeral v) + n) = (let pv = nat (numeral v - 1) in f (pv + n))"
   1.747 +  by (subst expand_Suc, simp only: nat.cases nat_numeral_diff_1 Let_def add_Suc)
   1.748  
   1.749 -lemma nat_rec_number_of [simp]:
   1.750 -     "nat_rec a f (number_of v) =
   1.751 -        (let pv = number_of (Int.pred v) in
   1.752 -         if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
   1.753 -apply (case_tac " (number_of v) ::nat")
   1.754 -apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
   1.755 -apply (simp split add: split_if_asm)
   1.756 -done
   1.757 +lemma nat_rec_numeral [simp]:
   1.758 +  "nat_rec a f (numeral v) = (let pv = nat (numeral v - 1) in f pv (nat_rec a f pv))"
   1.759 +  by (subst expand_Suc, simp only: nat_rec_Suc nat_numeral_diff_1 Let_def)
   1.760  
   1.761  lemma nat_rec_add_eq_if [simp]:
   1.762 -     "nat_rec a f (number_of v + n) =
   1.763 -        (let pv = number_of (Int.pred v) in
   1.764 -         if neg pv then nat_rec a f n
   1.765 -                   else f (nat pv + n) (nat_rec a f (nat pv + n)))"
   1.766 -apply (subst add_eq_if)
   1.767 -apply (simp split add: nat.split
   1.768 -            del: semiring_numeral_1_eq_1
   1.769 -            add: semiring_numeral_1_eq_1 [symmetric]
   1.770 -                 numeral_1_eq_Suc_0 [symmetric]
   1.771 -                 neg_number_of_pred_iff_0)
   1.772 -done
   1.773 +  "nat_rec a f (numeral v + n) =
   1.774 +    (let pv = nat (numeral v - 1) in f (pv + n) (nat_rec a f (pv + n)))"
   1.775 +  by (subst expand_Suc, simp only: nat_rec_Suc nat_numeral_diff_1 Let_def add_Suc)
   1.776  
   1.777  
   1.778  subsubsection{*Various Other Lemmas*}
   1.779 @@ -887,14 +517,14 @@
   1.780  
   1.781  text{*Lemmas for specialist use, NOT as default simprules*}
   1.782  lemma nat_mult_2: "2 * z = (z+z::nat)"
   1.783 -by (rule semiring_mult_2)
   1.784 +by (rule mult_2) (* FIXME: duplicate *)
   1.785  
   1.786  lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
   1.787 -by (rule semiring_mult_2_right)
   1.788 +by (rule mult_2_right) (* FIXME: duplicate *)
   1.789  
   1.790  text{*Case analysis on @{term "n<2"}*}
   1.791  lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
   1.792 -by (auto simp add: nat_1_add_1 [symmetric])
   1.793 +by (auto simp add: numeral_2_eq_2)
   1.794  
   1.795  text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
   1.796  
   1.797 @@ -908,4 +538,8 @@
   1.798  lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
   1.799  by simp
   1.800  
   1.801 +text{*Legacy theorems*}
   1.802 +
   1.803 +lemmas nat_1_add_1 = one_add_one [where 'a=nat]
   1.804 +
   1.805  end