equal
deleted
inserted
replaced
506 (************************************************) |
506 (************************************************) |
507 |
507 |
508 Goalw [dvd_def] "n = m * k ==> m dvd n"; |
508 Goalw [dvd_def] "n = m * k ==> m dvd n"; |
509 by (Blast_tac 1); |
509 by (Blast_tac 1); |
510 qed "dvdI"; |
510 qed "dvdI"; |
511 AddXIs [dvdI]; |
|
512 |
511 |
513 Goalw [dvd_def] "!!P. [|m dvd n; !!k. n = m*k ==> P|] ==> P"; |
512 Goalw [dvd_def] "!!P. [|m dvd n; !!k. n = m*k ==> P|] ==> P"; |
514 by (Blast_tac 1); |
513 by (Blast_tac 1); |
515 qed "dvdE"; |
514 qed "dvdE"; |
516 AddXEs [dvdE]; |
|
517 |
515 |
518 Goalw [dvd_def] "m dvd (0::nat)"; |
516 Goalw [dvd_def] "m dvd (0::nat)"; |
519 by (blast_tac (claset() addIs [mult_0_right RS sym]) 1); |
517 by (blast_tac (claset() addIs [mult_0_right RS sym]) 1); |
520 qed "dvd_0_right"; |
518 qed "dvd_0_right"; |
521 AddIffs [dvd_0_right]; |
519 AddIffs [dvd_0_right]; |