--- 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
--- 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
--- 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;
--- 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