src/HOL/Decision_Procs/approximation.ML
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 56923 c062543d380e
child 58893 9e0ecb66d6a7
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
     1 (*  Title:      HOL/Decision_Procs/approximation.ML
     2     Author:     Johannes Hoelzl, TU Muenchen
     3 *)
     4 
     5 signature APPROXIMATION =
     6 sig
     7   val approx: int -> Proof.context -> term -> term
     8 end
     9 
    10 structure Approximation: APPROXIMATION =
    11 struct
    12 
    13 fun calculated_subterms (@{const Trueprop} $ t) = calculated_subterms t
    14   | calculated_subterms (@{const HOL.implies} $ _ $ t) = calculated_subterms t
    15   | calculated_subterms (@{term "op <= :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]
    16   | calculated_subterms (@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]
    17   | calculated_subterms (@{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ t1 $
    18                          (@{term "atLeastAtMost :: real \<Rightarrow> real \<Rightarrow> real set"} $ t2 $ t3)) = [t1, t2, t3]
    19   | calculated_subterms t = raise TERM ("calculated_subterms", [t])
    20 
    21 fun dest_interpret_form (@{const "interpret_form"} $ b $ xs) = (b, xs)
    22   | dest_interpret_form t = raise TERM ("dest_interpret_form", [t])
    23 
    24 fun dest_interpret (@{const "interpret_floatarith"} $ b $ xs) = (b, xs)
    25   | dest_interpret t = raise TERM ("dest_interpret", [t])
    26 
    27 
    28 fun dest_float (@{const "Float"} $ m $ e) =
    29   (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
    30 
    31 fun dest_ivl (Const (@{const_name "Some"}, _) $
    32               (Const (@{const_name Pair}, _) $ u $ l)) = SOME (dest_float u, dest_float l)
    33   | dest_ivl (Const (@{const_name "None"}, _)) = NONE
    34   | dest_ivl t = raise TERM ("dest_result", [t])
    35 
    36 fun mk_approx' prec t = (@{const "approx'"}
    37                        $ HOLogic.mk_number @{typ nat} prec
    38                        $ t $ @{term "[] :: (float * float) option list"})
    39 
    40 fun mk_approx_form_eval prec t xs = (@{const "approx_form_eval"}
    41                        $ HOLogic.mk_number @{typ nat} prec
    42                        $ t $ xs)
    43 
    44 fun float2_float10 prec round_down (m, e) = (
    45   let
    46     val (m, e) = (if e < 0 then (m,e) else (m * Integer.pow e 2, 0))
    47 
    48     fun frac c p 0 digits cnt = (digits, cnt, 0)
    49       | frac c 0 r digits cnt = (digits, cnt, r)
    50       | frac c p r digits cnt = (let
    51         val (d, r) = Integer.div_mod (r * 10) (Integer.pow (~e) 2)
    52       in frac (c orelse d <> 0) (if d <> 0 orelse c then p - 1 else p) r
    53               (digits * 10 + d) (cnt + 1)
    54       end)
    55 
    56     val sgn = Int.sign m
    57     val m = abs m
    58 
    59     val round_down = (sgn = 1 andalso round_down) orelse
    60                      (sgn = ~1 andalso not round_down)
    61 
    62     val (x, r) = Integer.div_mod m (Integer.pow (~e) 2)
    63 
    64     val p = ((if x = 0 then prec else prec - (IntInf.log2 x + 1)) * 3) div 10 + 1
    65 
    66     val (digits, e10, r) = if p > 0 then frac (x <> 0) p r 0 0 else (0,0,0)
    67 
    68     val digits = if round_down orelse r = 0 then digits else digits + 1
    69 
    70   in (sgn * (digits + x * (Integer.pow e10 10)), ~e10)
    71   end)
    72 
    73 fun mk_result prec (SOME (l, u)) =
    74   (let
    75     fun mk_float10 rnd x = (let val (m, e) = float2_float10 prec rnd x
    76                        in if e = 0 then HOLogic.mk_number @{typ real} m
    77                      else if e = 1 then @{term "divide :: real \<Rightarrow> real \<Rightarrow> real"} $
    78                                         HOLogic.mk_number @{typ real} m $
    79                                         @{term "10"}
    80                                    else @{term "divide :: real \<Rightarrow> real \<Rightarrow> real"} $
    81                                         HOLogic.mk_number @{typ real} m $
    82                                         (@{term "power 10 :: nat \<Rightarrow> real"} $
    83                                          HOLogic.mk_number @{typ nat} (~e)) end)
    84     in @{term "atLeastAtMost :: real \<Rightarrow> real \<Rightarrow> real set"} $ mk_float10 true l $ mk_float10 false u end)
    85   | mk_result _ NONE = @{term "UNIV :: real set"}
    86 
    87 fun realify t =
    88   let
    89     val t = Logic.varify_global t
    90     val m = map (fn (name, _) => (name, @{typ real})) (Term.add_tvars t [])
    91     val t = Term.subst_TVars m t
    92   in t end
    93 
    94 fun apply_tactic ctxt term tactic =
    95   cterm_of (Proof_Context.theory_of ctxt) term
    96   |> Goal.init
    97   |> SINGLE tactic
    98   |> the |> prems_of |> hd
    99 
   100 fun prepare_form ctxt term = apply_tactic ctxt term (
   101     REPEAT (FIRST' [etac @{thm intervalE}, etac @{thm meta_eqE}, rtac @{thm impI}] 1)
   102     THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems 1) ctxt 1
   103     THEN DETERM (TRY (filter_prems_tac (K false) 1)))
   104 
   105 fun reify_form ctxt term = apply_tactic ctxt term
   106    (Reification.tac ctxt form_equations NONE 1)
   107 
   108 fun approx_form prec ctxt t =
   109         realify t
   110      |> prepare_form ctxt
   111      |> (fn arith_term => reify_form ctxt arith_term
   112          |> HOLogic.dest_Trueprop |> dest_interpret_form
   113          |> (fn (data, xs) =>
   114             mk_approx_form_eval prec data (HOLogic.mk_list @{typ "(float * float) option"}
   115               (map (fn _ => @{term "None :: (float * float) option"}) (HOLogic.dest_list xs)))
   116          |> approximate ctxt
   117          |> HOLogic.dest_list
   118          |> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term)
   119          |> map (fn (elem, s) => @{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ elem $ mk_result prec (dest_ivl s))
   120          |> foldr1 HOLogic.mk_conj))
   121 
   122 fun approx_arith prec ctxt t = realify t
   123      |> Thm.cterm_of (Proof_Context.theory_of ctxt)
   124      |> Reification.conv ctxt form_equations
   125      |> prop_of
   126      |> Logic.dest_equals |> snd
   127      |> dest_interpret |> fst
   128      |> mk_approx' prec
   129      |> approximate ctxt
   130      |> dest_ivl
   131      |> mk_result prec
   132 
   133 fun approx prec ctxt t =
   134   if type_of t = @{typ prop} then approx_form prec ctxt t
   135   else if type_of t = @{typ bool} then approx_form prec ctxt (@{const Trueprop} $ t)
   136   else approx_arith prec ctxt t
   137 
   138 fun approximate_cmd modes raw_t state =
   139   let
   140     val ctxt = Toplevel.context_of state;
   141     val t = Syntax.read_term ctxt raw_t;
   142     val t' = approx 30 ctxt t;
   143     val ty' = Term.type_of t';
   144     val ctxt' = Variable.auto_fixes t' ctxt;
   145     val p = Print_Mode.with_modes modes (fn () =>
   146       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
   147         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
   148   in Pretty.writeln p end;
   149 
   150 val opt_modes =
   151   Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
   152 
   153 val _ =
   154   Outer_Syntax.improper_command @{command_spec "approximate"} "print approximation of term"
   155     (opt_modes -- Parse.term
   156       >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t)));
   157 
   158 end;