uniform _ div _ as infix syntax for ring division
authorhaftmann
Fri Jun 12 08:53:23 2015 +0200 (2015-06-12)
changeset 60429d3d1e185cd63
parent 60428 5e9de4faef98
child 60430 ce559c850a27
uniform _ div _ as infix syntax for ring division
NEWS
src/Doc/Tutorial/Misc/appendix.thy
src/HOL/Complex.thy
src/HOL/Divides.thy
src/HOL/Enum.thy
src/HOL/Groups_Big.thy
src/HOL/Import/HOL_Light_Maps.thy
src/HOL/Library/Bit.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Fraction_Field.thy
src/HOL/Library/Function_Division.thy
src/HOL/Library/Polynomial.thy
src/HOL/NSA/StarDef.thy
src/HOL/Rat.thy
src/HOL/Real.thy
src/HOL/Rings.thy
src/HOL/Word/Word.thy
src/HOL/ex/Arith_Examples.thy
src/HOL/ex/Dedekind_Real.thy
     1.1 --- a/NEWS	Thu Jun 11 21:41:55 2015 +0100
     1.2 +++ b/NEWS	Fri Jun 12 08:53:23 2015 +0200
     1.3 @@ -65,13 +65,13 @@
     1.4  * Nitpick:
     1.5    - Removed "check_potential" and "check_genuine" options.
     1.6  
     1.7 -* Constants Fields.divide (... / ...) and Divides.div (... div ...)
     1.8 +* Former constants Fields.divide (_ / _) and Divides.div (_ div _)
     1.9  are logically unified to Rings.divide in syntactic type class
    1.10 -Rings.divide, with particular infix syntax added as abbreviations
    1.11 -in classes Fields.inverse and Divides.div respectively.  INCOMPATIBILITY,
    1.12 -instantiatios must refer to Rings.divide rather than the former
    1.13 -separate constants, and infix syntax is usually not available during
    1.14 -instantiation.
    1.15 +Rings.divide, with infix syntax (_ div _).  Infix syntax (_ / _)
    1.16 +for field division is added later as abbreviation in class Fields.inverse.
    1.17 +INCOMPATIBILITY,  instantiatios must refer to Rings.divide rather
    1.18 +than the former separate constants, hence infix syntax (_ / _) is usually
    1.19 +not available during instantiation.
    1.20  
    1.21  * Library/Multiset:
    1.22    - Renamed multiset inclusion operators:
     2.1 --- a/src/Doc/Tutorial/Misc/appendix.thy	Thu Jun 11 21:41:55 2015 +0100
     2.2 +++ b/src/Doc/Tutorial/Misc/appendix.thy	Fri Jun 12 08:53:23 2015 +0200
     2.3 @@ -14,8 +14,8 @@
     2.4  @{term [source] minus} & @{typeof [show_sorts] "minus"} & (infixl $-$ 65) \\
     2.5  @{term [source] uminus} & @{typeof [show_sorts] "uminus"} & $- x$ \\
     2.6  @{term [source] times} & @{typeof [show_sorts] "times"} & (infixl $*$ 70) \\
     2.7 -@{term [source] divide} & @{typeof [show_sorts] "divide"} & (infixl $/$ 70) \\
     2.8 -@{term [source] Divides.div} & @{typeof [show_sorts] "Divides.div"} & (infixl $div$ 70) \\
     2.9 +@{term [source] inverse_divide} & @{typeof [show_sorts] "inverse_divide"} & (infixl $/$ 70) \\
    2.10 +@{term [source] divide} & @{typeof [show_sorts] "divide"} & (infixl $div$ 70) \\
    2.11  @{term [source] Divides.mod} & @{typeof [show_sorts] "Divides.mod"} & (infixl $mod$ 70) \\
    2.12  @{term [source] abs} & @{typeof [show_sorts] "abs"} & ${\mid} x {\mid}$ \\
    2.13  @{term [source] sgn} & @{typeof [show_sorts] "sgn"} \\
     3.1 --- a/src/HOL/Complex.thy	Thu Jun 11 21:41:55 2015 +0100
     3.2 +++ b/src/HOL/Complex.thy	Fri Jun 12 08:53:23 2015 +0200
     3.3 @@ -70,7 +70,7 @@
     3.4    "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
     3.5  | "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
     3.6  
     3.7 -definition "divide x (y\<Colon>complex) = x * inverse y"
     3.8 +definition "x div (y\<Colon>complex) = x * inverse y"
     3.9  
    3.10  instance
    3.11    by intro_classes
     4.1 --- a/src/HOL/Divides.thy	Thu Jun 11 21:41:55 2015 +0100
     4.2 +++ b/src/HOL/Divides.thy	Fri Jun 12 08:53:23 2015 +0200
     4.3 @@ -9,19 +9,10 @@
     4.4  imports Parity
     4.5  begin
     4.6  
     4.7 -subsection {* Syntactic division operations *}
     4.8 +subsection {* Abstract division in commutative semirings. *}
     4.9  
    4.10  class div = dvd + divide +
    4.11    fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
    4.12 -begin
    4.13 -
    4.14 -abbreviation div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
    4.15 -where
    4.16 -  "op div \<equiv> divide"
    4.17 -
    4.18 -end
    4.19 -
    4.20 -subsection {* Abstract division in commutative semirings. *}
    4.21  
    4.22  class semiring_div = semidom + div +
    4.23    assumes mod_div_equality: "a div b * b + a mod b = a"
    4.24 @@ -47,7 +38,7 @@
    4.25    "n \<noteq> 0 \<Longrightarrow> a ^ n = 0 \<longleftrightarrow> a = 0"
    4.26    using power_not_zero [of a n] by (auto simp add: zero_power)
    4.27  
    4.28 -text {* @{const div} and @{const mod} *}
    4.29 +text {* @{const divide} and @{const mod} *}
    4.30  
    4.31  lemma mod_div_equality2: "b * (a div b) + a mod b = a"
    4.32    unfolding mult.commute [of b]
    4.33 @@ -874,7 +865,7 @@
    4.34  subsection {* Division on @{typ nat} *}
    4.35  
    4.36  text {*
    4.37 -  We define @{const div} and @{const mod} on @{typ nat} by means
    4.38 +  We define @{const divide} and @{const mod} on @{typ nat} by means
    4.39    of a characteristic relation with two input arguments
    4.40    @{term "m\<Colon>nat"}, @{term "n\<Colon>nat"} and two output arguments
    4.41    @{term "q\<Colon>nat"}(uotient) and @{term "r\<Colon>nat"}(emainder).
    4.42 @@ -964,21 +955,14 @@
    4.43    shows "divmod_nat m n = qr"
    4.44    using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
    4.45  
    4.46 -instantiation nat :: "Divides.div"
    4.47 +instantiation nat :: semiring_div
    4.48  begin
    4.49  
    4.50  definition divide_nat where
    4.51 -  div_nat_def: "divide m n = fst (divmod_nat m n)"
    4.52 +  div_nat_def: "m div n = fst (divmod_nat m n)"
    4.53  
    4.54  definition mod_nat where
    4.55    "m mod n = snd (divmod_nat m n)"
    4.56 -  
    4.57 -instance ..
    4.58 -
    4.59 -end
    4.60 -
    4.61 -instantiation nat :: semiring_div
    4.62 -begin
    4.63  
    4.64  lemma fst_divmod_nat [simp]:
    4.65    "fst (divmod_nat m n) = m div n"
    4.66 @@ -1024,7 +1008,7 @@
    4.67      unfolding divmod_nat_rel_def using assms by auto
    4.68  qed
    4.69  
    4.70 -text {* The ''recursion'' equations for @{const div} and @{const mod} *}
    4.71 +text {* The ''recursion'' equations for @{const divide} and @{const mod} *}
    4.72  
    4.73  lemma div_less [simp]:
    4.74    fixes m n :: nat
    4.75 @@ -1082,7 +1066,7 @@
    4.76    let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
    4.77    by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
    4.78  
    4.79 -text {* Simproc for cancelling @{const div} and @{const mod} *}
    4.80 +text {* Simproc for cancelling @{const divide} and @{const mod} *}
    4.81  
    4.82  ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
    4.83  
    4.84 @@ -1699,19 +1683,15 @@
    4.85                    if 0 < b then negDivAlg a b
    4.86                    else apsnd uminus (posDivAlg (-a) (-b)))"
    4.87  
    4.88 -instantiation int :: Divides.div
    4.89 +instantiation int :: ring_div
    4.90  begin
    4.91  
    4.92  definition divide_int where
    4.93 -  div_int_def: "divide a b = fst (divmod_int a b)"
    4.94 +  div_int_def: "a div b = fst (divmod_int a b)"
    4.95  
    4.96  definition mod_int where
    4.97    "a mod b = snd (divmod_int a b)"
    4.98  
    4.99 -instance ..
   4.100 -
   4.101 -end
   4.102 -
   4.103  lemma fst_divmod_int [simp]:
   4.104    "fst (divmod_int a b) = a div b"
   4.105    by (simp add: div_int_def)
   4.106 @@ -1897,7 +1877,7 @@
   4.107  lemma mod_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a mod b = r"
   4.108    by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])
   4.109  
   4.110 -instance int :: ring_div
   4.111 +instance
   4.112  proof
   4.113    fix a b :: int
   4.114    show "a div b * b + a mod b = a"
   4.115 @@ -1932,6 +1912,8 @@
   4.116      by (rule div_int_unique, auto simp add: divmod_int_rel_def)
   4.117  qed
   4.118  
   4.119 +end
   4.120 +
   4.121  text{*Basic laws about division and remainder*}
   4.122  
   4.123  lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
   4.124 @@ -2479,7 +2461,7 @@
   4.125                        split_neg_lemma [of concl: "%x y. P y"])
   4.126  done
   4.127  
   4.128 -text {* Enable (lin)arith to deal with @{const div} and @{const mod}
   4.129 +text {* Enable (lin)arith to deal with @{const divide} and @{const mod}
   4.130    when these are applied to some constant that is of the form
   4.131    @{term "numeral k"}: *}
   4.132  declare split_zdiv [of _ _ "numeral k", arith_split] for k
     5.1 --- a/src/HOL/Enum.thy	Thu Jun 11 21:41:55 2015 +0100
     5.2 +++ b/src/HOL/Enum.thy	Fri Jun 12 08:53:23 2015 +0200
     5.3 @@ -817,7 +817,7 @@
     5.4  definition "x - y = x + (- y :: finite_3)"
     5.5  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)"
     5.6  definition "inverse = (\<lambda>x :: finite_3. x)" 
     5.7 -definition "divide x y = x * inverse (y :: finite_3)"
     5.8 +definition "x div y = x * inverse (y :: finite_3)"
     5.9  definition "abs = (\<lambda>x :: finite_3. x)"
    5.10  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)"
    5.11  definition "sgn = (\<lambda>x. case x of a\<^sub>1 \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
     6.1 --- a/src/HOL/Groups_Big.thy	Thu Jun 11 21:41:55 2015 +0100
     6.2 +++ b/src/HOL/Groups_Big.thy	Fri Jun 12 08:53:23 2015 +0200
     6.3 @@ -1155,7 +1155,7 @@
     6.4  
     6.5  lemma (in semidom_divide) setprod_diff1:
     6.6    assumes "finite A" and "f a \<noteq> 0"
     6.7 -  shows "setprod f (A - {a}) = (if a \<in> A then divide (setprod f A) (f a) else setprod f A)"
     6.8 +  shows "setprod f (A - {a}) = (if a \<in> A then setprod f A div f a else setprod f A)"
     6.9  proof (cases "a \<notin> A")
    6.10    case True then show ?thesis by simp
    6.11  next
     7.1 --- a/src/HOL/Import/HOL_Light_Maps.thy	Thu Jun 11 21:41:55 2015 +0100
     7.2 +++ b/src/HOL/Import/HOL_Light_Maps.thy	Fri Jun 12 08:53:23 2015 +0200
     7.3 @@ -198,7 +198,7 @@
     7.4    by simp
     7.5  
     7.6  import_const_map MOD : mod
     7.7 -import_const_map DIV : div
     7.8 +import_const_map DIV : divide
     7.9  
    7.10  lemma DIVISION_0:
    7.11    "\<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"
     8.1 --- a/src/HOL/Library/Bit.thy	Thu Jun 11 21:41:55 2015 +0100
     8.2 +++ b/src/HOL/Library/Bit.thy	Fri Jun 12 08:53:23 2015 +0200
     8.3 @@ -117,7 +117,7 @@
     8.4    "inverse x = (x :: bit)"
     8.5  
     8.6  definition divide_bit_def [simp]:
     8.7 -  "divide x y = (x * y :: bit)"
     8.8 +  "x div y = (x * y :: bit)"
     8.9  
    8.10  lemmas field_bit_defs =
    8.11    plus_bit_def times_bit_def minus_bit_def uminus_bit_def
     9.1 --- a/src/HOL/Library/Extended_Real.thy	Thu Jun 11 21:41:55 2015 +0100
     9.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri Jun 12 08:53:23 2015 +0200
     9.3 @@ -1403,7 +1403,7 @@
     9.4    by (auto intro: ereal_cases)
     9.5  termination by (relation "{}") simp
     9.6  
     9.7 -definition "divide x y = x * inverse (y :: ereal)"
     9.8 +definition "x div y = x * inverse (y :: ereal)"
     9.9  
    9.10  instance ..
    9.11  
    10.1 --- a/src/HOL/Library/Fraction_Field.thy	Thu Jun 11 21:41:55 2015 +0100
    10.2 +++ b/src/HOL/Library/Fraction_Field.thy	Fri Jun 12 08:53:23 2015 +0200
    10.3 @@ -241,9 +241,9 @@
    10.4      by (simp add: Fract_def inverse_fract_def UN_fractrel)
    10.5  qed
    10.6  
    10.7 -definition divide_fract_def: "divide q r = q * inverse (r:: 'a fract)"
    10.8 +definition divide_fract_def: "q div r = q * inverse (r:: 'a fract)"
    10.9  
   10.10 -lemma divide_fract [simp]: "divide (Fract a b) (Fract c d) = Fract (a * d) (b * c)"
   10.11 +lemma divide_fract [simp]: "Fract a b div Fract c d = Fract (a * d) (b * c)"
   10.12    by (simp add: divide_fract_def)
   10.13  
   10.14  instance
   10.15 @@ -255,7 +255,7 @@
   10.16        (simp_all add: fract_expand eq_fract mult.commute)
   10.17  next
   10.18    fix q r :: "'a fract"
   10.19 -  show "divide q r = q * inverse r" by (simp add: divide_fract_def)
   10.20 +  show "q div r = q * inverse r" by (simp add: divide_fract_def)
   10.21  next
   10.22    show "inverse 0 = (0:: 'a fract)"
   10.23      by (simp add: fract_expand) (simp add: fract_collapse)
    11.1 --- a/src/HOL/Library/Function_Division.thy	Thu Jun 11 21:41:55 2015 +0100
    11.2 +++ b/src/HOL/Library/Function_Division.thy	Fri Jun 12 08:53:23 2015 +0200
    11.3 @@ -15,7 +15,7 @@
    11.4  
    11.5  definition "inverse f = inverse \<circ> f"
    11.6  
    11.7 -definition "divide f g = (\<lambda>x. f x / g x)"
    11.8 +definition "f div g = (\<lambda>x. f x / g x)"
    11.9  
   11.10  instance ..
   11.11  
    12.1 --- a/src/HOL/Library/Polynomial.thy	Thu Jun 11 21:41:55 2015 +0100
    12.2 +++ b/src/HOL/Library/Polynomial.thy	Fri Jun 12 08:53:23 2015 +0200
    12.3 @@ -1361,13 +1361,13 @@
    12.4  begin
    12.5  
    12.6  definition divide_poly where
    12.7 -  div_poly_def: "divide x y = (THE q. \<exists>r. pdivmod_rel x y q r)"
    12.8 +  div_poly_def: "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)"
    12.9  
   12.10  definition mod_poly where
   12.11    "x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)"
   12.12  
   12.13  lemma div_poly_eq:
   12.14 -  "pdivmod_rel x y q r \<Longrightarrow> divide x y = q"
   12.15 +  "pdivmod_rel x y q r \<Longrightarrow> x div y = q"
   12.16  unfolding div_poly_def
   12.17  by (fast elim: pdivmod_rel_unique_div)
   12.18  
   12.19 @@ -1377,7 +1377,7 @@
   12.20  by (fast elim: pdivmod_rel_unique_mod)
   12.21  
   12.22  lemma pdivmod_rel:
   12.23 -  "pdivmod_rel x y (divide x y) (x mod y)"
   12.24 +  "pdivmod_rel x y (x div y) (x mod y)"
   12.25  proof -
   12.26    from pdivmod_rel_exists
   12.27      obtain q r where "pdivmod_rel x y q r" by fast
   12.28 @@ -1387,41 +1387,41 @@
   12.29  
   12.30  instance proof
   12.31    fix x y :: "'a poly"
   12.32 -  show "divide x y * y + x mod y = x"
   12.33 +  show "x div y * y + x mod y = x"
   12.34      using pdivmod_rel [of x y]
   12.35      by (simp add: pdivmod_rel_def)
   12.36  next
   12.37    fix x :: "'a poly"
   12.38    have "pdivmod_rel x 0 0 x"
   12.39      by (rule pdivmod_rel_by_0)
   12.40 -  thus "divide x 0 = 0"
   12.41 +  thus "x div 0 = 0"
   12.42      by (rule div_poly_eq)
   12.43  next
   12.44    fix y :: "'a poly"
   12.45    have "pdivmod_rel 0 y 0 0"
   12.46      by (rule pdivmod_rel_0)
   12.47 -  thus "divide 0 y = 0"
   12.48 +  thus "0 div y = 0"
   12.49      by (rule div_poly_eq)
   12.50  next
   12.51    fix x y z :: "'a poly"
   12.52    assume "y \<noteq> 0"
   12.53 -  hence "pdivmod_rel (x + z * y) y (z + divide x y) (x mod y)"
   12.54 +  hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
   12.55      using pdivmod_rel [of x y]
   12.56      by (simp add: pdivmod_rel_def distrib_right)
   12.57 -  thus "divide (x + z * y) y = z + divide x y"
   12.58 +  thus "(x + z * y) div y = z + x div y"
   12.59      by (rule div_poly_eq)
   12.60  next
   12.61    fix x y z :: "'a poly"
   12.62    assume "x \<noteq> 0"
   12.63 -  show "divide (x * y) (x * z) = divide y z"
   12.64 +  show "(x * y) div (x * z) = y div z"
   12.65    proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
   12.66      have "\<And>x::'a poly. pdivmod_rel x 0 0 x"
   12.67        by (rule pdivmod_rel_by_0)
   12.68 -    then have [simp]: "\<And>x::'a poly. divide x 0 = 0"
   12.69 +    then have [simp]: "\<And>x::'a poly. x div 0 = 0"
   12.70        by (rule div_poly_eq)
   12.71      have "\<And>x::'a poly. pdivmod_rel 0 x 0 0"
   12.72        by (rule pdivmod_rel_0)
   12.73 -    then have [simp]: "\<And>x::'a poly. divide 0 x = 0"
   12.74 +    then have [simp]: "\<And>x::'a poly. 0 div x = 0"
   12.75        by (rule div_poly_eq)
   12.76      case False then show ?thesis by auto
   12.77    next
   12.78 @@ -1430,8 +1430,8 @@
   12.79      have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> pdivmod_rel (x * y) (x * z) q (x * r)"
   12.80        by (auto simp add: pdivmod_rel_def algebra_simps)
   12.81          (rule classical, simp add: degree_mult_eq)
   12.82 -    moreover from pdivmod_rel have "pdivmod_rel y z (divide y z) (y mod z)" .
   12.83 -    ultimately have "pdivmod_rel (x * y) (x * z) (divide y z) (x * (y mod z))" .
   12.84 +    moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" .
   12.85 +    ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" .
   12.86      then show ?thesis by (simp add: div_poly_eq)
   12.87    qed
   12.88  qed
    13.1 --- a/src/HOL/NSA/StarDef.thy	Thu Jun 11 21:41:55 2015 +0100
    13.2 +++ b/src/HOL/NSA/StarDef.thy	Fri Jun 12 08:53:23 2015 +0200
    13.3 @@ -577,7 +577,7 @@
    13.4  lemma Standard_mult: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x * y \<in> Standard"
    13.5  by (simp add: star_mult_def)
    13.6  
    13.7 -lemma Standard_divide: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> divide x y \<in> Standard"
    13.8 +lemma Standard_divide: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x / y \<in> Standard"
    13.9  by (simp add: star_divide_def)
   13.10  
   13.11  lemma Standard_inverse: "x \<in> Standard \<Longrightarrow> inverse x \<in> Standard"
   13.12 @@ -855,9 +855,9 @@
   13.13  instance star :: (semidom) semidom ..
   13.14  instance star :: (semidom_divide) semidom_divide
   13.15  proof
   13.16 -  show "\<And>b a :: 'a star. b \<noteq> 0 \<Longrightarrow> divide (a * b) b = a"
   13.17 +  show "\<And>b a :: 'a star. b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
   13.18      by transfer simp
   13.19 -  show "\<And>a :: 'a star. divide a 0 = 0"
   13.20 +  show "\<And>a :: 'a star. a div 0 = 0"
   13.21      by transfer simp
   13.22  qed
   13.23  instance star :: (semiring_div) semiring_div
    14.1 --- a/src/HOL/Rat.thy	Thu Jun 11 21:41:55 2015 +0100
    14.2 +++ b/src/HOL/Rat.thy	Fri Jun 12 08:53:23 2015 +0200
    14.3 @@ -162,9 +162,9 @@
    14.4    by transfer simp
    14.5  
    14.6  definition
    14.7 -  divide_rat_def: "divide q r = q * inverse (r::rat)"
    14.8 +  divide_rat_def: "q div r = q * inverse (r::rat)"
    14.9  
   14.10 -lemma divide_rat [simp]: "divide (Fract a b) (Fract c d) = Fract (a * d) (b * c)"
   14.11 +lemma divide_rat [simp]: "Fract a b div Fract c d = Fract (a * d) (b * c)"
   14.12    by (simp add: divide_rat_def)
   14.13  
   14.14  instance proof
   14.15 @@ -191,7 +191,7 @@
   14.16      by transfer simp
   14.17    { assume "q \<noteq> 0" thus "inverse q * q = 1"
   14.18      by transfer simp }
   14.19 -  show "divide q r = q * inverse r"
   14.20 +  show "q div r = q * inverse r"
   14.21      by (fact divide_rat_def)
   14.22    show "inverse 0 = (0::rat)"
   14.23      by transfer simp
    15.1 --- a/src/HOL/Real.thy	Thu Jun 11 21:41:55 2015 +0100
    15.2 +++ b/src/HOL/Real.thy	Fri Jun 12 08:53:23 2015 +0200
    15.3 @@ -438,7 +438,7 @@
    15.4    "x - y = (x::real) + - y"
    15.5  
    15.6  definition
    15.7 -  "divide x y = (x::real) * inverse y"
    15.8 +  "x div y = (x::real) * inverse y"
    15.9  
   15.10  lemma add_Real:
   15.11    assumes X: "cauchy X" and Y: "cauchy Y"
   15.12 @@ -501,7 +501,7 @@
   15.13      apply (rule_tac x=k in exI, clarify)
   15.14      apply (drule_tac x=n in spec, simp)
   15.15      done
   15.16 -  show "divide a b = a * inverse b"
   15.17 +  show "a div b = a * inverse b"
   15.18      by (rule divide_real_def)
   15.19    show "inverse (0::real) = 0"
   15.20      by transfer (simp add: realrel_def)
    16.1 --- a/src/HOL/Rings.thy	Thu Jun 11 21:41:55 2015 +0100
    16.2 +++ b/src/HOL/Rings.thy	Fri Jun 12 08:53:23 2015 +0200
    16.3 @@ -559,7 +559,7 @@
    16.4  *}
    16.5  
    16.6  class divide =
    16.7 -  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    16.8 +  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
    16.9  
   16.10  setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
   16.11  
   16.12 @@ -567,8 +567,8 @@
   16.13  begin
   16.14  
   16.15  lemma [field_simps]:
   16.16 -  shows distrib_left_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
   16.17 -    and distrib_right_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
   16.18 +  shows distrib_left_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
   16.19 +    and distrib_right_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
   16.20    by (rule distrib_left distrib_right)+
   16.21  
   16.22  end
   16.23 @@ -577,8 +577,8 @@
   16.24  begin
   16.25  
   16.26  lemma [field_simps]:
   16.27 -  shows left_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
   16.28 -    and right_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
   16.29 +  shows left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
   16.30 +    and right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
   16.31    by (rule left_diff_distrib right_diff_distrib)+
   16.32  
   16.33  end
   16.34 @@ -586,12 +586,12 @@
   16.35  setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
   16.36  
   16.37  class semidom_divide = semidom + divide +
   16.38 -  assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> divide (a * b) b = a"
   16.39 -  assumes divide_zero [simp]: "divide a 0 = 0"
   16.40 +  assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
   16.41 +  assumes divide_zero [simp]: "a div 0 = 0"
   16.42  begin
   16.43  
   16.44  lemma nonzero_mult_divide_cancel_left [simp]:
   16.45 -  "a \<noteq> 0 \<Longrightarrow> divide (a * b) a = b"
   16.46 +  "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
   16.47    using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)
   16.48  
   16.49  end
    17.1 --- a/src/HOL/Word/Word.thy	Thu Jun 11 21:41:55 2015 +0100
    17.2 +++ b/src/HOL/Word/Word.thy	Fri Jun 12 08:53:23 2015 +0200
    17.3 @@ -307,7 +307,7 @@
    17.4    by (metis bintr_ariths(4))
    17.5  
    17.6  definition
    17.7 -  word_div_def: "divide a b = word_of_int (uint a div uint b)"
    17.8 +  word_div_def: "a div b = word_of_int (uint a div uint b)"
    17.9  
   17.10  definition
   17.11    word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
    18.1 --- a/src/HOL/ex/Arith_Examples.thy	Thu Jun 11 21:41:55 2015 +0100
    18.2 +++ b/src/HOL/ex/Arith_Examples.thy	Fri Jun 12 08:53:23 2015 +0200
    18.3 @@ -31,7 +31,7 @@
    18.4  
    18.5  subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
    18.6             @{term minus}, @{term nat}, @{term Divides.mod},
    18.7 -           @{term Divides.div} *}
    18.8 +           @{term divide} *}
    18.9  
   18.10  lemma "(i::nat) <= max i j"
   18.11    by linarith
    19.1 --- a/src/HOL/ex/Dedekind_Real.thy	Thu Jun 11 21:41:55 2015 +0100
    19.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Fri Jun 12 08:53:23 2015 +0200
    19.3 @@ -102,7 +102,7 @@
    19.4    preal_inverse_def:
    19.5      "inverse R == Abs_preal (inverse_set (Rep_preal R))"
    19.6  
    19.7 -definition "divide R S = R * inverse (S\<Colon>preal)"
    19.8 +definition "R div S = R * inverse (S\<Colon>preal)"
    19.9  
   19.10  definition
   19.11    preal_one_def:
   19.12 @@ -1222,7 +1222,7 @@
   19.13    real_inverse_def: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
   19.14  
   19.15  definition
   19.16 -  real_divide_def: "divide R (S::real) = R * inverse S"
   19.17 +  real_divide_def: "R div (S::real) = R * inverse S"
   19.18  
   19.19  definition
   19.20    real_le_def: "z \<le> (w::real) \<longleftrightarrow>