250 val diff_add_0 = result(); |
248 val diff_add_0 = result(); |
251 |
249 |
252 |
250 |
253 (*** Remainder ***) |
251 (*** Remainder ***) |
254 |
252 |
255 (*In ordinary notation: if 0<n and n<=m then m-n < m *) |
253 goal Arith.thy "!!m n. [| 0<n; n le m; m:nat |] ==> m #- n < m"; |
256 goal Arith.thy "!!m n. [| 0:n; ~ m:n; m:nat; n:nat |] ==> m #- n : m"; |
254 by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1); |
257 by (etac rev_mp 1); |
255 by (etac rev_mp 1); |
258 by (etac rev_mp 1); |
256 by (etac rev_mp 1); |
259 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
257 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
260 by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_less_succ,diff_succ_succ]))); |
258 by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_le_self,diff_succ_succ]))); |
261 val div_termination = result(); |
259 val div_termination = result(); |
262 |
260 |
263 val div_rls = |
261 val div_rls = (*for mod and div*) |
264 [Ord_transrec_type, apply_type, div_termination, if_type] @ |
262 nat_typechecks @ |
265 nat_typechecks; |
263 [Ord_transrec_type, apply_type, div_termination RS ltD, if_type, |
|
264 naturals_are_ordinals, not_lt_iff_le RS iffD1]; |
|
265 |
|
266 val div_ss = ZF_ss addsimps [naturals_are_ordinals, div_termination RS ltD, |
|
267 not_lt_iff_le RS iffD2]; |
266 |
268 |
267 (*Type checking depends upon termination!*) |
269 (*Type checking depends upon termination!*) |
268 val prems = goalw Arith.thy [mod_def] |
270 goalw Arith.thy [mod_def] "!!m n. [| 0<n; m:nat; n:nat |] ==> m mod n : nat"; |
269 "[| 0:n; m:nat; n:nat |] ==> m mod n : nat"; |
271 by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1)); |
270 by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1)); |
|
271 val mod_type = result(); |
272 val mod_type = result(); |
272 |
273 |
273 val div_ss = ZF_ss addsimps [naturals_are_ordinals,div_termination]; |
274 goal Arith.thy "!!m n. [| 0<n; m<n |] ==> m mod n = m"; |
274 |
|
275 val prems = goal Arith.thy "[| 0:n; m:n; m:nat; n:nat |] ==> m mod n = m"; |
|
276 by (rtac (mod_def RS def_transrec RS trans) 1); |
275 by (rtac (mod_def RS def_transrec RS trans) 1); |
277 by (simp_tac (div_ss addsimps prems) 1); |
276 by (asm_simp_tac div_ss 1); |
278 val mod_less = result(); |
277 val mod_less = result(); |
279 |
278 |
280 val prems = goal Arith.thy |
279 goal Arith.thy "!!m n. [| 0<n; n le m; m:nat |] ==> m mod n = (m#-n) mod n"; |
281 "[| 0:n; ~m:n; m:nat; n:nat |] ==> m mod n = (m#-n) mod n"; |
280 by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1); |
282 by (rtac (mod_def RS def_transrec RS trans) 1); |
281 by (rtac (mod_def RS def_transrec RS trans) 1); |
283 by (simp_tac (div_ss addsimps prems) 1); |
282 by (asm_simp_tac div_ss 1); |
284 val mod_geq = result(); |
283 val mod_geq = result(); |
285 |
284 |
286 (*** Quotient ***) |
285 (*** Quotient ***) |
287 |
286 |
288 (*Type checking depends upon termination!*) |
287 (*Type checking depends upon termination!*) |
289 val prems = goalw Arith.thy [div_def] |
288 goalw Arith.thy [div_def] |
290 "[| 0:n; m:nat; n:nat |] ==> m div n : nat"; |
289 "!!m n. [| 0<n; m:nat; n:nat |] ==> m div n : nat"; |
291 by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1)); |
290 by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1)); |
292 val div_type = result(); |
291 val div_type = result(); |
293 |
292 |
294 val prems = goal Arith.thy |
293 goal Arith.thy "!!m n. [| 0<n; m<n |] ==> m div n = 0"; |
295 "[| 0:n; m:n; m:nat; n:nat |] ==> m div n = 0"; |
|
296 by (rtac (div_def RS def_transrec RS trans) 1); |
294 by (rtac (div_def RS def_transrec RS trans) 1); |
297 by (simp_tac (div_ss addsimps prems) 1); |
295 by (asm_simp_tac div_ss 1); |
298 val div_less = result(); |
296 val div_less = result(); |
299 |
297 |
300 val prems = goal Arith.thy |
298 goal Arith.thy |
301 "[| 0:n; ~m:n; m:nat; n:nat |] ==> m div n = succ((m#-n) div n)"; |
299 "!!m n. [| 0<n; n le m; m:nat |] ==> m div n = succ((m#-n) div n)"; |
|
300 by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1); |
302 by (rtac (div_def RS def_transrec RS trans) 1); |
301 by (rtac (div_def RS def_transrec RS trans) 1); |
303 by (simp_tac (div_ss addsimps prems) 1); |
302 by (asm_simp_tac div_ss 1); |
304 val div_geq = result(); |
303 val div_geq = result(); |
305 |
304 |
306 (*Main Result.*) |
305 (*Main Result.*) |
307 val prems = goal Arith.thy |
306 goal Arith.thy |
308 "[| 0:n; m:nat; n:nat |] ==> (m div n)#*n #+ m mod n = m"; |
307 "!!m n. [| 0<n; m:nat; n:nat |] ==> (m div n)#*n #+ m mod n = m"; |
309 by (res_inst_tac [("i","m")] complete_induct 1); |
308 by (etac complete_induct 1); |
310 by (resolve_tac prems 1); |
309 by (res_inst_tac [("Q","x<n")] (excluded_middle RS disjE) 1); |
311 by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1); |
310 (*case x<n*) |
312 by (ALLGOALS |
311 by (asm_simp_tac (arith_ss addsimps [mod_less, div_less]) 2); |
313 (asm_simp_tac |
312 (*case n le x*) |
314 (arith_ss addsimps ([mod_type,div_type] @ prems @ |
313 by (asm_full_simp_tac |
315 [mod_less,mod_geq, div_less, div_geq, |
314 (arith_ss addsimps [not_lt_iff_le, naturals_are_ordinals, |
316 add_assoc, add_diff_inverse, div_termination])))); |
315 mod_geq, div_geq, add_assoc, |
|
316 div_termination RS ltD, add_diff_inverse]) 1); |
317 val mod_div_equality = result(); |
317 val mod_div_equality = result(); |
318 |
318 |
319 |
319 |
320 (**** Additional theorems about "less than" ****) |
320 (**** Additional theorems about "le" ****) |
321 |
321 |
322 val [mnat,nnat] = goal Arith.thy |
322 goal Arith.thy "!!m n. [| m:nat; n:nat |] ==> m le m #+ n"; |
323 "[| m:nat; n:nat |] ==> ~ (m #+ n) : n"; |
323 by (etac nat_induct 1); |
324 by (rtac (mnat RS nat_induct) 1); |
324 by (ALLGOALS (asm_simp_tac arith_ss)); |
325 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl]))); |
325 val add_le_self = result(); |
326 by (rtac notI 1); |
326 |
327 by (etac notE 1); |
327 goal Arith.thy "!!m n. [| m:nat; n:nat |] ==> m le n #+ m"; |
328 by (etac (succI1 RS Ord_trans) 1); |
|
329 by (rtac (nnat RS naturals_are_ordinals) 1); |
|
330 val add_not_less_self = result(); |
|
331 |
|
332 val [mnat,nnat] = goal Arith.thy |
|
333 "[| m:nat; n:nat |] ==> m : succ(m #+ n)"; |
|
334 by (rtac (mnat RS nat_induct) 1); |
|
335 (*May not simplify even with ZF_ss because it would expand m:succ(...) *) |
|
336 by (rtac (add_0 RS ssubst) 1); |
|
337 by (rtac (add_succ RS ssubst) 2); |
|
338 by (REPEAT (ares_tac [nnat, nat_0_in_succ, succ_mem_succI, |
|
339 naturals_are_ordinals, nat_succI, add_type] 1)); |
|
340 val add_less_succ_self = result(); |
|
341 |
|
342 goal Arith.thy "!!m n. [| m:nat; n:nat |] ==> m <= m #+ n"; |
|
343 by (rtac (add_less_succ_self RS member_succD) 1); |
|
344 by (REPEAT (ares_tac [naturals_are_ordinals, add_type] 1)); |
|
345 val add_leq_self = result(); |
|
346 |
|
347 goal Arith.thy "!!m n. [| m:nat; n:nat |] ==> m <= n #+ m"; |
|
348 by (rtac (add_commute RS ssubst) 1); |
328 by (rtac (add_commute RS ssubst) 1); |
349 by (REPEAT (ares_tac [add_leq_self] 1)); |
329 by (REPEAT (ares_tac [add_le_self] 1)); |
350 val add_leq_self2 = result(); |
330 val add_le_self2 = result(); |
351 |
331 |
352 (** Monotonicity of addition **) |
332 (** Monotonicity of addition **) |
353 |
333 |
354 (*strict, in 1st argument*) |
334 (*strict, in 1st argument*) |
355 goal Arith.thy "!!i j k. [| i:j; j:nat |] ==> i#+k : j#+k"; |
335 goal Arith.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> i#+k < j#+k"; |
356 by (etac succ_less_induct 1); |
336 by (forward_tac [lt_nat_in_nat] 1); |
357 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [succ_iff]))); |
337 ba 1; |
358 val add_less_mono1 = result(); |
338 by (etac succ_lt_induct 1); |
|
339 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [leI]))); |
|
340 val add_lt_mono1 = result(); |
359 |
341 |
360 (*strict, in both arguments*) |
342 (*strict, in both arguments*) |
361 goal Arith.thy "!!i j k l. [| i:j; k:l; j:nat; l:nat |] ==> i#+k : j#+l"; |
343 goal Arith.thy "!!i j k l. [| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l"; |
362 by (rtac (add_less_mono1 RS Ord_trans) 1); |
344 by (rtac (add_lt_mono1 RS lt_trans) 1); |
363 by (REPEAT_FIRST (ares_tac [add_type, naturals_are_ordinals])); |
345 by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1)); |
364 by (EVERY [rtac (add_commute RS ssubst) 1, |
346 by (EVERY [rtac (add_commute RS ssubst) 1, |
365 rtac (add_commute RS ssubst) 3, |
347 rtac (add_commute RS ssubst) 3, |
366 rtac add_less_mono1 5]); |
348 rtac add_lt_mono1 5]); |
367 by (REPEAT (ares_tac [Ord_nat RSN (3,Ord_trans)] 1)); |
349 by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1)); |
368 val add_less_mono = result(); |
350 val add_lt_mono = result(); |
369 |
351 |
370 (*A [clumsy] way of lifting < monotonictity to <= monotonicity *) |
352 (*A [clumsy] way of lifting < monotonicity to le monotonicity *) |
371 val less_mono::ford::prems = goal Ord.thy |
353 val lt_mono::ford::prems = goal Ord.thy |
372 "[| !!i j. [| i:j; j:k |] ==> f(i) : f(j); \ |
354 "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j); \ |
373 \ !!i. i:k ==> f(i):k; \ |
355 \ !!i. i:k ==> Ord(f(i)); \ |
374 \ i<=j; i:k; j:k; Ord(k) \ |
356 \ i le j; j:k \ |
375 \ |] ==> f(i) <= f(j)"; |
357 \ |] ==> f(i) le f(j)"; |
376 by (cut_facts_tac prems 1); |
358 by (cut_facts_tac prems 1); |
377 by (rtac member_succD 1); |
359 by (fast_tac (lt_cs addSIs [lt_mono,ford] addSEs [leE]) 1); |
378 by (dtac member_succI 1); |
360 val Ord_lt_mono_imp_le_mono = result(); |
379 by (fast_tac (ZF_cs addSIs [less_mono]) 3); |
361 |
380 by (REPEAT (ares_tac [ford,Ord_in_Ord] 1)); |
362 (*le monotonicity, 1st argument*) |
381 val Ord_less_mono_imp_mono = result(); |
|
382 |
|
383 (*<=, in 1st argument*) |
|
384 goal Arith.thy |
363 goal Arith.thy |
385 "!!i j k. [| i<=j; i:nat; j:nat; k:nat |] ==> i#+k <= j#+k"; |
364 "!!i j k. [| i le j; j:nat; k:nat |] ==> i#+k le j#+k"; |
386 by (res_inst_tac [("f", "%j.j#+k")] Ord_less_mono_imp_mono 1); |
365 by (res_inst_tac [("f", "%j.j#+k")] Ord_lt_mono_imp_le_mono 1); |
387 by (REPEAT (ares_tac [add_less_mono1, add_type, Ord_nat] 1)); |
366 by (REPEAT (ares_tac [add_lt_mono1, add_type RS naturals_are_ordinals] 1)); |
388 val add_mono1 = result(); |
367 val add_le_mono1 = result(); |
389 |
368 |
390 (*<=, in both arguments*) |
369 (* le monotonicity, BOTH arguments*) |
391 goal Arith.thy |
370 goal Arith.thy |
392 "!!i j k. [| i<=j; k<=l; i:nat; j:nat; k:nat; l:nat |] ==> i#+k <= j#+l"; |
371 "!!i j k. [| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l"; |
393 by (rtac (add_mono1 RS subset_trans) 1); |
372 by (rtac (add_le_mono1 RS le_trans) 1); |
394 by (REPEAT (assume_tac 1)); |
373 by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1)); |
395 by (EVERY [rtac (add_commute RS ssubst) 1, |
374 by (EVERY [rtac (add_commute RS ssubst) 1, |
396 rtac (add_commute RS ssubst) 3, |
375 rtac (add_commute RS ssubst) 3, |
397 rtac add_mono1 5]); |
376 rtac add_le_mono1 5]); |
398 by (REPEAT (assume_tac 1)); |
377 by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1)); |
399 val add_mono = result(); |
378 val add_le_mono = result(); |