src/HOL/Decision_Procs/approximation.ML
changeset 71037 f630f2e707a6
parent 71034 e0755162093f
child 73019 05e2cab9af8b
--- a/src/HOL/Decision_Procs/approximation.ML	Sun Nov 03 19:58:02 2019 -0500
+++ b/src/HOL/Decision_Procs/approximation.ML	Sun Nov 03 19:59:56 2019 -0500
@@ -10,7 +10,7 @@
   val approximation_tac : int -> (string * int) list -> int option -> Proof.context -> int -> tactic
 end
 
-structure Approximation: APPROXIMATION =
+structure Approximation =
 struct
 
 fun reorder_bounds_tac ctxt prems i =
@@ -45,9 +45,9 @@
 fun approximate ctxt t = case fastype_of t
    of \<^typ>\<open>bool\<close> =>
         Approximation_Computation.approx_bool ctxt t
-    | \<^typ>\<open>(float \<times> float) option\<close> =>
+    | \<^typ>\<open>(float interval) option\<close> =>
         Approximation_Computation.approx_arith ctxt t
-    | \<^typ>\<open>(float \<times> float) option list\<close> =>
+    | \<^typ>\<open>(float interval) option list\<close> =>
         Approximation_Computation.approx_form_eval ctxt t
     | _ => error ("Bad term: " ^ Syntax.string_of_term ctxt t);
 
@@ -121,14 +121,16 @@
   | dest_float t = raise TERM ("dest_float", [t])
 
 
-fun dest_ivl (Const (\<^const_name>\<open>Some\<close>, _) $
-              (Const (\<^const_name>\<open>Pair\<close>, _) $ u $ l)) = SOME (dest_float u, dest_float l)
+fun dest_ivl
+  (Const (\<^const_name>\<open>Some\<close>, _) $
+    (Const (\<^const_name>\<open>Interval\<close>, _) $ ((Const (\<^const_name>\<open>Pair\<close>, _) $ u $ l)))) =
+      SOME (dest_float u, dest_float l)
   | dest_ivl (Const (\<^const_name>\<open>None\<close>, _)) = NONE
   | dest_ivl t = raise TERM ("dest_result", [t])
 
 fun mk_approx' prec t = (\<^const>\<open>approx'\<close>
                        $ HOLogic.mk_number \<^typ>\<open>nat\<close> prec
-                       $ t $ \<^term>\<open>[] :: (float * float) option list\<close>)
+                       $ t $ \<^term>\<open>[] :: (float interval) option list\<close>)
 
 fun mk_approx_form_eval prec t xs = (\<^const>\<open>approx_form_eval\<close>
                        $ HOLogic.mk_number \<^typ>\<open>nat\<close> prec
@@ -237,8 +239,8 @@
          |> HOLogic.dest_Trueprop
          |> dest_interpret_form
          |> (fn (data, xs) =>
-            mk_approx_form_eval prec data (HOLogic.mk_list \<^typ>\<open>(float * float) option\<close>
-              (map (fn _ => \<^term>\<open>None :: (float * float) option\<close>) (HOLogic.dest_list xs)))
+            mk_approx_form_eval prec data (HOLogic.mk_list \<^typ>\<open>(float interval) option\<close>
+              (map (fn _ => \<^term>\<open>None :: (float interval) option\<close>) (HOLogic.dest_list xs)))
          |> approximate ctxt
          |> HOLogic.dest_list
          |> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term)