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