# HG changeset patch # User haftmann # Date 1737959988 -3600 # Node ID 6c052e21664f277ab43f2d5e48c0592f3ae2c88b # Parent e86a7b8d7adadb80509d15eb3a374fa64980dec2 more explicit real operations diff -r e86a7b8d7ada -r 6c052e21664f src/HOL/Decision_Procs/approximation_generator.ML --- a/src/HOL/Decision_Procs/approximation_generator.ML Sun Jan 26 13:27:41 2025 +0000 +++ b/src/HOL/Decision_Procs/approximation_generator.ML Mon Jan 27 07:39:48 2025 +0100 @@ -38,13 +38,13 @@ handle TERM _ => raise TERM ("mapprox_float", [t]); (* TODO: define using compiled terms? *) -fun mapprox_floatarith \<^Const_>\Add for a b\ xs = mapprox_floatarith a xs + mapprox_floatarith b xs - | mapprox_floatarith \<^Const_>\Minus for a\ xs = ~ (mapprox_floatarith a xs) - | mapprox_floatarith \<^Const_>\Mult for a b\ xs = mapprox_floatarith a xs * mapprox_floatarith b xs - | mapprox_floatarith \<^Const_>\Inverse for a\ xs = 1.0 / mapprox_floatarith a xs +fun mapprox_floatarith \<^Const_>\Add for a b\ xs = Real.+ (mapprox_floatarith a xs, mapprox_floatarith b xs) + | mapprox_floatarith \<^Const_>\Minus for a\ xs = Real.~ (mapprox_floatarith a xs) + | mapprox_floatarith \<^Const_>\Mult for a b\ xs = Real.* (mapprox_floatarith a xs, mapprox_floatarith b xs) + | mapprox_floatarith \<^Const_>\Inverse for a\ xs = 1.0 / (mapprox_floatarith a xs : real) | mapprox_floatarith \<^Const_>\Cos for a\ xs = Math.cos (mapprox_floatarith a xs) | mapprox_floatarith \<^Const_>\Arctan for a\ xs = Math.atan (mapprox_floatarith a xs) - | mapprox_floatarith \<^Const_>\Abs for a\ xs = abs (mapprox_floatarith a xs) + | mapprox_floatarith \<^Const_>\Abs for a\ xs = Real.abs (mapprox_floatarith a xs : real) | mapprox_floatarith \<^Const_>\Max for a b\ xs = Real.max (mapprox_floatarith a xs, mapprox_floatarith b xs) | mapprox_floatarith \<^Const_>\Min for a b\ xs = @@ -66,15 +66,15 @@ let val x' = mapprox_floatarith x xs in - mapprox_floatarith a xs + eps <= x' andalso x' + eps <= mapprox_floatarith b xs + Real.<= (Real.+ (mapprox_floatarith a xs, eps), x') andalso Real.<= (Real.+ (x', eps), mapprox_floatarith b xs) end fun mapprox_form eps \<^Const_>\Bound for x a b f\ xs = (not (mapprox_atLeastAtMost eps x a b xs)) orelse mapprox_form eps f xs | mapprox_form eps \<^Const_>\Assign for x a f\ xs = (Real.!= (mapprox_floatarith x xs, mapprox_floatarith a xs)) orelse mapprox_form eps f xs -| mapprox_form eps \<^Const_>\Less for a b\ xs = mapprox_floatarith a xs + eps < mapprox_floatarith b xs -| mapprox_form eps \<^Const_>\LessEqual for a b\ xs = mapprox_floatarith a xs + eps <= mapprox_floatarith b xs +| mapprox_form eps \<^Const_>\Less for a b\ xs = Real.< (Real.+ (mapprox_floatarith a xs, eps), mapprox_floatarith b xs) +| mapprox_form eps \<^Const_>\LessEqual for a b\ xs = Real.<= (Real.+ (mapprox_floatarith a xs, eps), mapprox_floatarith b xs) | mapprox_form eps \<^Const_>\AtLeastAtMost for x a b\ xs = mapprox_atLeastAtMost eps x a b xs | mapprox_form eps \<^Const_>\Conj for f g\ xs = mapprox_form eps f xs andalso mapprox_form eps g xs | mapprox_form eps \<^Const_>\Disj for f g\ xs = mapprox_form eps f xs orelse mapprox_form eps g xs