# HG changeset patch # User immler # Date 1474473385 -7200 # Node ID b673e7221b1650bcae71160e55ffa7fb0679182f # Parent d81fb5b46a5c01c2eb35a8524a0229f1c9c3c565 approximation: rewrite for reduction to base expressions diff -r d81fb5b46a5c -r b673e7221b16 src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Wed Sep 21 16:59:51 2016 +0100 +++ b/src/HOL/Decision_Procs/Approximation.thy Wed Sep 21 17:56:25 2016 +0200 @@ -2863,29 +2863,6 @@ interpret_floatarith_divide interpret_floatarith_diff by auto -lemma interpret_floatarith_tan: - "interpret_floatarith (Mult (Cos (Add (Mult Pi (Num (Float 1 (- 1)))) (Minus a))) (Inverse (Cos a))) vs = - tan (interpret_floatarith a vs)" - unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def divide_inverse - by auto - -lemma interpret_floatarith_log: - "interpret_floatarith ((Mult (Ln x) (Inverse (Ln b)))) vs = - log (interpret_floatarith b vs) (interpret_floatarith x vs)" - unfolding log_def interpret_floatarith.simps divide_inverse .. - -lemma interpret_floatarith_num: - shows "interpret_floatarith (Num (Float 0 0)) vs = 0" - and "interpret_floatarith (Num (Float 1 0)) vs = 1" - and "interpret_floatarith (Num (Float (- 1) 0)) vs = - 1" - and "interpret_floatarith (Num (Float (numeral a) 0)) vs = numeral a" - and "interpret_floatarith (Num (Float (- numeral a) 0)) vs = - numeral a" - by auto - -lemma interpret_floatarith_ceiling: - "interpret_floatarith (Minus (Floor (Minus a))) vs = ceiling (interpret_floatarith a vs)" - unfolding ceiling_def interpret_floatarith.simps of_int_minus .. - subsection "Implement approximation function" @@ -4289,10 +4266,6 @@ subsection \Implement proof method \texttt{approximation}\ -lemmas interpret_form_equations = interpret_form.simps interpret_floatarith.simps interpret_floatarith_num - interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_log - interpret_floatarith_sin interpret_floatarith_ceiling - oracle approximation_oracle = \fn (thy, t) => let fun bad t = error ("Bad term: " ^ Syntax.string_of_term_global thy t); @@ -4400,6 +4373,24 @@ lemma meta_eqE: "x \ a \ \ x = a \ P\ \ P" by auto +named_theorems approximation_preproc + +lemma approximation_preproc_floatarith[approximation_preproc]: + "0 = real_of_float 0" + "1 = real_of_float 1" + "0 = Float 0 0" + "1 = Float 1 0" + "numeral a = Float (numeral a) 0" + "numeral a = real_of_float (numeral a)" + "x - y = x + - y" + "x / y = x * inverse y" + "ceiling x = - floor (- x)" + "log x y = ln y * inverse (ln x)" + "sin x = cos (pi / 2 - x)" + "tan x = sin x / cos x" + "real_of_int (- i) = - real_of_int i" + by (simp_all add: inverse_eq_divide ceiling_def log_def sin_cos_eq tan_def real_of_float_eq) + ML_file "approximation.ML" method_setup approximation = \ @@ -4421,6 +4412,17 @@ section "Quickcheck Generator" +lemma approximation_preproc_push_neg[approximation_preproc]: + fixes a b::real + shows + "\ (a < b) \ b \ a" + "\ (a \ b) \ b < a" + "\ (a = b) \ b < a \ a < b" + "\ (p \ q) \ \ p \ \ q" + "\ (p \ q) \ \ p \ \ q" + "\ \ q \ q" + by auto + ML_file "approximation_generator.ML" setup "Approximation_Generator.setup" diff -r d81fb5b46a5c -r b673e7221b16 src/HOL/Decision_Procs/approximation.ML --- a/src/HOL/Decision_Procs/approximation.ML Wed Sep 21 16:59:51 2016 +0100 +++ b/src/HOL/Decision_Procs/approximation.ML Wed Sep 21 17:56:25 2016 +0200 @@ -4,6 +4,7 @@ signature APPROXIMATION = sig + val reify_form: Proof.context -> term -> term val approx: int -> Proof.context -> term -> term val approximate: Proof.context -> term -> term val approximation_tac : int -> (string * int) list -> int option -> Proof.context -> int -> tactic @@ -54,8 +55,6 @@ (Object_Logic.judgment_conv ctxt (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)) THEN' resolve_tac ctxt [TrueI] -val form_equations = @{thms interpret_form_equations}; - fun rewrite_interpret_form_tac ctxt prec splitting taylor i st = let fun lookup_splitting (Free (name, _)) = case AList.lookup (op =) splitting name @@ -190,21 +189,39 @@ |> SINGLE tactic |> the |> Thm.prems_of |> hd -fun prepare_form ctxt term = apply_tactic ctxt term ( - REPEAT (FIRST' [eresolve_tac ctxt @{thms intervalE}, - eresolve_tac ctxt @{thms meta_eqE}, - resolve_tac ctxt @{thms impI}] 1) - THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => reorder_bounds_tac ctxt' prems 1) ctxt 1 - THEN DETERM (TRY (filter_prems_tac ctxt (K false) 1))) +fun preproc_form_conv ctxt = + Simplifier.rewrite + (put_simpset HOL_basic_ss ctxt addsimps + (Named_Theorems.get ctxt @{named_theorems approximation_preproc})) + +fun reify_form_conv ctxt = + (Reification.conv ctxt @{thms interpret_form.simps interpret_floatarith.simps}) + +fun reify_form_tac ctxt i = CONVERSION (Conv.arg_conv (reify_form_conv ctxt)) i -fun reify_form ctxt term = apply_tactic ctxt term - (Reification.tac ctxt form_equations NONE 1) +fun prepare_form_tac ctxt i = + REPEAT (FIRST' [eresolve_tac ctxt @{thms intervalE}, + eresolve_tac ctxt @{thms meta_eqE}, + resolve_tac ctxt @{thms impI}] i) + THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => reorder_bounds_tac ctxt' prems i) ctxt i + THEN DETERM (TRY (filter_prems_tac ctxt (K false) i)) + THEN CONVERSION (Conv.arg_conv (preproc_form_conv ctxt)) i + +fun prepare_form ctxt term = apply_tactic ctxt term (prepare_form_tac ctxt 1) + +fun apply_reify_form ctxt t = apply_tactic ctxt t (reify_form_tac ctxt 1) + +fun reify_form ctxt t = HOLogic.mk_Trueprop t + |> prepare_form ctxt + |> apply_reify_form ctxt + |> HOLogic.dest_Trueprop fun approx_form prec ctxt t = realify t |> prepare_form ctxt - |> (fn arith_term => reify_form ctxt arith_term - |> HOLogic.dest_Trueprop |> dest_interpret_form + |> (fn arith_term => apply_reify_form ctxt arith_term + |> HOLogic.dest_Trueprop + |> dest_interpret_form |> (fn (data, xs) => mk_approx_form_eval prec data (HOLogic.mk_list @{typ "(float * float) option"} (map (fn _ => @{term "None :: (float * float) option"}) (HOLogic.dest_list xs))) @@ -216,7 +233,7 @@ fun approx_arith prec ctxt t = realify t |> Thm.cterm_of ctxt - |> Reification.conv ctxt form_equations + |> (preproc_form_conv ctxt then_conv reify_form_conv ctxt) |> Thm.prop_of |> Logic.dest_equals |> snd |> dest_interpret |> fst @@ -252,13 +269,9 @@ >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t))); fun approximation_tac prec splitting taylor ctxt i = - REPEAT (FIRST' [eresolve_tac ctxt @{thms intervalE}, - eresolve_tac ctxt @{thms meta_eqE}, - resolve_tac ctxt @{thms impI}] i) - THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => reorder_bounds_tac ctxt' prems i) ctxt i - THEN DETERM (TRY (filter_prems_tac ctxt (K false) i)) - THEN DETERM (Reification.tac ctxt form_equations NONE i) + prepare_form_tac ctxt i + THEN reify_form_tac ctxt i THEN rewrite_interpret_form_tac ctxt prec splitting taylor i THEN gen_eval_tac (approximation_conv ctxt) ctxt i - + end; diff -r d81fb5b46a5c -r b673e7221b16 src/HOL/Decision_Procs/approximation_generator.ML --- a/src/HOL/Decision_Procs/approximation_generator.ML Wed Sep 21 16:59:51 2016 +0100 +++ b/src/HOL/Decision_Procs/approximation_generator.ML Wed Sep 21 17:56:25 2016 +0200 @@ -154,19 +154,12 @@ "a = b \ a \ b \ b \ a" "(p \ q) \ \p \ q" "(p \ q) \ (p \ q) \ (q \ p)" - "\ (a < b) \ b \ a" - "\ (a \ b) \ b < a" - "\ (p \ q) \ \ p \ \ q" - "\ (p \ q) \ \ p \ \ q" - "\ \ q \ q" by auto} -val form_equations = @{thms interpret_form_equations}; - fun reify_goal ctxt t = HOLogic.mk_not t |> conv_term ctxt (rewrite_with ctxt preproc_form_eqs) - |> conv_term ctxt (Reification.conv ctxt form_equations) + |> Approximation.reify_form ctxt |> dest_interpret_form ||> HOLogic.dest_list