--- 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:
--- 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"} \\
--- 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
--- 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
--- 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)"
--- 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
--- 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"
--- 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
--- 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 ..
--- 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)
--- 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 ..
--- 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
--- 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
--- 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
--- 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)
--- 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
--- 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)"
--- 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
--- 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>