1.1 --- a/src/HOL/NatBin.thy Thu Apr 16 17:29:56 2009 +0200
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