1 (* Title: HOL/nat_bin.ML
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright 1999 University of Cambridge
6 Binary arithmetic for the natural numbers
9 val nat_number_of_def = thm "nat_number_of_def";
11 (** nat (coercion from int to nat) **)
13 Goal "nat (number_of w) = number_of w";
14 by (simp_tac (simpset() addsimps [nat_number_of_def]) 1);
16 Addsimps [nat_number_of, nat_0, nat_1];
18 Goal "Numeral0 = (0::nat)";
19 by (simp_tac (simpset() addsimps [nat_number_of_def]) 1);
22 Goal "Numeral1 = (1::nat)";
23 by (simp_tac (simpset() addsimps [nat_1, nat_number_of_def]) 1);
26 Goal "Numeral1 = Suc 0";
27 by (simp_tac (simpset() addsimps [numeral_1_eq_1]) 1);
28 qed "numeral_1_eq_Suc_0";
30 Goalw [nat_number_of_def] "2 = Suc (Suc 0)";
34 (** int (coercion from nat to int) **)
36 (*"neg" is used in rewrite rules for binary comparisons*)
37 Goal "int (number_of v :: nat) = \
38 \ (if neg (number_of v) then 0 \
39 \ else (number_of v :: int))";
41 (simpset_of Int.thy addsimps [neg_nat, nat_number_of_def,
42 not_neg_nat, int_0]) 1);
43 qed "int_nat_number_of";
44 Addsimps [int_nat_number_of];
47 val nat_bin_arith_setup =
49 (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
50 {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
53 simpset = simpset addsimps [int_nat_number_of, not_neg_number_of_Pls,
54 neg_number_of_Min,neg_number_of_BIT]})];
58 Goal "(0::int) <= z ==> Suc (nat z) = nat (1 + z)";
60 by (asm_simp_tac (simpset() addsimps [nat_eq_iff, int_Suc]) 1);
61 qed "Suc_nat_eq_nat_zadd1";
63 Goal "Suc (number_of v + n) = \
64 \ (if neg (number_of v) then 1+n else number_of (bin_succ v) + n)";
66 (simpset_of Int.thy addsimps [neg_nat, nat_1, not_neg_eq_ge_0,
67 nat_number_of_def, int_Suc,
68 Suc_nat_eq_nat_zadd1, number_of_succ]) 1);
69 qed "Suc_nat_number_of_add";
71 Goal "Suc (number_of v) = \
72 \ (if neg (number_of v) then 1 else number_of (bin_succ v))";
73 by (cut_inst_tac [("n","0")] Suc_nat_number_of_add 1);
74 by (asm_full_simp_tac (simpset() delcongs [if_weak_cong]) 1);
75 qed "Suc_nat_number_of";
76 Addsimps [Suc_nat_number_of];
80 Goal "[| (0::int) <= z; 0 <= z' |] ==> nat (z+z') = nat z + nat z'";
81 by (rtac (inj_int RS injD) 1);
82 by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1);
83 qed "nat_add_distrib";
85 (*"neg" is used in rewrite rules for binary comparisons*)
86 Goal "(number_of v :: nat) + number_of v' = \
87 \ (if neg (number_of v) then number_of v' \
88 \ else if neg (number_of v') then number_of v \
89 \ else number_of (bin_add v v'))";
91 (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
92 nat_add_distrib RS sym, number_of_add]) 1);
93 qed "add_nat_number_of";
95 Addsimps [add_nat_number_of];
100 Goal "[| (0::int) <= z'; z' <= z |] ==> nat (z-z') = nat z - nat z'";
101 by (rtac (inj_int RS injD) 1);
102 by (asm_simp_tac (simpset() addsimps [zdiff_int RS sym, nat_le_eq_zle]) 1);
103 qed "nat_diff_distrib";
106 Goal "nat z - nat z' = \
107 \ (if neg z' then nat z \
108 \ else let d = z-z' in \
109 \ if neg d then 0 else nat d)";
110 by (simp_tac (simpset() addsimps [Let_def, nat_diff_distrib RS sym,
111 neg_eq_less_0, not_neg_eq_ge_0]) 1);
112 by (simp_tac (simpset() addsimps [diff_is_0_eq, nat_le_eq_zle]) 1);
113 qed "diff_nat_eq_if";
115 Goalw [nat_number_of_def]
116 "(number_of v :: nat) - number_of v' = \
117 \ (if neg (number_of v') then number_of v \
118 \ else let d = number_of (bin_add v (bin_minus v')) in \
119 \ if neg d then 0 else nat d)";
121 (simpset_of Int.thy delcongs [if_weak_cong]
122 addsimps [not_neg_eq_ge_0, nat_0,
123 diff_nat_eq_if, diff_number_of_eq]) 1);
124 qed "diff_nat_number_of";
126 Addsimps [diff_nat_number_of];
129 (** Multiplication **)
131 Goal "(0::int) <= z ==> nat (z*z') = nat z * nat z'";
132 by (case_tac "0 <= z'" 1);
133 by (asm_full_simp_tac (simpset() addsimps [zmult_le_0_iff]) 2);
134 by (rtac (inj_int RS injD) 1);
135 by (asm_simp_tac (simpset() addsimps [zmult_int RS sym,
136 int_0_le_mult_iff]) 1);
137 qed "nat_mult_distrib";
139 Goal "z <= (0::int) ==> nat(z*z') = nat(-z) * nat(-z')";
141 by (rtac nat_mult_distrib 2);
143 qed "nat_mult_distrib_neg";
145 Goal "(number_of v :: nat) * number_of v' = \
146 \ (if neg (number_of v) then 0 else number_of (bin_mult v v'))";
148 (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
149 nat_mult_distrib RS sym, number_of_mult,
151 qed "mult_nat_number_of";
153 Addsimps [mult_nat_number_of];
158 Goal "(0::int) <= z ==> nat (z div z') = nat z div nat z'";
159 by (case_tac "0 <= z'" 1);
160 by (auto_tac (claset(),
161 simpset() addsimps [div_nonneg_neg_le0, DIVISION_BY_ZERO_DIV]));
162 by (zdiv_undefined_case_tac "z' = 0" 1);
163 by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_DIV]) 1);
164 by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
165 by (rename_tac "m m'" 1);
166 by (subgoal_tac "0 <= int m div int m'" 1);
167 by (asm_full_simp_tac
168 (simpset() addsimps [numeral_0_eq_0, pos_imp_zdiv_nonneg_iff]) 2);
169 by (rtac (inj_int RS injD) 1);
171 by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1);
173 by (asm_full_simp_tac
174 (simpset() addsimps [nat_less_iff RS sym, quorem_def,
175 numeral_0_eq_0, zadd_int, zmult_int]) 1);
176 by (rtac (mod_div_equality RS sym RS trans) 1);
177 by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
178 qed "nat_div_distrib";
180 Goal "(number_of v :: nat) div number_of v' = \
181 \ (if neg (number_of v) then 0 \
182 \ else nat (number_of v div number_of v'))";
184 (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, neg_nat,
185 nat_div_distrib RS sym, nat_0]) 1);
186 qed "div_nat_number_of";
188 Addsimps [div_nat_number_of];
193 (*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
194 Goal "[| (0::int) <= z; 0 <= z' |] ==> nat (z mod z') = nat z mod nat z'";
195 by (zdiv_undefined_case_tac "z' = 0" 1);
196 by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_MOD]) 1);
197 by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
198 by (rename_tac "m m'" 1);
199 by (subgoal_tac "0 <= int m mod int m'" 1);
200 by (asm_full_simp_tac
201 (simpset() addsimps [nat_less_iff, numeral_0_eq_0, pos_mod_sign]) 2);
202 by (rtac (inj_int RS injD) 1);
204 by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1);
206 by (asm_full_simp_tac
207 (simpset() addsimps [nat_less_iff RS sym, quorem_def,
208 numeral_0_eq_0, zadd_int, zmult_int]) 1);
209 by (rtac (mod_div_equality RS sym RS trans) 1);
210 by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
211 qed "nat_mod_distrib";
213 Goal "(number_of v :: nat) mod number_of v' = \
214 \ (if neg (number_of v) then 0 \
215 \ else if neg (number_of v') then number_of v \
216 \ else nat (number_of v mod number_of v'))";
218 (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def,
219 neg_nat, nat_0, DIVISION_BY_ZERO_MOD,
220 nat_mod_distrib RS sym]) 1);
221 qed "mod_nat_number_of";
223 Addsimps [mod_nat_number_of];
225 structure NatAbstractNumeralsData =
227 val dest_eq = HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of
228 val is_numeral = Bin_Simprocs.is_numeral
229 val numeral_0_eq_0 = numeral_0_eq_0
230 val numeral_1_eq_1 = numeral_1_eq_Suc_0
231 val prove_conv = Bin_Simprocs.prove_conv_nohyps "nat_abstract_numerals"
232 fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps))
233 val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq
236 structure NatAbstractNumerals = AbstractNumeralsFun (NatAbstractNumeralsData)
238 val nat_eval_numerals =
239 map Bin_Simprocs.prep_simproc
240 [("nat_div_eval_numerals",
241 Bin_Simprocs.prep_pats ["(Suc 0) div m"],
242 NatAbstractNumerals.proc div_nat_number_of),
243 ("nat_mod_eval_numerals",
244 Bin_Simprocs.prep_pats ["(Suc 0) mod m"],
245 NatAbstractNumerals.proc mod_nat_number_of)];
247 Addsimprocs nat_eval_numerals;
250 (*** Comparisons ***)
254 Goal "[| (0::int) <= z; 0 <= z' |] ==> (nat z = nat z') = (z=z')";
255 by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
256 qed "eq_nat_nat_iff";
258 (*"neg" is used in rewrite rules for binary comparisons*)
259 Goal "((number_of v :: nat) = number_of v') = \
260 \ (if neg (number_of v) then (iszero (number_of v') | neg (number_of v')) \
261 \ else if neg (number_of v') then iszero (number_of v) \
262 \ else iszero (number_of (bin_add v (bin_minus v'))))";
264 (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
265 eq_nat_nat_iff, eq_number_of_eq, nat_0]) 1);
266 by (simp_tac (simpset_of Int.thy addsimps [nat_eq_iff, nat_eq_iff2,
268 by (simp_tac (simpset () addsimps [not_neg_eq_ge_0 RS sym]) 1);
269 qed "eq_nat_number_of";
271 Addsimps [eq_nat_number_of];
273 (** Less-than (<) **)
275 (*"neg" is used in rewrite rules for binary comparisons*)
276 Goal "((number_of v :: nat) < number_of v') = \
277 \ (if neg (number_of v) then neg (number_of (bin_minus v')) \
278 \ else neg (number_of (bin_add v (bin_minus v'))))";
280 (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
281 nat_less_eq_zless, less_number_of_eq_neg,
283 by (simp_tac (simpset_of Int.thy addsimps [neg_eq_less_0, zminus_zless,
284 number_of_minus, zless_nat_eq_int_zless]) 1);
285 qed "less_nat_number_of";
287 Addsimps [less_nat_number_of];
290 (** Less-than-or-equals (<=) **)
292 Goal "(number_of x <= (number_of y::nat)) = \
293 \ (~ number_of y < (number_of x::nat))";
294 by (rtac (linorder_not_less RS sym) 1);
295 qed "le_nat_number_of_eq_not_less";
297 Addsimps [le_nat_number_of_eq_not_less];
300 (*Maps #n to n for n = 0, 1, 2*)
301 bind_thms ("numerals", [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2]);
302 val numeral_ss = simpset() addsimps numerals;
306 Goal "0 < n ==> n = Suc(n - 1)";
307 by (asm_full_simp_tac numeral_ss 1);
310 (*Expresses a natural number constant as the Suc of another one.
311 NOT suitable for rewriting because n recurs in the condition.*)
312 bind_thm ("expand_Suc", inst "n" "number_of ?v" Suc_pred');
316 Goal "Suc n = n + 1";
317 by (asm_simp_tac numeral_ss 1);
318 qed "Suc_eq_add_numeral_1";
320 (* These two can be useful when m = number_of... *)
322 Goal "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))";
324 by (ALLGOALS (asm_simp_tac numeral_ss));
327 Goal "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))";
329 by (ALLGOALS (asm_simp_tac numeral_ss));
332 Goal "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))";
334 by (ALLGOALS (asm_simp_tac numeral_ss));
337 Goal "[| 0<n; 0<m |] ==> m - n < (m::nat)";
338 by (asm_full_simp_tac (numeral_ss addsimps [diff_less]) 1);
341 Addsimps [inst "n" "number_of ?v" diff_less'];
345 Goal "(p::nat) ^ 2 = p*p";
346 by (simp_tac numeral_ss 1);
350 (*** Comparisons involving (0::nat) ***)
352 Goal "(number_of v = (0::nat)) = \
353 \ (if neg (number_of v) then True else iszero (number_of v))";
354 by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym, iszero_0]) 1);
355 qed "eq_number_of_0";
357 Goal "((0::nat) = number_of v) = \
358 \ (if neg (number_of v) then True else iszero (number_of v))";
359 by (rtac ([eq_sym_conv, eq_number_of_0] MRS trans) 1);
360 qed "eq_0_number_of";
362 Goal "((0::nat) < number_of v) = neg (number_of (bin_minus v))";
363 by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
364 qed "less_0_number_of";
366 (*Simplification already handles n<0, n<=0 and 0<=n.*)
367 Addsimps [eq_number_of_0, eq_0_number_of, less_0_number_of];
369 Goal "neg (number_of v) ==> number_of v = (0::nat)";
370 by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym, iszero_0]) 1);
371 qed "neg_imp_number_of_eq_0";
375 (*** Comparisons involving Suc ***)
377 Goal "(number_of v = Suc n) = \
378 \ (let pv = number_of (bin_pred v) in \
379 \ if neg pv then False else nat pv = n)";
381 (simpset_of Int.thy addsimps
382 [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
383 nat_number_of_def, zadd_0] @ zadd_ac) 1);
384 by (res_inst_tac [("x", "number_of v")] spec 1);
385 by (auto_tac (claset(), simpset() addsimps [nat_eq_iff]));
386 qed "eq_number_of_Suc";
388 Goal "(Suc n = number_of v) = \
389 \ (let pv = number_of (bin_pred v) in \
390 \ if neg pv then False else nat pv = n)";
391 by (rtac ([eq_sym_conv, eq_number_of_Suc] MRS trans) 1);
392 qed "Suc_eq_number_of";
394 Goal "(number_of v < Suc n) = \
395 \ (let pv = number_of (bin_pred v) in \
396 \ if neg pv then True else nat pv < n)";
398 (simpset_of Int.thy addsimps
399 [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
400 nat_number_of_def, zadd_0] @ zadd_ac) 1);
401 by (res_inst_tac [("x", "number_of v")] spec 1);
402 by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
403 qed "less_number_of_Suc";
405 Goal "(Suc n < number_of v) = \
406 \ (let pv = number_of (bin_pred v) in \
407 \ if neg pv then False else n < nat pv)";
409 (simpset_of Int.thy addsimps
410 [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
411 nat_number_of_def, zadd_0] @ zadd_ac) 1);
412 by (res_inst_tac [("x", "number_of v")] spec 1);
413 by (auto_tac (claset(), simpset() addsimps [zless_nat_eq_int_zless]));
414 qed "less_Suc_number_of";
416 Goal "(number_of v <= Suc n) = \
417 \ (let pv = number_of (bin_pred v) in \
418 \ if neg pv then True else nat pv <= n)";
421 [Let_def, less_Suc_number_of, linorder_not_less RS sym]) 1);
422 qed "le_number_of_Suc";
424 Goal "(Suc n <= number_of v) = \
425 \ (let pv = number_of (bin_pred v) in \
426 \ if neg pv then False else n <= nat pv)";
429 [Let_def, less_number_of_Suc, linorder_not_less RS sym]) 1);
430 qed "le_Suc_number_of";
432 Addsimps [eq_number_of_Suc, Suc_eq_number_of,
433 less_number_of_Suc, less_Suc_number_of,
434 le_number_of_Suc, le_Suc_number_of];
436 (* Push int(.) inwards: *)
437 Addsimps [zadd_int RS sym];
439 Goal "(m+m = n+n) = (m = (n::int))";
441 val lemma1 = result();
443 Goal "m+m ~= (1::int) + n + n";
445 by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
446 by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
447 val lemma2 = result();
449 Goal "((number_of (v BIT x) ::int) = number_of (w BIT y)) = \
450 \ (x=y & (((number_of v) ::int) = number_of w))";
451 by (simp_tac (simpset_of Int.thy addsimps
452 [number_of_BIT, lemma1, lemma2, eq_commute]) 1);
453 qed "eq_number_of_BIT_BIT";
455 Goal "((number_of (v BIT x) ::int) = number_of Pls) = \
456 \ (x=False & (((number_of v) ::int) = number_of Pls))";
457 by (simp_tac (simpset_of Int.thy addsimps
458 [number_of_BIT, number_of_Pls, eq_commute]) 1);
459 by (res_inst_tac [("x", "number_of v")] spec 1);
461 by (ALLGOALS Full_simp_tac);
462 by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
463 by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
464 qed "eq_number_of_BIT_Pls";
466 Goal "((number_of (v BIT x) ::int) = number_of Min) = \
467 \ (x=True & (((number_of v) ::int) = number_of Min))";
468 by (simp_tac (simpset_of Int.thy addsimps
469 [number_of_BIT, number_of_Min, eq_commute]) 1);
470 by (res_inst_tac [("x", "number_of v")] spec 1);
472 by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
474 qed "eq_number_of_BIT_Min";
476 Goal "(number_of Pls ::int) ~= number_of Min";
478 qed "eq_number_of_Pls_Min";
481 (*** Further lemmas about "nat" ***)
483 Goal "nat (abs (w * z)) = nat (abs w) * nat (abs z)";
484 by (case_tac "z=0 | w=0" 1);
486 by (simp_tac (simpset() addsimps [zabs_def, nat_mult_distrib RS sym,
487 nat_mult_distrib_neg RS sym, zmult_less_0_iff]) 1);
489 qed "nat_abs_mult_distrib";
491 (*Distributive laws for literals*)
492 Addsimps (map (inst "k" "number_of ?v")
493 [add_mult_distrib, add_mult_distrib2,
494 diff_mult_distrib, diff_mult_distrib2]);
497 (*** Literal arithmetic involving powers, type nat ***)
499 Goal "(0::int) <= z ==> nat (z^n) = nat z ^ n";
500 by (induct_tac "n" 1);
501 by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib])));
504 Goal "(number_of v :: nat) ^ n = \
505 \ (if neg (number_of v) then 0^n else nat ((number_of v :: int) ^ n))";
507 (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
509 qed "power_nat_number_of";
511 Addsimps [inst "n" "number_of ?w" power_nat_number_of];
515 (*** Literal arithmetic involving powers, type int ***)
517 Goal "(z::int) ^ (2*a) = (z^a)^2";
518 by (simp_tac (simpset() addsimps [zpower_zpower, mult_commute]) 1);
521 Goal "(p::int) ^ 2 = p*p";
522 by (simp_tac numeral_ss 1);
525 Goal "(z::int) ^ (2*a + 1) = z * (z^a)^2";
526 by (simp_tac (simpset() addsimps [zpower_even, zpower_zadd_distrib]) 1);
529 Goal "(z::int) ^ number_of (w BIT False) = \
530 \ (let w = z ^ (number_of w) in w*w)";
531 by (simp_tac (simpset_of Int.thy addsimps [nat_number_of_def,
532 number_of_BIT, Let_def]) 1);
533 by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1);
534 by (case_tac "(0::int) <= x" 1);
535 by (auto_tac (claset(),
536 simpset() addsimps [nat_mult_distrib, zpower_even, zpower_two]));
537 qed "zpower_number_of_even";
539 Goal "(z::int) ^ number_of (w BIT True) = \
540 \ (if (0::int) <= number_of w \
541 \ then (let w = z ^ (number_of w) in z*w*w) \
543 by (simp_tac (simpset_of Int.thy addsimps [nat_number_of_def,
544 number_of_BIT, Let_def]) 1);
545 by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1);
546 by (case_tac "(0::int) <= x" 1);
547 by (auto_tac (claset(),
548 simpset() addsimps [nat_add_distrib, nat_mult_distrib,
549 zpower_even, zpower_two]));
550 qed "zpower_number_of_odd";
552 Addsimps (map (inst "z" "number_of ?v")
553 [zpower_number_of_even, zpower_number_of_odd]);