author  paulson 
Mon, 02 Nov 1998 12:36:16 +0100  
changeset 5787  4e5c74b7cd9e 
parent 5588  a3ab526bb891 
child 7077  60b098bb8b8a 
permissions  rwrr 
5588  1 
(* Title : Real/RealDef.thy 
2 
Author : Jacques D. Fleuriot 

3 
Copyright : 1998 University of Cambridge 

4 
Description : The reals 

5 
*) 

6 

7 
RealDef = PReal + 

8 

9 
constdefs 

10 
realrel :: "((preal * preal) * (preal * preal)) set" 

11 
"realrel == {p. ? x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}" 

12 

13 
typedef real = "{x::(preal*preal).True}/realrel" (Equiv.quotient_def) 

14 

15 

16 
instance 

17 
real :: {ord, plus, times, minus} 

18 

19 
consts 

20 

21 
"0r" :: real ("0r") 

22 
"1r" :: real ("1r") 

23 

24 
defs 

25 

26 
real_zero_def "0r == Abs_real(realrel^^{(@#($#1p),@#($#1p))})" 

27 
real_one_def "1r == Abs_real(realrel^^{(@#($#1p) + @#($#1p),@#($#1p))})" 

28 

29 
real_minus_def 

30 
" R == Abs_real(UN p:Rep_real(R). split (%x y. realrel^^{(y,x)}) p)" 

31 

32 
real_diff_def "x  y == x + (y::real)" 

33 

34 
constdefs 

35 

5787
4e5c74b7cd9e
increased precedence of unary minus from 80 to 100
paulson
parents:
5588
diff
changeset

36 
real_preal :: preal => real ("%#_" [100] 100) 
5588  37 
"%# m == Abs_real(realrel^^{(m+@#($#1p),@#($#1p))})" 
38 

39 
rinv :: real => real 

40 
"rinv(R) == (@S. R ~= 0r & S*R = 1r)" 

41 

5787
4e5c74b7cd9e
increased precedence of unary minus from 80 to 100
paulson
parents:
5588
diff
changeset

42 
real_nat :: nat => real ("%%# _" [100] 100) 
5588  43 
"%%# n == %#(@#($#(*# n)))" 
44 

45 
defs 

46 

47 
real_add_def 

48 
"P + Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q). 

49 
split(%x1 y1. split(%x2 y2. realrel^^{(x1+x2, y1+y2)}) p2) p1)" 

50 

51 
real_mult_def 

52 
"P * Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q). 

53 
split(%x1 y1. split(%x2 y2. realrel^^{(x1*x2+y1*y2,x1*y2+x2*y1)}) p2) p1)" 

54 

55 
real_less_def 

56 
"P < Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & 

57 
(x1,y1):Rep_real(P) & 

58 
(x2,y2):Rep_real(Q)" 

59 
real_le_def 

60 
"P <= (Q::real) == ~(Q < P)" 

61 

62 
end 