src/HOL/Divides.thy
 changeset 47138 f8cf96545eed parent 47137 7f5f0531cae6 child 47139 98bddfa0f717
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.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.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.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.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.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.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.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.76  subsubsection {* An ``induction'' law for modulus arithmetic. *}
1.77 @@ -1071,17 +1052,14 @@
1.78  qed
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.87  lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
1.88  by (simp add: nat_mult_2 [symmetric])
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.101  declare Suc_times_mod_eq [of "numeral w", simp] for w
1.103 -lemma [simp]: "n div k \<le> (Suc n) div k"