src/HOL/Decision_Procs/approximation.ML

 *)
 
 signature APPROXIMATION =
 sig
   val approx: int -> Proof.context -> term -> term
+  val approximate: Proof.context -> term -> term
+  val approximation_tac : int -> (string * int) list -> int option -> Proof.context -> int -> tactic
 end
 
 structure Approximation: APPROXIMATION =
 struct
+
+fun reorder_bounds_tac prems i =
+  let
+    fun variable_of_bound (Const (@{const_name Trueprop}, _) $
+                           (Const (@{const_name Set.member}, _) $
+                            Free (name, _) $ _)) = name
+      | variable_of_bound (Const (@{const_name Trueprop}, _) $
+                           (Const (@{const_name HOL.eq}, _) $
+                            Free (name, _) $ _)) = name
+      | variable_of_bound t = raise TERM ("variable_of_bound", [t])
+
+    val variable_bounds
+      = map (`(variable_of_bound o Thm.prop_of)) prems
+
+    fun add_deps (name, bnds)
+      = Graph.add_deps_acyclic (name,
+          remove (op =) name (Term.add_free_names (Thm.prop_of bnds) []))
+
+    val order = Graph.empty
+                |> fold Graph.new_node variable_bounds
+                |> fold add_deps variable_bounds
+                |> Graph.strong_conn |> map the_single |> rev
+                |> map_filter (AList.lookup (op =) variable_bounds)
+
+    fun prepend_prem th tac
+      = tac THEN rtac (th RSN (2, @{thm mp})) i
+  in
+    fold prepend_prem order all_tac
+  end
+
+fun approximation_conv ctxt ct =
+  approximation_oracle (Proof_Context.theory_of ctxt, Thm.term_of ct |> tap (tracing o Syntax.string_of_term ctxt));
+
+fun approximate ctxt t =
+  approximation_oracle (Proof_Context.theory_of ctxt, t)
+  |> Thm.prop_of |> Logic.dest_equals |> snd;
+
+(* Should be in HOL.thy ? *)
+fun gen_eval_tac conv ctxt = CONVERSION
+  (Object_Logic.judgment_conv (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt))
+  THEN' rtac TrueI
+
+val form_equations = @{thms interpret_form_equations};
+
+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 nat} s
+         | NONE => @{term "0 :: nat"}
+    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 nat}
+            |> Thm.cterm_of ctxt
+  in case taylor
+  of NONE => let
+       val n = vs |> length
+               |> HOLogic.mk_number @{typ nat}
+               |> Thm.cterm_of ctxt
+       val s = vs
+               |> map lookup_splitting
+               |> HOLogic.mk_list @{typ nat}
+               |> Thm.cterm_of ctxt
+     in
+       (rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n),
+                                   (@{cpat "?prec::nat"}, p),
+                                   (@{cpat "?ss::nat list"}, s)])
+            @{thm "approx_form"}) i
+        THEN simp_tac (put_simpset (simpset_of @{context}) ctxt) i) st
+     end
+
+   | 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 nat}
+            |> Thm.cterm_of ctxt
+       val s = vs |> map lookup_splitting |> hd
+            |> Thm.cterm_of ctxt
+     in
+       rtac (Thm.instantiate ([], [(@{cpat "?s::nat"}, s),
+                                   (@{cpat "?t::nat"}, t),
+                                   (@{cpat "?prec::nat"}, p)])
+            @{thm "approx_tse_form"}) i st
+     end
+  end
 
 fun calculated_subterms (@{const Trueprop} $ t) = calculated_subterms t
   | calculated_subterms (@{const HOL.implies} $ _ $ t) = calculated_subterms t
   | calculated_subterms (@{term "op <= :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]
   | calculated_subterms (@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]

 val _ =
   Outer_Syntax.command @{command_spec "approximate"} "print approximation of term"
     (opt_modes -- Parse.term
       >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t)));
 
+fun approximation_tac prec splitting taylor ctxt i =
+  REPEAT (FIRST' [etac @{thm intervalE},
+                  etac @{thm meta_eqE},
+                  rtac @{thm impI}] i)
+  THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) ctxt i
+  THEN DETERM (TRY (filter_prems_tac ctxt (K false) i))
+  THEN DETERM (Reification.tac ctxt form_equations NONE i)
+  THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
+  THEN gen_eval_tac (approximation_conv ctxt) ctxt i
+    
 end;