--- 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 \<open>Implement proof method \texttt{approximation}\<close>
-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 = \<open>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 \<equiv> a \<Longrightarrow> \<lbrakk> x = a \<Longrightarrow> P\<rbrakk> \<Longrightarrow> 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 = \<open>
@@ -4421,6 +4412,17 @@
section "Quickcheck Generator"
+lemma approximation_preproc_push_neg[approximation_preproc]:
+ fixes a b::real
+ shows
+ "\<not> (a < b) \<longleftrightarrow> b \<le> a"
+ "\<not> (a \<le> b) \<longleftrightarrow> b < a"
+ "\<not> (a = b) \<longleftrightarrow> b < a \<or> a < b"
+ "\<not> (p \<and> q) \<longleftrightarrow> \<not> p \<or> \<not> q"
+ "\<not> (p \<or> q) \<longleftrightarrow> \<not> p \<and> \<not> q"
+ "\<not> \<not> q \<longleftrightarrow> q"
+ by auto
+
ML_file "approximation_generator.ML"
setup "Approximation_Generator.setup"
--- 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;
--- 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 \<longleftrightarrow> a \<le> b \<and> b \<le> a"
"(p \<longrightarrow> q) \<longleftrightarrow> \<not>p \<or> q"
"(p \<longleftrightarrow> q) \<longleftrightarrow> (p \<longrightarrow> q) \<and> (q \<longrightarrow> p)"
- "\<not> (a < b) \<longleftrightarrow> b \<le> a"
- "\<not> (a \<le> b) \<longleftrightarrow> b < a"
- "\<not> (p \<and> q) \<longleftrightarrow> \<not> p \<or> \<not> q"
- "\<not> (p \<or> q) \<longleftrightarrow> \<not> p \<and> \<not> q"
- "\<not> \<not> q \<longleftrightarrow> 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