src/HOL/Real/RealDef.thy
changeset 10606 e3229a37d53f
parent 9391 a6ab3a442da6
child 10648 a8c647cfa31f
--- a/src/HOL/Real/RealDef.thy	Wed Dec 06 12:28:52 2000 +0100
+++ b/src/HOL/Real/RealDef.thy	Wed Dec 06 12:34:12 2000 +0100
@@ -15,7 +15,7 @@
 
 
 instance
-   real  :: {ord, zero, plus, times, minus}
+   real  :: {ord, zero, plus, times, minus, inverse}
 
 consts 
 
@@ -24,17 +24,24 @@
 defs
 
   real_zero_def  
-     "0 == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p),
+  "0 == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p),
                                 preal_of_prat(prat_of_pnat 1p))})"
   real_one_def   
-     "1r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p) + 
+  "1r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p) + 
             preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})"
 
   real_minus_def
-    "- R ==  Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})"
+  "- R ==  Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})"
+
+  real_diff_def
+  "R - (S::real) == R + - S"
 
-  real_diff_def "x - y == x + (- y :: real)"
+  real_inverse_def
+  "inverse (R::real) == (@S. R ~= 0 & S*R = 1r)"
 
+  real_divide_def
+  "R / (S::real) == R * inverse S"
+  
 constdefs
 
   real_of_preal :: preal => real            
@@ -42,9 +49,6 @@
            Abs_real(realrel^^{(m+preal_of_prat(prat_of_pnat 1p),
                                preal_of_prat(prat_of_pnat 1p))})"
 
-  rinv       :: real => real
-  "rinv(R)   == (@S. R ~= 0 & S*R = 1r)"
-
   real_of_posnat :: nat => real             
   "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))"