src/HOL/Nat_Numeral.thy
changeset 30925 c38cbc0ac8d1
parent 30685 dd5fe091ff04
child 30960 fec1a04b7220
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Wed Apr 15 15:30:39 2009 +0200
     1.3 @@ -0,0 +1,975 @@
     1.4 +(*  Title:      HOL/Nat_Numeral.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 numerals for the natural numbers *}
    1.10 +
    1.11 +theory Nat_Numeral
    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