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.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.106 +
1.107 +lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)"
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.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.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.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.154 +
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.162 +
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.168 +
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.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.265 +val Suc_nat_number_of = thm"Suc_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.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.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.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.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.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.460 +
1.461 +lemma Suc_eq_add_numeral_1_left: "Suc n = 1 + n"
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.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.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.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.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.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.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.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.749 +
1.750 +
1.751 +subsubsection{*For @{text cancel_numerals}*}
1.752 +
1.754 +     "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
1.756 +
1.758 +     "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
1.760 +
1.762 +     "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
1.764 +
1.766 +     "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
1.768 +
1.770 +     "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
1.772 +
1.774 +     "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
1.776 +
1.778 +     "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
1.780 +
1.782 +     "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
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.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.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.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.869 +
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.875 +apply (simp split add: nat.split
1.876 +            del: nat_numeral_1_eq_1
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.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.897 +apply (simp split add: nat.split
1.898 +            del: nat_numeral_1_eq_1
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.960 +
1.961 +lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
1.963 +
1.964 +lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
1.966 +
1.967 +lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"