1031 "(float interval) option list" |
1031 "(float interval) option list" |
1032 floatarith |
1032 floatarith |
1033 form |
1033 form |
1034 } ctxt ct |
1034 } ctxt ct |
1035 |
1035 |
1036 fun term_of_bool true = \<^term>\<open>True\<close> |
1036 fun term_of_bool true = \<^Const>\<open>True\<close> |
1037 | term_of_bool false = \<^term>\<open>False\<close>; |
1037 | term_of_bool false = \<^Const>\<open>False\<close>; |
1038 |
1038 |
1039 val mk_int = HOLogic.mk_number \<^typ>\<open>int\<close> o @{code integer_of_int}; |
1039 val mk_int = HOLogic.mk_number \<^Type>\<open>int\<close> o @{code integer_of_int}; |
1040 |
1040 |
1041 fun term_of_float (@{code Float} (k, l)) = |
1041 fun term_of_float (@{code Float} (k, l)) = |
1042 \<^term>\<open>Float\<close> $ mk_int k $ mk_int l; |
1042 \<^Const>\<open>Float for \<open>mk_int k\<close> \<open>mk_int l\<close>\<close>; |
1043 |
1043 |
1044 fun term_of_float_interval x = @{term "Interval::_\<Rightarrow>float interval"} $ |
1044 fun term_of_float_interval x = @{term "Interval::_\<Rightarrow>float interval"} $ |
1045 HOLogic.mk_prod |
1045 HOLogic.mk_prod |
1046 (apply2 term_of_float (@{code lowerF} x, @{code upperF} x)) |
1046 (apply2 term_of_float (@{code lowerF} x, @{code upperF} x)) |
1047 |
1047 |
1048 fun term_of_float_interval_option NONE = \<^term>\<open>None :: (float interval) option\<close> |
1048 fun term_of_float_interval_option NONE = \<^Const>\<open>None \<^typ>\<open>float interval option\<close>\<close> |
1049 | term_of_float_interval_option (SOME ff) = \<^term>\<open>Some :: float interval \<Rightarrow> _\<close> |
1049 | term_of_float_interval_option (SOME ff) = |
1050 $ (term_of_float_interval ff); |
1050 \<^Const>\<open>Some \<^typ>\<open>float interval\<close> for \<open>term_of_float_interval ff\<close>\<close>; |
1051 |
1051 |
1052 val term_of_float_interval_option_list = |
1052 val term_of_float_interval_option_list = |
1053 HOLogic.mk_list \<^typ>\<open>(float interval) option\<close> o map term_of_float_interval_option; |
1053 HOLogic.mk_list \<^typ>\<open>float interval option\<close> o map term_of_float_interval_option; |
1054 |
1054 |
1055 val approx_bool = @{computation bool} |
1055 val approx_bool = @{computation bool} |
1056 (fn _ => fn x => case x of SOME b => term_of_bool b |
1056 (fn _ => fn x => case x of SOME b => term_of_bool b |
1057 | NONE => error "Computation approx_bool failed.") |
1057 | NONE => error "Computation approx_bool failed.") |
1058 val approx_arith = @{computation "float interval option"} |
1058 val approx_arith = @{computation "float interval option"} |