src/HOL/Decision_Procs/approximation_generator.ML
changeset 61609 77b453bd616f
parent 59850 f339ff48a6ee
child 63929 b673e7221b16
     1.1 --- a/src/HOL/Decision_Procs/approximation_generator.ML	Tue Nov 03 11:20:21 2015 +0100
     1.2 +++ b/src/HOL/Decision_Procs/approximation_generator.ML	Tue Nov 10 14:18:41 2015 +0000
     1.3 @@ -94,17 +94,17 @@
     1.4  
     1.5  val postproc_form_eqs =
     1.6    @{lemma
     1.7 -    "real (Float 0 a) = 0"
     1.8 -    "real (Float (numeral m) 0) = numeral m"
     1.9 -    "real (Float 1 0) = 1"
    1.10 -    "real (Float (- 1) 0) = - 1"
    1.11 -    "real (Float 1 (numeral e)) = 2 ^ numeral e"
    1.12 -    "real (Float 1 (- numeral e)) = 1 / 2 ^ numeral e"
    1.13 -    "real (Float a 1) = a * 2"
    1.14 -    "real (Float a (-1)) = a / 2"
    1.15 -    "real (Float (- a) b) = - real (Float a b)"
    1.16 -    "real (Float (numeral m) (numeral e)) = numeral m * 2 ^ (numeral e)"
    1.17 -    "real (Float (numeral m) (- numeral e)) = numeral m / 2 ^ (numeral e)"
    1.18 +    "real_of_float (Float 0 a) = 0"
    1.19 +    "real_of_float (Float (numeral m) 0) = numeral m"
    1.20 +    "real_of_float (Float 1 0) = 1"
    1.21 +    "real_of_float (Float (- 1) 0) = - 1"
    1.22 +    "real_of_float (Float 1 (numeral e)) = 2 ^ numeral e"
    1.23 +    "real_of_float (Float 1 (- numeral e)) = 1 / 2 ^ numeral e"
    1.24 +    "real_of_float (Float a 1) = a * 2"
    1.25 +    "real_of_float (Float a (-1)) = a / 2"
    1.26 +    "real_of_float (Float (- a) b) = - real_of_float (Float a b)"
    1.27 +    "real_of_float (Float (numeral m) (numeral e)) = numeral m * 2 ^ (numeral e)"
    1.28 +    "real_of_float (Float (numeral m) (- numeral e)) = numeral m / 2 ^ (numeral e)"
    1.29      "- (c * d::real) = -c * d"
    1.30      "- (c / d::real) = -c / d"
    1.31      "- (0::real) = 0"
    1.32 @@ -137,7 +137,7 @@
    1.33          val ts' = map
    1.34            (AList.lookup op = (map dest_Free xs ~~ ts)
    1.35              #> the_default Term.dummy
    1.36 -            #> curry op $ @{term "real::float\<Rightarrow>_"}
    1.37 +            #> curry op $ @{term "real_of_float::float\<Rightarrow>_"}
    1.38              #> conv_term ctxt (rewrite_with ctxt postproc_form_eqs))
    1.39            frees
    1.40        in