prefer separate command for approximation
authorhaftmann
Fri May 09 08:13:36 2014 +0200 (2014-05-09)
changeset 56923c062543d380e
parent 56922 d411a81b8356
child 56924 2f94c9a50f06
prefer separate command for approximation
NEWS
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/approximation.ML
src/HOL/Decision_Procs/ex/Approximation_Ex.thy
     1.1 --- a/NEWS	Fri May 09 08:13:36 2014 +0200
     1.2 +++ b/NEWS	Fri May 09 08:13:36 2014 +0200
     1.3 @@ -204,6 +204,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Separate command ''approximate'' for approximative computation
     1.8 +in Decision_Procs/Approximation.  Minor INCOMPATBILITY.
     1.9 +
    1.10  * Adjustion of INF and SUP operations:
    1.11    * Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
    1.12    * Consolidated theorem names containing INFI and SUPR: have INF
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Fri May 09 08:13:36 2014 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Fri May 09 08:13:36 2014 +0200
     2.3 @@ -9,6 +9,7 @@
     2.4    "~~/src/HOL/Library/Float"
     2.5    Dense_Linear_Order
     2.6    "~~/src/HOL/Library/Code_Target_Numeral"
     2.7 +keywords "approximate" :: diag
     2.8  begin
     2.9  
    2.10  declare powr_one [simp]
    2.11 @@ -3449,6 +3450,4 @@
    2.12  
    2.13  ML_file "approximation.ML"
    2.14  
    2.15 -setup {* Value.add_evaluator ("approximate", Approximation.approx 30) *}
    2.16 -
    2.17  end
     3.1 --- a/src/HOL/Decision_Procs/approximation.ML	Fri May 09 08:13:36 2014 +0200
     3.2 +++ b/src/HOL/Decision_Procs/approximation.ML	Fri May 09 08:13:36 2014 +0200
     3.3 @@ -91,11 +91,6 @@
     3.4      val t = Term.subst_TVars m t
     3.5    in t end
     3.6  
     3.7 -fun converted_result t =
     3.8 -        prop_of t
     3.9 -     |> HOLogic.dest_Trueprop
    3.10 -     |> HOLogic.dest_eq |> snd
    3.11 -
    3.12  fun apply_tactic ctxt term tactic =
    3.13    cterm_of (Proof_Context.theory_of ctxt) term
    3.14    |> Goal.init
    3.15 @@ -140,4 +135,24 @@
    3.16    else if type_of t = @{typ bool} then approx_form prec ctxt (@{const Trueprop} $ t)
    3.17    else approx_arith prec ctxt t
    3.18  
    3.19 +fun approximate_cmd modes raw_t state =
    3.20 +  let
    3.21 +    val ctxt = Toplevel.context_of state;
    3.22 +    val t = Syntax.read_term ctxt raw_t;
    3.23 +    val t' = approx 30 ctxt t;
    3.24 +    val ty' = Term.type_of t';
    3.25 +    val ctxt' = Variable.auto_fixes t' ctxt;
    3.26 +    val p = Print_Mode.with_modes modes (fn () =>
    3.27 +      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
    3.28 +        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
    3.29 +  in Pretty.writeln p end;
    3.30 +
    3.31 +val opt_modes =
    3.32 +  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
    3.33 +
    3.34 +val _ =
    3.35 +  Outer_Syntax.improper_command @{command_spec "approximate"} "print approximation of term"
    3.36 +    (opt_modes -- Parse.term
    3.37 +      >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t)));
    3.38 +
    3.39  end;
     4.1 --- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Fri May 09 08:13:36 2014 +0200
     4.2 +++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Fri May 09 08:13:36 2014 +0200
     4.3 @@ -75,6 +75,6 @@
     4.4  lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x\<^sup>2 \<le> x"
     4.5    by (approximation 30 splitting: x=1 taylor: x = 3)
     4.6  
     4.7 -value [approximate] "10"
     4.8 +approximate "10"
     4.9  
    4.10  end