src/HOL/Divides.ML
changeset 7493 e6f74eebfab3
parent 7082 f444e632cdf5
child 7499 23e090051cb8
equal deleted inserted replaced
7492:44b333fb5b80 7493:e6f74eebfab3
   435 qed "dvd_mult2";
   435 qed "dvd_mult2";
   436 
   436 
   437 (* k dvd (m*k) *)
   437 (* k dvd (m*k) *)
   438 AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
   438 AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
   439 
   439 
       
   440 Goal "k dvd (n + k) = k dvd (n::nat)";
       
   441 br iffI 1;
       
   442 be  dvd_add 2;
       
   443 br  dvd_refl 2;
       
   444 by (subgoal_tac "n = (n+k)-k" 1);
       
   445 by  (Simp_tac 2);
       
   446 be ssubst 1;
       
   447 be dvd_diff 1;
       
   448 br dvd_refl 1;
       
   449 qed "dvd_reduce";
       
   450 
   440 Goalw [dvd_def] "[| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
   451 Goalw [dvd_def] "[| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
   441 by (Clarify_tac 1);
   452 by (Clarify_tac 1);
   442 by (Full_simp_tac 1);
   453 by (Full_simp_tac 1);
   443 by (res_inst_tac 
   454 by (res_inst_tac 
   444     [("x", "(((k div ka)*ka + k mod ka) - ((f*k) div (f*ka)) * ka)")] 
   455     [("x", "(((k div ka)*ka + k mod ka) - ((f*k) div (f*ka)) * ka)")]