src/HOL/Divides.ML
changeset 12304 8df202daf55d
parent 11701 3d51fbf81c17
equal deleted inserted replaced
12303:67ca723a02dd 12304:8df202daf55d
   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];