# HG changeset patch
# User haftmann
# Date 1399616016 -7200
# Node ID c062543d380e90d82a4628b74db6c25efc187428
# Parent  d411a81b83564bc5eb4faca00f61fd7b2ea2ad5a
prefer separate command for approximation

diff -r d411a81b8356 -r c062543d380e NEWS
--- a/NEWS	Fri May 09 08:13:36 2014 +0200
+++ b/NEWS	Fri May 09 08:13:36 2014 +0200
@@ -204,6 +204,9 @@
 
 *** HOL ***
 
+* Separate command ''approximate'' for approximative computation
+in Decision_Procs/Approximation.  Minor INCOMPATBILITY.
+
 * Adjustion of INF and SUP operations:
   * Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
   * Consolidated theorem names containing INFI and SUPR: have INF
diff -r d411a81b8356 -r c062543d380e src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Fri May 09 08:13:36 2014 +0200
@@ -9,6 +9,7 @@
   "~~/src/HOL/Library/Float"
   Dense_Linear_Order
   "~~/src/HOL/Library/Code_Target_Numeral"
+keywords "approximate" :: diag
 begin
 
 declare powr_one [simp]
@@ -3449,6 +3450,4 @@
 
 ML_file "approximation.ML"
 
-setup {* Value.add_evaluator ("approximate", Approximation.approx 30) *}
-
 end
diff -r d411a81b8356 -r c062543d380e src/HOL/Decision_Procs/approximation.ML
--- a/src/HOL/Decision_Procs/approximation.ML	Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/Decision_Procs/approximation.ML	Fri May 09 08:13:36 2014 +0200
@@ -91,11 +91,6 @@
     val t = Term.subst_TVars m t
   in t end
 
-fun converted_result t =
-        prop_of t
-     |> HOLogic.dest_Trueprop
-     |> HOLogic.dest_eq |> snd
-
 fun apply_tactic ctxt term tactic =
   cterm_of (Proof_Context.theory_of ctxt) term
   |> Goal.init
@@ -140,4 +135,24 @@
   else if type_of t = @{typ bool} then approx_form prec ctxt (@{const Trueprop} $ t)
   else approx_arith prec ctxt t
 
+fun approximate_cmd modes raw_t state =
+  let
+    val ctxt = Toplevel.context_of state;
+    val t = Syntax.read_term ctxt raw_t;
+    val t' = approx 30 ctxt t;
+    val ty' = Term.type_of t';
+    val ctxt' = Variable.auto_fixes t' ctxt;
+    val p = Print_Mode.with_modes modes (fn () =>
+      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
+        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
+  in Pretty.writeln p end;
+
+val opt_modes =
+  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
+
+val _ =
+  Outer_Syntax.improper_command @{command_spec "approximate"} "print approximation of term"
+    (opt_modes -- Parse.term
+      >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t)));
+
 end;
diff -r d411a81b8356 -r c062543d380e src/HOL/Decision_Procs/ex/Approximation_Ex.thy
--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Fri May 09 08:13:36 2014 +0200
@@ -75,6 +75,6 @@
 lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x\<^sup>2 \<le> x"
   by (approximation 30 splitting: x=1 taylor: x = 3)
 
-value [approximate] "10"
+approximate "10"
 
 end