1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Wed May 19 10:17:31 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed May 19 12:35:20 2010 +0200
     1.3 @@ -3209,12 +3209,96 @@
     1.4    interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_powr interpret_floatarith_log
     1.5    interpret_floatarith_sin
     1.6  
     1.7 -code_reflect Float_Arith
     1.8 -  datatypes float = Float
     1.9 -  and floatarith = Add | Minus | Mult | Inverse | Cos | Arctan
    1.10 -    | Abs | Max | Min | Pi | Sqrt | Exp | Ln | Power | Var | Num
    1.11 -  and form = Bound | Assign | Less | LessEqual | AtLeastAtMost
    1.12 -  functions approx_form approx_tse_form approx' approx_form_eval
    1.13 +oracle approximation_oracle = {* fn (thy, t) =>
    1.14 +let
    1.15 +
    1.16 +  fun bad t = error ("Bad term: " ^ Syntax.string_of_term_global thy t);
    1.17 +
    1.18 +  fun term_of_bool True = @{term True}
    1.19 +    | term_of_bool False = @{term False};
    1.20 +
    1.21 +  fun term_of_float (@{code Float} (k, l)) =
    1.22 +    @{term Float} $ HOLogic.mk_number @{typ int} k $ HOLogic.mk_number @{typ int} l;
    1.23 +
    1.24 +  fun term_of_float_float_option NONE = @{term "None :: (float \<times> float) option"}
    1.25 +    | term_of_float_float_option (SOME ff) = @{term "Some :: float \<times> float \<Rightarrow> _"}
    1.26 +        $ HOLogic.mk_prod (pairself term_of_float ff);
    1.27 +
    1.28 +  val term_of_float_float_option_list =
    1.29 +    HOLogic.mk_list @{typ "(float \<times> float) option"} o map term_of_float_float_option;
    1.30 +
    1.31 +  fun nat_of_term t = HOLogic.dest_nat t handle TERM _ => snd (HOLogic.dest_number t);
    1.32 +
    1.33 +  fun float_of_term (@{term Float} $ k $ l) =
    1.34 +        @{code Float} (snd (HOLogic.dest_number k), snd (HOLogic.dest_number l))
    1.35 +    | float_of_term t = bad t;
    1.36 +
    1.37 +  fun floatarith_of_term (@{term Add} $ a $ b) = @{code Add} (floatarith_of_term a, floatarith_of_term b)
    1.38 +    | floatarith_of_term (@{term Minus} $ a) = @{code Minus} (floatarith_of_term a)
    1.39 +    | floatarith_of_term (@{term Mult} $ a $ b) = @{code Mult} (floatarith_of_term a, floatarith_of_term b)
    1.40 +    | floatarith_of_term (@{term Inverse} $ a) = @{code Inverse} (floatarith_of_term a)
    1.41 +    | floatarith_of_term (@{term Cos} $ a) = @{code Cos} (floatarith_of_term a)
    1.42 +    | floatarith_of_term (@{term Arctan} $ a) = @{code Arctan} (floatarith_of_term a)
    1.43 +    | floatarith_of_term (@{term Abs} $ a) = @{code Abs} (floatarith_of_term a)
    1.44 +    | floatarith_of_term (@{term Max} $ a $ b) = @{code Max} (floatarith_of_term a, floatarith_of_term b)
    1.45 +    | floatarith_of_term (@{term Min} $ a $ b) = @{code Min} (floatarith_of_term a, floatarith_of_term b)
    1.46 +    | floatarith_of_term @{term Pi} = @{code Pi}
    1.47 +    | floatarith_of_term (@{term Sqrt} $ a) = @{code Sqrt} (floatarith_of_term a)
    1.48 +    | floatarith_of_term (@{term Exp} $ a) = @{code Exp} (floatarith_of_term a)
    1.49 +    | floatarith_of_term (@{term Ln} $ a) = @{code Ln} (floatarith_of_term a)
    1.50 +    | floatarith_of_term (@{term Power} $ a $ n) =
    1.51 +        @{code Power} (floatarith_of_term a, nat_of_term n)
    1.52 +    | floatarith_of_term (@{term Var} $ n) = @{code Var} (nat_of_term n)
    1.53 +    | floatarith_of_term (@{term Num} $ m) = @{code Num} (float_of_term m)
    1.54 +    | floatarith_of_term t = bad t;
    1.55 +
    1.56 +  fun form_of_term (@{term Bound} $ a $ b $ c $ p) = @{code Bound}
    1.57 +        (floatarith_of_term a, floatarith_of_term b, floatarith_of_term c, form_of_term p)
    1.58 +    | form_of_term (@{term Assign} $ a $ b $ p) = @{code Assign}
    1.59 +        (floatarith_of_term a, floatarith_of_term b, form_of_term p)
    1.60 +    | form_of_term (@{term Less} $ a $ b) = @{code Less}
    1.61 +        (floatarith_of_term a, floatarith_of_term b)
    1.62 +    | form_of_term (@{term LessEqual} $ a $ b) = @{code LessEqual}
    1.63 +        (floatarith_of_term a, floatarith_of_term b)
    1.64 +    | form_of_term (@{term AtLeastAtMost} $ a $ b $ c) = @{code AtLeastAtMost}
    1.65 +        (floatarith_of_term a, floatarith_of_term b, floatarith_of_term c)
    1.66 +    | form_of_term t = bad t;
    1.67 +
    1.68 +  fun float_float_option_of_term @{term "None :: (float \<times> float) option"} = NONE
    1.69 +    | float_float_option_of_term (@{term "Some :: float \<times> float \<Rightarrow> _"} $ ff) =
    1.70 +        SOME (pairself float_of_term (HOLogic.dest_prod ff))
    1.71 +    | float_float_option_of_term (@{term approx'} $ n $ a $ ffs) = @{code approx'}
    1.72 +        (nat_of_term n) (floatarith_of_term a) (float_float_option_list_of_term ffs)
    1.73 +    | float_float_option_of_term t = bad t
    1.74 +  and float_float_option_list_of_term
    1.75 +        (@{term "replicate :: _ \<Rightarrow> (float \<times> float) option \<Rightarrow> _"} $ n $ @{term "None :: (float \<times> float) option"}) =
    1.76 +          @{code replicate} (nat_of_term n) NONE
    1.77 +    | float_float_option_list_of_term (@{term approx_form_eval} $ n $ p $ ffs) =
    1.78 +        @{code approx_form_eval} (nat_of_term n) (form_of_term p) (float_float_option_list_of_term ffs)
    1.79 +    | float_float_option_list_of_term t = map float_float_option_of_term
    1.80 +        (HOLogic.dest_list t);
    1.81 +
    1.82 +  val nat_list_of_term = map nat_of_term o HOLogic.dest_list ;
    1.83 +
    1.84 +  fun bool_of_term (@{term approx_form} $ n $ p $ ffs $ ms) = @{code approx_form}
    1.85 +        (nat_of_term n) (form_of_term p) (float_float_option_list_of_term ffs) (nat_list_of_term ms)
    1.86 +    | bool_of_term (@{term approx_tse_form} $ m $ n $ q $ p) =
    1.87 +        @{code approx_tse_form} (nat_of_term m) (nat_of_term n) (nat_of_term q) (form_of_term p)
    1.88 +    | bool_of_term t = bad t;
    1.89 +
    1.90 +  fun eval t = case fastype_of t
    1.91 +   of @{typ bool} =>
    1.92 +        (term_of_bool o bool_of_term) t
    1.93 +    | @{typ "(float \<times> float) option"} =>
    1.94 +        (term_of_float_float_option o float_float_option_of_term) t
    1.95 +    | @{typ "(float \<times> float) option list"} =>
    1.96 +        (term_of_float_float_option_list o float_float_option_list_of_term) t
    1.97 +    | _ => bad t;
    1.98 +
    1.99 +  val normalize = eval o Envir.beta_norm o Pattern.eta_long [];
   1.100 +
   1.101 +in Thm.cterm_of thy (Logic.mk_equals (t, normalize t)) end
   1.102 +*}
   1.103  
   1.104  ML {*
   1.105    fun reorder_bounds_tac prems i =
   1.106 @@ -3246,9 +3330,17 @@
   1.107        fold prepend_prem order all_tac
   1.108      end
   1.109  
   1.110 +  fun approximation_conv ctxt ct =
   1.111 +    approximation_oracle (ProofContext.theory_of ctxt, Thm.term_of ct |> tap (tracing o Syntax.string_of_term ctxt));
   1.112 +
   1.113 +  fun approximate ctxt t =
   1.114 +    approximation_oracle (ProofContext.theory_of ctxt, t)
   1.115 +    |> Thm.prop_of |> Logic.dest_equals |> snd;
   1.116 +
   1.117    (* Should be in HOL.thy ? *)
   1.118 -  fun gen_eval_tac conv ctxt = CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
   1.119 -                               THEN' rtac TrueI
   1.120 +  fun gen_eval_tac conv ctxt = CONVERSION
   1.121 +    (Object_Logic.judgment_conv (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt))
   1.122 +    THEN' rtac TrueI
   1.123  
   1.124    val form_equations = PureThy.get_thms @{theory} "interpret_form_equations";
   1.125  
   1.126 @@ -3327,7 +3419,7 @@
   1.127        THEN DETERM (TRY (filter_prems_tac (K false) i))
   1.128        THEN DETERM (Reflection.genreify_tac ctxt form_equations NONE i)
   1.129        THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
   1.130 -      THEN gen_eval_tac eval_oracle ctxt i))
   1.131 +      THEN gen_eval_tac (approximation_conv ctxt) ctxt i))
   1.132   *} "real number approximation"
   1.133  
   1.134  ML {*
   1.135 @@ -3435,7 +3527,7 @@
   1.136         |> (fn (data, xs) =>
   1.137            mk_approx_form_eval prec data (HOLogic.mk_list @{typ "(float * float) option"}
   1.138              (map (fn _ => @{term "None :: (float * float) option"}) (HOLogic.dest_list xs)))
   1.139 -       |> Codegen.eval_term @{theory}
   1.140 +       |> approximate ctxt
   1.141         |> HOLogic.dest_list
   1.142         |> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term)
   1.143         |> map (fn (elem, s) => @{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ elem $ mk_result prec (dest_ivl s))
   1.144 @@ -3448,7 +3540,7 @@
   1.145         |> HOLogic.dest_eq |> snd
   1.146         |> dest_interpret |> fst
   1.147         |> mk_approx' prec
   1.148 -       |> Codegen.eval_term @{theory}
   1.149 +       |> approximate ctxt
   1.150         |> dest_ivl
   1.151         |> mk_result prec
   1.152