src/HOL/Decision_Procs/approximation.ML

 structure Approximation =
 struct
 
 fun reorder_bounds_tac ctxt prems i =
   let
-    fun variable_of_bound (Const (\<^const_name>\<open>Trueprop\<close>, _) $
-                           (Const (\<^const_name>\<open>Set.member\<close>, _) $
-                            Free (name, _) $ _)) = name
-      | variable_of_bound (Const (\<^const_name>\<open>Trueprop\<close>, _) $
-                           (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
-                            Free (name, _) $ _)) = name
+    fun variable_of_bound \<^Const_>\<open>Trueprop for \<^Const_>\<open>Set.member _ for \<open>Free (name, _)\<close> _\<close>\<close> = name
+      | variable_of_bound \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for \<open>Free (name, _)\<close> _\<close>\<close> = name
       | variable_of_bound t = raise TERM ("variable_of_bound", [t])
 
     val variable_bounds
       = map (`(variable_of_bound o Thm.prop_of)) prems
 

   in
     fold prepend_prem order all_tac
   end
 
 fun approximate ctxt t = case fastype_of t
-   of \<^typ>\<open>bool\<close> =>
+   of \<^Type>\<open>bool\<close> =>
         Approximation_Computation.approx_bool ctxt t
-    | \<^typ>\<open>(float interval) option\<close> =>
+    | \<^typ>\<open>float interval option\<close> =>
         Approximation_Computation.approx_arith ctxt t
-    | \<^typ>\<open>(float interval) 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);
 
 fun rewrite_interpret_form_tac ctxt prec splitting taylor i st = let
     fun lookup_splitting (Free (name, _)) =
         (case AList.lookup (op =) splitting name
-          of SOME s => HOLogic.mk_number \<^typ>\<open>nat\<close> s
+          of SOME s => HOLogic.mk_number \<^Type>\<open>nat\<close> s
            | NONE => \<^term>\<open>0 :: nat\<close>)
       | lookup_splitting t = raise TERM ("lookup_splitting", [t])
     val vs = nth (Thm.prems_of st) (i - 1)
              |> Logic.strip_imp_concl
              |> HOLogic.dest_Trueprop
              |> Term.strip_comb |> snd |> List.last
              |> HOLogic.dest_list
     val p = prec
-            |> HOLogic.mk_number \<^typ>\<open>nat\<close>
+            |> HOLogic.mk_number \<^Type>\<open>nat\<close>
             |> Thm.cterm_of ctxt
   in case taylor
   of NONE => let
        val n = vs |> length
-               |> HOLogic.mk_number \<^typ>\<open>nat\<close>
+               |> HOLogic.mk_number \<^Type>\<open>nat\<close>
                |> Thm.cterm_of ctxt
        val s = vs
                |> map lookup_splitting
-               |> HOLogic.mk_list \<^typ>\<open>nat\<close>
+               |> HOLogic.mk_list \<^Type>\<open>nat\<close>
                |> Thm.cterm_of ctxt
      in
        (resolve_tac ctxt [Thm.instantiate (TVars.empty,
            Vars.make [(\<^var>\<open>?n::nat\<close>, n), (\<^var>\<open>?prec::nat\<close>, p), (\<^var>\<open>?ss::nat list\<close>, s)])
             @{thm approx_form}] i

    | SOME t =>
      if length vs <> 1
      then raise (TERM ("More than one variable used for taylor series expansion", [Thm.prop_of st]))
      else let
        val t = t
-            |> HOLogic.mk_number \<^typ>\<open>nat\<close>
+            |> HOLogic.mk_number \<^Type>\<open>nat\<close>
             |> Thm.cterm_of ctxt
        val s = vs |> map lookup_splitting |> hd
             |> Thm.cterm_of ctxt
      in
        resolve_tac ctxt [Thm.instantiate (TVars.empty,
             Vars.make [(\<^var>\<open>?s::nat\<close>, s), (\<^var>\<open>?t::nat\<close>, t), (\<^var>\<open>?prec::nat\<close>, p)])
             @{thm approx_tse_form}] i st
      end
   end
 
-fun calculated_subterms (\<^const>\<open>Trueprop\<close> $ t) = calculated_subterms t
-  | calculated_subterms (\<^const>\<open>HOL.implies\<close> $ _ $ t) = calculated_subterms t
-  | calculated_subterms (\<^term>\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) = [t1, t2]
-  | calculated_subterms (\<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) = [t1, t2]
-  | calculated_subterms (\<^term>\<open>(\<in>) :: real \<Rightarrow> real set \<Rightarrow> bool\<close> $ t1 $
-                         (\<^term>\<open>atLeastAtMost :: real \<Rightarrow> real \<Rightarrow> real set\<close> $ t2 $ t3)) = [t1, t2, t3]
+fun calculated_subterms \<^Const_>\<open>Trueprop for t\<close> = calculated_subterms t
+  | calculated_subterms \<^Const_>\<open>implies for _ t\<close> = calculated_subterms t
+  | calculated_subterms \<^Const_>\<open>less_eq \<^Type>\<open>real\<close> for t1 t2\<close> = [t1, t2]
+  | calculated_subterms \<^Const_>\<open>less \<^Type>\<open>real\<close> for t1 t2\<close> = [t1, t2]
+  | calculated_subterms \<^Const_>\<open>Set.member \<^Type>\<open>real\<close> for
+      t1 \<^Const_>\<open>atLeastAtMost \<^Type>\<open>real\<close> for t2 t3\<close>\<close> = [t1, t2, t3]
   | calculated_subterms t = raise TERM ("calculated_subterms", [t])
 
-fun dest_interpret_form (\<^const>\<open>interpret_form\<close> $ b $ xs) = (b, xs)
+fun dest_interpret_form \<^Const_>\<open>interpret_form for b xs\<close> = (b, xs)
   | dest_interpret_form t = raise TERM ("dest_interpret_form", [t])
 
-fun dest_interpret (\<^const>\<open>interpret_floatarith\<close> $ b $ xs) = (b, xs)
+fun dest_interpret \<^Const_>\<open>interpret_floatarith for b xs\<close> = (b, xs)
   | dest_interpret t = raise TERM ("dest_interpret", [t])
 
-fun dest_interpret_env (\<^const>\<open>interpret_form\<close> $ _ $ xs) = xs
-  | dest_interpret_env (\<^const>\<open>interpret_floatarith\<close> $ _ $ xs) = xs
+fun dest_interpret_env \<^Const_>\<open>interpret_form for _ xs\<close> = xs
+  | dest_interpret_env \<^Const_>\<open>interpret_floatarith for _ xs\<close> = xs
   | dest_interpret_env t = raise TERM ("dest_interpret_env", [t])
 
-fun dest_float (\<^const>\<open>Float\<close> $ m $ e) = (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
+fun dest_float \<^Const_>\<open>Float for m e\<close> = (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
   | dest_float t = raise TERM ("dest_float", [t])
 
 
-fun dest_ivl
-  (Const (\<^const_name>\<open>Some\<close>, _) $
-    (Const (\<^const_name>\<open>Interval\<close>, _) $ ((Const (\<^const_name>\<open>Pair\<close>, _) $ u $ l)))) =
+fun dest_ivl \<^Const_>\<open>Some _ for \<^Const_>\<open>Interval _ for \<^Const_>\<open>Pair _ _ for u l\<close>\<close>\<close> =
       SOME (dest_float u, dest_float l)
-  | dest_ivl (Const (\<^const_name>\<open>None\<close>, _)) = NONE
+  | dest_ivl \<^Const_>\<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 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
-                       $ t $ xs)
+fun mk_approx' prec t =
+  \<^Const>\<open>approx' for \<open>HOLogic.mk_number \<^Type>\<open>nat\<close> prec\<close> t \<^Const>\<open>Nil \<^typ>\<open>float interval option\<close>\<close>\<close>
+
+fun mk_approx_form_eval prec t xs =
+  \<^Const>\<open>approx_form_eval for \<open>HOLogic.mk_number \<^Type>\<open>nat\<close> prec\<close> t xs\<close>
 
 fun float2_float10 prec round_down (m, e) = (
   let
     val (m, e) = (if e < 0 then (m,e) else (m * Integer.pow e 2, 0))
 

   end)
 
 fun mk_result prec (SOME (l, u)) =
   (let
     fun mk_float10 rnd x = (let val (m, e) = float2_float10 prec rnd x
-                       in if e = 0 then HOLogic.mk_number \<^typ>\<open>real\<close> m
-                     else if e = 1 then \<^term>\<open>divide :: real \<Rightarrow> real \<Rightarrow> real\<close> $
-                                        HOLogic.mk_number \<^typ>\<open>real\<close> m $
+                       in if e = 0 then HOLogic.mk_number \<^Type>\<open>real\<close> m
+                     else if e = 1 then \<^Const>\<open>divide \<^Type>\<open>real\<close>\<close> $
+                                        HOLogic.mk_number \<^Type>\<open>real\<close> m $
                                         \<^term>\<open>10\<close>
-                                   else \<^term>\<open>divide :: real \<Rightarrow> real \<Rightarrow> real\<close> $
-                                        HOLogic.mk_number \<^typ>\<open>real\<close> m $
+                                   else \<^Const>\<open>divide \<^Type>\<open>real\<close>\<close> $
+                                        HOLogic.mk_number \<^Type>\<open>real\<close> m $
                                         (\<^term>\<open>power 10 :: nat \<Rightarrow> real\<close> $
-                                         HOLogic.mk_number \<^typ>\<open>nat\<close> (~e)) end)
-    in \<^term>\<open>atLeastAtMost :: real \<Rightarrow> real \<Rightarrow> real set\<close> $ mk_float10 true l $ mk_float10 false u end)
+                                         HOLogic.mk_number \<^Type>\<open>nat\<close> (~e)) end)
+    in \<^Const>\<open>atLeastAtMost \<^Type>\<open>real\<close> for \<open>mk_float10 true l\<close> \<open>mk_float10 false u\<close>\<close> end)
   | mk_result _ NONE = \<^term>\<open>UNIV :: real set\<close>
 
 fun realify t =
   let
     val t = Logic.varify_global t
-    val m = map (fn (name, _) => (name, \<^typ>\<open>real\<close>)) (Term.add_tvars t [])
+    val m = map (fn (name, _) => (name, \<^Type>\<open>real\<close>)) (Term.add_tvars t [])
     val t = Term.subst_TVars m t
   in t end
 
 fun apply_tactic ctxt term tactic =
   Thm.cterm_of ctxt term

      |> prepare_form ctxt
      |> (fn arith_term => apply_reify_form ctxt arith_term
          |> HOLogic.dest_Trueprop
          |> dest_interpret_form
          |> (fn (data, 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)))
+            mk_approx_form_eval prec data (HOLogic.mk_list \<^typ>\<open>float interval option\<close>
+              (map (fn _ => \<^Const>\<open>None \<^typ>\<open>float interval option\<close>\<close>) (HOLogic.dest_list xs)))
          |> approximate ctxt
          |> HOLogic.dest_list
          |> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term)
-         |> map (fn (elem, s) => \<^term>\<open>(\<in>) :: real \<Rightarrow> real set \<Rightarrow> bool\<close> $ elem $ mk_result prec (dest_ivl s))
+         |> map (fn (elem, s) => \<^Const>\<open>Set.member \<^Type>\<open>real\<close> for elem \<open>mk_result prec (dest_ivl s)\<close>\<close>)
          |> foldr1 HOLogic.mk_conj))
 
 fun approx_arith prec ctxt t = realify t
      |> Thm.cterm_of ctxt
      |> (preproc_form_conv ctxt then_conv reify_form_conv ctxt)

      |> approximate ctxt
      |> dest_ivl
      |> mk_result prec
 
 fun approx prec ctxt t =
-  if type_of t = \<^typ>\<open>prop\<close> then approx_form prec ctxt t
-  else if type_of t = \<^typ>\<open>bool\<close> then approx_form prec ctxt (\<^const>\<open>Trueprop\<close> $ t)
+  if type_of t = \<^Type>\<open>prop\<close> then approx_form prec ctxt t
+  else if type_of t = \<^Type>\<open>bool\<close> then approx_form prec ctxt \<^Const>\<open>Trueprop for t\<close>
   else approx_arith prec ctxt t
 
 fun approximate_cmd modes raw_t state =
   let
     val ctxt = Toplevel.context_of state;