Added new evaluator "approximate"
authorhoelzl
Mon Jun 08 18:37:35 2009 +0200 (2009-06-08)
changeset 31810a6b800855cdd
parent 31809 06372924e86c
child 31811 64dea9a15031
Added new evaluator "approximate"
NEWS
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Library/reflection.ML
     1.1 --- a/NEWS	Mon Jun 15 12:14:40 2009 +0200
     1.2 +++ b/NEWS	Mon Jun 08 18:37:35 2009 +0200
     1.3 @@ -65,6 +65,8 @@
     1.4  * Abbreviation "arbitrary" of "undefined" has disappeared; use "undefined" directly.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* New evaluator "approximate" approximates an real valued term using the same method as the
     1.8 +approximation method. 
     1.9  
    1.10  *** ML ***
    1.11  
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Mon Jun 15 12:14:40 2009 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Jun 08 18:37:35 2009 +0200
     2.3 @@ -2546,6 +2546,7 @@
     2.4  @{code_datatype inequality = Less | LessEqual }
     2.5  
     2.6  val approx_inequality = @{code approx_inequality}
     2.7 +val approx' = @{code approx'}
     2.8  
     2.9  end
    2.10  *}
    2.11 @@ -2569,6 +2570,7 @@
    2.12  code_const Less and LessEqual (Eval "Float'_Arith.Less/ (_,/ _)" and "Float'_Arith.LessEqual/ (_,/ _)")
    2.13  
    2.14  code_const approx_inequality (Eval "Float'_Arith.approx'_inequality")
    2.15 +code_const approx' (Eval "Float'_Arith.approx''")
    2.16  
    2.17  ML {*
    2.18    val ineq_equations = PureThy.get_thms @{theory} "interpret_inequality_equations";
    2.19 @@ -2662,4 +2664,89 @@
    2.20        THEN (gen_eval_tac eval_oracle ctxt) i)))
    2.21  *} "real number approximation"
    2.22  
    2.23 +ML {*
    2.24 +  fun dest_interpret (@{const "interpret_floatarith"} $ b $ xs) = (b, xs)
    2.25 +  | dest_interpret t = raise TERM ("dest_interpret", [t])
    2.26 +
    2.27 +  fun mk_approx' prec t = (@{const "approx'"}
    2.28 +                         $ HOLogic.mk_number @{typ nat} prec
    2.29 +                         $ t $ @{term "[] :: (float * float) list"})
    2.30 +
    2.31 +  fun dest_result (Const (@{const_name "Some"}, _) $
    2.32 +                   ((Const (@{const_name "Pair"}, _)) $
    2.33 +                    (@{const "Float"} $ lm $ le) $
    2.34 +                    (@{const "Float"} $ um $ ue)))
    2.35 +                   = SOME ((snd (HOLogic.dest_number lm), snd (HOLogic.dest_number le)),
    2.36 +                           (snd (HOLogic.dest_number um), snd (HOLogic.dest_number ue)))
    2.37 +    | dest_result (Const (@{const_name "None"}, _)) = NONE
    2.38 +    | dest_result t = raise TERM ("dest_result", [t])
    2.39 +
    2.40 +  fun float2_float10 prec round_down (m, e) = (
    2.41 +    let
    2.42 +      val (m, e) = (if e < 0 then (m,e) else (m * Integer.pow e 2, 0))
    2.43 +
    2.44 +      fun frac c p 0 digits cnt = (digits, cnt, 0)
    2.45 +        | frac c 0 r digits cnt = (digits, cnt, r)
    2.46 +        | frac c p r digits cnt = (let
    2.47 +          val (d, r) = Integer.div_mod (r * 10) (Integer.pow (~e) 2)
    2.48 +        in frac (c orelse d <> 0) (if d <> 0 orelse c then p - 1 else p) r
    2.49 +                (digits * 10 + d) (cnt + 1)
    2.50 +        end)
    2.51 +
    2.52 +      val sgn = Int.sign m
    2.53 +      val m = abs m
    2.54 +
    2.55 +      val round_down = (sgn = 1 andalso round_down) orelse
    2.56 +                       (sgn = ~1 andalso not round_down)
    2.57 +
    2.58 +      val (x, r) = Integer.div_mod m (Integer.pow (~e) 2)
    2.59 +
    2.60 +      val p = ((if x = 0 then prec else prec - (IntInf.log2 x + 1)) * 3) div 10 + 1
    2.61 +
    2.62 +      val (digits, e10, r) = if p > 0 then frac (x <> 0) p r 0 0 else (0,0,0)
    2.63 +
    2.64 +      val digits = if round_down orelse r = 0 then digits else digits + 1
    2.65 +
    2.66 +    in (sgn * (digits + x * (Integer.pow e10 10)), ~e10)
    2.67 +    end)
    2.68 +
    2.69 +  fun mk_result prec (SOME (l, u)) = (let
    2.70 +      fun mk_float10 rnd x = (let val (m, e) = float2_float10 prec rnd x
    2.71 +                         in if e = 0 then HOLogic.mk_number @{typ real} m
    2.72 +                       else if e = 1 then @{term "divide :: real \<Rightarrow> real \<Rightarrow> real"} $
    2.73 +                                          HOLogic.mk_number @{typ real} m $
    2.74 +                                          @{term "10"}
    2.75 +                                     else @{term "divide :: real \<Rightarrow> real \<Rightarrow> real"} $
    2.76 +                                          HOLogic.mk_number @{typ real} m $
    2.77 +                                          (@{term "power 10 :: nat \<Rightarrow> real"} $
    2.78 +                                           HOLogic.mk_number @{typ nat} (~e)) end)
    2.79 +      in @{term "atLeastAtMost :: real \<Rightarrow> real \<Rightarrow> real set"} $
    2.80 +         mk_float10 true l $ mk_float10 false u end)
    2.81 +    | mk_result prec NONE = @{term "UNIV :: real set"}
    2.82 +
    2.83 +
    2.84 +  fun realify t = let
    2.85 +      val t = Logic.varify t
    2.86 +      val m = map (fn (name, sort) => (name, @{typ real})) (Term.add_tvars t [])
    2.87 +      val t = Term.subst_TVars m t
    2.88 +    in t end
    2.89 +
    2.90 +  fun approx prec ctxt t = let val t = realify t in
    2.91 +          t
    2.92 +       |> Reflection.genreif ctxt ineq_equations
    2.93 +       |> prop_of
    2.94 +       |> HOLogic.dest_Trueprop
    2.95 +       |> HOLogic.dest_eq |> snd
    2.96 +       |> dest_interpret |> fst
    2.97 +       |> mk_approx' prec
    2.98 +       |> Codegen.eval_term @{theory}
    2.99 +       |> dest_result
   2.100 +       |> mk_result prec
   2.101 +    end
   2.102 +*}
   2.103 +
   2.104 +setup {*
   2.105 +  Value.add_evaluator ("approximate", approx 30)
   2.106 +*}
   2.107 +
   2.108  end
     3.1 --- a/src/HOL/Library/reflection.ML	Mon Jun 15 12:14:40 2009 +0200
     3.2 +++ b/src/HOL/Library/reflection.ML	Mon Jun 08 18:37:35 2009 +0200
     3.3 @@ -10,6 +10,7 @@
     3.4    val reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic
     3.5    val gen_reflection_tac: Proof.context -> (cterm -> thm)
     3.6      -> thm list -> thm list -> term option -> int -> tactic
     3.7 +  val genreif : Proof.context -> thm list -> term -> thm
     3.8  end;
     3.9  
    3.10  structure Reflection : REFLECTION =