1 (* Title: HOL/NatBin.ML
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright 1999 University of Cambridge
6 Binary arithmetic for the natural numbers
9 (** nat (coercion from int to nat) **)
11 Goal "nat (number_of w) = number_of w";
12 by (simp_tac (simpset() addsimps [nat_number_of_def]) 1);
14 Addsimps [nat_number_of];
16 (*These rewrites should one day be re-oriented...*)
19 by (simp_tac (simpset_of Int.thy addsimps [nat_0, nat_number_of_def]) 1);
23 by (simp_tac (simpset_of Int.thy addsimps [nat_1, nat_number_of_def]) 1);
27 by (simp_tac (simpset_of Int.thy addsimps [nat_2, nat_number_of_def]) 1);
31 (** int (coercion from nat to int) **)
33 (*"neg" is used in rewrite rules for binary comparisons*)
34 Goal "int (number_of v :: nat) = \
35 \ (if neg (number_of v) then #0 \
36 \ else (number_of v :: int))";
38 (simpset_of Int.thy addsimps [neg_nat, nat_number_of_def,
39 not_neg_nat, int_0]) 1);
40 qed "int_nat_number_of";
41 Addsimps [int_nat_number_of];
46 Goal "(#0::int) <= z ==> Suc (nat z) = nat (#1 + z)";
48 by (asm_simp_tac (simpset() addsimps [nat_eq_iff]) 1);
49 qed "Suc_nat_eq_nat_zadd1";
51 Goal "Suc (number_of v) = \
52 \ (if neg (number_of v) then #1 else number_of (bin_succ v))";
54 (simpset_of Int.thy addsimps [neg_nat, nat_1, not_neg_eq_ge_0,
55 nat_number_of_def, int_Suc,
56 Suc_nat_eq_nat_zadd1, number_of_succ]) 1);
57 qed "Suc_nat_number_of";
60 by (simp_tac (simpset() addsimps [Suc_nat_number_of]) 1);
61 qed "Suc_numeral_0_eq_1";
64 by (simp_tac (simpset() addsimps [Suc_nat_number_of]) 1);
65 qed "Suc_numeral_1_eq_2";
69 Goal "[| (#0::int) <= z; #0 <= z' |] ==> nat (z+z') = nat z + nat z'";
70 by (rtac (inj_int RS injD) 1);
71 by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1);
72 qed "nat_add_distrib";
74 (*"neg" is used in rewrite rules for binary comparisons*)
75 Goal "(number_of v :: nat) + number_of v' = \
76 \ (if neg (number_of v) then number_of v' \
77 \ else if neg (number_of v') then number_of v \
78 \ else number_of (bin_add v v'))";
80 (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
81 nat_add_distrib RS sym, number_of_add]) 1);
82 qed "add_nat_number_of";
84 Addsimps [add_nat_number_of];
89 Goal "[| (#0::int) <= z'; z' <= z |] ==> nat (z-z') = nat z - nat z'";
90 by (rtac (inj_int RS injD) 1);
91 by (asm_simp_tac (simpset() addsimps [zdiff_int RS sym, nat_le_eq_zle]) 1);
92 qed "nat_diff_distrib";
95 Goal "nat z - nat z' = \
96 \ (if neg z' then nat z \
97 \ else let d = z-z' in \
98 \ if neg d then 0 else nat d)";
99 by (simp_tac (simpset() addsimps [Let_def, nat_diff_distrib RS sym,
100 neg_eq_less_0, not_neg_eq_ge_0]) 1);
101 by (simp_tac (simpset() addsimps zcompare_rls@
102 [diff_is_0_eq, nat_le_eq_zle]) 1);
103 qed "diff_nat_eq_if";
105 Goalw [nat_number_of_def]
106 "(number_of v :: nat) - number_of v' = \
107 \ (if neg (number_of v') then number_of v \
108 \ else let d = number_of (bin_add v (bin_minus v')) in \
109 \ if neg d then #0 else nat d)";
111 (simpset_of Int.thy delcongs [if_weak_cong]
112 addsimps [not_neg_eq_ge_0, nat_0,
113 diff_nat_eq_if, diff_number_of_eq]) 1);
114 qed "diff_nat_number_of";
116 Addsimps [diff_nat_number_of];
119 (** Multiplication **)
121 Goal "(#0::int) <= z ==> nat (z*z') = nat z * nat z'";
122 by (case_tac "#0 <= z'" 1);
123 by (subgoal_tac "z'*z <= #0" 2);
124 by (rtac (neg_imp_zmult_nonpos_iff RS iffD2) 3);
125 by (auto_tac (claset(),
126 simpset() addsimps [zmult_commute]));
127 by (subgoal_tac "#0 <= z*z'" 1);
128 by (force_tac (claset() addDs [zmult_zle_mono1], simpset()) 2);
129 by (rtac (inj_int RS injD) 1);
130 by (asm_simp_tac (simpset() addsimps [zmult_int RS sym]) 1);
131 qed "nat_mult_distrib";
133 Goal "(number_of v :: nat) * number_of v' = \
134 \ (if neg (number_of v) then #0 else number_of (bin_mult v v'))";
136 (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
137 nat_mult_distrib RS sym, number_of_mult,
139 qed "mult_nat_number_of";
141 Addsimps [mult_nat_number_of];
146 Goal "(#0::int) <= z ==> nat (z div z') = nat z div nat z'";
147 by (case_tac "#0 <= z'" 1);
148 by (auto_tac (claset(),
149 simpset() addsimps [div_nonneg_neg_le0, DIVISION_BY_ZERO_DIV]));
150 by (zdiv_undefined_case_tac "z' = #0" 1);
151 by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_DIV]) 1);
152 by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
153 by (rename_tac "m m'" 1);
154 by (subgoal_tac "#0 <= int m div int m'" 1);
155 by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, numeral_0_eq_0,
156 pos_imp_zdiv_nonneg_iff]) 2);
157 by (rtac (inj_int RS injD) 1);
159 by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1);
161 by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, quorem_def,
162 numeral_0_eq_0, zadd_int, zmult_int,
163 mod_less_divisor]) 1);
164 by (rtac (mod_div_equality RS sym RS trans) 1);
165 by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
166 qed "nat_div_distrib";
168 Goal "(number_of v :: nat) div number_of v' = \
169 \ (if neg (number_of v) then #0 \
170 \ else nat (number_of v div number_of v'))";
172 (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, neg_nat,
173 nat_div_distrib RS sym, nat_0]) 1);
174 qed "div_nat_number_of";
176 Addsimps [div_nat_number_of];
181 (*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
182 Goal "[| (#0::int) <= z; #0 <= z' |] ==> nat (z mod z') = nat z mod nat z'";
183 by (zdiv_undefined_case_tac "z' = #0" 1);
184 by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_MOD]) 1);
185 by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
186 by (rename_tac "m m'" 1);
187 by (subgoal_tac "#0 <= int m mod int m'" 1);
188 by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, numeral_0_eq_0,
190 by (rtac (inj_int RS injD) 1);
192 by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1);
194 by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, quorem_def,
195 numeral_0_eq_0, zadd_int, zmult_int,
196 mod_less_divisor]) 1);
197 by (rtac (mod_div_equality RS sym RS trans) 1);
198 by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
199 qed "nat_mod_distrib";
201 Goal "(number_of v :: nat) mod number_of v' = \
202 \ (if neg (number_of v) then #0 \
203 \ else if neg (number_of v') then number_of v \
204 \ else nat (number_of v mod number_of v'))";
206 (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def,
207 neg_nat, nat_0, DIVISION_BY_ZERO_MOD,
208 nat_mod_distrib RS sym]) 1);
209 qed "mod_nat_number_of";
211 Addsimps [mod_nat_number_of];
214 (*** Comparisons ***)
218 Goal "[| (#0::int) <= z; #0 <= z' |] ==> (nat z = nat z') = (z=z')";
219 by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
220 qed "eq_nat_nat_iff";
222 (*"neg" is used in rewrite rules for binary comparisons*)
223 Goal "((number_of v :: nat) = number_of v') = \
224 \ (if neg (number_of v) then ((#0::nat) = number_of v') \
225 \ else if neg (number_of v') then iszero (number_of v) \
226 \ else iszero (number_of (bin_add v (bin_minus v'))))";
228 (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
229 eq_nat_nat_iff, eq_number_of_eq, nat_0]) 1);
230 by (simp_tac (simpset_of Int.thy addsimps [nat_eq_iff, iszero_def]) 1);
231 qed "eq_nat_number_of";
233 Addsimps [eq_nat_number_of];
235 (** Less-than (<) **)
237 (*"neg" is used in rewrite rules for binary comparisons*)
238 Goal "((number_of v :: nat) < number_of v') = \
239 \ (if neg (number_of v) then neg (number_of (bin_minus v')) \
240 \ else neg (number_of (bin_add v (bin_minus v'))))";
242 (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
243 nat_less_eq_zless, less_number_of_eq_neg,
245 by (simp_tac (simpset_of Int.thy addsimps [neg_eq_less_int0, zminus_zless,
246 number_of_minus, zless_nat_eq_int_zless]) 1);
247 qed "less_nat_number_of";
249 Addsimps [less_nat_number_of];
252 (** Less-than-or-equals (<=) **)
254 Goal "(number_of x <= (number_of y::nat)) = \
255 \ (~ number_of y < (number_of x::nat))";
256 by (rtac (linorder_not_less RS sym) 1);
257 qed "le_nat_number_of_eq_not_less";
259 Addsimps [le_nat_number_of_eq_not_less];
262 (*** New versions of existing theorems involving 0, 1, 2 ***)
264 fun change_theory thy th =
265 [th, read_instantiate_sg (sign_of thy) [("t","dummyVar")] refl]
266 MRS (conjI RS conjunct1) |> standard;
268 (*Maps n to #n for n = 0, 1, 2*)
270 HOL_ss addsimps [numeral_0_eq_0 RS sym,
271 numeral_1_eq_1 RS sym,
272 numeral_2_eq_2 RS sym,
273 Suc_numeral_1_eq_2, Suc_numeral_0_eq_1];
275 fun rename_numerals thy th = simplify numeral_sym_ss (change_theory thy th);
277 (*Maps #n to n for n = 0, 1, 2*)
279 simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2];
283 Goal "#0 < n ==> n = Suc(n - #1)";
284 by (asm_full_simp_tac numeral_ss 1);
288 fun inst x t = read_instantiate_sg (sign_of NatBin.thy) [(x,t)];
290 (*Expresses a natural number constant as the Suc of another one.
291 NOT suitable for rewriting because n recurs in the condition.*)
292 bind_thm ("expand_Suc", inst "n" "number_of ?v" Suc_pred');
296 Addsimps (map (rename_numerals thy)
297 [min_0L, min_0R, max_0L, max_0R]);
299 AddIffs (map (rename_numerals thy)
300 [Suc_not_Zero, Zero_not_Suc, zero_less_Suc, not_less0, less_one,
302 neq0_conv, zero_neq_conv, not_gr0]);
306 Addsimps (map (rename_numerals thy)
307 [diff_0_eq_0, add_0, add_0_right, add_pred,
308 diff_is_0_eq, zero_is_diff_eq, zero_less_diff,
309 mult_0, mult_0_right, mult_1, mult_1_right,
310 mult_is_0, zero_is_mult, zero_less_mult_iff,
313 AddIffs (map (rename_numerals thy) [add_is_0, zero_is_add, add_gr_0]);
315 Goal "Suc n = n + #1";
316 by (asm_simp_tac numeral_ss 1);
317 qed "Suc_eq_add_numeral_1";
319 (* These two can be useful when m = number_of... *)
321 Goal "(m::nat) + n = (if m=#0 then n else Suc ((m - #1) + n))";
322 by (exhaust_tac "m" 1);
323 by (ALLGOALS (asm_simp_tac numeral_ss));
326 Goal "(m::nat) * n = (if m=#0 then #0 else n + ((m - #1) * n))";
327 by (exhaust_tac "m" 1);
328 by (ALLGOALS (asm_simp_tac numeral_ss));
331 Goal "(p ^ m :: nat) = (if m=#0 then #1 else p * (p ^ (m - #1)))";
332 by (exhaust_tac "m" 1);
333 by (ALLGOALS (asm_simp_tac numeral_ss));
336 Goal "[| #0<n; #0<m |] ==> m - n < (m::nat)";
337 by (asm_full_simp_tac (numeral_ss addsimps [diff_less]) 1);
340 Addsimps [inst "n" "number_of ?v" diff_less'];
342 (*various theorems that aren't in the default simpset*)
343 val add_is_one' = rename_numerals thy add_is_1;
344 val one_is_add' = rename_numerals thy one_is_add;
345 val zero_induct' = rename_numerals thy zero_induct;
346 val diff_self_eq_0' = rename_numerals thy diff_self_eq_0;
347 val mult_eq_self_implies_10' = rename_numerals thy mult_eq_self_implies_10;
348 val le_pred_eq' = rename_numerals thy le_pred_eq;
349 val less_pred_eq' = rename_numerals thy less_pred_eq;
353 Addsimps (map (rename_numerals thy)
354 [mod_1, mod_0, div_1, div_0, mod2_gr_0, mod2_add_self_eq_0,
357 AddIffs (map (rename_numerals thy)
358 [dvd_1_left, dvd_0_right]);
361 val mod_self' = rename_numerals thy mod_self;
362 val div_self' = rename_numerals thy div_self;
363 val div_less' = rename_numerals thy div_less;
364 val mod_mult_self_is_zero' = rename_numerals thy mod_mult_self_is_0;
368 Goal "(p::nat) ^ #0 = #1";
369 by (simp_tac numeral_ss 1);
371 Addsimps [power_zero];
373 val binomial_zero = rename_numerals thy binomial_0;
374 val binomial_Suc' = rename_numerals thy binomial_Suc;
375 val binomial_n_n' = rename_numerals thy binomial_n_n;
377 (*binomial_0_Suc doesn't work well on numerals*)
378 Addsimps (map (rename_numerals thy)
379 [binomial_n_0, binomial_zero, binomial_1]);
382 (*** Comparisons involving 0 ***)
384 Goal "(number_of v = 0) = \
385 \ (if neg (number_of v) then True else iszero (number_of v))";
386 by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
387 qed "eq_number_of_0";
389 Goal "(0 = number_of v) = \
390 \ (if neg (number_of v) then True else iszero (number_of v))";
391 by (rtac ([eq_sym_conv, eq_number_of_0] MRS trans) 1);
392 qed "eq_0_number_of";
394 Goal "(0 < number_of v) = neg (number_of (bin_minus v))";
395 by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
396 qed "less_0_number_of";
398 (*Simplification already handles n<0, n<=0 and 0<=n.*)
399 Addsimps [eq_number_of_0, eq_0_number_of, less_0_number_of];
402 (*** Comparisons involving Suc ***)
404 Goal "(number_of v = Suc n) = \
405 \ (let pv = number_of (bin_pred v) in \
406 \ if neg pv then False else nat pv = n)";
408 (simpset_of Int.thy addsimps
409 [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
410 nat_number_of_def, zadd_0]@zadd_ac@zcompare_rls) 1);
411 by (res_inst_tac [("x", "number_of v")] spec 1);
412 by (auto_tac (claset(),
413 simpset() addsimps [nat_eq_iff]@zcompare_rls));
414 qed "eq_number_of_Suc";
416 Goal "(Suc n = number_of v) = \
417 \ (let pv = number_of (bin_pred v) in \
418 \ if neg pv then False else nat pv = n)";
419 by (rtac ([eq_sym_conv, eq_number_of_Suc] MRS trans) 1);
420 qed "Suc_eq_number_of";
422 Goal "(number_of v < Suc n) = \
423 \ (let pv = number_of (bin_pred v) in \
424 \ if neg pv then True else nat pv < n)";
426 (simpset_of Int.thy addsimps
427 [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
428 nat_number_of_def, zadd_0]@zadd_ac@zcompare_rls) 1);
429 by (res_inst_tac [("x", "number_of v")] spec 1);
430 by (auto_tac (claset(),
431 simpset() addsimps [nat_less_iff]@zcompare_rls));
432 qed "less_number_of_Suc";
434 Goal "(Suc n < number_of v) = \
435 \ (let pv = number_of (bin_pred v) in \
436 \ if neg pv then False else n < nat pv)";
438 (simpset_of Int.thy addsimps
439 [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
440 nat_number_of_def, zadd_0]@zadd_ac@zcompare_rls) 1);
441 by (res_inst_tac [("x", "number_of v")] spec 1);
442 by (auto_tac (claset(),
443 simpset() addsimps [zless_nat_eq_int_zless]@zcompare_rls));
444 qed "less_Suc_number_of";
446 Goal "(number_of v <= Suc n) = \
447 \ (let pv = number_of (bin_pred v) in \
448 \ if neg pv then True else nat pv <= n)";
450 (simpset_of Int.thy addsimps
451 [Let_def, less_Suc_number_of, linorder_not_less RS sym]) 1);
452 qed "le_number_of_Suc";
454 Goal "(Suc n <= number_of v) = \
455 \ (let pv = number_of (bin_pred v) in \
456 \ if neg pv then False else n <= nat pv)";
458 (simpset_of Int.thy addsimps
459 [Let_def, less_number_of_Suc, linorder_not_less RS sym]) 1);
460 qed "le_Suc_number_of";
462 Addsimps [eq_number_of_Suc, Suc_eq_number_of,
463 less_number_of_Suc, less_Suc_number_of,
464 le_number_of_Suc, le_Suc_number_of];