src/HOL/Hyperreal/NSA.thy
changeset 20554 c433e78d4203
parent 20552 2c31dd358c21
child 20562 c2f672be8522
equal deleted inserted replaced
20553:7ced6152e52c 20554:c433e78d4203
    45 
    45 
    46 const_syntax (HTML output)
    46 const_syntax (HTML output)
    47   approx  (infixl "\<approx>" 50)
    47   approx  (infixl "\<approx>" 50)
    48 
    48 
    49 
    49 
    50 defs (overloaded)
    50 lemma hypreal_of_real_of_real_eq: "hypreal_of_real r = of_real r"
    51   SReal_def:      "Reals == {x. \<exists>r. x = hypreal_of_real r}"
    51 proof -
    52     --{*the standard real numbers as a subset of the hyperreals*}
    52   have "hypreal_of_real r = hypreal_of_real (of_real r)" by simp
    53 
    53   also have "\<dots> = of_real r" by (rule star_of_of_real)
       
    54   finally show ?thesis .
       
    55 qed
       
    56 
       
    57 lemma SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}"
       
    58 by (simp add: Reals_def image_def hypreal_of_real_of_real_eq)
    54 
    59 
    55 
    60 
    56 subsection{*Nonstandard extension of the norm function*}
    61 subsection{*Nonstandard extension of the norm function*}
    57 
    62 
    58 declare hnorm_def [transfer_unfold]
    63 declare hnorm_def [transfer_unfold]