7032
|
1 |
(* Title: HOL/NatBin.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1999 University of Cambridge
|
|
5 |
|
|
6 |
Binary arithmetic for the natural numbers
|
|
7 |
*)
|
|
8 |
|
|
9 |
(** nat (coercion from int to nat) **)
|
|
10 |
|
|
11 |
Goal "nat (number_of w) = number_of w";
|
|
12 |
by (simp_tac (simpset() addsimps [nat_number_of_def]) 1);
|
|
13 |
qed "nat_number_of";
|
|
14 |
Addsimps [nat_number_of];
|
|
15 |
|
|
16 |
(*These rewrites should one day be re-oriented...*)
|
|
17 |
|
|
18 |
Goal "#0 = 0";
|
|
19 |
by (simp_tac (simpset_of Int.thy addsimps [nat_0, nat_number_of_def]) 1);
|
|
20 |
qed "numeral_0_eq_0";
|
|
21 |
|
|
22 |
Goal "#1 = 1";
|
|
23 |
by (simp_tac (simpset_of Int.thy addsimps [nat_1, nat_number_of_def]) 1);
|
|
24 |
qed "numeral_1_eq_1";
|
|
25 |
|
|
26 |
Goal "#2 = 2";
|
|
27 |
by (simp_tac (simpset_of Int.thy addsimps [nat_2, nat_number_of_def]) 1);
|
|
28 |
qed "numeral_2_eq_2";
|
|
29 |
|
|
30 |
|
|
31 |
(** int (coercion from nat to int) **)
|
|
32 |
|
|
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))";
|
|
37 |
by (simp_tac
|
|
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];
|
|
42 |
|
|
43 |
|
|
44 |
(** Successor **)
|
|
45 |
|
|
46 |
Goal "(#0::int) <= z ==> Suc (nat z) = nat (#1 + z)";
|
|
47 |
br sym 1;
|
|
48 |
by (asm_simp_tac (simpset() addsimps [nat_eq_iff]) 1);
|
|
49 |
qed "Suc_nat_eq_nat_zadd1";
|
|
50 |
|
|
51 |
Goal "Suc (number_of v) = \
|
|
52 |
\ (if neg (number_of v) then #1 else number_of (bin_succ v))";
|
|
53 |
by (simp_tac
|
|
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";
|
|
58 |
|
|
59 |
Goal "Suc #0 = #1";
|
|
60 |
by (simp_tac (simpset() addsimps [Suc_nat_number_of]) 1);
|
|
61 |
qed "Suc_numeral_0_eq_1";
|
|
62 |
|
|
63 |
Goal "Suc #1 = #2";
|
|
64 |
by (simp_tac (simpset() addsimps [Suc_nat_number_of]) 1);
|
|
65 |
qed "Suc_numeral_1_eq_2";
|
|
66 |
|
|
67 |
(** Addition **)
|
|
68 |
|
|
69 |
Goal "[| (#0::int) <= z; #0 <= z' |] ==> nat z + nat z' = nat (z+z')";
|
|
70 |
by (rtac (inj_int RS injD) 1);
|
|
71 |
by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1);
|
|
72 |
qed "add_nat_eq_nat_zadd";
|
|
73 |
|
|
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'))";
|
|
79 |
by (simp_tac
|
|
80 |
(simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
|
|
81 |
add_nat_eq_nat_zadd, number_of_add]) 1);
|
|
82 |
qed "add_nat_number_of";
|
|
83 |
|
|
84 |
Addsimps [add_nat_number_of];
|
|
85 |
|
|
86 |
|
|
87 |
(** Subtraction **)
|
|
88 |
|
|
89 |
Goal "[| (#0::int) <= z'; z' <= z |] ==> nat z - nat z' = nat (z-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 "diff_nat_eq_nat_zdiff";
|
|
93 |
|
|
94 |
|
|
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, diff_nat_eq_nat_zdiff,
|
|
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";
|
|
104 |
|
|
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)";
|
|
110 |
by (simp_tac
|
|
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";
|
|
115 |
|
|
116 |
Addsimps [diff_nat_number_of];
|
|
117 |
|
|
118 |
|
|
119 |
(** Multiplication **)
|
|
120 |
|
|
121 |
Goal "(#0::int) <= z ==> nat z * nat z' = nat (z*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;
|
|
126 |
by (subgoal_tac "#0 <= z*z'" 1);
|
|
127 |
by (force_tac (claset() addDs [zmult_zle_mono1], simpset()) 2);
|
|
128 |
by (rtac (inj_int RS injD) 1);
|
|
129 |
by (asm_simp_tac (simpset() addsimps [zmult_int RS sym]) 1);
|
|
130 |
qed "mult_nat_eq_nat_zmult";
|
|
131 |
|
|
132 |
Goal "(number_of v :: nat) * number_of v' = \
|
|
133 |
\ (if neg (number_of v) then #0 else number_of (bin_mult v v'))";
|
|
134 |
by (simp_tac
|
|
135 |
(simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
|
|
136 |
mult_nat_eq_nat_zmult, number_of_mult,
|
|
137 |
nat_0]) 1);
|
|
138 |
qed "mult_nat_number_of";
|
|
139 |
|
|
140 |
Addsimps [mult_nat_number_of];
|
|
141 |
|
|
142 |
|
|
143 |
(** Quotient **)
|
|
144 |
|
|
145 |
Goal "(#0::int) <= z ==> nat z div nat z' = nat (z div z')";
|
|
146 |
by (case_tac "#0 <= z'" 1);
|
|
147 |
by (auto_tac (claset(),
|
|
148 |
simpset() addsimps [div_nonneg_neg, DIVISION_BY_ZERO_DIV]));
|
|
149 |
by (zdiv_undefined_case_tac "z' = #0" 1);
|
|
150 |
by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_DIV]) 1);
|
|
151 |
by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
|
|
152 |
by (rename_tac "m m'" 1);
|
|
153 |
by (subgoal_tac "#0 <= int m div int m'" 1);
|
|
154 |
by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, numeral_0_eq_0,
|
|
155 |
pos_imp_zdiv_nonneg_iff]) 2);
|
|
156 |
by (rtac (inj_int RS injD) 1);
|
|
157 |
by (Asm_simp_tac 1);
|
|
158 |
by (rtac sym 1);
|
|
159 |
by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1);
|
|
160 |
by (Force_tac 2);
|
|
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 "div_nat_eq_nat_zdiv";
|
|
167 |
|
|
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'))";
|
|
171 |
by (simp_tac
|
|
172 |
(simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, neg_nat,
|
|
173 |
div_nat_eq_nat_zdiv, nat_0]) 1);
|
|
174 |
qed "div_nat_number_of";
|
|
175 |
|
|
176 |
Addsimps [div_nat_number_of];
|
|
177 |
|
|
178 |
|
|
179 |
(** Remainder **)
|
|
180 |
|
|
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 nat z' = nat (z mod 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,
|
|
189 |
pos_mod_sign]) 2);
|
|
190 |
by (rtac (inj_int RS injD) 1);
|
|
191 |
by (Asm_simp_tac 1);
|
|
192 |
by (rtac sym 1);
|
|
193 |
by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1);
|
|
194 |
by (Force_tac 2);
|
|
195 |
by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, quorem_def,
|
|
196 |
numeral_0_eq_0, zadd_int, zmult_int,
|
|
197 |
mod_less_divisor]) 1);
|
|
198 |
by (rtac (mod_div_equality RS sym RS trans) 1);
|
|
199 |
by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
|
|
200 |
qed "mod_nat_eq_nat_zmod";
|
|
201 |
|
|
202 |
Goal "(number_of v :: nat) mod number_of v' = \
|
|
203 |
\ (if neg (number_of v) then #0 \
|
|
204 |
\ else if neg (number_of v') then number_of v \
|
|
205 |
\ else nat (number_of v mod number_of v'))";
|
|
206 |
by (simp_tac
|
|
207 |
(simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def,
|
|
208 |
neg_nat, nat_0, DIVISION_BY_ZERO_MOD,
|
|
209 |
mod_nat_eq_nat_zmod]) 1);
|
|
210 |
qed "mod_nat_number_of";
|
|
211 |
|
|
212 |
Addsimps [mod_nat_number_of];
|
|
213 |
|
|
214 |
|
|
215 |
(*** Comparisons ***)
|
|
216 |
|
|
217 |
(** Equals (=) **)
|
|
218 |
|
|
219 |
Goal "[| (#0::int) <= z; #0 <= z' |] ==> (nat z = nat z') = (z=z')";
|
|
220 |
by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
|
|
221 |
qed "eq_nat_nat_iff";
|
|
222 |
|
|
223 |
(*"neg" is used in rewrite rules for binary comparisons*)
|
|
224 |
Goal "((number_of v :: nat) = number_of v') = \
|
|
225 |
\ (if neg (number_of v) then ((#0::nat) = number_of v') \
|
|
226 |
\ else if neg (number_of v') then iszero (number_of v) \
|
|
227 |
\ else iszero (number_of (bin_add v (bin_minus v'))))";
|
|
228 |
by (simp_tac
|
|
229 |
(simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
|
|
230 |
eq_nat_nat_iff, eq_number_of_eq, nat_0]) 1);
|
|
231 |
by (simp_tac (simpset_of Int.thy addsimps [nat_eq_iff, iszero_def]) 1);
|
|
232 |
qed "eq_nat_number_of";
|
|
233 |
|
|
234 |
Addsimps [eq_nat_number_of];
|
|
235 |
|
|
236 |
(** Less-than (<) **)
|
|
237 |
|
|
238 |
(*"neg" is used in rewrite rules for binary comparisons*)
|
|
239 |
Goal "((number_of v :: nat) < number_of v') = \
|
|
240 |
\ (if neg (number_of v) then neg (number_of (bin_minus v')) \
|
|
241 |
\ else neg (number_of (bin_add v (bin_minus v'))))";
|
|
242 |
by (simp_tac
|
|
243 |
(simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
|
|
244 |
nat_less_eq_zless, less_number_of_eq_neg,
|
|
245 |
nat_0]) 1);
|
|
246 |
by (simp_tac (simpset_of Int.thy addsimps [neg_eq_less_int0, zminus_zless,
|
|
247 |
number_of_minus, zless_zero_nat]) 1);
|
|
248 |
qed "less_nat_number_of";
|
|
249 |
|
|
250 |
Addsimps [less_nat_number_of];
|
|
251 |
|
|
252 |
|
|
253 |
(** Less-than-or-equals (<=) **)
|
|
254 |
|
|
255 |
Goal "(number_of x <= (number_of y::nat)) = \
|
|
256 |
\ (~ number_of y < (number_of x::nat))";
|
|
257 |
by (rtac (linorder_not_less RS sym) 1);
|
|
258 |
qed "le_nat_number_of_eq_not_less";
|
|
259 |
|
|
260 |
Addsimps [le_nat_number_of_eq_not_less];
|
|
261 |
|
|
262 |
|
|
263 |
(*** New versions of existing theorems involving 0, 1, 2 ***)
|
|
264 |
|
|
265 |
fun change_theory thy th =
|
|
266 |
[th, read_instantiate_sg (sign_of thy) [("t","dummyVar")] refl]
|
|
267 |
MRS (conjI RS conjunct1) |> standard;
|
|
268 |
|
|
269 |
(*Maps n to #n for n = 0, 1, 2*)
|
|
270 |
val numeral_sym_ss =
|
|
271 |
HOL_ss addsimps [numeral_0_eq_0 RS sym,
|
|
272 |
numeral_1_eq_1 RS sym,
|
|
273 |
numeral_2_eq_2 RS sym,
|
|
274 |
Suc_numeral_1_eq_2, Suc_numeral_0_eq_1];
|
|
275 |
|
|
276 |
fun rename_numerals thy th = simplify numeral_sym_ss (change_theory thy th);
|
|
277 |
|
|
278 |
(*Maps #n to n for n = 0, 1, 2*)
|
|
279 |
val numeral_ss =
|
|
280 |
simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2];
|
|
281 |
|
|
282 |
(** Nat **)
|
|
283 |
|
|
284 |
Goal "#0 < n ==> n = Suc(n - #1)";
|
|
285 |
by (asm_full_simp_tac numeral_ss 1);
|
|
286 |
qed "Suc_pred'";
|
|
287 |
|
|
288 |
|
|
289 |
fun inst x t = read_instantiate_sg (sign_of NatBin.thy) [(x,t)];
|
|
290 |
|
|
291 |
(*Expresses a natural number constant as the Suc of another one.
|
|
292 |
NOT suitable for rewriting because n recurs in the condition.*)
|
|
293 |
bind_thm ("expand_Suc", inst "n" "number_of ?v" Suc_pred');
|
|
294 |
|
|
295 |
(** Arith **)
|
|
296 |
|
|
297 |
Addsimps (map (rename_numerals thy)
|
|
298 |
[diff_0_eq_0, add_0, add_0_right, add_pred,
|
|
299 |
diff_is_0_eq RS iffD2, zero_less_diff,
|
|
300 |
mult_0, mult_0_right, mult_1, mult_1_right,
|
|
301 |
mult_is_0, zero_less_mult_iff,
|
|
302 |
mult_eq_1_iff]);
|
|
303 |
|
|
304 |
AddIffs (map (rename_numerals thy) [add_is_0, zero_is_add, add_gr_0]);
|
|
305 |
|
|
306 |
(* These two can be useful when m = number_of... *)
|
|
307 |
|
|
308 |
Goal "(m::nat) + n = (if m=#0 then n else Suc ((m - #1) + n))";
|
|
309 |
by (exhaust_tac "m" 1);
|
|
310 |
by (ALLGOALS (asm_simp_tac numeral_ss));
|
|
311 |
qed "add_eq_if";
|
|
312 |
|
|
313 |
Goal "(m::nat) * n = (if m=#0 then #0 else n + ((m - #1) * n))";
|
|
314 |
by (exhaust_tac "m" 1);
|
|
315 |
by (ALLGOALS (asm_simp_tac numeral_ss));
|
|
316 |
qed "mult_eq_if";
|
|
317 |
|
|
318 |
(*various theorems that aren't in the default simpset*)
|
|
319 |
val add_is_one' = rename_numerals thy add_is_1;
|
|
320 |
val one_is_add' = rename_numerals thy one_is_add;
|
|
321 |
val zero_induct' = rename_numerals thy zero_induct;
|
|
322 |
val diff_self_eq_0' = rename_numerals thy diff_self_eq_0;
|
|
323 |
val mult_eq_self_implies_10' = rename_numerals thy mult_eq_self_implies_10;
|
|
324 |
val le_pred_eq' = rename_numerals thy le_pred_eq;
|
|
325 |
val less_pred_eq' = rename_numerals thy less_pred_eq;
|
|
326 |
|
|
327 |
(** Divides **)
|
|
328 |
|
|
329 |
Addsimps (map (rename_numerals thy)
|
|
330 |
[mod_1, mod_0, div_1, div_0, mod2_gr_0, mod2_add_self_eq_0,
|
|
331 |
mod2_add_self]);
|
|
332 |
|
|
333 |
AddIffs (map (rename_numerals thy)
|
|
334 |
[dvd_1_left, dvd_0_right]);
|
|
335 |
|
|
336 |
(*useful?*)
|
|
337 |
val mod_self' = rename_numerals thy mod_self;
|
|
338 |
val div_self' = rename_numerals thy div_self;
|
|
339 |
val div_less' = rename_numerals thy div_less;
|
|
340 |
val mod_mult_self_is_zero' = rename_numerals thy mod_mult_self_is_0;
|
|
341 |
|
|
342 |
(** Power **)
|
|
343 |
|
|
344 |
Goal "(p::nat) ^ #0 = #1";
|
|
345 |
by (simp_tac numeral_ss 1);
|
|
346 |
qed "power_zero";
|
|
347 |
Addsimps [power_zero];
|
|
348 |
|
|
349 |
val binomial_zero = rename_numerals thy binomial_0;
|
|
350 |
val binomial_Suc' = rename_numerals thy binomial_Suc;
|
|
351 |
val binomial_n_n' = rename_numerals thy binomial_n_n;
|
|
352 |
|
|
353 |
(*binomial_0_Suc doesn't work well on numerals*)
|
|
354 |
Addsimps (map (rename_numerals thy)
|
|
355 |
[binomial_n_0, binomial_zero, binomial_1]);
|
|
356 |
|