src/HOL/Real/PRat.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/PRat.thy	Thu Jun 25 13:57:34 1998 +0200
@@ -0,0 +1,49 @@
+(*  Title       : PRat.thy
+    Author      : Jacques D. Fleuriot
+    Copyright   : 1998  University of Cambridge
+    Description : The positive rationals
+*) 
+
+PRat = PNat + Equiv +
+
+constdefs
+    ratrel   ::  "((pnat * pnat) * (pnat * pnat)) set"
+    "ratrel  ==  {p. ? x1 y1 x2 y2. p=((x1::pnat,y1),(x2,y2)) & x1*y2 = x2*y1}" 
+
+typedef prat = "{x::(pnat*pnat).True}/ratrel"          (Equiv.quotient_def)
+
+instance
+   prat  :: {ord,plus,times}
+
+
+constdefs
+
+  prat_pnat :: pnat => prat              ("$#_" [80] 80)
+  "$# m     == Abs_prat(ratrel^^{(m,Abs_pnat 1)})"
+
+  qinv      :: prat => prat
+  "qinv(Q)  == Abs_prat(UN p:Rep_prat(Q). split (%x y. ratrel^^{(y,x)}) p)" 
+
+defs
+
+  prat_add_def  
+  "P + Q == Abs_prat(UN p1:Rep_prat(P). UN p2:Rep_prat(Q).
+                split(%x1 y1. split(%x2 y2. ratrel^^{(x1*y2 + x2*y1, y1*y2)}) p2) p1)"
+
+  prat_mult_def  
+  "P * Q == Abs_prat(UN p1:Rep_prat(P). UN p2:Rep_prat(Q).
+                split(%x1 y1. split(%x2 y2. ratrel^^{(x1*x2, y1*y2)}) p2) p1)"
+ 
+  (*** Gleason p. 119 ***)
+  prat_less_def
+  "P < (Q::prat) == ? T. P + T = Q"
+
+  prat_le_def
+  "P <= (Q::prat) == ~(Q < P)" 
+
+end
+  
+
+
+
+