|
1 (* Title: HOL/Arith.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Proofs about elementary arithmetic: addition, multiplication, etc. |
|
7 Tests definitions and simplifier. |
|
8 *) |
|
9 |
|
10 open Arith; |
|
11 |
|
12 (*** Basic rewrite rules for the arithmetic operators ***) |
|
13 |
|
14 val [pred_0, pred_Suc] = nat_recs pred_def; |
|
15 val [add_0,add_Suc] = nat_recs add_def; |
|
16 val [mult_0,mult_Suc] = nat_recs mult_def; |
|
17 |
|
18 (** Difference **) |
|
19 |
|
20 val diff_0 = diff_def RS def_nat_rec_0; |
|
21 |
|
22 qed_goalw "diff_0_eq_0" Arith.thy [diff_def, pred_def] |
|
23 "0 - n = 0" |
|
24 (fn _ => [nat_ind_tac "n" 1, ALLGOALS(asm_simp_tac nat_ss)]); |
|
25 |
|
26 (*Must simplify BEFORE the induction!! (Else we get a critical pair) |
|
27 Suc(m) - Suc(n) rewrites to pred(Suc(m) - n) *) |
|
28 qed_goalw "diff_Suc_Suc" Arith.thy [diff_def, pred_def] |
|
29 "Suc(m) - Suc(n) = m - n" |
|
30 (fn _ => |
|
31 [simp_tac nat_ss 1, nat_ind_tac "n" 1, ALLGOALS(asm_simp_tac nat_ss)]); |
|
32 |
|
33 (*** Simplification over add, mult, diff ***) |
|
34 |
|
35 val arith_simps = |
|
36 [pred_0, pred_Suc, add_0, add_Suc, mult_0, mult_Suc, |
|
37 diff_0, diff_0_eq_0, diff_Suc_Suc]; |
|
38 |
|
39 val arith_ss = nat_ss addsimps arith_simps; |
|
40 |
|
41 (**** Inductive properties of the operators ****) |
|
42 |
|
43 (*** Addition ***) |
|
44 |
|
45 qed_goal "add_0_right" Arith.thy "m + 0 = m" |
|
46 (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); |
|
47 |
|
48 qed_goal "add_Suc_right" Arith.thy "m + Suc(n) = Suc(m+n)" |
|
49 (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); |
|
50 |
|
51 val arith_ss = arith_ss addsimps [add_0_right,add_Suc_right]; |
|
52 |
|
53 (*Associative law for addition*) |
|
54 qed_goal "add_assoc" Arith.thy "(m + n) + k = m + ((n + k)::nat)" |
|
55 (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); |
|
56 |
|
57 (*Commutative law for addition*) |
|
58 qed_goal "add_commute" Arith.thy "m + n = n + (m::nat)" |
|
59 (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); |
|
60 |
|
61 qed_goal "add_left_commute" Arith.thy "x+(y+z)=y+((x+z)::nat)" |
|
62 (fn _ => [rtac (add_commute RS trans) 1, rtac (add_assoc RS trans) 1, |
|
63 rtac (add_commute RS arg_cong) 1]); |
|
64 |
|
65 (*Addition is an AC-operator*) |
|
66 val add_ac = [add_assoc, add_commute, add_left_commute]; |
|
67 |
|
68 goal Arith.thy "!!k::nat. (k + m = k + n) = (m=n)"; |
|
69 by (nat_ind_tac "k" 1); |
|
70 by (simp_tac arith_ss 1); |
|
71 by (asm_simp_tac arith_ss 1); |
|
72 qed "add_left_cancel"; |
|
73 |
|
74 goal Arith.thy "!!k::nat. (m + k = n + k) = (m=n)"; |
|
75 by (nat_ind_tac "k" 1); |
|
76 by (simp_tac arith_ss 1); |
|
77 by (asm_simp_tac arith_ss 1); |
|
78 qed "add_right_cancel"; |
|
79 |
|
80 goal Arith.thy "!!k::nat. (k + m <= k + n) = (m<=n)"; |
|
81 by (nat_ind_tac "k" 1); |
|
82 by (simp_tac arith_ss 1); |
|
83 by (asm_simp_tac (arith_ss addsimps [Suc_le_mono]) 1); |
|
84 qed "add_left_cancel_le"; |
|
85 |
|
86 goal Arith.thy "!!k::nat. (k + m < k + n) = (m<n)"; |
|
87 by (nat_ind_tac "k" 1); |
|
88 by (simp_tac arith_ss 1); |
|
89 by (asm_simp_tac arith_ss 1); |
|
90 qed "add_left_cancel_less"; |
|
91 |
|
92 (*** Multiplication ***) |
|
93 |
|
94 (*right annihilation in product*) |
|
95 qed_goal "mult_0_right" Arith.thy "m * 0 = 0" |
|
96 (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); |
|
97 |
|
98 (*right Sucessor law for multiplication*) |
|
99 qed_goal "mult_Suc_right" Arith.thy "m * Suc(n) = m + (m * n)" |
|
100 (fn _ => [nat_ind_tac "m" 1, |
|
101 ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]); |
|
102 |
|
103 val arith_ss = arith_ss addsimps [mult_0_right,mult_Suc_right]; |
|
104 |
|
105 (*Commutative law for multiplication*) |
|
106 qed_goal "mult_commute" Arith.thy "m * n = n * (m::nat)" |
|
107 (fn _ => [nat_ind_tac "m" 1, ALLGOALS (asm_simp_tac arith_ss)]); |
|
108 |
|
109 (*addition distributes over multiplication*) |
|
110 qed_goal "add_mult_distrib" Arith.thy "(m + n)*k = (m*k) + ((n*k)::nat)" |
|
111 (fn _ => [nat_ind_tac "m" 1, |
|
112 ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]); |
|
113 |
|
114 qed_goal "add_mult_distrib2" Arith.thy "k*(m + n) = (k*m) + ((k*n)::nat)" |
|
115 (fn _ => [nat_ind_tac "m" 1, |
|
116 ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]); |
|
117 |
|
118 val arith_ss = arith_ss addsimps [add_mult_distrib,add_mult_distrib2]; |
|
119 |
|
120 (*Associative law for multiplication*) |
|
121 qed_goal "mult_assoc" Arith.thy "(m * n) * k = m * ((n * k)::nat)" |
|
122 (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); |
|
123 |
|
124 qed_goal "mult_left_commute" Arith.thy "x*(y*z) = y*((x*z)::nat)" |
|
125 (fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1, |
|
126 rtac mult_assoc 1, rtac (mult_commute RS arg_cong) 1]); |
|
127 |
|
128 val mult_ac = [mult_assoc,mult_commute,mult_left_commute]; |
|
129 |
|
130 (*** Difference ***) |
|
131 |
|
132 qed_goal "diff_self_eq_0" Arith.thy "m - m = 0" |
|
133 (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); |
|
134 |
|
135 (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *) |
|
136 val [prem] = goal Arith.thy "[| ~ m<n |] ==> n+(m-n) = (m::nat)"; |
|
137 by (rtac (prem RS rev_mp) 1); |
|
138 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
|
139 by (ALLGOALS(asm_simp_tac arith_ss)); |
|
140 qed "add_diff_inverse"; |
|
141 |
|
142 |
|
143 (*** Remainder ***) |
|
144 |
|
145 goal Arith.thy "m - n < Suc(m)"; |
|
146 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
|
147 by (etac less_SucE 3); |
|
148 by (ALLGOALS(asm_simp_tac arith_ss)); |
|
149 qed "diff_less_Suc"; |
|
150 |
|
151 goal Arith.thy "!!m::nat. m - n <= m"; |
|
152 by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1); |
|
153 by (ALLGOALS (asm_simp_tac arith_ss)); |
|
154 by (etac le_trans 1); |
|
155 by (simp_tac (HOL_ss addsimps [le_eq_less_or_eq, lessI]) 1); |
|
156 qed "diff_le_self"; |
|
157 |
|
158 goal Arith.thy "!!n::nat. (n+m) - n = m"; |
|
159 by (nat_ind_tac "n" 1); |
|
160 by (ALLGOALS (asm_simp_tac arith_ss)); |
|
161 qed "diff_add_inverse"; |
|
162 |
|
163 goal Arith.thy "!!n::nat. n - (n+m) = 0"; |
|
164 by (nat_ind_tac "n" 1); |
|
165 by (ALLGOALS (asm_simp_tac arith_ss)); |
|
166 qed "diff_add_0"; |
|
167 |
|
168 (*In ordinary notation: if 0<n and n<=m then m-n < m *) |
|
169 goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m"; |
|
170 by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1); |
|
171 by (fast_tac HOL_cs 1); |
|
172 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
|
173 by (ALLGOALS(asm_simp_tac(arith_ss addsimps [diff_less_Suc]))); |
|
174 qed "div_termination"; |
|
175 |
|
176 val wf_less_trans = wf_pred_nat RS wf_trancl RSN (2, def_wfrec RS trans); |
|
177 |
|
178 goalw Nat.thy [less_def] "<m,n> : pred_nat^+ = (m<n)"; |
|
179 by (rtac refl 1); |
|
180 qed "less_eq"; |
|
181 |
|
182 goal Arith.thy "!!m. m<n ==> m mod n = m"; |
|
183 by (rtac (mod_def RS wf_less_trans) 1); |
|
184 by(asm_simp_tac HOL_ss 1); |
|
185 qed "mod_less"; |
|
186 |
|
187 goal Arith.thy "!!m. [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n"; |
|
188 by (rtac (mod_def RS wf_less_trans) 1); |
|
189 by(asm_simp_tac (nat_ss addsimps [div_termination, cut_apply, less_eq]) 1); |
|
190 qed "mod_geq"; |
|
191 |
|
192 |
|
193 (*** Quotient ***) |
|
194 |
|
195 goal Arith.thy "!!m. m<n ==> m div n = 0"; |
|
196 by (rtac (div_def RS wf_less_trans) 1); |
|
197 by(asm_simp_tac nat_ss 1); |
|
198 qed "div_less"; |
|
199 |
|
200 goal Arith.thy "!!M. [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)"; |
|
201 by (rtac (div_def RS wf_less_trans) 1); |
|
202 by(asm_simp_tac (nat_ss addsimps [div_termination, cut_apply, less_eq]) 1); |
|
203 qed "div_geq"; |
|
204 |
|
205 (*Main Result about quotient and remainder.*) |
|
206 goal Arith.thy "!!m. 0<n ==> (m div n)*n + m mod n = m"; |
|
207 by (res_inst_tac [("n","m")] less_induct 1); |
|
208 by (rename_tac "k" 1); (*Variable name used in line below*) |
|
209 by (case_tac "k<n" 1); |
|
210 by (ALLGOALS (asm_simp_tac(arith_ss addsimps (add_ac @ |
|
211 [mod_less, mod_geq, div_less, div_geq, |
|
212 add_diff_inverse, div_termination])))); |
|
213 qed "mod_div_equality"; |
|
214 |
|
215 |
|
216 (*** More results about difference ***) |
|
217 |
|
218 val [prem] = goal Arith.thy "m < Suc(n) ==> m-n = 0"; |
|
219 by (rtac (prem RS rev_mp) 1); |
|
220 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
|
221 by (ALLGOALS (asm_simp_tac arith_ss)); |
|
222 qed "less_imp_diff_is_0"; |
|
223 |
|
224 val prems = goal Arith.thy "m-n = 0 --> n-m = 0 --> m=n"; |
|
225 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
|
226 by (REPEAT(simp_tac arith_ss 1 THEN TRY(atac 1))); |
|
227 qed "diffs0_imp_equal_lemma"; |
|
228 |
|
229 (* [| m-n = 0; n-m = 0 |] ==> m=n *) |
|
230 bind_thm ("diffs0_imp_equal", (diffs0_imp_equal_lemma RS mp RS mp)); |
|
231 |
|
232 val [prem] = goal Arith.thy "m<n ==> 0<n-m"; |
|
233 by (rtac (prem RS rev_mp) 1); |
|
234 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
|
235 by (ALLGOALS(asm_simp_tac arith_ss)); |
|
236 qed "less_imp_diff_positive"; |
|
237 |
|
238 val [prem] = goal Arith.thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)"; |
|
239 by (rtac (prem RS rev_mp) 1); |
|
240 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
|
241 by (ALLGOALS(asm_simp_tac arith_ss)); |
|
242 qed "Suc_diff_n"; |
|
243 |
|
244 goal Arith.thy "Suc(m)-n = if (m<n) 0 (Suc m-n)"; |
|
245 by(simp_tac (nat_ss addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n] |
|
246 setloop (split_tac [expand_if])) 1); |
|
247 qed "if_Suc_diff_n"; |
|
248 |
|
249 goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)"; |
|
250 by (res_inst_tac [("m","k"),("n","i")] diff_induct 1); |
|
251 by (ALLGOALS (strip_tac THEN' simp_tac arith_ss THEN' TRY o fast_tac HOL_cs)); |
|
252 qed "zero_induct_lemma"; |
|
253 |
|
254 val prems = goal Arith.thy "[| P(k); !!n. P(Suc(n)) ==> P(n) |] ==> P(0)"; |
|
255 by (rtac (diff_self_eq_0 RS subst) 1); |
|
256 by (rtac (zero_induct_lemma RS mp RS mp) 1); |
|
257 by (REPEAT (ares_tac ([impI,allI]@prems) 1)); |
|
258 qed "zero_induct"; |
|
259 |
|
260 (*13 July 1992: loaded in 105.7s*) |
|
261 |
|
262 (**** Additional theorems about "less than" ****) |
|
263 |
|
264 goal Arith.thy "!!m. m<n --> (? k. n=Suc(m+k))"; |
|
265 by (nat_ind_tac "n" 1); |
|
266 by (ALLGOALS(simp_tac arith_ss)); |
|
267 by (REPEAT_FIRST (ares_tac [conjI, impI])); |
|
268 by (res_inst_tac [("x","0")] exI 2); |
|
269 by (simp_tac arith_ss 2); |
|
270 by (safe_tac HOL_cs); |
|
271 by (res_inst_tac [("x","Suc(k)")] exI 1); |
|
272 by (simp_tac arith_ss 1); |
|
273 val less_eq_Suc_add_lemma = result(); |
|
274 |
|
275 (*"m<n ==> ? k. n = Suc(m+k)"*) |
|
276 bind_thm ("less_eq_Suc_add", less_eq_Suc_add_lemma RS mp); |
|
277 |
|
278 |
|
279 goal Arith.thy "n <= ((m + n)::nat)"; |
|
280 by (nat_ind_tac "m" 1); |
|
281 by (ALLGOALS(simp_tac arith_ss)); |
|
282 by (etac le_trans 1); |
|
283 by (rtac (lessI RS less_imp_le) 1); |
|
284 qed "le_add2"; |
|
285 |
|
286 goal Arith.thy "n <= ((n + m)::nat)"; |
|
287 by (simp_tac (arith_ss addsimps add_ac) 1); |
|
288 by (rtac le_add2 1); |
|
289 qed "le_add1"; |
|
290 |
|
291 bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans))); |
|
292 bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans))); |
|
293 |
|
294 (*"i <= j ==> i <= j+m"*) |
|
295 bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans)); |
|
296 |
|
297 (*"i <= j ==> i <= m+j"*) |
|
298 bind_thm ("trans_le_add2", le_add2 RSN (2,le_trans)); |
|
299 |
|
300 (*"i < j ==> i < j+m"*) |
|
301 bind_thm ("trans_less_add1", le_add1 RSN (2,less_le_trans)); |
|
302 |
|
303 (*"i < j ==> i < m+j"*) |
|
304 bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans)); |
|
305 |
|
306 goal Arith.thy "!!k::nat. m <= n ==> m <= n+k"; |
|
307 by (eresolve_tac [le_trans] 1); |
|
308 by (resolve_tac [le_add1] 1); |
|
309 qed "le_imp_add_le"; |
|
310 |
|
311 goal Arith.thy "!!k::nat. m < n ==> m < n+k"; |
|
312 by (eresolve_tac [less_le_trans] 1); |
|
313 by (resolve_tac [le_add1] 1); |
|
314 qed "less_imp_add_less"; |
|
315 |
|
316 goal Arith.thy "m+k<=n --> m<=(n::nat)"; |
|
317 by (nat_ind_tac "k" 1); |
|
318 by (ALLGOALS (asm_simp_tac arith_ss)); |
|
319 by (fast_tac (HOL_cs addDs [Suc_leD]) 1); |
|
320 val add_leD1_lemma = result(); |
|
321 bind_thm ("add_leD1", add_leD1_lemma RS mp);; |
|
322 |
|
323 goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n"; |
|
324 by (safe_tac (HOL_cs addSDs [less_eq_Suc_add])); |
|
325 by (asm_full_simp_tac |
|
326 (HOL_ss addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1); |
|
327 by (eresolve_tac [subst] 1); |
|
328 by (simp_tac (arith_ss addsimps [less_add_Suc1]) 1); |
|
329 qed "less_add_eq_less"; |
|
330 |
|
331 |
|
332 (** Monotonicity of addition (from ZF/Arith) **) |
|
333 |
|
334 (** Monotonicity results **) |
|
335 |
|
336 (*strict, in 1st argument*) |
|
337 goal Arith.thy "!!i j k::nat. i < j ==> i + k < j + k"; |
|
338 by (nat_ind_tac "k" 1); |
|
339 by (ALLGOALS (asm_simp_tac arith_ss)); |
|
340 qed "add_less_mono1"; |
|
341 |
|
342 (*strict, in both arguments*) |
|
343 goal Arith.thy "!!i j k::nat. [|i < j; k < l|] ==> i + k < j + l"; |
|
344 by (rtac (add_less_mono1 RS less_trans) 1); |
|
345 by (REPEAT (etac asm_rl 1)); |
|
346 by (nat_ind_tac "j" 1); |
|
347 by (ALLGOALS(asm_simp_tac arith_ss)); |
|
348 qed "add_less_mono"; |
|
349 |
|
350 (*A [clumsy] way of lifting < monotonicity to <= monotonicity *) |
|
351 val [lt_mono,le] = goal Arith.thy |
|
352 "[| !!i j::nat. i<j ==> f(i) < f(j); \ |
|
353 \ i <= j \ |
|
354 \ |] ==> f(i) <= (f(j)::nat)"; |
|
355 by (cut_facts_tac [le] 1); |
|
356 by (asm_full_simp_tac (HOL_ss addsimps [le_eq_less_or_eq]) 1); |
|
357 by (fast_tac (HOL_cs addSIs [lt_mono]) 1); |
|
358 qed "less_mono_imp_le_mono"; |
|
359 |
|
360 (*non-strict, in 1st argument*) |
|
361 goal Arith.thy "!!i j k::nat. i<=j ==> i + k <= j + k"; |
|
362 by (res_inst_tac [("f", "%j.j+k")] less_mono_imp_le_mono 1); |
|
363 by (eresolve_tac [add_less_mono1] 1); |
|
364 by (assume_tac 1); |
|
365 qed "add_le_mono1"; |
|
366 |
|
367 (*non-strict, in both arguments*) |
|
368 goal Arith.thy "!!k l::nat. [|i<=j; k<=l |] ==> i + k <= j + l"; |
|
369 by (etac (add_le_mono1 RS le_trans) 1); |
|
370 by (simp_tac (HOL_ss addsimps [add_commute]) 1); |
|
371 (*j moves to the end because it is free while k, l are bound*) |
|
372 by (eresolve_tac [add_le_mono1] 1); |
|
373 qed "add_le_mono"; |