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