src/HOL/Decision_Procs/approximation_generator.ML

 
 fun int_of_term t = snd (HOLogic.dest_number t) handle TERM _ => raise TERM ("int_of_term", [t]);
 
 fun real_of_man_exp m e = Real.fromManExp {man = Real.fromInt m, exp = e}
 
-fun mapprox_float (\<^term>\<open>Float\<close> $ m $ e) = real_of_man_exp (int_of_term m) (int_of_term e)
+fun mapprox_float \<^Const_>\<open>Float for m e\<close> = real_of_man_exp (int_of_term m) (int_of_term e)
   | mapprox_float t = Real.fromInt (snd (HOLogic.dest_number t))
       handle TERM _ => raise TERM ("mapprox_float", [t]);
 
 (* TODO: define using compiled terms? *)
-fun mapprox_floatarith (\<^term>\<open>Add\<close> $ a $ b) xs = mapprox_floatarith a xs + mapprox_floatarith b xs
-  | mapprox_floatarith (\<^term>\<open>Minus\<close> $ a) xs = ~ (mapprox_floatarith a xs)
-  | mapprox_floatarith (\<^term>\<open>Mult\<close> $ a $ b) xs = mapprox_floatarith a xs * mapprox_floatarith b xs
-  | mapprox_floatarith (\<^term>\<open>Inverse\<close> $ a) xs = 1.0 / mapprox_floatarith a xs
-  | mapprox_floatarith (\<^term>\<open>Cos\<close> $ a) xs = Math.cos (mapprox_floatarith a xs)
-  | mapprox_floatarith (\<^term>\<open>Arctan\<close> $ a) xs = Math.atan (mapprox_floatarith a xs)
-  | mapprox_floatarith (\<^term>\<open>Abs\<close> $ a) xs = abs (mapprox_floatarith a xs)
-  | mapprox_floatarith (\<^term>\<open>Max\<close> $ a $ b) xs =
+fun mapprox_floatarith \<^Const_>\<open>Add for a b\<close> xs = mapprox_floatarith a xs + mapprox_floatarith b xs
+  | mapprox_floatarith \<^Const_>\<open>Minus for a\<close> xs = ~ (mapprox_floatarith a xs)
+  | mapprox_floatarith \<^Const_>\<open>Mult for a b\<close> xs = mapprox_floatarith a xs * mapprox_floatarith b xs
+  | mapprox_floatarith \<^Const_>\<open>Inverse for a\<close> xs = 1.0 / mapprox_floatarith a xs
+  | mapprox_floatarith \<^Const_>\<open>Cos for a\<close> xs = Math.cos (mapprox_floatarith a xs)
+  | mapprox_floatarith \<^Const_>\<open>Arctan for a\<close> xs = Math.atan (mapprox_floatarith a xs)
+  | mapprox_floatarith \<^Const_>\<open>Abs for a\<close> xs = abs (mapprox_floatarith a xs)
+  | mapprox_floatarith \<^Const_>\<open>Max for a b\<close> xs =
       Real.max (mapprox_floatarith a xs, mapprox_floatarith b xs)
-  | mapprox_floatarith (\<^term>\<open>Min\<close> $ a $ b) xs =
+  | mapprox_floatarith \<^Const_>\<open>Min for a b\<close> xs =
       Real.min (mapprox_floatarith a xs, mapprox_floatarith b xs)
-  | mapprox_floatarith \<^term>\<open>Pi\<close> _ = Math.pi
-  | mapprox_floatarith (\<^term>\<open>Sqrt\<close> $ a) xs = Math.sqrt (mapprox_floatarith a xs)
-  | mapprox_floatarith (\<^term>\<open>Exp\<close> $ a) xs = Math.exp (mapprox_floatarith a xs)
-  | mapprox_floatarith (\<^term>\<open>Powr\<close> $ a $ b) xs =
+  | mapprox_floatarith \<^Const_>\<open>Pi\<close> _ = Math.pi
+  | mapprox_floatarith \<^Const_>\<open>Sqrt for a\<close> xs = Math.sqrt (mapprox_floatarith a xs)
+  | mapprox_floatarith \<^Const_>\<open>Exp for a\<close> xs = Math.exp (mapprox_floatarith a xs)
+  | mapprox_floatarith \<^Const_>\<open>Powr for a b\<close> xs =
       Math.pow (mapprox_floatarith a xs, mapprox_floatarith b xs)
-  | mapprox_floatarith (\<^term>\<open>Ln\<close> $ a) xs = Math.ln (mapprox_floatarith a xs)
-  | mapprox_floatarith (\<^term>\<open>Power\<close> $ a $ n) xs =
+  | mapprox_floatarith \<^Const_>\<open>Ln for a\<close> xs = Math.ln (mapprox_floatarith a xs)
+  | mapprox_floatarith \<^Const_>\<open>Power for a n\<close> xs =
       Math.pow (mapprox_floatarith a xs, Real.fromInt (nat_of_term n))
-  | mapprox_floatarith (\<^term>\<open>Floor\<close> $ a) xs = Real.fromInt (floor (mapprox_floatarith a xs))
-  | mapprox_floatarith (\<^term>\<open>Var\<close> $ n) xs = nth xs (nat_of_term n)
-  | mapprox_floatarith (\<^term>\<open>Num\<close> $ m) _ = mapprox_float m
+  | mapprox_floatarith \<^Const_>\<open>Floor for a\<close> xs = Real.fromInt (floor (mapprox_floatarith a xs))
+  | mapprox_floatarith \<^Const_>\<open>Var for n\<close> xs = nth xs (nat_of_term n)
+  | mapprox_floatarith \<^Const_>\<open>Num for m\<close> _ = mapprox_float m
   | mapprox_floatarith t _ = raise TERM ("mapprox_floatarith", [t])
 
 fun mapprox_atLeastAtMost eps x a b xs =
     let
       val x' = mapprox_floatarith x xs
     in
       mapprox_floatarith a xs + eps <= x' andalso x' + eps <= mapprox_floatarith b xs
     end
 
-fun mapprox_form eps (\<^term>\<open>Bound\<close> $ x $ a $ b $ f) xs =
+fun mapprox_form eps \<^Const_>\<open>Bound for x a b f\<close> xs =
     (not (mapprox_atLeastAtMost eps x a b xs)) orelse mapprox_form eps f xs
-| mapprox_form eps (\<^term>\<open>Assign\<close> $ x $ a $ f) xs =
+| mapprox_form eps \<^Const_>\<open>Assign for x a f\<close> xs =
     (Real.!= (mapprox_floatarith x xs, mapprox_floatarith a xs)) orelse mapprox_form eps f xs
-| mapprox_form eps (\<^term>\<open>Less\<close> $ a $ b) xs = mapprox_floatarith a xs + eps < mapprox_floatarith b xs
-| mapprox_form eps (\<^term>\<open>LessEqual\<close> $ a $ b) xs = mapprox_floatarith a xs + eps <= mapprox_floatarith b xs
-| mapprox_form eps (\<^term>\<open>AtLeastAtMost\<close> $ x $ a $ b) xs = mapprox_atLeastAtMost eps x a b xs
-| mapprox_form eps (\<^term>\<open>Conj\<close> $ f $ g) xs = mapprox_form eps f xs andalso mapprox_form eps g xs
-| mapprox_form eps (\<^term>\<open>Disj\<close> $ f $ g) xs = mapprox_form eps f xs orelse mapprox_form eps g xs
+| mapprox_form eps \<^Const_>\<open>Less for a b\<close> xs = mapprox_floatarith a xs + eps < mapprox_floatarith b xs
+| mapprox_form eps \<^Const_>\<open>LessEqual for a b\<close> xs = mapprox_floatarith a xs + eps <= mapprox_floatarith b xs
+| mapprox_form eps \<^Const_>\<open>AtLeastAtMost for x a b\<close> xs = mapprox_atLeastAtMost eps x a b xs
+| mapprox_form eps \<^Const_>\<open>Conj for f g\<close> xs = mapprox_form eps f xs andalso mapprox_form eps g xs
+| mapprox_form eps \<^Const_>\<open>Disj for f g\<close> xs = mapprox_form eps f xs orelse mapprox_form eps g xs
 | mapprox_form _ t _ = raise TERM ("mapprox_form", [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 optionT t = Type (\<^type_name>\<open>option\<close>, [t])
-fun mk_Some t = Const (\<^const_name>\<open>Some\<close>, t --> optionT t)
 
 fun random_float_list size xs seed =
   fold (K (apsnd (random_float size) #-> (fn c => apfst (fn b => b::c)))) xs ([],seed)
 
 fun real_of_Float (@{code Float} (m, e)) =

 
 fun term_of_int i = (HOLogic.mk_number @{typ int} (@{code integer_of_int} i))
 
 fun term_of_Float (@{code Float} (m, e)) = @{term Float} $ term_of_int m $ term_of_int e
 
-fun is_True \<^term>\<open>True\<close> = true
+fun is_True \<^Const_>\<open>True\<close> = true
   | is_True _ = false
 
 val postproc_form_eqs =
   @{lemma
     "real_of_float (Float 0 a) = 0"

 
 fun approx_random ctxt prec eps frees e xs genuine_only size seed =
   let
     val (rs, seed') = random_float_list size xs seed
     fun mk_approx_form e ts =
-      \<^const>\<open>approx_form\<close> $
-        HOLogic.mk_number \<^typ>\<open>nat\<close> prec $
+      \<^Const>\<open>approx_form\<close> $
+        HOLogic.mk_number \<^Type>\<open>nat\<close> prec $
         e $
-        (HOLogic.mk_list \<^typ>\<open>(float interval) option\<close>
-          (map (fn t => mk_Some \<^typ>\<open>float interval\<close> $ (\<^term>\<open>interval_of::float\<Rightarrow>_\<close> $ t)) ts)) $
-        \<^term>\<open>[] :: nat list\<close>
+        (HOLogic.mk_list \<^typ>\<open>float interval option\<close>
+          (map (fn t => \<^Const>\<open>Some \<^typ>\<open>float interval\<close>\<close> $ \<^Const>\<open>interval_of \<^Type>\<open>float\<close> for t\<close>) ts)) $
+        \<^Const>\<open>Nil \<^Type>\<open>nat\<close>\<close>
   in
     (if
       mapprox_form eps e (map (real_of_Float o fst) rs)
       handle
         General.Overflow => false

       let
         val ts = map (fn x => term_of_Float (fst x)) rs
         val ts' = map
           (AList.lookup op = (map dest_Free xs ~~ ts)
             #> the_default Term.dummy
-            #> curry op $ \<^term>\<open>real_of_float::float\<Rightarrow>_\<close>
+            #> curry op $ \<^Const>\<open>real_of_float\<close>
             #> conv_term ctxt (rewrite_with ctxt postproc_form_eqs))
           frees
       in
         if Approximation.approximate ctxt (mk_approx_form e ts) |> is_True
         then SOME (true, ts')