# HG changeset patch # User eberlm # Date 1427705574 -7200 # Node ID f339ff48a6ee85dc4b3c94e87fb459824fe76134 # Parent c3d126c7944f94e7176a95200ebbd328a993f67a exposed approximation in ML diff -r c3d126c7944f -r f339ff48a6ee src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Mon Mar 30 00:13:37 2015 +0200 +++ b/src/HOL/Decision_Procs/Approximation.thy Mon Mar 30 10:52:54 2015 +0200 @@ -3583,130 +3583,31 @@ in Thm.global_cterm_of thy (Logic.mk_equals (t, normalize t)) end *} -ML {* - fun reorder_bounds_tac prems i = - let - fun variable_of_bound (Const (@{const_name Trueprop}, _) $ - (Const (@{const_name Set.member}, _) $ - Free (name, _) $ _)) = name - | variable_of_bound (Const (@{const_name Trueprop}, _) $ - (Const (@{const_name HOL.eq}, _) $ - Free (name, _) $ _)) = name - | variable_of_bound t = raise TERM ("variable_of_bound", [t]) - - val variable_bounds - = map (`(variable_of_bound o Thm.prop_of)) prems - - fun add_deps (name, bnds) - = Graph.add_deps_acyclic (name, - remove (op =) name (Term.add_free_names (Thm.prop_of bnds) [])) - - val order = Graph.empty - |> fold Graph.new_node variable_bounds - |> fold add_deps variable_bounds - |> Graph.strong_conn |> map the_single |> rev - |> map_filter (AList.lookup (op =) variable_bounds) - - fun prepend_prem th tac - = tac THEN rtac (th RSN (2, @{thm mp})) i - in - fold prepend_prem order all_tac - end - - fun approximation_conv ctxt ct = - approximation_oracle (Proof_Context.theory_of ctxt, Thm.term_of ct |> tap (tracing o Syntax.string_of_term ctxt)); - - fun approximate ctxt t = - approximation_oracle (Proof_Context.theory_of ctxt, t) - |> Thm.prop_of |> Logic.dest_equals |> snd; - - (* Should be in HOL.thy ? *) - fun gen_eval_tac conv ctxt = CONVERSION - (Object_Logic.judgment_conv (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)) - THEN' rtac 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 - of SOME s => HOLogic.mk_number @{typ nat} s - | NONE => @{term "0 :: nat"} - val vs = nth (Thm.prems_of st) (i - 1) - |> Logic.strip_imp_concl - |> HOLogic.dest_Trueprop - |> Term.strip_comb |> snd |> List.last - |> HOLogic.dest_list - val p = prec - |> HOLogic.mk_number @{typ nat} - |> Thm.cterm_of ctxt - in case taylor - of NONE => let - val n = vs |> length - |> HOLogic.mk_number @{typ nat} - |> Thm.cterm_of ctxt - val s = vs - |> map lookup_splitting - |> HOLogic.mk_list @{typ nat} - |> Thm.cterm_of ctxt - in - (rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n), - (@{cpat "?prec::nat"}, p), - (@{cpat "?ss::nat list"}, s)]) - @{thm "approx_form"}) i - THEN simp_tac (put_simpset (simpset_of @{context}) ctxt) i) st - end - - | SOME t => - if length vs <> 1 - then raise (TERM ("More than one variable used for taylor series expansion", [Thm.prop_of st])) - else let - val t = t - |> HOLogic.mk_number @{typ nat} - |> Thm.cterm_of ctxt - val s = vs |> map lookup_splitting |> hd - |> Thm.cterm_of ctxt - in - rtac (Thm.instantiate ([], [(@{cpat "?s::nat"}, s), - (@{cpat "?t::nat"}, t), - (@{cpat "?prec::nat"}, p)]) - @{thm "approx_tse_form"}) i st - end - end - - val free = Args.context -- Args.term >> (fn (_, Free (n, _)) => n | (ctxt, t) => - error ("Bad free variable: " ^ Syntax.string_of_term ctxt t)); -*} - lemma intervalE: "a \ x \ x \ b \ \ x \ { a .. b } \ P\ \ P" by auto lemma meta_eqE: "x \ a \ \ x = a \ P\ \ P" by auto +ML_file "approximation.ML" + method_setup approximation = {* - Scan.lift Parse.nat - -- - Scan.optional (Scan.lift (Args.$$$ "splitting" |-- Args.colon) - |-- Parse.and_list' (free --| Scan.lift (Args.$$$ "=") -- Scan.lift Parse.nat)) [] - -- - Scan.option (Scan.lift (Args.$$$ "taylor" |-- Args.colon) - |-- (free |-- Scan.lift (Args.$$$ "=") |-- Scan.lift Parse.nat)) - >> - (fn ((prec, splitting), taylor) => fn ctxt => - SIMPLE_METHOD' (fn i => - REPEAT (FIRST' [etac @{thm intervalE}, - etac @{thm meta_eqE}, - rtac @{thm impI}] i) - THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) ctxt i - THEN DETERM (TRY (filter_prems_tac ctxt (K false) i)) - THEN DETERM (Reification.tac ctxt form_equations NONE i) - THEN rewrite_interpret_form_tac ctxt prec splitting taylor i - THEN gen_eval_tac (approximation_conv ctxt) ctxt i)) + let val free = Args.context -- Args.term >> (fn (_, Free (n, _)) => n | (ctxt, t) => + error ("Bad free variable: " ^ Syntax.string_of_term ctxt t)); + in + Scan.lift Parse.nat + -- + Scan.optional (Scan.lift (Args.$$$ "splitting" |-- Args.colon) + |-- Parse.and_list' (free --| Scan.lift (Args.$$$ "=") -- Scan.lift Parse.nat)) [] + -- + Scan.option (Scan.lift (Args.$$$ "taylor" |-- Args.colon) + |-- (free |-- Scan.lift (Args.$$$ "=") |-- Scan.lift Parse.nat)) + >> + (fn ((prec, splitting), taylor) => fn ctxt => + SIMPLE_METHOD' (Approximation.approximation_tac prec splitting taylor ctxt)) + end *} "real number approximation" -ML_file "approximation.ML" - section "Quickcheck Generator" diff -r c3d126c7944f -r f339ff48a6ee src/HOL/Decision_Procs/approximation.ML --- a/src/HOL/Decision_Procs/approximation.ML Mon Mar 30 00:13:37 2015 +0200 +++ b/src/HOL/Decision_Procs/approximation.ML Mon Mar 30 10:52:54 2015 +0200 @@ -5,11 +5,103 @@ signature APPROXIMATION = sig 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 end structure Approximation: APPROXIMATION = struct +fun reorder_bounds_tac prems i = + let + fun variable_of_bound (Const (@{const_name Trueprop}, _) $ + (Const (@{const_name Set.member}, _) $ + Free (name, _) $ _)) = name + | variable_of_bound (Const (@{const_name Trueprop}, _) $ + (Const (@{const_name HOL.eq}, _) $ + Free (name, _) $ _)) = name + | variable_of_bound t = raise TERM ("variable_of_bound", [t]) + + val variable_bounds + = map (`(variable_of_bound o Thm.prop_of)) prems + + fun add_deps (name, bnds) + = Graph.add_deps_acyclic (name, + remove (op =) name (Term.add_free_names (Thm.prop_of bnds) [])) + + val order = Graph.empty + |> fold Graph.new_node variable_bounds + |> fold add_deps variable_bounds + |> Graph.strong_conn |> map the_single |> rev + |> map_filter (AList.lookup (op =) variable_bounds) + + fun prepend_prem th tac + = tac THEN rtac (th RSN (2, @{thm mp})) i + in + fold prepend_prem order all_tac + end + +fun approximation_conv ctxt ct = + approximation_oracle (Proof_Context.theory_of ctxt, Thm.term_of ct |> tap (tracing o Syntax.string_of_term ctxt)); + +fun approximate ctxt t = + approximation_oracle (Proof_Context.theory_of ctxt, t) + |> Thm.prop_of |> Logic.dest_equals |> snd; + +(* Should be in HOL.thy ? *) +fun gen_eval_tac conv ctxt = CONVERSION + (Object_Logic.judgment_conv (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)) + THEN' rtac 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 + of SOME s => HOLogic.mk_number @{typ nat} s + | NONE => @{term "0 :: nat"} + val vs = nth (Thm.prems_of st) (i - 1) + |> Logic.strip_imp_concl + |> HOLogic.dest_Trueprop + |> Term.strip_comb |> snd |> List.last + |> HOLogic.dest_list + val p = prec + |> HOLogic.mk_number @{typ nat} + |> Thm.cterm_of ctxt + in case taylor + of NONE => let + val n = vs |> length + |> HOLogic.mk_number @{typ nat} + |> Thm.cterm_of ctxt + val s = vs + |> map lookup_splitting + |> HOLogic.mk_list @{typ nat} + |> Thm.cterm_of ctxt + in + (rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n), + (@{cpat "?prec::nat"}, p), + (@{cpat "?ss::nat list"}, s)]) + @{thm "approx_form"}) i + THEN simp_tac (put_simpset (simpset_of @{context}) ctxt) i) st + end + + | SOME t => + if length vs <> 1 + then raise (TERM ("More than one variable used for taylor series expansion", [Thm.prop_of st])) + else let + val t = t + |> HOLogic.mk_number @{typ nat} + |> Thm.cterm_of ctxt + val s = vs |> map lookup_splitting |> hd + |> Thm.cterm_of ctxt + in + rtac (Thm.instantiate ([], [(@{cpat "?s::nat"}, s), + (@{cpat "?t::nat"}, t), + (@{cpat "?prec::nat"}, p)]) + @{thm "approx_tse_form"}) i st + end + end + fun calculated_subterms (@{const Trueprop} $ t) = calculated_subterms t | calculated_subterms (@{const HOL.implies} $ _ $ t) = calculated_subterms t | calculated_subterms (@{term "op <= :: real \ real \ bool"} $ t1 $ t2) = [t1, t2] @@ -156,4 +248,14 @@ (opt_modes -- Parse.term >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t))); -end; +fun approximation_tac prec splitting taylor ctxt i = + REPEAT (FIRST' [etac @{thm intervalE}, + etac @{thm meta_eqE}, + rtac @{thm impI}] i) + THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) ctxt i + THEN DETERM (TRY (filter_prems_tac ctxt (K false) i)) + THEN DETERM (Reification.tac ctxt form_equations NONE i) + THEN rewrite_interpret_form_tac ctxt prec splitting taylor i + THEN gen_eval_tac (approximation_conv ctxt) ctxt i + +end; \ No newline at end of file diff -r c3d126c7944f -r f339ff48a6ee src/HOL/Decision_Procs/approximation_generator.ML --- a/src/HOL/Decision_Procs/approximation_generator.ML Mon Mar 30 00:13:37 2015 +0200 +++ b/src/HOL/Decision_Procs/approximation_generator.ML Mon Mar 30 10:52:54 2015 +0200 @@ -141,7 +141,7 @@ #> conv_term ctxt (rewrite_with ctxt postproc_form_eqs)) frees in - if approximate ctxt (mk_approx_form e ts) |> is_True + if Approximation.approximate ctxt (mk_approx_form e ts) |> is_True then SOME (true, ts') else (if genuine_only then NONE else SOME (false, ts')) end @@ -161,6 +161,8 @@ "\ \ 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)