src/HOL/NatBin.thy
changeset 31007 7c871a9cf6f4
parent 31006 644d18da3c77
parent 31003 ed7364584aa7
child 31008 b8f4e351b5bf
     1.1 --- a/src/HOL/NatBin.thy	Wed Apr 22 11:00:25 2009 -0700
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,975 +0,0 @@
     1.4 -(*  Title:      HOL/NatBin.thy
     1.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6 -    Copyright   1999  University of Cambridge
     1.7 -*)
     1.8 -
     1.9 -header {* Binary arithmetic for the natural numbers *}
    1.10 -
    1.11 -theory NatBin
    1.12 -imports IntDiv
    1.13 -uses ("Tools/nat_simprocs.ML")
    1.14 -begin
    1.15 -
    1.16 -text {*
    1.17 -  Arithmetic for naturals is reduced to that for the non-negative integers.
    1.18 -*}
    1.19 -
    1.20 -instantiation nat :: number
    1.21 -begin
    1.22 -
    1.23 -definition
    1.24 -  nat_number_of_def [code inline, code del]: "number_of v = nat (number_of v)"
    1.25 -
    1.26 -instance ..
    1.27 -
    1.28 -end
    1.29 -
    1.30 -lemma [code post]:
    1.31 -  "nat (number_of v) = number_of v"
    1.32 -  unfolding nat_number_of_def ..
    1.33 -
    1.34 -abbreviation (xsymbols)
    1.35 -  power2 :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999) where
    1.36 -  "x\<twosuperior> == x^2"
    1.37 -
    1.38 -notation (latex output)
    1.39 -  power2  ("(_\<twosuperior>)" [1000] 999)
    1.40 -
    1.41 -notation (HTML output)
    1.42 -  power2  ("(_\<twosuperior>)" [1000] 999)
    1.43 -
    1.44 -
    1.45 -subsection {* Predicate for negative binary numbers *}
    1.46 -
    1.47 -definition neg  :: "int \<Rightarrow> bool" where
    1.48 -  "neg Z \<longleftrightarrow> Z < 0"
    1.49 -
    1.50 -lemma not_neg_int [simp]: "~ neg (of_nat n)"
    1.51 -by (simp add: neg_def)
    1.52 -
    1.53 -lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
    1.54 -by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
    1.55 -
    1.56 -lemmas neg_eq_less_0 = neg_def
    1.57 -
    1.58 -lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
    1.59 -by (simp add: neg_def linorder_not_less)
    1.60 -
    1.61 -text{*To simplify inequalities when Numeral1 can get simplified to 1*}
    1.62 -
    1.63 -lemma not_neg_0: "~ neg 0"
    1.64 -by (simp add: One_int_def neg_def)
    1.65 -
    1.66 -lemma not_neg_1: "~ neg 1"
    1.67 -by (simp add: neg_def linorder_not_less zero_le_one)
    1.68 -
    1.69 -lemma neg_nat: "neg z ==> nat z = 0"
    1.70 -by (simp add: neg_def order_less_imp_le) 
    1.71 -
    1.72 -lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
    1.73 -by (simp add: linorder_not_less neg_def)
    1.74 -
    1.75 -text {*
    1.76 -  If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
    1.77 -  @{term Numeral0} IS @{term "number_of Pls"}
    1.78 -*}
    1.79 -
    1.80 -lemma not_neg_number_of_Pls: "~ neg (number_of Int.Pls)"
    1.81 -  by (simp add: neg_def)
    1.82 -
    1.83 -lemma neg_number_of_Min: "neg (number_of Int.Min)"
    1.84 -  by (simp add: neg_def)
    1.85 -
    1.86 -lemma neg_number_of_Bit0:
    1.87 -  "neg (number_of (Int.Bit0 w)) = neg (number_of w)"
    1.88 -  by (simp add: neg_def)
    1.89 -
    1.90 -lemma neg_number_of_Bit1:
    1.91 -  "neg (number_of (Int.Bit1 w)) = neg (number_of w)"
    1.92 -  by (simp add: neg_def)
    1.93 -
    1.94 -lemmas neg_simps [simp] =
    1.95 -  not_neg_0 not_neg_1
    1.96 -  not_neg_number_of_Pls neg_number_of_Min
    1.97 -  neg_number_of_Bit0 neg_number_of_Bit1
    1.98 -
    1.99 -
   1.100 -subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
   1.101 -
   1.102 -declare nat_0 [simp] nat_1 [simp]
   1.103 -
   1.104 -lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
   1.105 -by (simp add: nat_number_of_def)
   1.106 -
   1.107 -lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)"
   1.108 -by (simp add: nat_number_of_def)
   1.109 -
   1.110 -lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
   1.111 -by (simp add: nat_1 nat_number_of_def)
   1.112 -
   1.113 -lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
   1.114 -by (simp add: nat_numeral_1_eq_1)
   1.115 -
   1.116 -lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
   1.117 -apply (unfold nat_number_of_def)
   1.118 -apply (rule nat_2)
   1.119 -done
   1.120 -
   1.121 -
   1.122 -subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
   1.123 -
   1.124 -lemma int_nat_number_of [simp]:
   1.125 -     "int (number_of v) =  
   1.126 -         (if neg (number_of v :: int) then 0  
   1.127 -          else (number_of v :: int))"
   1.128 -  unfolding nat_number_of_def number_of_is_id neg_def
   1.129 -  by simp
   1.130 -
   1.131 -
   1.132 -subsubsection{*Successor *}
   1.133 -
   1.134 -lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
   1.135 -apply (rule sym)
   1.136 -apply (simp add: nat_eq_iff int_Suc)
   1.137 -done
   1.138 -
   1.139 -lemma Suc_nat_number_of_add:
   1.140 -     "Suc (number_of v + n) =  
   1.141 -        (if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)"
   1.142 -  unfolding nat_number_of_def number_of_is_id neg_def numeral_simps
   1.143 -  by (simp add: Suc_nat_eq_nat_zadd1 add_ac)
   1.144 -
   1.145 -lemma Suc_nat_number_of [simp]:
   1.146 -     "Suc (number_of v) =  
   1.147 -        (if neg (number_of v :: int) then 1 else number_of (Int.succ v))"
   1.148 -apply (cut_tac n = 0 in Suc_nat_number_of_add)
   1.149 -apply (simp cong del: if_weak_cong)
   1.150 -done
   1.151 -
   1.152 -
   1.153 -subsubsection{*Addition *}
   1.154 -
   1.155 -lemma add_nat_number_of [simp]:
   1.156 -     "(number_of v :: nat) + number_of v' =  
   1.157 -         (if v < Int.Pls then number_of v'  
   1.158 -          else if v' < Int.Pls then number_of v  
   1.159 -          else number_of (v + v'))"
   1.160 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   1.161 -  by (simp add: nat_add_distrib)
   1.162 -
   1.163 -lemma nat_number_of_add_1 [simp]:
   1.164 -  "number_of v + (1::nat) =
   1.165 -    (if v < Int.Pls then 1 else number_of (Int.succ v))"
   1.166 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   1.167 -  by (simp add: nat_add_distrib)
   1.168 -
   1.169 -lemma nat_1_add_number_of [simp]:
   1.170 -  "(1::nat) + number_of v =
   1.171 -    (if v < Int.Pls then 1 else number_of (Int.succ v))"
   1.172 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   1.173 -  by (simp add: nat_add_distrib)
   1.174 -
   1.175 -lemma nat_1_add_1 [simp]: "1 + 1 = (2::nat)"
   1.176 -  by (rule int_int_eq [THEN iffD1]) simp
   1.177 -
   1.178 -
   1.179 -subsubsection{*Subtraction *}
   1.180 -
   1.181 -lemma diff_nat_eq_if:
   1.182 -     "nat z - nat z' =  
   1.183 -        (if neg z' then nat z   
   1.184 -         else let d = z-z' in     
   1.185 -              if neg d then 0 else nat d)"
   1.186 -by (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
   1.187 -
   1.188 -
   1.189 -lemma diff_nat_number_of [simp]: 
   1.190 -     "(number_of v :: nat) - number_of v' =  
   1.191 -        (if v' < Int.Pls then number_of v  
   1.192 -         else let d = number_of (v + uminus v') in     
   1.193 -              if neg d then 0 else nat d)"
   1.194 -  unfolding nat_number_of_def number_of_is_id numeral_simps neg_def
   1.195 -  by auto
   1.196 -
   1.197 -lemma nat_number_of_diff_1 [simp]:
   1.198 -  "number_of v - (1::nat) =
   1.199 -    (if v \<le> Int.Pls then 0 else number_of (Int.pred v))"
   1.200 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   1.201 -  by auto
   1.202 -
   1.203 -
   1.204 -subsubsection{*Multiplication *}
   1.205 -
   1.206 -lemma mult_nat_number_of [simp]:
   1.207 -     "(number_of v :: nat) * number_of v' =  
   1.208 -       (if v < Int.Pls then 0 else number_of (v * v'))"
   1.209 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   1.210 -  by (simp add: nat_mult_distrib)
   1.211 -
   1.212 -
   1.213 -subsubsection{*Quotient *}
   1.214 -
   1.215 -lemma div_nat_number_of [simp]:
   1.216 -     "(number_of v :: nat)  div  number_of v' =  
   1.217 -          (if neg (number_of v :: int) then 0  
   1.218 -           else nat (number_of v div number_of v'))"
   1.219 -  unfolding nat_number_of_def number_of_is_id neg_def
   1.220 -  by (simp add: nat_div_distrib)
   1.221 -
   1.222 -lemma one_div_nat_number_of [simp]:
   1.223 -     "Suc 0 div number_of v' = nat (1 div number_of v')" 
   1.224 -by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
   1.225 -
   1.226 -
   1.227 -subsubsection{*Remainder *}
   1.228 -
   1.229 -lemma mod_nat_number_of [simp]:
   1.230 -     "(number_of v :: nat)  mod  number_of v' =  
   1.231 -        (if neg (number_of v :: int) then 0  
   1.232 -         else if neg (number_of v' :: int) then number_of v  
   1.233 -         else nat (number_of v mod number_of v'))"
   1.234 -  unfolding nat_number_of_def number_of_is_id neg_def
   1.235 -  by (simp add: nat_mod_distrib)
   1.236 -
   1.237 -lemma one_mod_nat_number_of [simp]:
   1.238 -     "Suc 0 mod number_of v' =  
   1.239 -        (if neg (number_of v' :: int) then Suc 0
   1.240 -         else nat (1 mod number_of v'))"
   1.241 -by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
   1.242 -
   1.243 -
   1.244 -subsubsection{* Divisibility *}
   1.245 -
   1.246 -lemmas dvd_eq_mod_eq_0_number_of =
   1.247 -  dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]
   1.248 -
   1.249 -declare dvd_eq_mod_eq_0_number_of [simp]
   1.250 -
   1.251 -ML
   1.252 -{*
   1.253 -val nat_number_of_def = thm"nat_number_of_def";
   1.254 -
   1.255 -val nat_number_of = thm"nat_number_of";
   1.256 -val nat_numeral_0_eq_0 = thm"nat_numeral_0_eq_0";
   1.257 -val nat_numeral_1_eq_1 = thm"nat_numeral_1_eq_1";
   1.258 -val numeral_1_eq_Suc_0 = thm"numeral_1_eq_Suc_0";
   1.259 -val numeral_2_eq_2 = thm"numeral_2_eq_2";
   1.260 -val nat_div_distrib = thm"nat_div_distrib";
   1.261 -val nat_mod_distrib = thm"nat_mod_distrib";
   1.262 -val int_nat_number_of = thm"int_nat_number_of";
   1.263 -val Suc_nat_eq_nat_zadd1 = thm"Suc_nat_eq_nat_zadd1";
   1.264 -val Suc_nat_number_of_add = thm"Suc_nat_number_of_add";
   1.265 -val Suc_nat_number_of = thm"Suc_nat_number_of";
   1.266 -val add_nat_number_of = thm"add_nat_number_of";
   1.267 -val diff_nat_eq_if = thm"diff_nat_eq_if";
   1.268 -val diff_nat_number_of = thm"diff_nat_number_of";
   1.269 -val mult_nat_number_of = thm"mult_nat_number_of";
   1.270 -val div_nat_number_of = thm"div_nat_number_of";
   1.271 -val mod_nat_number_of = thm"mod_nat_number_of";
   1.272 -*}
   1.273 -
   1.274 -
   1.275 -subsection{*Comparisons*}
   1.276 -
   1.277 -subsubsection{*Equals (=) *}
   1.278 -
   1.279 -lemma eq_nat_nat_iff:
   1.280 -     "[| (0::int) <= z;  0 <= z' |] ==> (nat z = nat z') = (z=z')"
   1.281 -by (auto elim!: nonneg_eq_int)
   1.282 -
   1.283 -lemma eq_nat_number_of [simp]:
   1.284 -     "((number_of v :: nat) = number_of v') =  
   1.285 -      (if neg (number_of v :: int) then (number_of v' :: int) \<le> 0
   1.286 -       else if neg (number_of v' :: int) then (number_of v :: int) = 0
   1.287 -       else v = v')"
   1.288 -  unfolding nat_number_of_def number_of_is_id neg_def
   1.289 -  by auto
   1.290 -
   1.291 -
   1.292 -subsubsection{*Less-than (<) *}
   1.293 -
   1.294 -lemma less_nat_number_of [simp]:
   1.295 -  "(number_of v :: nat) < number_of v' \<longleftrightarrow>
   1.296 -    (if v < v' then Int.Pls < v' else False)"
   1.297 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   1.298 -  by auto
   1.299 -
   1.300 -
   1.301 -subsubsection{*Less-than-or-equal *}
   1.302 -
   1.303 -lemma le_nat_number_of [simp]:
   1.304 -  "(number_of v :: nat) \<le> number_of v' \<longleftrightarrow>
   1.305 -    (if v \<le> v' then True else v \<le> Int.Pls)"
   1.306 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   1.307 -  by auto
   1.308 -
   1.309 -(*Maps #n to n for n = 0, 1, 2*)
   1.310 -lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2
   1.311 -
   1.312 -
   1.313 -subsection{*Powers with Numeric Exponents*}
   1.314 -
   1.315 -text{*We cannot refer to the number @{term 2} in @{text Ring_and_Field.thy}.
   1.316 -We cannot prove general results about the numeral @{term "-1"}, so we have to
   1.317 -use @{term "- 1"} instead.*}
   1.318 -
   1.319 -lemma power2_eq_square: "(a::'a::recpower)\<twosuperior> = a * a"
   1.320 -  by (simp add: numeral_2_eq_2 Power.power_Suc)
   1.321 -
   1.322 -lemma zero_power2 [simp]: "(0::'a::{semiring_1,recpower})\<twosuperior> = 0"
   1.323 -  by (simp add: power2_eq_square)
   1.324 -
   1.325 -lemma one_power2 [simp]: "(1::'a::{semiring_1,recpower})\<twosuperior> = 1"
   1.326 -  by (simp add: power2_eq_square)
   1.327 -
   1.328 -lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x"
   1.329 -  apply (subgoal_tac "3 = Suc (Suc (Suc 0))")
   1.330 -  apply (erule ssubst)
   1.331 -  apply (simp add: power_Suc mult_ac)
   1.332 -  apply (unfold nat_number_of_def)
   1.333 -  apply (subst nat_eq_iff)
   1.334 -  apply simp
   1.335 -done
   1.336 -
   1.337 -text{*Squares of literal numerals will be evaluated.*}
   1.338 -lemmas power2_eq_square_number_of =
   1.339 -    power2_eq_square [of "number_of w", standard]
   1.340 -declare power2_eq_square_number_of [simp]
   1.341 -
   1.342 -
   1.343 -lemma zero_le_power2[simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
   1.344 -  by (simp add: power2_eq_square)
   1.345 -
   1.346 -lemma zero_less_power2[simp]:
   1.347 -     "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,recpower}))"
   1.348 -  by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
   1.349 -
   1.350 -lemma power2_less_0[simp]:
   1.351 -  fixes a :: "'a::{ordered_idom,recpower}"
   1.352 -  shows "~ (a\<twosuperior> < 0)"
   1.353 -by (force simp add: power2_eq_square mult_less_0_iff) 
   1.354 -
   1.355 -lemma zero_eq_power2[simp]:
   1.356 -     "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,recpower}))"
   1.357 -  by (force simp add: power2_eq_square mult_eq_0_iff)
   1.358 -
   1.359 -lemma abs_power2[simp]:
   1.360 -     "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_idom,recpower})"
   1.361 -  by (simp add: power2_eq_square abs_mult abs_mult_self)
   1.362 -
   1.363 -lemma power2_abs[simp]:
   1.364 -     "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_idom,recpower})"
   1.365 -  by (simp add: power2_eq_square abs_mult_self)
   1.366 -
   1.367 -lemma power2_minus[simp]:
   1.368 -     "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,recpower})"
   1.369 -  by (simp add: power2_eq_square)
   1.370 -
   1.371 -lemma power2_le_imp_le:
   1.372 -  fixes x y :: "'a::{ordered_semidom,recpower}"
   1.373 -  shows "\<lbrakk>x\<twosuperior> \<le> y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x \<le> y"
   1.374 -unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
   1.375 -
   1.376 -lemma power2_less_imp_less:
   1.377 -  fixes x y :: "'a::{ordered_semidom,recpower}"
   1.378 -  shows "\<lbrakk>x\<twosuperior> < y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x < y"
   1.379 -by (rule power_less_imp_less_base)
   1.380 -
   1.381 -lemma power2_eq_imp_eq:
   1.382 -  fixes x y :: "'a::{ordered_semidom,recpower}"
   1.383 -  shows "\<lbrakk>x\<twosuperior> = y\<twosuperior>; 0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> x = y"
   1.384 -unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base, simp)
   1.385 -
   1.386 -lemma power_minus1_even[simp]: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
   1.387 -proof (induct n)
   1.388 -  case 0 show ?case by simp
   1.389 -next
   1.390 -  case (Suc n) then show ?case by (simp add: power_Suc power_add)
   1.391 -qed
   1.392 -
   1.393 -lemma power_minus1_odd: "(- 1) ^ Suc(2*n) = -(1::'a::{comm_ring_1,recpower})"
   1.394 -  by (simp add: power_Suc) 
   1.395 -
   1.396 -lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
   1.397 -by (subst mult_commute) (simp add: power_mult)
   1.398 -
   1.399 -lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
   1.400 -by (simp add: power_even_eq) 
   1.401 -
   1.402 -lemma power_minus_even [simp]:
   1.403 -     "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
   1.404 -by (simp add: power_minus1_even power_minus [of a]) 
   1.405 -
   1.406 -lemma zero_le_even_power'[simp]:
   1.407 -     "0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)"
   1.408 -proof (induct "n")
   1.409 -  case 0
   1.410 -    show ?case by (simp add: zero_le_one)
   1.411 -next
   1.412 -  case (Suc n)
   1.413 -    have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
   1.414 -      by (simp add: mult_ac power_add power2_eq_square)
   1.415 -    thus ?case
   1.416 -      by (simp add: prems zero_le_mult_iff)
   1.417 -qed
   1.418 -
   1.419 -lemma odd_power_less_zero:
   1.420 -     "(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0"
   1.421 -proof (induct "n")
   1.422 -  case 0
   1.423 -  then show ?case by simp
   1.424 -next
   1.425 -  case (Suc n)
   1.426 -  have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
   1.427 -    by (simp add: mult_ac power_add power2_eq_square)
   1.428 -  thus ?case
   1.429 -    by (simp del: power_Suc add: prems mult_less_0_iff mult_neg_neg)
   1.430 -qed
   1.431 -
   1.432 -lemma odd_0_le_power_imp_0_le:
   1.433 -     "0 \<le> a  ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_idom,recpower})"
   1.434 -apply (insert odd_power_less_zero [of a n]) 
   1.435 -apply (force simp add: linorder_not_less [symmetric]) 
   1.436 -done
   1.437 -
   1.438 -text{*Simprules for comparisons where common factors can be cancelled.*}
   1.439 -lemmas zero_compare_simps =
   1.440 -    add_strict_increasing add_strict_increasing2 add_increasing
   1.441 -    zero_le_mult_iff zero_le_divide_iff 
   1.442 -    zero_less_mult_iff zero_less_divide_iff 
   1.443 -    mult_le_0_iff divide_le_0_iff 
   1.444 -    mult_less_0_iff divide_less_0_iff 
   1.445 -    zero_le_power2 power2_less_0
   1.446 -
   1.447 -subsubsection{*Nat *}
   1.448 -
   1.449 -lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
   1.450 -by (simp add: numerals)
   1.451 -
   1.452 -(*Expresses a natural number constant as the Suc of another one.
   1.453 -  NOT suitable for rewriting because n recurs in the condition.*)
   1.454 -lemmas expand_Suc = Suc_pred' [of "number_of v", standard]
   1.455 -
   1.456 -subsubsection{*Arith *}
   1.457 -
   1.458 -lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
   1.459 -by (simp add: numerals)
   1.460 -
   1.461 -lemma Suc_eq_add_numeral_1_left: "Suc n = 1 + n"
   1.462 -by (simp add: numerals)
   1.463 -
   1.464 -(* These two can be useful when m = number_of... *)
   1.465 -
   1.466 -lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
   1.467 -  unfolding One_nat_def by (cases m) simp_all
   1.468 -
   1.469 -lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"
   1.470 -  unfolding One_nat_def by (cases m) simp_all
   1.471 -
   1.472 -lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
   1.473 -  unfolding One_nat_def by (cases m) simp_all
   1.474 -
   1.475 -
   1.476 -subsection{*Comparisons involving (0::nat) *}
   1.477 -
   1.478 -text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
   1.479 -
   1.480 -lemma eq_number_of_0 [simp]:
   1.481 -  "number_of v = (0::nat) \<longleftrightarrow> v \<le> Int.Pls"
   1.482 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   1.483 -  by auto
   1.484 -
   1.485 -lemma eq_0_number_of [simp]:
   1.486 -  "(0::nat) = number_of v \<longleftrightarrow> v \<le> Int.Pls"
   1.487 -by (rule trans [OF eq_sym_conv eq_number_of_0])
   1.488 -
   1.489 -lemma less_0_number_of [simp]:
   1.490 -   "(0::nat) < number_of v \<longleftrightarrow> Int.Pls < v"
   1.491 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   1.492 -  by simp
   1.493 -
   1.494 -lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
   1.495 -by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
   1.496 -
   1.497 -
   1.498 -
   1.499 -subsection{*Comparisons involving  @{term Suc} *}
   1.500 -
   1.501 -lemma eq_number_of_Suc [simp]:
   1.502 -     "(number_of v = Suc n) =  
   1.503 -        (let pv = number_of (Int.pred v) in  
   1.504 -         if neg pv then False else nat pv = n)"
   1.505 -apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   1.506 -                  number_of_pred nat_number_of_def 
   1.507 -            split add: split_if)
   1.508 -apply (rule_tac x = "number_of v" in spec)
   1.509 -apply (auto simp add: nat_eq_iff)
   1.510 -done
   1.511 -
   1.512 -lemma Suc_eq_number_of [simp]:
   1.513 -     "(Suc n = number_of v) =  
   1.514 -        (let pv = number_of (Int.pred v) in  
   1.515 -         if neg pv then False else nat pv = n)"
   1.516 -by (rule trans [OF eq_sym_conv eq_number_of_Suc])
   1.517 -
   1.518 -lemma less_number_of_Suc [simp]:
   1.519 -     "(number_of v < Suc n) =  
   1.520 -        (let pv = number_of (Int.pred v) in  
   1.521 -         if neg pv then True else nat pv < n)"
   1.522 -apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   1.523 -                  number_of_pred nat_number_of_def  
   1.524 -            split add: split_if)
   1.525 -apply (rule_tac x = "number_of v" in spec)
   1.526 -apply (auto simp add: nat_less_iff)
   1.527 -done
   1.528 -
   1.529 -lemma less_Suc_number_of [simp]:
   1.530 -     "(Suc n < number_of v) =  
   1.531 -        (let pv = number_of (Int.pred v) in  
   1.532 -         if neg pv then False else n < nat pv)"
   1.533 -apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   1.534 -                  number_of_pred nat_number_of_def
   1.535 -            split add: split_if)
   1.536 -apply (rule_tac x = "number_of v" in spec)
   1.537 -apply (auto simp add: zless_nat_eq_int_zless)
   1.538 -done
   1.539 -
   1.540 -lemma le_number_of_Suc [simp]:
   1.541 -     "(number_of v <= Suc n) =  
   1.542 -        (let pv = number_of (Int.pred v) in  
   1.543 -         if neg pv then True else nat pv <= n)"
   1.544 -by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
   1.545 -
   1.546 -lemma le_Suc_number_of [simp]:
   1.547 -     "(Suc n <= number_of v) =  
   1.548 -        (let pv = number_of (Int.pred v) in  
   1.549 -         if neg pv then False else n <= nat pv)"
   1.550 -by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
   1.551 -
   1.552 -
   1.553 -lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Int.Min"
   1.554 -by auto
   1.555 -
   1.556 -
   1.557 -
   1.558 -subsection{*Max and Min Combined with @{term Suc} *}
   1.559 -
   1.560 -lemma max_number_of_Suc [simp]:
   1.561 -     "max (Suc n) (number_of v) =  
   1.562 -        (let pv = number_of (Int.pred v) in  
   1.563 -         if neg pv then Suc n else Suc(max n (nat pv)))"
   1.564 -apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   1.565 -            split add: split_if nat.split)
   1.566 -apply (rule_tac x = "number_of v" in spec) 
   1.567 -apply auto
   1.568 -done
   1.569 - 
   1.570 -lemma max_Suc_number_of [simp]:
   1.571 -     "max (number_of v) (Suc n) =  
   1.572 -        (let pv = number_of (Int.pred v) in  
   1.573 -         if neg pv then Suc n else Suc(max (nat pv) n))"
   1.574 -apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   1.575 -            split add: split_if nat.split)
   1.576 -apply (rule_tac x = "number_of v" in spec) 
   1.577 -apply auto
   1.578 -done
   1.579 - 
   1.580 -lemma min_number_of_Suc [simp]:
   1.581 -     "min (Suc n) (number_of v) =  
   1.582 -        (let pv = number_of (Int.pred v) in  
   1.583 -         if neg pv then 0 else Suc(min n (nat pv)))"
   1.584 -apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   1.585 -            split add: split_if nat.split)
   1.586 -apply (rule_tac x = "number_of v" in spec) 
   1.587 -apply auto
   1.588 -done
   1.589 - 
   1.590 -lemma min_Suc_number_of [simp]:
   1.591 -     "min (number_of v) (Suc n) =  
   1.592 -        (let pv = number_of (Int.pred v) in  
   1.593 -         if neg pv then 0 else Suc(min (nat pv) n))"
   1.594 -apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   1.595 -            split add: split_if nat.split)
   1.596 -apply (rule_tac x = "number_of v" in spec) 
   1.597 -apply auto
   1.598 -done
   1.599 - 
   1.600 -subsection{*Literal arithmetic involving powers*}
   1.601 -
   1.602 -lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n"
   1.603 -apply (induct "n")
   1.604 -apply (simp_all (no_asm_simp) add: nat_mult_distrib)
   1.605 -done
   1.606 -
   1.607 -lemma power_nat_number_of:
   1.608 -     "(number_of v :: nat) ^ n =  
   1.609 -       (if neg (number_of v :: int) then 0^n else nat ((number_of v :: int) ^ n))"
   1.610 -by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq
   1.611 -         split add: split_if cong: imp_cong)
   1.612 -
   1.613 -
   1.614 -lemmas power_nat_number_of_number_of = power_nat_number_of [of _ "number_of w", standard]
   1.615 -declare power_nat_number_of_number_of [simp]
   1.616 -
   1.617 -
   1.618 -
   1.619 -text{*For arbitrary rings*}
   1.620 -
   1.621 -lemma power_number_of_even:
   1.622 -  fixes z :: "'a::{number_ring,recpower}"
   1.623 -  shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
   1.624 -unfolding Let_def nat_number_of_def number_of_Bit0
   1.625 -apply (rule_tac x = "number_of w" in spec, clarify)
   1.626 -apply (case_tac " (0::int) <= x")
   1.627 -apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square)
   1.628 -done
   1.629 -
   1.630 -lemma power_number_of_odd:
   1.631 -  fixes z :: "'a::{number_ring,recpower}"
   1.632 -  shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
   1.633 -     then (let w = z ^ (number_of w) in z * w * w) else 1)"
   1.634 -unfolding Let_def nat_number_of_def number_of_Bit1
   1.635 -apply (rule_tac x = "number_of w" in spec, auto)
   1.636 -apply (simp only: nat_add_distrib nat_mult_distrib)
   1.637 -apply simp
   1.638 -apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat power_Suc)
   1.639 -done
   1.640 -
   1.641 -lemmas zpower_number_of_even = power_number_of_even [where 'a=int]
   1.642 -lemmas zpower_number_of_odd = power_number_of_odd [where 'a=int]
   1.643 -
   1.644 -lemmas power_number_of_even_number_of [simp] =
   1.645 -    power_number_of_even [of "number_of v", standard]
   1.646 -
   1.647 -lemmas power_number_of_odd_number_of [simp] =
   1.648 -    power_number_of_odd [of "number_of v", standard]
   1.649 -
   1.650 -
   1.651 -
   1.652 -ML
   1.653 -{*
   1.654 -val numeral_ss = @{simpset} addsimps @{thms numerals};
   1.655 -
   1.656 -val nat_bin_arith_setup =
   1.657 - Lin_Arith.map_data
   1.658 -   (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
   1.659 -     {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
   1.660 -      inj_thms = inj_thms,
   1.661 -      lessD = lessD, neqE = neqE,
   1.662 -      simpset = simpset addsimps @{thms neg_simps} @
   1.663 -        [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]})
   1.664 -*}
   1.665 -
   1.666 -declaration {* K nat_bin_arith_setup *}
   1.667 -
   1.668 -(* Enable arith to deal with div/mod k where k is a numeral: *)
   1.669 -declare split_div[of _ _ "number_of k", standard, arith_split]
   1.670 -declare split_mod[of _ _ "number_of k", standard, arith_split]
   1.671 -
   1.672 -lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
   1.673 -  by (simp add: number_of_Pls nat_number_of_def)
   1.674 -
   1.675 -lemma nat_number_of_Min: "number_of Int.Min = (0::nat)"
   1.676 -  apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
   1.677 -  done
   1.678 -
   1.679 -lemma nat_number_of_Bit0:
   1.680 -    "number_of (Int.Bit0 w) = (let n::nat = number_of w in n + n)"
   1.681 -  unfolding nat_number_of_def number_of_is_id numeral_simps Let_def
   1.682 -  by auto
   1.683 -
   1.684 -lemma nat_number_of_Bit1:
   1.685 -  "number_of (Int.Bit1 w) =
   1.686 -    (if neg (number_of w :: int) then 0
   1.687 -     else let n = number_of w in Suc (n + n))"
   1.688 -  unfolding nat_number_of_def number_of_is_id numeral_simps neg_def Let_def
   1.689 -  by auto
   1.690 -
   1.691 -lemmas nat_number =
   1.692 -  nat_number_of_Pls nat_number_of_Min
   1.693 -  nat_number_of_Bit0 nat_number_of_Bit1
   1.694 -
   1.695 -lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
   1.696 -  by (simp add: Let_def)
   1.697 -
   1.698 -lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,recpower})"
   1.699 -by (simp add: power_mult power_Suc); 
   1.700 -
   1.701 -lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,recpower})"
   1.702 -by (simp add: power_mult power_Suc); 
   1.703 -
   1.704 -
   1.705 -subsection{*Literal arithmetic and @{term of_nat}*}
   1.706 -
   1.707 -lemma of_nat_double:
   1.708 -     "0 \<le> x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)"
   1.709 -by (simp only: mult_2 nat_add_distrib of_nat_add) 
   1.710 -
   1.711 -lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
   1.712 -by (simp only: nat_number_of_def)
   1.713 -
   1.714 -lemma of_nat_number_of_lemma:
   1.715 -     "of_nat (number_of v :: nat) =  
   1.716 -         (if 0 \<le> (number_of v :: int) 
   1.717 -          then (number_of v :: 'a :: number_ring)
   1.718 -          else 0)"
   1.719 -by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat);
   1.720 -
   1.721 -lemma of_nat_number_of_eq [simp]:
   1.722 -     "of_nat (number_of v :: nat) =  
   1.723 -         (if neg (number_of v :: int) then 0  
   1.724 -          else (number_of v :: 'a :: number_ring))"
   1.725 -by (simp only: of_nat_number_of_lemma neg_def, simp) 
   1.726 -
   1.727 -
   1.728 -subsection {*Lemmas for the Combination and Cancellation Simprocs*}
   1.729 -
   1.730 -lemma nat_number_of_add_left:
   1.731 -     "number_of v + (number_of v' + (k::nat)) =  
   1.732 -         (if neg (number_of v :: int) then number_of v' + k  
   1.733 -          else if neg (number_of v' :: int) then number_of v + k  
   1.734 -          else number_of (v + v') + k)"
   1.735 -  unfolding nat_number_of_def number_of_is_id neg_def
   1.736 -  by auto
   1.737 -
   1.738 -lemma nat_number_of_mult_left:
   1.739 -     "number_of v * (number_of v' * (k::nat)) =  
   1.740 -         (if v < Int.Pls then 0
   1.741 -          else number_of (v * v') * k)"
   1.742 -by simp
   1.743 -
   1.744 -
   1.745 -subsubsection{*For @{text combine_numerals}*}
   1.746 -
   1.747 -lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
   1.748 -by (simp add: add_mult_distrib)
   1.749 -
   1.750 -
   1.751 -subsubsection{*For @{text cancel_numerals}*}
   1.752 -
   1.753 -lemma nat_diff_add_eq1:
   1.754 -     "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
   1.755 -by (simp split add: nat_diff_split add: add_mult_distrib)
   1.756 -
   1.757 -lemma nat_diff_add_eq2:
   1.758 -     "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
   1.759 -by (simp split add: nat_diff_split add: add_mult_distrib)
   1.760 -
   1.761 -lemma nat_eq_add_iff1:
   1.762 -     "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
   1.763 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   1.764 -
   1.765 -lemma nat_eq_add_iff2:
   1.766 -     "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
   1.767 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   1.768 -
   1.769 -lemma nat_less_add_iff1:
   1.770 -     "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
   1.771 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   1.772 -
   1.773 -lemma nat_less_add_iff2:
   1.774 -     "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
   1.775 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   1.776 -
   1.777 -lemma nat_le_add_iff1:
   1.778 -     "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
   1.779 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   1.780 -
   1.781 -lemma nat_le_add_iff2:
   1.782 -     "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
   1.783 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   1.784 -
   1.785 -
   1.786 -subsubsection{*For @{text cancel_numeral_factors} *}
   1.787 -
   1.788 -lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
   1.789 -by auto
   1.790 -
   1.791 -lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
   1.792 -by auto
   1.793 -
   1.794 -lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
   1.795 -by auto
   1.796 -
   1.797 -lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
   1.798 -by auto
   1.799 -
   1.800 -lemma nat_mult_dvd_cancel_disj[simp]:
   1.801 -  "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
   1.802 -by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
   1.803 -
   1.804 -lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
   1.805 -by(auto)
   1.806 -
   1.807 -
   1.808 -subsubsection{*For @{text cancel_factor} *}
   1.809 -
   1.810 -lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
   1.811 -by auto
   1.812 -
   1.813 -lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
   1.814 -by auto
   1.815 -
   1.816 -lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
   1.817 -by auto
   1.818 -
   1.819 -lemma nat_mult_div_cancel_disj[simp]:
   1.820 -     "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
   1.821 -by (simp add: nat_mult_div_cancel1)
   1.822 -
   1.823 -
   1.824 -subsection {* Simprocs for the Naturals *}
   1.825 -
   1.826 -use "Tools/nat_simprocs.ML"
   1.827 -declaration {* K nat_simprocs_setup *}
   1.828 -
   1.829 -subsubsection{*For simplifying @{term "Suc m - K"} and  @{term "K - Suc m"}*}
   1.830 -
   1.831 -text{*Where K above is a literal*}
   1.832 -
   1.833 -lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
   1.834 -by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
   1.835 -
   1.836 -text {*Now just instantiating @{text n} to @{text "number_of v"} does
   1.837 -  the right simplification, but with some redundant inequality
   1.838 -  tests.*}
   1.839 -lemma neg_number_of_pred_iff_0:
   1.840 -  "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))"
   1.841 -apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ")
   1.842 -apply (simp only: less_Suc_eq_le le_0_eq)
   1.843 -apply (subst less_number_of_Suc, simp)
   1.844 -done
   1.845 -
   1.846 -text{*No longer required as a simprule because of the @{text inverse_fold}
   1.847 -   simproc*}
   1.848 -lemma Suc_diff_number_of:
   1.849 -     "Int.Pls < v ==>
   1.850 -      Suc m - (number_of v) = m - (number_of (Int.pred v))"
   1.851 -apply (subst Suc_diff_eq_diff_pred)
   1.852 -apply simp
   1.853 -apply (simp del: nat_numeral_1_eq_1)
   1.854 -apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
   1.855 -                        neg_number_of_pred_iff_0)
   1.856 -done
   1.857 -
   1.858 -lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
   1.859 -by (simp add: numerals split add: nat_diff_split)
   1.860 -
   1.861 -
   1.862 -subsubsection{*For @{term nat_case} and @{term nat_rec}*}
   1.863 -
   1.864 -lemma nat_case_number_of [simp]:
   1.865 -     "nat_case a f (number_of v) =
   1.866 -        (let pv = number_of (Int.pred v) in
   1.867 -         if neg pv then a else f (nat pv))"
   1.868 -by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
   1.869 -
   1.870 -lemma nat_case_add_eq_if [simp]:
   1.871 -     "nat_case a f ((number_of v) + n) =
   1.872 -       (let pv = number_of (Int.pred v) in
   1.873 -         if neg pv then nat_case a f n else f (nat pv + n))"
   1.874 -apply (subst add_eq_if)
   1.875 -apply (simp split add: nat.split
   1.876 -            del: nat_numeral_1_eq_1
   1.877 -            add: nat_numeral_1_eq_1 [symmetric]
   1.878 -                 numeral_1_eq_Suc_0 [symmetric]
   1.879 -                 neg_number_of_pred_iff_0)
   1.880 -done
   1.881 -
   1.882 -lemma nat_rec_number_of [simp]:
   1.883 -     "nat_rec a f (number_of v) =
   1.884 -        (let pv = number_of (Int.pred v) in
   1.885 -         if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
   1.886 -apply (case_tac " (number_of v) ::nat")
   1.887 -apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
   1.888 -apply (simp split add: split_if_asm)
   1.889 -done
   1.890 -
   1.891 -lemma nat_rec_add_eq_if [simp]:
   1.892 -     "nat_rec a f (number_of v + n) =
   1.893 -        (let pv = number_of (Int.pred v) in
   1.894 -         if neg pv then nat_rec a f n
   1.895 -                   else f (nat pv + n) (nat_rec a f (nat pv + n)))"
   1.896 -apply (subst add_eq_if)
   1.897 -apply (simp split add: nat.split
   1.898 -            del: nat_numeral_1_eq_1
   1.899 -            add: nat_numeral_1_eq_1 [symmetric]
   1.900 -                 numeral_1_eq_Suc_0 [symmetric]
   1.901 -                 neg_number_of_pred_iff_0)
   1.902 -done
   1.903 -
   1.904 -
   1.905 -subsubsection{*Various Other Lemmas*}
   1.906 -
   1.907 -text {*Evens and Odds, for Mutilated Chess Board*}
   1.908 -
   1.909 -text{*Lemmas for specialist use, NOT as default simprules*}
   1.910 -lemma nat_mult_2: "2 * z = (z+z::nat)"
   1.911 -proof -
   1.912 -  have "2*z = (1 + 1)*z" by simp
   1.913 -  also have "... = z+z" by (simp add: left_distrib)
   1.914 -  finally show ?thesis .
   1.915 -qed
   1.916 -
   1.917 -lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
   1.918 -by (subst mult_commute, rule nat_mult_2)
   1.919 -
   1.920 -text{*Case analysis on @{term "n<2"}*}
   1.921 -lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
   1.922 -by arith
   1.923 -
   1.924 -lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)"
   1.925 -by arith
   1.926 -
   1.927 -lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
   1.928 -by (simp add: nat_mult_2 [symmetric])
   1.929 -
   1.930 -lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
   1.931 -apply (subgoal_tac "m mod 2 < 2")
   1.932 -apply (erule less_2_cases [THEN disjE])
   1.933 -apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
   1.934 -done
   1.935 -
   1.936 -lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
   1.937 -apply (subgoal_tac "m mod 2 < 2")
   1.938 -apply (force simp del: mod_less_divisor, simp)
   1.939 -done
   1.940 -
   1.941 -text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
   1.942 -
   1.943 -lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
   1.944 -by simp
   1.945 -
   1.946 -lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
   1.947 -by simp
   1.948 -
   1.949 -text{*Can be used to eliminate long strings of Sucs, but not by default*}
   1.950 -lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
   1.951 -by simp
   1.952 -
   1.953 -
   1.954 -text{*These lemmas collapse some needless occurrences of Suc:
   1.955 -    at least three Sucs, since two and fewer are rewritten back to Suc again!
   1.956 -    We already have some rules to simplify operands smaller than 3.*}
   1.957 -
   1.958 -lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
   1.959 -by (simp add: Suc3_eq_add_3)
   1.960 -
   1.961 -lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
   1.962 -by (simp add: Suc3_eq_add_3)
   1.963 -
   1.964 -lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
   1.965 -by (simp add: Suc3_eq_add_3)
   1.966 -
   1.967 -lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
   1.968 -by (simp add: Suc3_eq_add_3)
   1.969 -
   1.970 -lemmas Suc_div_eq_add3_div_number_of =
   1.971 -    Suc_div_eq_add3_div [of _ "number_of v", standard]
   1.972 -declare Suc_div_eq_add3_div_number_of [simp]
   1.973 -
   1.974 -lemmas Suc_mod_eq_add3_mod_number_of =
   1.975 -    Suc_mod_eq_add3_mod [of _ "number_of v", standard]
   1.976 -declare Suc_mod_eq_add3_mod_number_of [simp]
   1.977 -
   1.978 -end