# 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