author  paulson 
Thu, 04 Jan 2001 10:23:01 +0100  
changeset 10778  2c6605049646 
parent 10752  c4f1bf2acf4c 
child 10797  028d22926a41 
permissions  rwrr 
5588  1 
(* Title : Real/RealDef.thy 
7219  2 
ID : $Id$ 
5588  3 
Author : Jacques D. Fleuriot 
4 
Copyright : 1998 University of Cambridge 

5 
Description : The reals 

6 
*) 

7 

8 
RealDef = PReal + 

9 

10752
c4f1bf2acf4c
tidying, and separation of HOLHyperreal from HOLReal
paulson
parents:
10648
diff
changeset

10 
instance preal :: order (preal_le_refl,preal_le_trans,preal_le_anti_sym, 
c4f1bf2acf4c
tidying, and separation of HOLHyperreal from HOLReal
paulson
parents:
10648
diff
changeset

11 
preal_less_le) 
c4f1bf2acf4c
tidying, and separation of HOLHyperreal from HOLReal
paulson
parents:
10648
diff
changeset

12 

5588  13 
constdefs 
14 
realrel :: "((preal * preal) * (preal * preal)) set" 

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

16 

9391  17 
typedef real = "UNIV//realrel" (Equiv.quotient_def) 
5588  18 

19 

20 
instance 

10606  21 
real :: {ord, zero, plus, times, minus, inverse} 
5588  22 

23 
consts 

10752
c4f1bf2acf4c
tidying, and separation of HOLHyperreal from HOLReal
paulson
parents:
10648
diff
changeset

24 
"1r" :: real ("1r") 
5588  25 

10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10752
diff
changeset

26 
(*Overloaded constants denoting the Nat and Real subsets of enclosing 
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10752
diff
changeset

27 
types such as hypreal and complex*) 
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10752
diff
changeset

28 
SNat, SReal :: "'a set" 
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10752
diff
changeset

29 

5588  30 

31 
defs 

32 

7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5787
diff
changeset

33 
real_zero_def 
10606  34 
"0 == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p), 
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5787
diff
changeset

35 
preal_of_prat(prat_of_pnat 1p))})" 
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5787
diff
changeset

36 
real_one_def 
10606  37 
"1r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p) + 
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5787
diff
changeset

38 
preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})" 
5588  39 

40 
real_minus_def 

10606  41 
" R == Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})" 
42 

43 
real_diff_def 

44 
"R  (S::real) == R +  S" 

5588  45 

10606  46 
real_inverse_def 
10648  47 
"inverse (R::real) == (SOME S. (R = 0 & S = 0)  S * R = 1r)" 
5588  48 

10606  49 
real_divide_def 
50 
"R / (S::real) == R * inverse S" 

51 

5588  52 
constdefs 
53 

7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5787
diff
changeset

54 
real_of_preal :: preal => real 
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5787
diff
changeset

55 
"real_of_preal m == 
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5787
diff
changeset

56 
Abs_real(realrel^^{(m+preal_of_prat(prat_of_pnat 1p), 
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5787
diff
changeset

57 
preal_of_prat(prat_of_pnat 1p))})" 
5588  58 

7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5787
diff
changeset

59 
real_of_posnat :: nat => real 
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5787
diff
changeset

60 
"real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))" 
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5787
diff
changeset

61 

60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5787
diff
changeset

62 
real_of_nat :: nat => real 
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset

63 
"real_of_nat n == real_of_posnat n + (1r)" 
5588  64 

65 
defs 

66 

67 
real_add_def 

10752
c4f1bf2acf4c
tidying, and separation of HOLHyperreal from HOLReal
paulson
parents:
10648
diff
changeset

68 
"P+Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q). 
c4f1bf2acf4c
tidying, and separation of HOLHyperreal from HOLReal
paulson
parents:
10648
diff
changeset

69 
(%(x1,y1). (%(x2,y2). realrel^^{(x1+x2, y1+y2)}) p2) p1)" 
5588  70 

71 
real_mult_def 

10752
c4f1bf2acf4c
tidying, and separation of HOLHyperreal from HOLReal
paulson
parents:
10648
diff
changeset

72 
"P*Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q). 
c4f1bf2acf4c
tidying, and separation of HOLHyperreal from HOLReal
paulson
parents:
10648
diff
changeset

73 
(%(x1,y1). (%(x2,y2). realrel^^{(x1*x2+y1*y2,x1*y2+x2*y1)}) 
c4f1bf2acf4c
tidying, and separation of HOLHyperreal from HOLReal
paulson
parents:
10648
diff
changeset

74 
p2) p1)" 
5588  75 

76 
real_less_def 

10752
c4f1bf2acf4c
tidying, and separation of HOLHyperreal from HOLReal
paulson
parents:
10648
diff
changeset

77 
"P<Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & 
c4f1bf2acf4c
tidying, and separation of HOLHyperreal from HOLReal
paulson
parents:
10648
diff
changeset

78 
(x1,y1):Rep_real(P) & (x2,y2):Rep_real(Q)" 
5588  79 
real_le_def 
80 
"P <= (Q::real) == ~(Q < P)" 

81 

10752
c4f1bf2acf4c
tidying, and separation of HOLHyperreal from HOLReal
paulson
parents:
10648
diff
changeset

82 
syntax (symbols) 
c4f1bf2acf4c
tidying, and separation of HOLHyperreal from HOLReal
paulson
parents:
10648
diff
changeset

83 
SReal :: "'a set" ("\\<real>") 
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10752
diff
changeset

84 
SNat :: "'a set" ("\\<nat>") 
10752
c4f1bf2acf4c
tidying, and separation of HOLHyperreal from HOLReal
paulson
parents:
10648
diff
changeset

85 

5588  86 
end 