diff -r 9290fbf0a30e -r b6ff7db522b5 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/HOL/Divides.thy	Wed Oct 28 17:44:03 2009 +0100
@@ -178,6 +178,9 @@
 lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b"
 by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0)
 
+lemma dvd_mult_div_cancel: "a dvd b \<Longrightarrow> a * (b div a) = b"
+by (drule dvd_div_mult_self) (simp add: mult_commute)
+
 lemma dvd_div_mult: "a dvd b \<Longrightarrow> (b div a) * c = b * c div a"
 apply (cases "a = 0")
  apply simp
@@ -866,79 +869,6 @@
 apply (auto simp add: Suc_diff_le le_mod_geq)
 done
 
-
-subsubsection {* The Divides Relation *}
-
-lemma dvd_1_left [iff]: "Suc 0 dvd k"
-  unfolding dvd_def by simp
-
-lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
-by (simp add: dvd_def)
-
-lemma nat_dvd_1_iff_1 [simp]: "m dvd (1::nat) \<longleftrightarrow> m = 1"
-by (simp add: dvd_def)
-
-lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
-  unfolding dvd_def
-  by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
-
-text {* @{term "op dvd"} is a partial order *}
-
-interpretation dvd: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
-  proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
-
-lemma dvd_diff_nat[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
-unfolding dvd_def
-by (blast intro: diff_mult_distrib2 [symmetric])
-
-lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"
-  apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
-  apply (blast intro: dvd_add)
-  done
-
-lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"
-by (drule_tac m = m in dvd_diff_nat, auto)
-
-lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
-  apply (rule iffI)
-   apply (erule_tac [2] dvd_add)
-   apply (rule_tac [2] dvd_refl)
-  apply (subgoal_tac "n = (n+k) -k")
-   prefer 2 apply simp
-  apply (erule ssubst)
-  apply (erule dvd_diff_nat)
-  apply (rule dvd_refl)
-  done
-
-lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
-  unfolding dvd_def
-  apply (erule exE)
-  apply (simp add: mult_ac)
-  done
-
-lemma dvd_mult_cancel1: "0<m ==> (m*n dvd m) = (n = (1::nat))"
-  apply auto
-   apply (subgoal_tac "m*n dvd m*1")
-   apply (drule dvd_mult_cancel, auto)
-  done
-
-lemma dvd_mult_cancel2: "0<m ==> (n*m dvd m) = (n = (1::nat))"
-  apply (subst mult_commute)
-  apply (erule dvd_mult_cancel1)
-  done
-
-lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
-  by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
-
-lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
-  by (simp add: dvd_eq_mod_eq_0 mult_div_cancel)
-
-lemma power_dvd_imp_le:
-  "i ^ m dvd i ^ n \<Longrightarrow> (1::nat) < i \<Longrightarrow> m \<le> n"
-  apply (rule power_le_imp_le_exp, assumption)
-  apply (erule dvd_imp_le, simp)
-  done
-
 lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
 by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
 
@@ -1162,9 +1092,4 @@
   with j show ?thesis by blast
 qed
 
-lemma nat_dvd_not_less:
-  fixes m n :: nat
-  shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
-by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
-
 end