# HG changeset patch
# User haftmann
# Date 1434092003 -7200
# Node ID d3d1e185cd637a0bbd8bd07c40f17adf0a7450d7
# Parent  5e9de4faef986a334fde37193d05f428ef05161d
uniform _ div _ as infix syntax for ring division

diff -r 5e9de4faef98 -r d3d1e185cd63 NEWS
--- a/NEWS	Thu Jun 11 21:41:55 2015 +0100
+++ b/NEWS	Fri Jun 12 08:53:23 2015 +0200
@@ -65,13 +65,13 @@
 * Nitpick:
   - Removed "check_potential" and "check_genuine" options.
 
-* Constants Fields.divide (... / ...) and Divides.div (... div ...)
+* Former constants Fields.divide (_ / _) and Divides.div (_ div _)
 are logically unified to Rings.divide in syntactic type class
-Rings.divide, with particular infix syntax added as abbreviations
-in classes Fields.inverse and Divides.div respectively.  INCOMPATIBILITY,
-instantiatios must refer to Rings.divide rather than the former
-separate constants, and infix syntax is usually not available during
-instantiation.
+Rings.divide, with infix syntax (_ div _).  Infix syntax (_ / _)
+for field division is added later as abbreviation in class Fields.inverse.
+INCOMPATIBILITY,  instantiatios must refer to Rings.divide rather
+than the former separate constants, hence infix syntax (_ / _) is usually
+not available during instantiation.
 
 * Library/Multiset:
   - Renamed multiset inclusion operators:
diff -r 5e9de4faef98 -r d3d1e185cd63 src/Doc/Tutorial/Misc/appendix.thy
--- a/src/Doc/Tutorial/Misc/appendix.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/Doc/Tutorial/Misc/appendix.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -14,8 +14,8 @@
 @{term [source] minus} & @{typeof [show_sorts] "minus"} & (infixl $-$ 65) \\
 @{term [source] uminus} & @{typeof [show_sorts] "uminus"} & $- x$ \\
 @{term [source] times} & @{typeof [show_sorts] "times"} & (infixl $*$ 70) \\
-@{term [source] divide} & @{typeof [show_sorts] "divide"} & (infixl $/$ 70) \\
-@{term [source] Divides.div} & @{typeof [show_sorts] "Divides.div"} & (infixl $div$ 70) \\
+@{term [source] inverse_divide} & @{typeof [show_sorts] "inverse_divide"} & (infixl $/$ 70) \\
+@{term [source] divide} & @{typeof [show_sorts] "divide"} & (infixl $div$ 70) \\
 @{term [source] Divides.mod} & @{typeof [show_sorts] "Divides.mod"} & (infixl $mod$ 70) \\
 @{term [source] abs} & @{typeof [show_sorts] "abs"} & ${\mid} x {\mid}$ \\
 @{term [source] sgn} & @{typeof [show_sorts] "sgn"} \\
diff -r 5e9de4faef98 -r d3d1e185cd63 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/Complex.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -70,7 +70,7 @@
   "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
 | "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
 
-definition "divide x (y\<Colon>complex) = x * inverse y"
+definition "x div (y\<Colon>complex) = x * inverse y"
 
 instance
   by intro_classes
diff -r 5e9de4faef98 -r d3d1e185cd63 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/Divides.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -9,19 +9,10 @@
 imports Parity
 begin
 
-subsection {* Syntactic division operations *}
+subsection {* Abstract division in commutative semirings. *}
 
 class div = dvd + divide +
   fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
-begin
-
-abbreviation div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
-where
-  "op div \<equiv> divide"
-
-end
-
-subsection {* Abstract division in commutative semirings. *}
 
 class semiring_div = semidom + div +
   assumes mod_div_equality: "a div b * b + a mod b = a"
@@ -47,7 +38,7 @@
   "n \<noteq> 0 \<Longrightarrow> a ^ n = 0 \<longleftrightarrow> a = 0"
   using power_not_zero [of a n] by (auto simp add: zero_power)
 
-text {* @{const div} and @{const mod} *}
+text {* @{const divide} and @{const mod} *}
 
 lemma mod_div_equality2: "b * (a div b) + a mod b = a"
   unfolding mult.commute [of b]
@@ -874,7 +865,7 @@
 subsection {* Division on @{typ nat} *}
 
 text {*
-  We define @{const div} and @{const mod} on @{typ nat} by means
+  We define @{const divide} and @{const mod} on @{typ nat} by means
   of a characteristic relation with two input arguments
   @{term "m\<Colon>nat"}, @{term "n\<Colon>nat"} and two output arguments
   @{term "q\<Colon>nat"}(uotient) and @{term "r\<Colon>nat"}(emainder).
@@ -964,21 +955,14 @@
   shows "divmod_nat m n = qr"
   using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
 
-instantiation nat :: "Divides.div"
+instantiation nat :: semiring_div
 begin
 
 definition divide_nat where
-  div_nat_def: "divide m n = fst (divmod_nat m n)"
+  div_nat_def: "m div n = fst (divmod_nat m n)"
 
 definition mod_nat where
   "m mod n = snd (divmod_nat m n)"
-  
-instance ..
-
-end
-
-instantiation nat :: semiring_div
-begin
 
 lemma fst_divmod_nat [simp]:
   "fst (divmod_nat m n) = m div n"
@@ -1024,7 +1008,7 @@
     unfolding divmod_nat_rel_def using assms by auto
 qed
 
-text {* The ''recursion'' equations for @{const div} and @{const mod} *}
+text {* The ''recursion'' equations for @{const divide} and @{const mod} *}
 
 lemma div_less [simp]:
   fixes m n :: nat
@@ -1082,7 +1066,7 @@
   let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
   by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
 
-text {* Simproc for cancelling @{const div} and @{const mod} *}
+text {* Simproc for cancelling @{const divide} and @{const mod} *}
 
 ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
 
@@ -1699,19 +1683,15 @@
                   if 0 < b then negDivAlg a b
                   else apsnd uminus (posDivAlg (-a) (-b)))"
 
-instantiation int :: Divides.div
+instantiation int :: ring_div
 begin
 
 definition divide_int where
-  div_int_def: "divide a b = fst (divmod_int a b)"
+  div_int_def: "a div b = fst (divmod_int a b)"
 
 definition mod_int where
   "a mod b = snd (divmod_int a b)"
 
-instance ..
-
-end
-
 lemma fst_divmod_int [simp]:
   "fst (divmod_int a b) = a div b"
   by (simp add: div_int_def)
@@ -1897,7 +1877,7 @@
 lemma mod_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a mod b = r"
   by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])
 
-instance int :: ring_div
+instance
 proof
   fix a b :: int
   show "a div b * b + a mod b = a"
@@ -1932,6 +1912,8 @@
     by (rule div_int_unique, auto simp add: divmod_int_rel_def)
 qed
 
+end
+
 text{*Basic laws about division and remainder*}
 
 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
@@ -2479,7 +2461,7 @@
                       split_neg_lemma [of concl: "%x y. P y"])
 done
 
-text {* Enable (lin)arith to deal with @{const div} and @{const mod}
+text {* Enable (lin)arith to deal with @{const divide} and @{const mod}
   when these are applied to some constant that is of the form
   @{term "numeral k"}: *}
 declare split_zdiv [of _ _ "numeral k", arith_split] for k
diff -r 5e9de4faef98 -r d3d1e185cd63 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/Enum.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -817,7 +817,7 @@
 definition "x - y = x + (- y :: finite_3)"
 definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>3) \<Rightarrow> a\<^sub>2 | (a\<^sub>2, a\<^sub>3) \<Rightarrow> a\<^sub>3 | (a\<^sub>3, a\<^sub>2) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
 definition "inverse = (\<lambda>x :: finite_3. x)" 
-definition "divide x y = x * inverse (y :: finite_3)"
+definition "x div y = x * inverse (y :: finite_3)"
 definition "abs = (\<lambda>x :: finite_3. x)"
 definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>1) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
 definition "sgn = (\<lambda>x. case x of a\<^sub>1 \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
diff -r 5e9de4faef98 -r d3d1e185cd63 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/Groups_Big.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -1155,7 +1155,7 @@
 
 lemma (in semidom_divide) setprod_diff1:
   assumes "finite A" and "f a \<noteq> 0"
-  shows "setprod f (A - {a}) = (if a \<in> A then divide (setprod f A) (f a) else setprod f A)"
+  shows "setprod f (A - {a}) = (if a \<in> A then setprod f A div f a else setprod f A)"
 proof (cases "a \<notin> A")
   case True then show ?thesis by simp
 next
diff -r 5e9de4faef98 -r d3d1e185cd63 src/HOL/Import/HOL_Light_Maps.thy
--- a/src/HOL/Import/HOL_Light_Maps.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/Import/HOL_Light_Maps.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -198,7 +198,7 @@
   by simp
 
 import_const_map MOD : mod
-import_const_map DIV : div
+import_const_map DIV : divide
 
 lemma DIVISION_0:
   "\<forall>m n\<Colon>nat. if n = id 0 then m div n = id 0 \<and> m mod n = m else m = m div n * n + m mod n \<and> m mod n < n"
diff -r 5e9de4faef98 -r d3d1e185cd63 src/HOL/Library/Bit.thy
--- a/src/HOL/Library/Bit.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/Library/Bit.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -117,7 +117,7 @@
   "inverse x = (x :: bit)"
 
 definition divide_bit_def [simp]:
-  "divide x y = (x * y :: bit)"
+  "x div y = (x * y :: bit)"
 
 lemmas field_bit_defs =
   plus_bit_def times_bit_def minus_bit_def uminus_bit_def
diff -r 5e9de4faef98 -r d3d1e185cd63 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -1403,7 +1403,7 @@
   by (auto intro: ereal_cases)
 termination by (relation "{}") simp
 
-definition "divide x y = x * inverse (y :: ereal)"
+definition "x div y = x * inverse (y :: ereal)"
 
 instance ..
 
diff -r 5e9de4faef98 -r d3d1e185cd63 src/HOL/Library/Fraction_Field.thy
--- a/src/HOL/Library/Fraction_Field.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/Library/Fraction_Field.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -241,9 +241,9 @@
     by (simp add: Fract_def inverse_fract_def UN_fractrel)
 qed
 
-definition divide_fract_def: "divide q r = q * inverse (r:: 'a fract)"
+definition divide_fract_def: "q div r = q * inverse (r:: 'a fract)"
 
-lemma divide_fract [simp]: "divide (Fract a b) (Fract c d) = Fract (a * d) (b * c)"
+lemma divide_fract [simp]: "Fract a b div Fract c d = Fract (a * d) (b * c)"
   by (simp add: divide_fract_def)
 
 instance
@@ -255,7 +255,7 @@
       (simp_all add: fract_expand eq_fract mult.commute)
 next
   fix q r :: "'a fract"
-  show "divide q r = q * inverse r" by (simp add: divide_fract_def)
+  show "q div r = q * inverse r" by (simp add: divide_fract_def)
 next
   show "inverse 0 = (0:: 'a fract)"
     by (simp add: fract_expand) (simp add: fract_collapse)
diff -r 5e9de4faef98 -r d3d1e185cd63 src/HOL/Library/Function_Division.thy
--- a/src/HOL/Library/Function_Division.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/Library/Function_Division.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -15,7 +15,7 @@
 
 definition "inverse f = inverse \<circ> f"
 
-definition "divide f g = (\<lambda>x. f x / g x)"
+definition "f div g = (\<lambda>x. f x / g x)"
 
 instance ..
 
diff -r 5e9de4faef98 -r d3d1e185cd63 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/Library/Polynomial.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -1361,13 +1361,13 @@
 begin
 
 definition divide_poly where
-  div_poly_def: "divide x y = (THE q. \<exists>r. pdivmod_rel x y q r)"
+  div_poly_def: "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)"
 
 definition mod_poly where
   "x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)"
 
 lemma div_poly_eq:
-  "pdivmod_rel x y q r \<Longrightarrow> divide x y = q"
+  "pdivmod_rel x y q r \<Longrightarrow> x div y = q"
 unfolding div_poly_def
 by (fast elim: pdivmod_rel_unique_div)
 
@@ -1377,7 +1377,7 @@
 by (fast elim: pdivmod_rel_unique_mod)
 
 lemma pdivmod_rel:
-  "pdivmod_rel x y (divide x y) (x mod y)"
+  "pdivmod_rel x y (x div y) (x mod y)"
 proof -
   from pdivmod_rel_exists
     obtain q r where "pdivmod_rel x y q r" by fast
@@ -1387,41 +1387,41 @@
 
 instance proof
   fix x y :: "'a poly"
-  show "divide x y * y + x mod y = x"
+  show "x div y * y + x mod y = x"
     using pdivmod_rel [of x y]
     by (simp add: pdivmod_rel_def)
 next
   fix x :: "'a poly"
   have "pdivmod_rel x 0 0 x"
     by (rule pdivmod_rel_by_0)
-  thus "divide x 0 = 0"
+  thus "x div 0 = 0"
     by (rule div_poly_eq)
 next
   fix y :: "'a poly"
   have "pdivmod_rel 0 y 0 0"
     by (rule pdivmod_rel_0)
-  thus "divide 0 y = 0"
+  thus "0 div y = 0"
     by (rule div_poly_eq)
 next
   fix x y z :: "'a poly"
   assume "y \<noteq> 0"
-  hence "pdivmod_rel (x + z * y) y (z + divide x y) (x mod y)"
+  hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
     using pdivmod_rel [of x y]
     by (simp add: pdivmod_rel_def distrib_right)
-  thus "divide (x + z * y) y = z + divide x y"
+  thus "(x + z * y) div y = z + x div y"
     by (rule div_poly_eq)
 next
   fix x y z :: "'a poly"
   assume "x \<noteq> 0"
-  show "divide (x * y) (x * z) = divide y z"
+  show "(x * y) div (x * z) = y div z"
   proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
     have "\<And>x::'a poly. pdivmod_rel x 0 0 x"
       by (rule pdivmod_rel_by_0)
-    then have [simp]: "\<And>x::'a poly. divide x 0 = 0"
+    then have [simp]: "\<And>x::'a poly. x div 0 = 0"
       by (rule div_poly_eq)
     have "\<And>x::'a poly. pdivmod_rel 0 x 0 0"
       by (rule pdivmod_rel_0)
-    then have [simp]: "\<And>x::'a poly. divide 0 x = 0"
+    then have [simp]: "\<And>x::'a poly. 0 div x = 0"
       by (rule div_poly_eq)
     case False then show ?thesis by auto
   next
@@ -1430,8 +1430,8 @@
     have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> pdivmod_rel (x * y) (x * z) q (x * r)"
       by (auto simp add: pdivmod_rel_def algebra_simps)
         (rule classical, simp add: degree_mult_eq)
-    moreover from pdivmod_rel have "pdivmod_rel y z (divide y z) (y mod z)" .
-    ultimately have "pdivmod_rel (x * y) (x * z) (divide y z) (x * (y mod z))" .
+    moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" .
+    ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" .
     then show ?thesis by (simp add: div_poly_eq)
   qed
 qed
diff -r 5e9de4faef98 -r d3d1e185cd63 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/NSA/StarDef.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -577,7 +577,7 @@
 lemma Standard_mult: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x * y \<in> Standard"
 by (simp add: star_mult_def)
 
-lemma Standard_divide: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> divide x y \<in> Standard"
+lemma Standard_divide: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x / y \<in> Standard"
 by (simp add: star_divide_def)
 
 lemma Standard_inverse: "x \<in> Standard \<Longrightarrow> inverse x \<in> Standard"
@@ -855,9 +855,9 @@
 instance star :: (semidom) semidom ..
 instance star :: (semidom_divide) semidom_divide
 proof
-  show "\<And>b a :: 'a star. b \<noteq> 0 \<Longrightarrow> divide (a * b) b = a"
+  show "\<And>b a :: 'a star. b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
     by transfer simp
-  show "\<And>a :: 'a star. divide a 0 = 0"
+  show "\<And>a :: 'a star. a div 0 = 0"
     by transfer simp
 qed
 instance star :: (semiring_div) semiring_div
diff -r 5e9de4faef98 -r d3d1e185cd63 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/Rat.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -162,9 +162,9 @@
   by transfer simp
 
 definition
-  divide_rat_def: "divide q r = q * inverse (r::rat)"
+  divide_rat_def: "q div r = q * inverse (r::rat)"
 
-lemma divide_rat [simp]: "divide (Fract a b) (Fract c d) = Fract (a * d) (b * c)"
+lemma divide_rat [simp]: "Fract a b div Fract c d = Fract (a * d) (b * c)"
   by (simp add: divide_rat_def)
 
 instance proof
@@ -191,7 +191,7 @@
     by transfer simp
   { assume "q \<noteq> 0" thus "inverse q * q = 1"
     by transfer simp }
-  show "divide q r = q * inverse r"
+  show "q div r = q * inverse r"
     by (fact divide_rat_def)
   show "inverse 0 = (0::rat)"
     by transfer simp
diff -r 5e9de4faef98 -r d3d1e185cd63 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/Real.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -438,7 +438,7 @@
   "x - y = (x::real) + - y"
 
 definition
-  "divide x y = (x::real) * inverse y"
+  "x div y = (x::real) * inverse y"
 
 lemma add_Real:
   assumes X: "cauchy X" and Y: "cauchy Y"
@@ -501,7 +501,7 @@
     apply (rule_tac x=k in exI, clarify)
     apply (drule_tac x=n in spec, simp)
     done
-  show "divide a b = a * inverse b"
+  show "a div b = a * inverse b"
     by (rule divide_real_def)
   show "inverse (0::real) = 0"
     by transfer (simp add: realrel_def)
diff -r 5e9de4faef98 -r d3d1e185cd63 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/Rings.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -559,7 +559,7 @@
 *}
 
 class divide =
-  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
 
 setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
 
@@ -567,8 +567,8 @@
 begin
 
 lemma [field_simps]:
-  shows distrib_left_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
-    and distrib_right_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
+  shows distrib_left_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
+    and distrib_right_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
   by (rule distrib_left distrib_right)+
 
 end
@@ -577,8 +577,8 @@
 begin
 
 lemma [field_simps]:
-  shows left_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
-    and right_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
+  shows left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
+    and right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
   by (rule left_diff_distrib right_diff_distrib)+
 
 end
@@ -586,12 +586,12 @@
 setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
 
 class semidom_divide = semidom + divide +
-  assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> divide (a * b) b = a"
-  assumes divide_zero [simp]: "divide a 0 = 0"
+  assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
+  assumes divide_zero [simp]: "a div 0 = 0"
 begin
 
 lemma nonzero_mult_divide_cancel_left [simp]:
-  "a \<noteq> 0 \<Longrightarrow> divide (a * b) a = b"
+  "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
   using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)
 
 end
diff -r 5e9de4faef98 -r d3d1e185cd63 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/Word/Word.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -307,7 +307,7 @@
   by (metis bintr_ariths(4))
 
 definition
-  word_div_def: "divide a b = word_of_int (uint a div uint b)"
+  word_div_def: "a div b = word_of_int (uint a div uint b)"
 
 definition
   word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
diff -r 5e9de4faef98 -r d3d1e185cd63 src/HOL/ex/Arith_Examples.thy
--- a/src/HOL/ex/Arith_Examples.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/ex/Arith_Examples.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -31,7 +31,7 @@
 
 subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
            @{term minus}, @{term nat}, @{term Divides.mod},
-           @{term Divides.div} *}
+           @{term divide} *}
 
 lemma "(i::nat) <= max i j"
   by linarith
diff -r 5e9de4faef98 -r d3d1e185cd63 src/HOL/ex/Dedekind_Real.thy
--- a/src/HOL/ex/Dedekind_Real.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/ex/Dedekind_Real.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -102,7 +102,7 @@
   preal_inverse_def:
     "inverse R == Abs_preal (inverse_set (Rep_preal R))"
 
-definition "divide R S = R * inverse (S\<Colon>preal)"
+definition "R div S = R * inverse (S\<Colon>preal)"
 
 definition
   preal_one_def:
@@ -1222,7 +1222,7 @@
   real_inverse_def: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
 
 definition
-  real_divide_def: "divide R (S::real) = R * inverse S"
+  real_divide_def: "R div (S::real) = R * inverse S"
 
 definition
   real_le_def: "z \<le> (w::real) \<longleftrightarrow>