author  wenzelm 
Fri, 05 Oct 2001 21:52:39 +0200  
changeset 11701  3d51fbf81c17 
parent 10919  144ede948e58 
child 11713  883d559b0b8c 
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" 

10919
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

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

10919
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

17 
typedef (REAL) 
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

18 
real = "UNIV//realrel" (Equiv.quotient_def) 
5588  19 

20 

21 
instance 

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

24 
consts 

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

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

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

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

28 
types such as hypreal and complex*) 
10919
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

29 
Nats, Reals :: "'a set" 
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10752
diff
changeset

30 

10919
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

31 
(*overloaded constant for injecting other types into "real"*) 
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

32 
real :: 'a => real 
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

33 

5588  34 

35 
defs 

36 

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

37 
real_zero_def 
10919
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

38 
"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

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

40 
real_one_def 
10919
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

41 
"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

42 
preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})" 
5588  43 

44 
real_minus_def 

10919
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

45 
" R == Abs_REAL(UN (x,y):Rep_REAL(R). realrel``{(y,x)})" 
10606  46 

47 
real_diff_def 

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

5588  49 

10606  50 
real_inverse_def 
10648  51 
"inverse (R::real) == (SOME S. (R = 0 & S = 0)  S * R = 1r)" 
5588  52 

10606  53 
real_divide_def 
54 
"R / (S::real) == R * inverse S" 

55 

5588  56 
constdefs 
57 

10919
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

58 
(** these don't use the overloaded real because users don't see them **) 
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

59 

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

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

61 
"real_of_preal m == 
10919
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

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

63 
preal_of_prat(prat_of_pnat 1p))})" 
5588  64 

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

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

66 
"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

67 

5588  68 

69 
defs 

70 

10919
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

71 
(*overloaded*) 
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10919
diff
changeset

72 
real_of_nat_def "real n == real_of_posnat n + ( 1r)" 
10919
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

73 

5588  74 
real_add_def 
10919
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

75 
"P+Q == Abs_REAL(UN p1:Rep_REAL(P). UN p2:Rep_REAL(Q). 
10834  76 
(%(x1,y1). (%(x2,y2). realrel``{(x1+x2, y1+y2)}) p2) p1)" 
5588  77 

78 
real_mult_def 

10919
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

79 
"P*Q == Abs_REAL(UN p1:Rep_REAL(P). UN p2:Rep_REAL(Q). 
10834  80 
(%(x1,y1). (%(x2,y2). realrel``{(x1*x2+y1*y2,x1*y2+x2*y1)}) 
10752
c4f1bf2acf4c
tidying, and separation of HOLHyperreal from HOLReal
paulson
parents:
10648
diff
changeset

81 
p2) p1)" 
5588  82 

83 
real_less_def 

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

84 
"P<Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & 
10919
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

85 
(x1,y1):Rep_REAL(P) & (x2,y2):Rep_REAL(Q)" 
5588  86 
real_le_def 
87 
"P <= (Q::real) == ~(Q < P)" 

88 

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

89 
syntax (symbols) 
10919
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

90 
Reals :: "'a set" ("\\<real>") 
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

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

92 

5588  93 
end 