Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
authorballarin
Tue Sep 25 12:56:27 2007 +0200 (2007-09-25)
changeset 247049a95634ab135
parent 24703 0041117b756c
child 24705 8e77a023d080
Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
src/HOL/Orderings.thy
src/Provers/order.ML
     1.1 --- a/src/HOL/Orderings.thy	Tue Sep 25 12:16:15 2007 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Tue Sep 25 12:56:27 2007 +0200
     1.3 @@ -243,7 +243,7 @@
     1.4  sig
     1.5    val print_structures: Proof.context -> unit
     1.6    val setup: theory -> theory
     1.7 -  val order_tac: Proof.context -> int -> tactic
     1.8 +  val order_tac: thm list -> Proof.context -> int -> tactic
     1.9  end;
    1.10  
    1.11  structure Orders: ORDERS =
    1.12 @@ -283,7 +283,7 @@
    1.13  
    1.14  (** Method **)
    1.15  
    1.16 -fun struct_tac ((s, [eq, le, less]), thms) =
    1.17 +fun struct_tac ((s, [eq, le, less]), thms) prems =
    1.18    let
    1.19      fun decomp thy (Trueprop $ t) =
    1.20        let
    1.21 @@ -306,13 +306,13 @@
    1.22        in dec t end;
    1.23    in
    1.24      case s of
    1.25 -      "order" => Order_Tac.partial_tac decomp thms
    1.26 -    | "linorder" => Order_Tac.linear_tac decomp thms
    1.27 +      "order" => Order_Tac.partial_tac decomp thms prems
    1.28 +    | "linorder" => Order_Tac.linear_tac decomp thms prems
    1.29      | _ => error ("Unknown kind of order `" ^ s ^ "' encountered in transitivity reasoner.")
    1.30    end
    1.31  
    1.32 -fun order_tac ctxt =
    1.33 -  FIRST' (map (fn s => CHANGED o struct_tac s) (Data.get (Context.Proof ctxt)));
    1.34 +fun order_tac prems ctxt =
    1.35 +  FIRST' (map (fn s => CHANGED o struct_tac s prems) (Data.get (Context.Proof ctxt)));
    1.36  
    1.37  
    1.38  (** Attribute **)
    1.39 @@ -349,7 +349,7 @@
    1.40  (** Setup **)
    1.41  
    1.42  val setup = let val _ = OuterSyntax.add_parsers [printP] in
    1.43 -    Method.add_methods [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac),
    1.44 +    Method.add_methods [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac []),
    1.45        "normalisation of algebraic structure")] #>
    1.46      Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")]
    1.47    end;
    1.48 @@ -513,7 +513,7 @@
    1.49        Simplifier.simproc thy name raw_ts proc)) procs); thy);
    1.50  fun add_solver name tac thy =
    1.51    (Simplifier.change_simpset_of thy (fn ss => ss addSolver
    1.52 -    (mk_solver' name (fn ss => tac (MetaSimplifier.the_context ss)))); thy);
    1.53 +    (mk_solver' name (fn ss => tac (MetaSimplifier.prems_of_ss ss) (MetaSimplifier.the_context ss)))); thy);
    1.54  
    1.55  in
    1.56    add_simprocs [
     2.1 --- a/src/Provers/order.ML	Tue Sep 25 12:16:15 2007 +0200
     2.2 +++ b/src/Provers/order.ML	Tue Sep 25 12:56:27 2007 +0200
     2.3 @@ -37,9 +37,9 @@
     2.4  
     2.5    (* Tactics *)
     2.6    val partial_tac:
     2.7 -    (theory -> term -> (term * string * term) option) -> less_arith -> int -> tactic
     2.8 +    (theory -> term -> (term * string * term) option) -> less_arith -> thm list -> int -> tactic
     2.9    val linear_tac:
    2.10 -    (theory -> term -> (term * string * term) option) -> less_arith -> int -> tactic
    2.11 +    (theory -> term -> (term * string * term) option) -> less_arith -> thm list -> int -> tactic
    2.12  end;
    2.13  
    2.14  structure Order_Tac: ORDER_TAC =
    2.15 @@ -411,7 +411,7 @@
    2.16       where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=",
    2.17       other relation symbols cause an error message *)
    2.18  
    2.19 -fun gen_order_tac mkasm mkconcl decomp (less_thms : less_arith) =
    2.20 +fun gen_order_tac mkasm mkconcl decomp (less_thms : less_arith) prems =
    2.21  
    2.22  let
    2.23  
    2.24 @@ -1232,14 +1232,14 @@
    2.25      SUBGOAL (fn (A, n, sign) =>
    2.26       let
    2.27        val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
    2.28 -      val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
    2.29 +      val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
    2.30        val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
    2.31        val lesss = List.concat (ListPair.map (mkasm decomp less_thms sign) (Hs, 0 upto (length Hs - 1)))
    2.32        val prfs = gen_solve mkconcl sign (lesss, C);
    2.33        val (subgoals, prf) = mkconcl decomp less_thms sign C;
    2.34       in
    2.35        METAHYPS (fn asms =>
    2.36 -	let val thms = map (prove asms) prfs
    2.37 +	let val thms = map (prove (prems @ asms)) prfs
    2.38  	in rtac (prove thms prf) 1 end) n
    2.39       end
    2.40       handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n