src/HOL/Real/Hyperreal/HyperDef.thy
changeset 10607 352f6f209775
parent 10568 a7701b1d6c6a
equal deleted inserted replaced
10606:e3229a37d53f 10607:352f6f209775
    23                    {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
    23                    {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
    24 
    24 
    25 typedef hypreal = "UNIV//hyprel"   (Equiv.quotient_def)
    25 typedef hypreal = "UNIV//hyprel"   (Equiv.quotient_def)
    26 
    26 
    27 instance
    27 instance
    28    hypreal  :: {ord, zero, plus, times, minus}
    28    hypreal  :: {ord, zero, plus, times, minus, inverse}
    29 
    29 
    30 consts 
    30 consts 
    31 
    31 
    32   "1hr"       :: hypreal               ("1hr")  
    32   "1hr"       :: hypreal               ("1hr")  
    33   "whr"       :: hypreal               ("whr")  
    33   "whr"       :: hypreal               ("whr")  
    34   "ehr"       :: hypreal               ("ehr")  
    34   "ehr"       :: hypreal               ("ehr")  
    35 
    35 
    36 
    36 
    37 defs
    37 defs
    38 
    38 
    39   hypreal_zero_def     "0 == Abs_hypreal(hyprel^^{%n::nat. (#0::real)})"
    39   hypreal_zero_def
    40   hypreal_one_def      "1hr == Abs_hypreal(hyprel^^{%n::nat. (#1::real)})"
    40   "0 == Abs_hypreal(hyprel^^{%n::nat. (#0::real)})"
       
    41 
       
    42   hypreal_one_def
       
    43   "1hr == Abs_hypreal(hyprel^^{%n::nat. (#1::real)})"
    41 
    44 
    42   (* an infinite number = [<1,2,3,...>] *)
    45   (* an infinite number = [<1,2,3,...>] *)
    43   omega_def   "whr == Abs_hypreal(hyprel^^{%n::nat. real_of_posnat n})"
    46   omega_def
       
    47   "whr == Abs_hypreal(hyprel^^{%n::nat. real_of_posnat n})"
    44     
    48     
    45   (* an infinitesimal number = [<1,1/2,1/3,...>] *)
    49   (* an infinitesimal number = [<1,1/2,1/3,...>] *)
    46   epsilon_def "ehr == Abs_hypreal(hyprel^^{%n::nat. rinv(real_of_posnat n)})"
    50   epsilon_def
       
    51   "ehr == Abs_hypreal(hyprel^^{%n::nat. inverse (real_of_posnat n)})"
    47 
    52 
    48   hypreal_minus_def
    53   hypreal_minus_def
    49   "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel^^{%n::nat. - (X n)})"
    54   "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel^^{%n::nat. - (X n)})"
    50 
    55 
    51   hypreal_diff_def 
    56   hypreal_diff_def 
    52   "x - y == x + -(y::hypreal)"
    57   "x - y == x + -(y::hypreal)"
    53 
    58 
       
    59   hypreal_inverse_def
       
    60   "inverse P == Abs_hypreal(UN X: Rep_hypreal(P). 
       
    61                     hyprel^^{%n. if X n = #0 then #0 else inverse (X n)})"
       
    62 
       
    63   hypreal_divide_def
       
    64   "P / Q::hypreal == P * inverse Q"
       
    65   
    54 constdefs
    66 constdefs
    55 
    67 
    56   hypreal_of_real  :: real => hypreal                 
    68   hypreal_of_real  :: real => hypreal                 
    57   "hypreal_of_real r         == Abs_hypreal(hyprel^^{%n::nat. r})"
    69   "hypreal_of_real r         == Abs_hypreal(hyprel^^{%n::nat. r})"
    58   
    70   
    59   hrinv       :: hypreal => hypreal
       
    60   "hrinv(P)   == Abs_hypreal(UN X: Rep_hypreal(P). 
       
    61                     hyprel^^{%n. if X n = #0 then #0 else rinv(X n)})"
       
    62 
       
    63   (* n::nat --> (n+1)::hypreal *)
    71   (* n::nat --> (n+1)::hypreal *)
    64   hypreal_of_posnat :: nat => hypreal                
    72   hypreal_of_posnat :: nat => hypreal                
    65   "hypreal_of_posnat n  == (hypreal_of_real(real_of_preal
    73   "hypreal_of_posnat n  == (hypreal_of_real(real_of_preal
    66                             (preal_of_prat(prat_of_pnat(pnat_of_nat n)))))"
    74                             (preal_of_prat(prat_of_pnat(pnat_of_nat n)))))"
    67 
    75