|
1 (* Title: ZF/arith.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 For arith.thy. Arithmetic operators and their definitions |
|
7 |
|
8 Proofs about elementary arithmetic: addition, multiplication, etc. |
|
9 |
|
10 Could prove def_rec_0, def_rec_succ... |
|
11 *) |
|
12 |
|
13 open Arith; |
|
14 |
|
15 (*"Difference" is subtraction of natural numbers. |
|
16 There are no negative numbers; we have |
|
17 m #- n = 0 iff m<=n and m #- n = succ(k) iff m>n. |
|
18 Also, rec(m, 0, %z w.z) is pred(m). |
|
19 *) |
|
20 |
|
21 (** rec -- better than nat_rec; the succ case has no type requirement! **) |
|
22 |
|
23 val rec_trans = rec_def RS def_transrec RS trans; |
|
24 |
|
25 goal Arith.thy "rec(0,a,b) = a"; |
|
26 by (rtac rec_trans 1); |
|
27 by (rtac nat_case_0 1); |
|
28 val rec_0 = result(); |
|
29 |
|
30 goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))"; |
|
31 val rec_ss = ZF_ss |
|
32 addcongs (mk_typed_congs Arith.thy [("b", "[i,i]=>i")]) |
|
33 addrews [nat_case_succ, nat_succI]; |
|
34 by (rtac rec_trans 1); |
|
35 by (SIMP_TAC rec_ss 1); |
|
36 val rec_succ = result(); |
|
37 |
|
38 val major::prems = goal Arith.thy |
|
39 "[| n: nat; \ |
|
40 \ a: C(0); \ |
|
41 \ !!m z. [| m: nat; z: C(m) |] ==> b(m,z): C(succ(m)) \ |
|
42 \ |] ==> rec(n,a,b) : C(n)"; |
|
43 by (rtac (major RS nat_induct) 1); |
|
44 by (ALLGOALS |
|
45 (ASM_SIMP_TAC (ZF_ss addrews (prems@[rec_0,rec_succ])))); |
|
46 val rec_type = result(); |
|
47 |
|
48 val prems = goalw Arith.thy [rec_def] |
|
49 "[| n=n'; a=a'; !!m z. b(m,z)=b'(m,z) \ |
|
50 \ |] ==> rec(n,a,b)=rec(n',a',b')"; |
|
51 by (SIMP_TAC (ZF_ss addcongs [transrec_cong,nat_case_cong] |
|
52 addrews (prems RL [sym])) 1); |
|
53 val rec_cong = result(); |
|
54 |
|
55 val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat]; |
|
56 |
|
57 val nat_ss = ZF_ss addcongs [nat_case_cong,rec_cong] |
|
58 addrews ([rec_0,rec_succ] @ nat_typechecks); |
|
59 |
|
60 |
|
61 (** Addition **) |
|
62 |
|
63 val add_type = prove_goalw Arith.thy [add_def] |
|
64 "[| m:nat; n:nat |] ==> m #+ n : nat" |
|
65 (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]); |
|
66 |
|
67 val add_0 = prove_goalw Arith.thy [add_def] |
|
68 "0 #+ n = n" |
|
69 (fn _ => [ (rtac rec_0 1) ]); |
|
70 |
|
71 val add_succ = prove_goalw Arith.thy [add_def] |
|
72 "succ(m) #+ n = succ(m #+ n)" |
|
73 (fn _=> [ (rtac rec_succ 1) ]); |
|
74 |
|
75 (** Multiplication **) |
|
76 |
|
77 val mult_type = prove_goalw Arith.thy [mult_def] |
|
78 "[| m:nat; n:nat |] ==> m #* n : nat" |
|
79 (fn prems=> |
|
80 [ (typechk_tac (prems@[add_type]@nat_typechecks@ZF_typechecks)) ]); |
|
81 |
|
82 val mult_0 = prove_goalw Arith.thy [mult_def] |
|
83 "0 #* n = 0" |
|
84 (fn _ => [ (rtac rec_0 1) ]); |
|
85 |
|
86 val mult_succ = prove_goalw Arith.thy [mult_def] |
|
87 "succ(m) #* n = n #+ (m #* n)" |
|
88 (fn _ => [ (rtac rec_succ 1) ]); |
|
89 |
|
90 (** Difference **) |
|
91 |
|
92 val diff_type = prove_goalw Arith.thy [diff_def] |
|
93 "[| m:nat; n:nat |] ==> m #- n : nat" |
|
94 (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]); |
|
95 |
|
96 val diff_0 = prove_goalw Arith.thy [diff_def] |
|
97 "m #- 0 = m" |
|
98 (fn _ => [ (rtac rec_0 1) ]); |
|
99 |
|
100 val diff_0_eq_0 = prove_goalw Arith.thy [diff_def] |
|
101 "n:nat ==> 0 #- n = 0" |
|
102 (fn [prem]=> |
|
103 [ (rtac (prem RS nat_induct) 1), |
|
104 (ALLGOALS (ASM_SIMP_TAC nat_ss)) ]); |
|
105 |
|
106 (*Must simplify BEFORE the induction!! (Else we get a critical pair) |
|
107 succ(m) #- succ(n) rewrites to pred(succ(m) #- n) *) |
|
108 val diff_succ_succ = prove_goalw Arith.thy [diff_def] |
|
109 "[| m:nat; n:nat |] ==> succ(m) #- succ(n) = m #- n" |
|
110 (fn prems=> |
|
111 [ (ASM_SIMP_TAC (nat_ss addrews prems) 1), |
|
112 (nat_ind_tac "n" prems 1), |
|
113 (ALLGOALS (ASM_SIMP_TAC (nat_ss addrews prems))) ]); |
|
114 |
|
115 val prems = goal Arith.thy |
|
116 "[| m:nat; n:nat |] ==> m #- n : succ(m)"; |
|
117 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
|
118 by (resolve_tac prems 1); |
|
119 by (resolve_tac prems 1); |
|
120 by (etac succE 3); |
|
121 by (ALLGOALS |
|
122 (ASM_SIMP_TAC |
|
123 (nat_ss addrews (prems@[diff_0,diff_0_eq_0,diff_succ_succ])))); |
|
124 val diff_leq = result(); |
|
125 |
|
126 (*** Simplification over add, mult, diff ***) |
|
127 |
|
128 val arith_typechecks = [add_type, mult_type, diff_type]; |
|
129 val arith_rews = [add_0, add_succ, |
|
130 mult_0, mult_succ, |
|
131 diff_0, diff_0_eq_0, diff_succ_succ]; |
|
132 |
|
133 val arith_congs = mk_congs Arith.thy ["op #+", "op #-", "op #*"]; |
|
134 |
|
135 val arith_ss = nat_ss addcongs arith_congs |
|
136 addrews (arith_rews@arith_typechecks); |
|
137 |
|
138 (*** Addition ***) |
|
139 |
|
140 (*Associative law for addition*) |
|
141 val add_assoc = prove_goal Arith.thy |
|
142 "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)" |
|
143 (fn prems=> |
|
144 [ (nat_ind_tac "m" prems 1), |
|
145 (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]); |
|
146 |
|
147 (*The following two lemmas are used for add_commute and sometimes |
|
148 elsewhere, since they are safe for rewriting.*) |
|
149 val add_0_right = prove_goal Arith.thy |
|
150 "m:nat ==> m #+ 0 = m" |
|
151 (fn prems=> |
|
152 [ (nat_ind_tac "m" prems 1), |
|
153 (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]); |
|
154 |
|
155 val add_succ_right = prove_goal Arith.thy |
|
156 "m:nat ==> m #+ succ(n) = succ(m #+ n)" |
|
157 (fn prems=> |
|
158 [ (nat_ind_tac "m" prems 1), |
|
159 (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]); |
|
160 |
|
161 (*Commutative law for addition*) |
|
162 val add_commute = prove_goal Arith.thy |
|
163 "[| m:nat; n:nat |] ==> m #+ n = n #+ m" |
|
164 (fn prems=> |
|
165 [ (nat_ind_tac "n" prems 1), |
|
166 (ALLGOALS |
|
167 (ASM_SIMP_TAC |
|
168 (arith_ss addrews (prems@[add_0_right, add_succ_right])))) ]); |
|
169 |
|
170 (*Cancellation law on the left*) |
|
171 val [knat,eqn] = goal Arith.thy |
|
172 "[| k:nat; k #+ m = k #+ n |] ==> m=n"; |
|
173 by (rtac (eqn RS rev_mp) 1); |
|
174 by (nat_ind_tac "k" [knat] 1); |
|
175 by (ALLGOALS (SIMP_TAC arith_ss)); |
|
176 by (fast_tac ZF_cs 1); |
|
177 val add_left_cancel = result(); |
|
178 |
|
179 (*** Multiplication ***) |
|
180 |
|
181 (*right annihilation in product*) |
|
182 val mult_0_right = prove_goal Arith.thy |
|
183 "m:nat ==> m #* 0 = 0" |
|
184 (fn prems=> |
|
185 [ (nat_ind_tac "m" prems 1), |
|
186 (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]); |
|
187 |
|
188 (*right successor law for multiplication*) |
|
189 val mult_succ_right = prove_goal Arith.thy |
|
190 "[| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)" |
|
191 (fn prems=> |
|
192 [ (nat_ind_tac "m" prems 1), |
|
193 (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))), |
|
194 (*The final goal requires the commutative law for addition*) |
|
195 (REPEAT (ares_tac (prems@[refl,add_commute]@ZF_congs@arith_congs) 1)) ]); |
|
196 |
|
197 (*Commutative law for multiplication*) |
|
198 val mult_commute = prove_goal Arith.thy |
|
199 "[| m:nat; n:nat |] ==> m #* n = n #* m" |
|
200 (fn prems=> |
|
201 [ (nat_ind_tac "m" prems 1), |
|
202 (ALLGOALS (ASM_SIMP_TAC |
|
203 (arith_ss addrews (prems@[mult_0_right, mult_succ_right])))) ]); |
|
204 |
|
205 (*addition distributes over multiplication*) |
|
206 val add_mult_distrib = prove_goal Arith.thy |
|
207 "[| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)" |
|
208 (fn prems=> |
|
209 [ (nat_ind_tac "m" prems 1), |
|
210 (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))) ]); |
|
211 |
|
212 (*Distributive law on the left; requires an extra typing premise*) |
|
213 val add_mult_distrib_left = prove_goal Arith.thy |
|
214 "[| m:nat; n:nat; k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)" |
|
215 (fn prems=> |
|
216 let val mult_commute' = read_instantiate [("m","k")] mult_commute |
|
217 val ss = arith_ss addrews ([mult_commute',add_mult_distrib]@prems) |
|
218 in [ (SIMP_TAC ss 1) ] |
|
219 end); |
|
220 |
|
221 (*Associative law for multiplication*) |
|
222 val mult_assoc = prove_goal Arith.thy |
|
223 "[| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k)" |
|
224 (fn prems=> |
|
225 [ (nat_ind_tac "m" prems 1), |
|
226 (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews (prems@[add_mult_distrib])))) ]); |
|
227 |
|
228 |
|
229 (*** Difference ***) |
|
230 |
|
231 val diff_self_eq_0 = prove_goal Arith.thy |
|
232 "m:nat ==> m #- m = 0" |
|
233 (fn prems=> |
|
234 [ (nat_ind_tac "m" prems 1), |
|
235 (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]); |
|
236 |
|
237 (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *) |
|
238 val notless::prems = goal Arith.thy |
|
239 "[| ~m:n; m:nat; n:nat |] ==> n #+ (m#-n) = m"; |
|
240 by (rtac (notless RS rev_mp) 1); |
|
241 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
|
242 by (resolve_tac prems 1); |
|
243 by (resolve_tac prems 1); |
|
244 by (ALLGOALS (ASM_SIMP_TAC |
|
245 (arith_ss addrews (prems@[succ_mem_succ_iff, Ord_0_mem_succ, |
|
246 naturals_are_ordinals])))); |
|
247 val add_diff_inverse = result(); |
|
248 |
|
249 |
|
250 (*Subtraction is the inverse of addition. *) |
|
251 val [mnat,nnat] = goal Arith.thy |
|
252 "[| m:nat; n:nat |] ==> (n#+m) #-n = m"; |
|
253 by (rtac (nnat RS nat_induct) 1); |
|
254 by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat]))); |
|
255 val diff_add_inverse = result(); |
|
256 |
|
257 val [mnat,nnat] = goal Arith.thy |
|
258 "[| m:nat; n:nat |] ==> n #- (n#+m) = 0"; |
|
259 by (rtac (nnat RS nat_induct) 1); |
|
260 by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat]))); |
|
261 val diff_add_0 = result(); |
|
262 |
|
263 |
|
264 (*** Remainder ***) |
|
265 |
|
266 (*In ordinary notation: if 0<n and n<=m then m-n < m *) |
|
267 val prems = goal Arith.thy |
|
268 "[| 0:n; ~ m:n; m:nat; n:nat |] ==> m #- n : m"; |
|
269 by (cut_facts_tac prems 1); |
|
270 by (etac rev_mp 1); |
|
271 by (etac rev_mp 1); |
|
272 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
|
273 by (resolve_tac prems 1); |
|
274 by (resolve_tac prems 1); |
|
275 by (ALLGOALS (ASM_SIMP_TAC |
|
276 (nat_ss addrews (prems@[diff_leq,diff_succ_succ])))); |
|
277 val div_termination = result(); |
|
278 |
|
279 val div_rls = |
|
280 [Ord_transrec_type, apply_type, div_termination, if_type] @ |
|
281 nat_typechecks; |
|
282 |
|
283 (*Type checking depends upon termination!*) |
|
284 val prems = goalw Arith.thy [mod_def] |
|
285 "[| 0:n; m:nat; n:nat |] ==> m mod n : nat"; |
|
286 by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1)); |
|
287 val mod_type = result(); |
|
288 |
|
289 val div_ss = ZF_ss addrews [naturals_are_ordinals,div_termination]; |
|
290 |
|
291 val prems = goal Arith.thy "[| 0:n; m:n; m:nat; n:nat |] ==> m mod n = m"; |
|
292 by (rtac (mod_def RS def_transrec RS trans) 1); |
|
293 by (SIMP_TAC (div_ss addrews prems) 1); |
|
294 val mod_less = result(); |
|
295 |
|
296 val prems = goal Arith.thy |
|
297 "[| 0:n; ~m:n; m:nat; n:nat |] ==> m mod n = (m#-n) mod n"; |
|
298 by (rtac (mod_def RS def_transrec RS trans) 1); |
|
299 by (SIMP_TAC (div_ss addrews prems) 1); |
|
300 val mod_geq = result(); |
|
301 |
|
302 (*** Quotient ***) |
|
303 |
|
304 (*Type checking depends upon termination!*) |
|
305 val prems = goalw Arith.thy [div_def] |
|
306 "[| 0:n; m:nat; n:nat |] ==> m div n : nat"; |
|
307 by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1)); |
|
308 val div_type = result(); |
|
309 |
|
310 val prems = goal Arith.thy |
|
311 "[| 0:n; m:n; m:nat; n:nat |] ==> m div n = 0"; |
|
312 by (rtac (div_def RS def_transrec RS trans) 1); |
|
313 by (SIMP_TAC (div_ss addrews prems) 1); |
|
314 val div_less = result(); |
|
315 |
|
316 val prems = goal Arith.thy |
|
317 "[| 0:n; ~m:n; m:nat; n:nat |] ==> m div n = succ((m#-n) div n)"; |
|
318 by (rtac (div_def RS def_transrec RS trans) 1); |
|
319 by (SIMP_TAC (div_ss addrews prems) 1); |
|
320 val div_geq = result(); |
|
321 |
|
322 (*Main Result.*) |
|
323 val prems = goal Arith.thy |
|
324 "[| 0:n; m:nat; n:nat |] ==> (m div n)#*n #+ m mod n = m"; |
|
325 by (res_inst_tac [("i","m")] complete_induct 1); |
|
326 by (resolve_tac prems 1); |
|
327 by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1); |
|
328 by (ALLGOALS |
|
329 (ASM_SIMP_TAC |
|
330 (arith_ss addrews ([mod_type,div_type] @ prems @ |
|
331 [mod_less,mod_geq, div_less, div_geq, |
|
332 add_assoc, add_diff_inverse, div_termination])))); |
|
333 val mod_div_equality = result(); |
|
334 |
|
335 |
|
336 (**** Additional theorems about "less than" ****) |
|
337 |
|
338 val [mnat,nnat] = goal Arith.thy |
|
339 "[| m:nat; n:nat |] ==> ~ (m #+ n) : n"; |
|
340 by (rtac (mnat RS nat_induct) 1); |
|
341 by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mem_not_refl]))); |
|
342 by (rtac notI 1); |
|
343 by (etac notE 1); |
|
344 by (etac (succI1 RS Ord_trans) 1); |
|
345 by (rtac (nnat RS naturals_are_ordinals) 1); |
|
346 val add_not_less_self = result(); |
|
347 |
|
348 val [mnat,nnat] = goal Arith.thy |
|
349 "[| m:nat; n:nat |] ==> m : succ(m #+ n)"; |
|
350 by (rtac (mnat RS nat_induct) 1); |
|
351 (*May not simplify even with ZF_ss because it would expand m:succ(...) *) |
|
352 by (rtac (add_0 RS ssubst) 1); |
|
353 by (rtac (add_succ RS ssubst) 2); |
|
354 by (REPEAT (ares_tac [nnat, Ord_0_mem_succ, succ_mem_succI, |
|
355 naturals_are_ordinals, nat_succI, add_type] 1)); |
|
356 val add_less_succ_self = result(); |