230 |
230 |
231 (***) (***) (***) (***) (***) (***) (***) (***) (***) |
231 (***) (***) (***) (***) (***) (***) (***) (***) (***) |
232 |
232 |
233 (*** pnat_less ***) |
233 (*** pnat_less ***) |
234 |
234 |
235 Goalw [pnat_less_def] |
|
236 "[| x < (y::pnat); y < z |] ==> x < z"; |
|
237 by ((etac less_trans 1) THEN assume_tac 1); |
|
238 qed "pnat_less_trans"; |
|
239 |
|
240 Goalw [pnat_less_def] "x < (y::pnat) ==> ~ y < x"; |
|
241 by (etac less_not_sym 1); |
|
242 qed "pnat_less_not_sym"; |
|
243 |
|
244 (* [| x < y; ~P ==> y < x |] ==> P *) |
|
245 bind_thm ("pnat_less_asym", pnat_less_not_sym RS contrapos_np); |
|
246 |
|
247 Goalw [pnat_less_def] "~ y < (y::pnat)"; |
235 Goalw [pnat_less_def] "~ y < (y::pnat)"; |
248 by Auto_tac; |
236 by Auto_tac; |
249 qed "pnat_less_not_refl"; |
237 qed "pnat_less_not_refl"; |
250 |
238 |
251 bind_thm ("pnat_less_irrefl",pnat_less_not_refl RS notE); |
239 bind_thm ("pnat_less_irrefl",pnat_less_not_refl RS notE); |
294 qed "lemma_less_ex_sum_Rep_pnat"; |
282 qed "lemma_less_ex_sum_Rep_pnat"; |
295 |
283 |
296 |
284 |
297 (*** pnat_le ***) |
285 (*** pnat_le ***) |
298 |
286 |
299 Goalw [pnat_le_def] "~ (x::pnat) < y ==> y <= x"; |
|
300 by (assume_tac 1); |
|
301 qed "pnat_leI"; |
|
302 |
|
303 Goalw [pnat_le_def] "(x::pnat) <= y ==> ~ y < x"; |
|
304 by (assume_tac 1); |
|
305 qed "pnat_leD"; |
|
306 |
|
307 bind_thm ("pnat_leE", make_elim pnat_leD); |
|
308 |
|
309 Goal "(~ (x::pnat) < y) = (y <= x)"; |
|
310 by (blast_tac (claset() addIs [pnat_leI] addEs [pnat_leE]) 1); |
|
311 qed "pnat_not_less_iff_le"; |
|
312 |
|
313 Goalw [pnat_le_def] "~(x::pnat) <= y ==> y < x"; |
|
314 by (Blast_tac 1); |
|
315 qed "pnat_not_leE"; |
|
316 |
|
317 Goalw [pnat_le_def] "(x::pnat) < y ==> x <= y"; |
|
318 by (blast_tac (claset() addEs [pnat_less_asym]) 1); |
|
319 qed "pnat_less_imp_le"; |
|
320 |
|
321 (** Equivalence of m<=n and m<n | m=n **) |
|
322 |
|
323 Goalw [pnat_le_def] "m <= n ==> m < n | m=(n::pnat)"; |
|
324 by (cut_facts_tac [pnat_less_linear] 1); |
|
325 by (blast_tac (claset() addEs [pnat_less_irrefl,pnat_less_asym]) 1); |
|
326 qed "pnat_le_imp_less_or_eq"; |
|
327 |
|
328 Goalw [pnat_le_def] "m<n | m=n ==> m <=(n::pnat)"; |
|
329 by (cut_facts_tac [pnat_less_linear] 1); |
|
330 by (blast_tac (claset() addSEs [pnat_less_irrefl] addEs [pnat_less_asym]) 1); |
|
331 qed "pnat_less_or_eq_imp_le"; |
|
332 |
|
333 Goal "(m <= (n::pnat)) = (m < n | m=n)"; |
|
334 by (REPEAT(ares_tac [iffI,pnat_less_or_eq_imp_le,pnat_le_imp_less_or_eq] 1)); |
|
335 qed "pnat_le_eq_less_or_eq"; |
|
336 |
|
337 Goal "n <= (n::pnat)"; |
|
338 by (simp_tac (simpset() addsimps [pnat_le_eq_less_or_eq]) 1); |
|
339 qed "pnat_le_refl"; |
|
340 |
|
341 Goal "[| i < j; j <= k |] ==> i < (k::pnat)"; |
|
342 by (dtac pnat_le_imp_less_or_eq 1); |
|
343 by (blast_tac (claset() addIs [pnat_less_trans]) 1); |
|
344 qed "pnat_less_le_trans"; |
|
345 |
|
346 Goal "[| i <= j; j <= k |] ==> i <= (k::pnat)"; |
|
347 by (EVERY1[dtac pnat_le_imp_less_or_eq, |
|
348 dtac pnat_le_imp_less_or_eq, |
|
349 rtac pnat_less_or_eq_imp_le, |
|
350 blast_tac (claset() addIs [pnat_less_trans])]); |
|
351 qed "pnat_le_trans"; |
|
352 |
|
353 Goal "[| m <= n; n <= m |] ==> m = (n::pnat)"; |
|
354 by (EVERY1[dtac pnat_le_imp_less_or_eq, |
|
355 dtac pnat_le_imp_less_or_eq, |
|
356 blast_tac (claset() addIs [pnat_less_asym])]); |
|
357 qed "pnat_le_anti_sym"; |
|
358 |
|
359 Goal "(m::pnat) < n = (m <= n & m ~= n)"; |
|
360 by (rtac iffI 1); |
|
361 by (rtac conjI 1); |
|
362 by (etac pnat_less_imp_le 1); |
|
363 by (etac pnat_less_not_refl2 1); |
|
364 by (blast_tac (claset() addSDs [pnat_le_imp_less_or_eq]) 1); |
|
365 qed "pnat_less_le"; |
|
366 |
|
367 |
|
368 (***) (***) (***) (***) (***) (***) (***) (***) |
|
369 |
|
370 (*** alternative definition for pnat_le ***) |
287 (*** alternative definition for pnat_le ***) |
371 Goalw [pnat_le_def,pnat_less_def] |
288 Goalw [pnat_le_def,pnat_less_def] |
372 "((m::pnat) <= n) = (Rep_pnat m <= Rep_pnat n)"; |
289 "((m::pnat) <= n) = (Rep_pnat m <= Rep_pnat n)"; |
373 by (auto_tac (claset() addSIs [leI] addSEs [leD],simpset())); |
290 by (auto_tac (claset() addSIs [leI] addSEs [leD],simpset())); |
374 qed "pnat_le_iff_Rep_pnat_le"; |
291 qed "pnat_le_iff_Rep_pnat_le"; |
401 |
318 |
402 AddIffs [pnat_not_add_less1, pnat_not_add_less2]; |
319 AddIffs [pnat_not_add_less1, pnat_not_add_less2]; |
403 |
320 |
404 Goal "m + k <= n --> m <= (n::pnat)"; |
321 Goal "m + k <= n --> m <= (n::pnat)"; |
405 by (simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le, |
322 by (simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le, |
406 sum_Rep_pnat_sum RS sym]) 1); |
323 sum_Rep_pnat_sum RS sym]) 1); |
407 qed_spec_mp "pnat_add_leD1"; |
324 qed_spec_mp "pnat_add_leD1"; |
408 |
325 |
409 Goal "!!n::pnat. m + k <= n ==> k <= n"; |
326 Goal "!!n::pnat. m + k <= n ==> k <= n"; |
410 by (full_simp_tac (simpset() addsimps [pnat_add_commute]) 1); |
327 by (full_simp_tac (simpset() addsimps [pnat_add_commute]) 1); |
411 by (etac pnat_add_leD1 1); |
328 by (etac pnat_add_leD1 1); |
446 by (Blast_tac 1); |
363 by (Blast_tac 1); |
447 qed "pnat_eq_lessI"; |
364 qed "pnat_eq_lessI"; |
448 |
365 |
449 (*** Monotonicity of Addition ***) |
366 (*** Monotonicity of Addition ***) |
450 |
367 |
451 (*strict, in 1st argument*) |
|
452 Goalw [pnat_less_def] "!!i j k::pnat. i < j ==> i + k < j + k"; |
|
453 by (auto_tac (claset() addIs [add_less_mono1], |
|
454 simpset() addsimps [sum_Rep_pnat_sum RS sym])); |
|
455 qed "pnat_add_less_mono1"; |
|
456 |
|
457 Goalw [pnat_less_def] "!!i j k::pnat. [|i < j; k < l|] ==> i + k < j + l"; |
|
458 by (auto_tac (claset() addIs [add_less_mono], |
|
459 simpset() addsimps [sum_Rep_pnat_sum RS sym])); |
|
460 qed "pnat_add_less_mono"; |
|
461 |
|
462 Goalw [pnat_less_def] |
|
463 "!!f. [| !!i j::pnat. i<j ==> f(i) < f(j); \ |
|
464 \ i <= j \ |
|
465 \ |] ==> f(i) <= (f(j)::pnat)"; |
|
466 by (auto_tac (claset() addSDs [inj_Rep_pnat RS injD], |
|
467 simpset() addsimps [pnat_le_iff_Rep_pnat_le, |
|
468 order_le_less])); |
|
469 qed "pnat_less_mono_imp_le_mono"; |
|
470 |
|
471 Goal "!!i j k::pnat. i<=j ==> i + k <= j + k"; |
|
472 by (res_inst_tac [("f", "%j. j+k")] pnat_less_mono_imp_le_mono 1); |
|
473 by (etac pnat_add_less_mono1 1); |
|
474 by (assume_tac 1); |
|
475 qed "pnat_add_le_mono1"; |
|
476 |
|
477 Goal "!!k l::pnat. [|i<=j; k<=l |] ==> i + k <= j + l"; |
|
478 by (etac (pnat_add_le_mono1 RS pnat_le_trans) 1); |
|
479 by (simp_tac (simpset() addsimps [pnat_add_commute]) 1); |
|
480 (*j moves to the end because it is free while k, l are bound*) |
|
481 by (etac pnat_add_le_mono1 1); |
|
482 qed "pnad_add_le_mono"; |
|
483 |
|
484 Goal "1 * Rep_pnat n = Rep_pnat n"; |
368 Goal "1 * Rep_pnat n = Rep_pnat n"; |
485 by (Asm_simp_tac 1); |
369 by (Asm_simp_tac 1); |
486 qed "Rep_pnat_mult_1"; |
370 qed "Rep_pnat_mult_1"; |
487 |
371 |
488 Goal "Rep_pnat n * 1 = Rep_pnat n"; |
372 Goal "Rep_pnat n * 1 = Rep_pnat n"; |
489 by (Asm_simp_tac 1); |
373 by (Asm_simp_tac 1); |
490 qed "Rep_pnat_mult_1_right"; |
374 qed "Rep_pnat_mult_1_right"; |
491 |
375 |
492 Goal |
376 Goal "(Rep_pnat x * Rep_pnat y): pnat"; |
493 "(Rep_pnat x * Rep_pnat y): pnat"; |
|
494 by (cut_facts_tac [[Rep_pnat_gt_zero, |
377 by (cut_facts_tac [[Rep_pnat_gt_zero, |
495 Rep_pnat_gt_zero] MRS mult_less_mono1,Collect_pnat_gt_0] 1); |
378 Rep_pnat_gt_zero] MRS mult_less_mono1,Collect_pnat_gt_0] 1); |
496 by (etac ssubst 1); |
379 by (etac ssubst 1); |
497 by Auto_tac; |
380 by Auto_tac; |
498 qed "mult_Rep_pnat"; |
381 qed "mult_Rep_pnat"; |
499 |
382 |
500 Goalw [pnat_mult_def] |
383 Goalw [pnat_mult_def] |
501 "Rep_pnat x * Rep_pnat y = Rep_pnat (x * y)"; |
384 "Rep_pnat x * Rep_pnat y = Rep_pnat (x * y)"; |
502 by (simp_tac (simpset() addsimps [mult_Rep_pnat RS |
385 by (simp_tac (simpset() addsimps [mult_Rep_pnat RS Abs_pnat_inverse]) 1); |
503 Abs_pnat_inverse]) 1); |
|
504 qed "mult_Rep_pnat_mult"; |
386 qed "mult_Rep_pnat_mult"; |
505 |
387 |
506 Goalw [pnat_mult_def] "m * n = n * (m::pnat)"; |
388 Goalw [pnat_mult_def] "m * n = n * (m::pnat)"; |
507 by (full_simp_tac (simpset() addsimps [mult_commute]) 1); |
389 by (full_simp_tac (simpset() addsimps [mult_commute]) 1); |
508 qed "pnat_mult_commute"; |
390 qed "pnat_mult_commute"; |