clarified prems_lin_arith_tac, with subtle change of semantics: structured prems are inserted as well;
--- a/src/HOL/Tools/lin_arith.ML Mon Feb 27 15:48:02 2012 +0100
+++ b/src/HOL/Tools/lin_arith.ML Mon Feb 27 16:05:51 2012 +0100
@@ -901,7 +901,7 @@
val setup =
init_arith_data #>
Simplifier.map_ss (fn ss => ss
- addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)));
+ addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.prems_lin_arith_tac)));
val global_setup =
Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))
--- a/src/Provers/Arith/fast_lin_arith.ML Mon Feb 27 15:48:02 2012 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Mon Feb 27 16:05:51 2012 +0100
@@ -1,9 +1,7 @@
(* Title: Provers/Arith/fast_lin_arith.ML
Author: Tobias Nipkow and Tjark Weber and Sascha Boehme
-A generic linear arithmetic package. It provides two tactics
-(cut_lin_arith_tac, lin_arith_tac) and a simplification procedure
-(lin_arith_simproc).
+A generic linear arithmetic package.
Only take premises and conclusions into account that are already
(negated) (in)equations. lin_arith_simproc tries to prove or disprove
@@ -88,7 +86,7 @@
signature FAST_LIN_ARITH =
sig
- val cut_lin_arith_tac: simpset -> int -> tactic
+ val prems_lin_arith_tac: simpset -> int -> tactic
val lin_arith_tac: Proof.context -> bool -> int -> tactic
val lin_arith_simproc: simpset -> term -> thm option
val map_data:
@@ -846,8 +844,8 @@
refute_tac ss (i, split_neq, js))
end);
-fun cut_lin_arith_tac ss =
- cut_facts_tac (Simplifier.prems_of ss) THEN'
+fun prems_lin_arith_tac ss =
+ Method.insert_tac (Simplifier.prems_of ss) THEN'
simpset_lin_arith_tac ss false;
fun lin_arith_tac ctxt =