src/HOL/Decision_Procs/approximation_generator.ML
 changeset 64519 51be997d0698 parent 63931 f17a1c60ac39 child 69597 ff784d5a5bfb
equal inserted replaced
64518:b87697eec2ac 64519:51be997d0698
50   | mapprox_floatarith (@{term Min} \$ a \$ b) xs =
50   | mapprox_floatarith (@{term Min} \$ a \$ b) xs =
51       Real.min (mapprox_floatarith a xs, mapprox_floatarith b xs)
51       Real.min (mapprox_floatarith a xs, mapprox_floatarith b xs)
52   | mapprox_floatarith @{term Pi} _ = Math.pi
52   | mapprox_floatarith @{term Pi} _ = Math.pi
53   | mapprox_floatarith (@{term Sqrt} \$ a) xs = Math.sqrt (mapprox_floatarith a xs)
53   | mapprox_floatarith (@{term Sqrt} \$ a) xs = Math.sqrt (mapprox_floatarith a xs)
54   | mapprox_floatarith (@{term Exp} \$ a) xs = Math.exp (mapprox_floatarith a xs)
54   | mapprox_floatarith (@{term Exp} \$ a) xs = Math.exp (mapprox_floatarith a xs)

55   | mapprox_floatarith (@{term Powr} \$ a \$ b) xs =

56       Math.pow (mapprox_floatarith a xs, mapprox_floatarith b xs)
55   | mapprox_floatarith (@{term Ln} \$ a) xs = Math.ln (mapprox_floatarith a xs)
57   | mapprox_floatarith (@{term Ln} \$ a) xs = Math.ln (mapprox_floatarith a xs)
56   | mapprox_floatarith (@{term Power} \$ a \$ n) xs =
58   | mapprox_floatarith (@{term Power} \$ a \$ n) xs =
57       Math.pow (mapprox_floatarith a xs, Real.fromInt (nat_of_term n))
59       Math.pow (mapprox_floatarith a xs, Real.fromInt (nat_of_term n))
58   | mapprox_floatarith (@{term Floor} \$ a) xs = Real.fromInt (floor (mapprox_floatarith a xs))
60   | mapprox_floatarith (@{term Floor} \$ a) xs = Real.fromInt (floor (mapprox_floatarith a xs))
59   | mapprox_floatarith (@{term Var} \$ n) xs = nth xs (nat_of_term n)
61   | mapprox_floatarith (@{term Var} \$ n) xs = nth xs (nat_of_term n)