src/HOL/Divides.ML

 Addsimps [mod_mult_self_is_0];
 
 (*** Quotient ***)
 
 Goal "(%m. m div n) = wfrec (trancl pred_nat) \
-                        \            (%f j. if j<n then 0 else Suc (f (j-n)))";
+\            (%f j. if j<n then 0 else Suc (f (j-n)))";
 by (simp_tac (simpset() addsimps [div_def]) 1);
 qed "div_eq";
 
 Goal "m<n ==> m div n = 0";
 by (rtac (div_eq RS wf_less_trans) 1);

 (*Avoids the ugly ~m<n above*)
 Goal "[| 0<n;  n<=m |] ==> m div n = Suc((m-n) div n)";
 by (asm_simp_tac (simpset() addsimps [div_geq, not_less_iff_le]) 1);
 qed "le_div_geq";
 
-(*NOT suitable for rewriting: loops*)
 Goal "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))";
 by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1);
 qed "div_if";
 
 (*Main Result about quotient and remainder.*)

 (*Restore the default*)
 Delrules [less_SucE];
 
 (*** More division laws ***)
 
-Goal "0<n ==> m*n div n = m";
+Goal "0<n ==> (m*n) div n = m";
 by (cut_inst_tac [("m", "m*n")] mod_div_equality 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [mod_mult_self_is_0]) 1);
 qed "div_mult_self_is_m";
 Addsimps [div_mult_self_is_m];