1.1 --- a/src/HOL/Divides.thy	Tue Mar 27 10:34:12 2012 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 11:02:18 2012 +0200
     1.3 @@ -713,19 +713,14 @@
     1.4  by (induct m) (simp_all add: mod_geq)
     1.5  
     1.6  lemma mod_mult_distrib: "(m mod n) * (k\<Colon>nat) = (m * k) mod (n * k)"
     1.7 -  apply (cases "n = 0", simp)
     1.8 -  apply (cases "k = 0", simp)
     1.9 -  apply (induct m rule: nat_less_induct)
    1.10 -  apply (subst mod_if, simp)
    1.11 -  apply (simp add: mod_geq diff_mult_distrib)
    1.12 -  done
    1.13 +  by (fact mod_mult_mult2 [symmetric]) (* FIXME: generalize *)
    1.14  
    1.15  lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
    1.16 -by (simp add: mult_commute [of k] mod_mult_distrib)
    1.17 +  by (fact mod_mult_mult1 [symmetric]) (* FIXME: generalize *)
    1.18  
    1.19  (* a simple rearrangement of mod_div_equality: *)
    1.20  lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
    1.21 -by (cut_tac a = m and b = n in mod_div_equality2, arith)
    1.22 +  using mod_div_equality2 [of n m] by arith
    1.23  
    1.24  lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
    1.25    apply (drule mod_less_divisor [where m = m])
    1.26 @@ -818,9 +813,9 @@
    1.27  done
    1.28  
    1.29  (* Similar for "less than" *)
    1.30 -lemma div_less_dividend [rule_format]:
    1.31 -     "!!n::nat. 1<n ==> 0 < m --> m div n < m"
    1.32 -apply (induct_tac m rule: nat_less_induct)
    1.33 +lemma div_less_dividend [simp]:
    1.34 +  "\<lbrakk>(1::nat) < n; 0 < m\<rbrakk> \<Longrightarrow> m div n < m"
    1.35 +apply (induct m rule: nat_less_induct)
    1.36  apply (rename_tac "m")
    1.37  apply (case_tac "m<n", simp)
    1.38  apply (subgoal_tac "0<n")
    1.39 @@ -833,8 +828,6 @@
    1.40    apply (simp_all)
    1.41  done
    1.42  
    1.43 -declare div_less_dividend [simp]
    1.44 -
    1.45  text{*A fact for the mutilated chess board*}
    1.46  lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
    1.47  apply (case_tac "n=0", simp)
    1.48 @@ -963,23 +956,11 @@
    1.49  qed
    1.50  
    1.51  theorem mod_div_equality': "(m::nat) mod n = m - (m div n) * n"
    1.52 -  apply (rule_tac P="%x. m mod n = x - (m div n) * n" in
    1.53 -    subst [OF mod_div_equality [of _ n]])
    1.54 -  apply arith
    1.55 -  done
    1.56 -
    1.57 -lemma div_mod_equality':
    1.58 -  fixes m n :: nat
    1.59 -  shows "m div n * n = m - m mod n"
    1.60 -proof -
    1.61 -  have "m mod n \<le> m mod n" ..
    1.62 -  from div_mod_equality have 
    1.63 -    "m div n * n + m mod n - m mod n = m - m mod n" by simp
    1.64 -  with diff_add_assoc [OF `m mod n \<le> m mod n`, of "m div n * n"] have
    1.65 -    "m div n * n + (m mod n - m mod n) = m - m mod n"
    1.66 -    by simp
    1.67 -  then show ?thesis by simp
    1.68 -qed
    1.69 +  using mod_div_equality [of m n] by arith
    1.70 +
    1.71 +lemma div_mod_equality': "(m::nat) div n * n = m - m mod n"
    1.72 +  using mod_div_equality [of m n] by arith
    1.73 +(* FIXME: very similar to mult_div_cancel *)
    1.74  
    1.75  
    1.76  subsubsection {* An ``induction'' law for modulus arithmetic. *}
    1.77 @@ -1071,17 +1052,14 @@
    1.78  qed
    1.79  
    1.80  lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)"
    1.81 -by (auto simp add: numeral_2_eq_2 le_div_geq)
    1.82 +  by (simp add: numeral_2_eq_2 le_div_geq)
    1.83 +
    1.84 +lemma mod2_Suc_Suc [simp]: "Suc (Suc m) mod 2 = m mod 2"
    1.85 +  by (simp add: numeral_2_eq_2 le_mod_geq)
    1.86  
    1.87  lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
    1.88  by (simp add: nat_mult_2 [symmetric])
    1.89  
    1.90 -lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
    1.91 -apply (subgoal_tac "m mod 2 < 2")
    1.92 -apply (erule less_2_cases [THEN disjE])
    1.93 -apply (simp_all (no_asm_simp) add: Let_def mod_Suc)
    1.94 -done
    1.95 -
    1.96  lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
    1.97  proof -
    1.98    { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }
    1.99 @@ -1117,8 +1095,8 @@
   1.100  
   1.101  declare Suc_times_mod_eq [of "numeral w", simp] for w
   1.102  
   1.103 -lemma [simp]: "n div k \<le> (Suc n) div k"
   1.104 -by (simp add: div_le_mono) 
   1.105 +lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
   1.106 +by (simp add: div_le_mono)
   1.107  
   1.108  lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
   1.109  by (cases n) simp_all