3207 |
3207 |
3208 lemmas interpret_form_equations = interpret_form.simps interpret_floatarith.simps interpret_floatarith_num |
3208 lemmas interpret_form_equations = interpret_form.simps interpret_floatarith.simps interpret_floatarith_num |
3209 interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_powr interpret_floatarith_log |
3209 interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_powr interpret_floatarith_log |
3210 interpret_floatarith_sin |
3210 interpret_floatarith_sin |
3211 |
3211 |
3212 ML {* |
3212 code_reflect |
3213 structure Float_Arith = |
3213 datatypes float = Float |
3214 struct |
3214 and floatarith = Add | Minus | Mult | Inverse | Cos | Arctan |
3215 |
3215 | Abs | Max | Min | Pi | Sqrt | Exp | Ln | Power | Var | Num |
3216 @{code_datatype float = Float} |
3216 and form = Bound | Assign | Less | LessEqual | AtLeastAtMost |
3217 @{code_datatype floatarith = Add | Minus | Mult | Inverse | Cos | Arctan |
3217 functions approx_form approx_tse_form approx' approx_form_eval |
3218 | Abs | Max | Min | Pi | Sqrt | Exp | Ln | Power | Var | Num } |
3218 module_name Float_Arith |
3219 @{code_datatype form = Bound | Assign | Less | LessEqual | AtLeastAtMost} |
|
3220 |
|
3221 val approx_form = @{code approx_form} |
|
3222 val approx_tse_form = @{code approx_tse_form} |
|
3223 val approx' = @{code approx'} |
|
3224 val approx_form_eval = @{code approx_form_eval} |
|
3225 |
|
3226 end |
|
3227 *} |
|
3228 |
|
3229 code_reserved Eval Float_Arith |
|
3230 |
|
3231 code_type float (Eval "Float'_Arith.float") |
|
3232 code_const Float (Eval "Float'_Arith.Float/ (_,/ _)") |
|
3233 |
|
3234 code_type floatarith (Eval "Float'_Arith.floatarith") |
|
3235 code_const Add and Minus and Mult and Inverse and Cos and Arctan and Abs and Max and Min and |
|
3236 Pi and Sqrt and Exp and Ln and Power and Var and Num |
|
3237 (Eval "Float'_Arith.Add/ (_,/ _)" and "Float'_Arith.Minus" and "Float'_Arith.Mult/ (_,/ _)" and |
|
3238 "Float'_Arith.Inverse" and "Float'_Arith.Cos" and |
|
3239 "Float'_Arith.Arctan" and "Float'_Arith.Abs" and "Float'_Arith.Max/ (_,/ _)" and |
|
3240 "Float'_Arith.Min/ (_,/ _)" and "Float'_Arith.Pi" and "Float'_Arith.Sqrt" and |
|
3241 "Float'_Arith.Exp" and "Float'_Arith.Ln" and "Float'_Arith.Power/ (_,/ _)" and |
|
3242 "Float'_Arith.Var" and "Float'_Arith.Num") |
|
3243 |
|
3244 code_type form (Eval "Float'_Arith.form") |
|
3245 code_const Bound and Assign and Less and LessEqual and AtLeastAtMost |
|
3246 (Eval "Float'_Arith.Bound/ (_,/ _,/ _,/ _)" and "Float'_Arith.Assign/ (_,/ _,/ _)" and |
|
3247 "Float'_Arith.Less/ (_,/ _)" and "Float'_Arith.LessEqual/ (_,/ _)" and |
|
3248 "Float'_Arith.AtLeastAtMost/ (_,/ _,/ _)") |
|
3249 |
|
3250 code_const approx_form (Eval "Float'_Arith.approx'_form") |
|
3251 code_const approx_tse_form (Eval "Float'_Arith.approx'_tse'_form") |
|
3252 code_const approx' (Eval "Float'_Arith.approx'") |
|
3253 |
3219 |
3254 ML {* |
3220 ML {* |
3255 fun reorder_bounds_tac prems i = |
3221 fun reorder_bounds_tac prems i = |
3256 let |
3222 let |
3257 fun variable_of_bound (Const ("Trueprop", _) $ |
3223 fun variable_of_bound (Const ("Trueprop", _) $ |