# HG changeset patch # User ballarin # Date 1190717787 -7200 # Node ID 9a95634ab13544cff1069d0ab7c4b1b6f9b35570 # Parent 0041117b756c9172d6ce49da7a31c4349fff48cc Transitivity reasoner gets additional argument of premises to improve integration with simplifier. diff -r 0041117b756c -r 9a95634ab135 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Tue Sep 25 12:16:15 2007 +0200 +++ b/src/HOL/Orderings.thy Tue Sep 25 12:56:27 2007 +0200 @@ -243,7 +243,7 @@ sig val print_structures: Proof.context -> unit val setup: theory -> theory - val order_tac: Proof.context -> int -> tactic + val order_tac: thm list -> Proof.context -> int -> tactic end; structure Orders: ORDERS = @@ -283,7 +283,7 @@ (** Method **) -fun struct_tac ((s, [eq, le, less]), thms) = +fun struct_tac ((s, [eq, le, less]), thms) prems = let fun decomp thy (Trueprop $ t) = let @@ -306,13 +306,13 @@ in dec t end; in case s of - "order" => Order_Tac.partial_tac decomp thms - | "linorder" => Order_Tac.linear_tac decomp thms + "order" => Order_Tac.partial_tac decomp thms prems + | "linorder" => Order_Tac.linear_tac decomp thms prems | _ => error ("Unknown kind of order `" ^ s ^ "' encountered in transitivity reasoner.") end -fun order_tac ctxt = - FIRST' (map (fn s => CHANGED o struct_tac s) (Data.get (Context.Proof ctxt))); +fun order_tac prems ctxt = + FIRST' (map (fn s => CHANGED o struct_tac s prems) (Data.get (Context.Proof ctxt))); (** Attribute **) @@ -349,7 +349,7 @@ (** Setup **) val setup = let val _ = OuterSyntax.add_parsers [printP] in - Method.add_methods [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac), + Method.add_methods [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac []), "normalisation of algebraic structure")] #> Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")] end; @@ -513,7 +513,7 @@ Simplifier.simproc thy name raw_ts proc)) procs); thy); fun add_solver name tac thy = (Simplifier.change_simpset_of thy (fn ss => ss addSolver - (mk_solver' name (fn ss => tac (MetaSimplifier.the_context ss)))); thy); + (mk_solver' name (fn ss => tac (MetaSimplifier.prems_of_ss ss) (MetaSimplifier.the_context ss)))); thy); in add_simprocs [ diff -r 0041117b756c -r 9a95634ab135 src/Provers/order.ML --- a/src/Provers/order.ML Tue Sep 25 12:16:15 2007 +0200 +++ b/src/Provers/order.ML Tue Sep 25 12:56:27 2007 +0200 @@ -37,9 +37,9 @@ (* Tactics *) val partial_tac: - (theory -> term -> (term * string * term) option) -> less_arith -> int -> tactic + (theory -> term -> (term * string * term) option) -> less_arith -> thm list -> int -> tactic val linear_tac: - (theory -> term -> (term * string * term) option) -> less_arith -> int -> tactic + (theory -> term -> (term * string * term) option) -> less_arith -> thm list -> int -> tactic end; structure Order_Tac: ORDER_TAC = @@ -411,7 +411,7 @@ where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=", other relation symbols cause an error message *) -fun gen_order_tac mkasm mkconcl decomp (less_thms : less_arith) = +fun gen_order_tac mkasm mkconcl decomp (less_thms : less_arith) prems = let @@ -1232,14 +1232,14 @@ SUBGOAL (fn (A, n, sign) => let val rfrees = map Free (rename_wrt_term A (Logic.strip_params A)) - val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) + val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) val C = subst_bounds (rfrees, Logic.strip_assums_concl A) val lesss = List.concat (ListPair.map (mkasm decomp less_thms sign) (Hs, 0 upto (length Hs - 1))) val prfs = gen_solve mkconcl sign (lesss, C); val (subgoals, prf) = mkconcl decomp less_thms sign C; in METAHYPS (fn asms => - let val thms = map (prove asms) prfs + let val thms = map (prove (prems @ asms)) prfs in rtac (prove thms prf) 1 end) n end handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n