# HG changeset patch
# User haftmann
# Date 1223613948 -7200
# Node ID 55c003a5600a0ff243f20ed8fd517c0b35ab6f4a
# Parent  2a6297b4273c9953f1554b1f082090d9a9c106de
tuned default rules of (dvd)

diff -r 2a6297b4273c -r 55c003a5600a NEWS
--- a/NEWS	Thu Oct 09 21:34:11 2008 +0200
+++ b/NEWS	Fri Oct 10 06:45:48 2008 +0200
@@ -91,8 +91,8 @@
 
 *** HOL ***
 
-* Unified theorem tables of both code code generators.  Thus [code]
-and [code func] behave identically.  INCOMPATIBILITY.
+* Unified theorem tables of both code code generators.  Thus [code func]
+has disappeared and only [code] remains.  INCOMPATIBILITY.
 
 * "undefined" replaces "arbitrary" in most occurences.
 
@@ -128,6 +128,7 @@
 
     dvd_def_mod ~>          dvd_eq_mod_eq_0
     zero_dvd_iff ~>         dvd_0_left_iff
+    dvd_0 ~>                dvd_0_right
     DIVISION_BY_ZERO_DIV ~> div_by_0
     DIVISION_BY_ZERO_MOD ~> mod_by_0
     mult_div ~>             div_mult_self2_is_id
diff -r 2a6297b4273c -r 55c003a5600a src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Thu Oct 09 21:34:11 2008 +0200
+++ b/src/HOL/Ring_and_Field.thy	Fri Oct 10 06:45:48 2008 +0200
@@ -109,10 +109,8 @@
 class dvd = times
 begin
 
-definition
-  dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)
-where
-  [code func del]: "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
+definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where
+  [code del]: "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
 
 lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
   unfolding dvd_def ..
@@ -129,34 +127,33 @@
 subclass semiring_1 ..
 
 lemma dvd_refl: "a dvd a"
-proof -
-  have "a = a * 1" by simp
-  then show ?thesis unfolding dvd_def ..
+proof
+  show "a = a * 1" by simp
 qed
 
 lemma dvd_trans:
   assumes "a dvd b" and "b dvd c"
   shows "a dvd c"
 proof -
-  from assms obtain v where "b = a * v" unfolding dvd_def by auto
-  moreover from assms obtain w where "c = b * w" unfolding dvd_def by auto
+  from assms obtain v where "b = a * v" by (auto elim!: dvdE)
+  moreover from assms obtain w where "c = b * w" by (auto elim!: dvdE)
   ultimately have "c = a * (v * w)" by (simp add: mult_assoc)
-  then show ?thesis unfolding dvd_def ..
+  then show ?thesis ..
 qed
 
 lemma dvd_0_left_iff [noatp, simp]: "0 dvd a \<longleftrightarrow> a = 0"
-  unfolding dvd_def by simp
-
-lemma dvd_0 [simp]: "a dvd 0"
-unfolding dvd_def proof
+  by (auto intro: dvd_refl elim!: dvdE)
+
+lemma dvd_0_right [iff]: "a dvd 0"
+proof
   show "0 = a * 0" by simp
 qed
 
 lemma one_dvd [simp]: "1 dvd a"
-  unfolding dvd_def by simp
+  by (auto intro!: dvdI)
 
 lemma dvd_mult: "a dvd c \<Longrightarrow> a dvd (b * c)"
-  unfolding dvd_def by (blast intro: mult_left_commute)
+  by (auto intro!: mult_left_commute dvdI elim!: dvdE)
 
 lemma dvd_mult2: "a dvd b \<Longrightarrow> a dvd (b * c)"
   apply (subst mult_commute)
@@ -186,12 +183,6 @@
 lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
   unfolding mult_ac [of a] by (rule dvd_mult_left)
 
-lemma dvd_0_right [iff]: "a dvd 0"
-proof -
-  have "0 = a * 0" by simp
-  then show ?thesis unfolding dvd_def ..
-qed
-
 lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
   by simp
 
@@ -533,7 +524,7 @@
 
 lemma divide_self_if [simp]:
   "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)"
-  by (simp add: divide_self)
+  by simp
 
 class mult_mono = times + zero + ord +
   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"