--- a/doc-src/HOL/HOL.tex Mon May 11 15:18:32 2009 +0200
+++ b/doc-src/HOL/HOL.tex Mon May 11 15:57:29 2009 +0200
@@ -1427,7 +1427,7 @@
provides a decision procedure for \emph{linear arithmetic}: formulae involving
addition and subtraction. The simplifier invokes a weak version of this
decision procedure automatically. If this is not sufficent, you can invoke the
-full procedure \ttindex{linear_arith_tac} explicitly. It copes with arbitrary
+full procedure \ttindex{Lin_Arith.tac} explicitly. It copes with arbitrary
formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt
min}, {\tt max} and numerical constants. Other subterms are treated as
atomic, while subformulae not involving numerical types are ignored. Quantified
@@ -1438,10 +1438,10 @@
If {\tt k} is a numeral, then {\tt div k}, {\tt mod k} and
{\tt k dvd} are also supported. The former two are eliminated
by case distinctions, again blowing up the running time.
-If the formula involves explicit quantifiers, \texttt{linear_arith_tac} may take
+If the formula involves explicit quantifiers, \texttt{Lin_Arith.tac} may take
super-exponential time and space.
-If \texttt{linear_arith_tac} fails, try to find relevant arithmetic results in
+If \texttt{Lin_Arith.tac} fails, try to find relevant arithmetic results in
the library. The theories \texttt{Nat} and \texttt{NatArith} contain
theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}.
Theory \texttt{Divides} contains theorems about \texttt{div} and
--- a/src/HOL/HoareParallel/OG_Examples.thy Mon May 11 15:18:32 2009 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy Mon May 11 15:57:29 2009 +0200
@@ -443,7 +443,7 @@
--{* 32 subgoals left *}
apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
-apply(tactic {* TRYALL (linear_arith_tac @{context}) *})
+apply(tactic {* TRYALL (Lin_Arith.tac @{context}) *})
--{* 9 subgoals left *}
apply (force simp add:less_Suc_eq)
apply(drule sym)
--- a/src/HOL/NSA/HyperDef.thy Mon May 11 15:18:32 2009 +0200
+++ b/src/HOL/NSA/HyperDef.thy Mon May 11 15:57:29 2009 +0200
@@ -351,7 +351,7 @@
#> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"})
#> Simplifier.map_ss (fn simpset => simpset addsimprocs [Simplifier.simproc @{theory}
"fast_hypreal_arith" ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
- (K Lin_Arith.lin_arith_simproc)]))
+ (K Lin_Arith.simproc)]))
*}
--- a/src/HOL/Tools/Qelim/cooper.ML Mon May 11 15:18:32 2009 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Mon May 11 15:57:29 2009 +0200
@@ -172,7 +172,7 @@
(* Canonical linear form for terms, formulae etc.. *)
fun provelin ctxt t = Goal.prove ctxt [] [] t
- (fn _ => EVERY [simp_tac lin_ss 1, TRY (linear_arith_tac ctxt 1)]);
+ (fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]);
fun linear_cmul 0 tm = zero
| linear_cmul n tm = case tm of
Const (@{const_name HOL.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
--- a/src/HOL/Tools/int_arith.ML Mon May 11 15:18:32 2009 +0200
+++ b/src/HOL/Tools/int_arith.ML Mon May 11 15:57:29 2009 +0200
@@ -82,7 +82,7 @@
Simplifier.simproc @{theory} "fast_int_arith"
["(m::'a::{ordered_idom,number_ring}) < n",
"(m::'a::{ordered_idom,number_ring}) <= n",
- "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.lin_arith_simproc);
+ "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
val global_setup = Simplifier.map_simpset
(fn simpset => simpset addsimprocs [fast_int_arith_simproc]);
--- a/src/HOL/Tools/lin_arith.ML Mon May 11 15:18:32 2009 +0200
+++ b/src/HOL/Tools/lin_arith.ML Mon May 11 15:57:29 2009 +0200
@@ -4,19 +4,12 @@
HOL setup for linear arithmetic (see Provers/Arith/fast_lin_arith.ML).
*)
-signature BASIC_LIN_ARITH =
-sig
- val lin_arith_simproc: simpset -> term -> thm option
- val fast_nat_arith_simproc: simproc
- val fast_arith_tac: Proof.context -> int -> tactic
- val fast_ex_arith_tac: Proof.context -> bool -> int -> tactic
- val linear_arith_tac: Proof.context -> int -> tactic
-end;
-
signature LIN_ARITH =
sig
- include BASIC_LIN_ARITH
val pre_tac: Proof.context -> int -> tactic
+ val simple_tac: Proof.context -> int -> tactic
+ val tac: Proof.context -> int -> tactic
+ val simproc: simpset -> term -> thm option
val add_inj_thms: thm list -> Context.generic -> Context.generic
val add_lessD: thm -> Context.generic -> Context.generic
val add_simps: thm list -> Context.generic -> Context.generic
@@ -240,15 +233,12 @@
end handle Rat.DIVZERO => NONE;
fun of_lin_arith_sort thy U =
- Sign.of_sort thy (U, ["Ring_and_Field.ordered_idom"]);
+ Sign.of_sort thy (U, @{sort Ring_and_Field.ordered_idom});
-fun allows_lin_arith sg (discrete : string list) (U as Type (D, [])) : bool * bool =
- if of_lin_arith_sort sg U then
- (true, D mem discrete)
- else (* special cases *)
- if D mem discrete then (true, true) else (false, false)
- | allows_lin_arith sg discrete U =
- (of_lin_arith_sort sg U, false);
+fun allows_lin_arith thy (discrete : string list) (U as Type (D, [])) : bool * bool =
+ if of_lin_arith_sort thy U then (true, member (op =) discrete D)
+ else if member (op =) discrete D then (true, true) else (false, false)
+ | allows_lin_arith sg discrete U = (of_lin_arith_sort sg U, false);
fun decomp_typecheck (thy, discrete, inj_consts) (T : typ, xxx) : decomp option =
case T of
@@ -284,7 +274,7 @@
| domain_is_nat (_ $ (Const ("Not", _) $ (Const (_, T) $ _ $ _))) = nT T
| domain_is_nat _ = false;
-fun number_of (n, T) = HOLogic.mk_number T n;
+val mk_number = HOLogic.mk_number;
(*---------------------------------------------------------------------------*)
(* the following code performs splitting of certain constants (e.g. min, *)
@@ -779,8 +769,8 @@
fun add_simps thms = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimps thms));
fun add_simprocs procs = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimprocs procs));
-fun fast_arith_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
-val fast_ex_arith_tac = Fast_Arith.lin_arith_tac;
+fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
+val lin_arith_tac = Fast_Arith.lin_arith_tac;
val trace = Fast_Arith.trace;
val warning_count = Fast_Arith.warning_count;
@@ -811,17 +801,7 @@
fun add_arith_facts ss =
add_prems (Arith_Data.get_arith_facts (MetaSimplifier.the_context ss)) ss;
-val lin_arith_simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
-
-val fast_nat_arith_simproc =
- Simplifier.simproc (the_context ()) "fast_nat_arith"
- ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K lin_arith_simproc);
-
-(* Because of fast_nat_arith_simproc, the arithmetic solver is really only
-useful to detect inconsistencies among the premises for subgoals which are
-*not* themselves (in)equalities, because the latter activate
-fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
-solver all the time rather than add the additional check. *)
+val simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
(* generic refutation procedure *)
@@ -871,7 +851,7 @@
local
-fun raw_arith_tac ctxt ex =
+fun raw_tac ctxt ex =
(* FIXME: K true should be replaced by a sensible test (perhaps "isSome o
decomp sg"? -- but note that the test is applied to terms already before
they are split/normalized) to speed things up in case there are lots of
@@ -880,21 +860,21 @@
(l <= min m n + k) = (l <= m+k & l <= n+k)
*)
refute_tac (K true)
- (* Splitting is also done inside fast_arith_tac, but not completely -- *)
+ (* Splitting is also done inside simple_tac, but not completely -- *)
(* split_tac may use split theorems that have not been implemented in *)
- (* fast_arith_tac (cf. pre_decomp and split_once_items above), and *)
+ (* simple_tac (cf. pre_decomp and split_once_items above), and *)
(* split_limit may trigger. *)
- (* Therefore splitting outside of fast_arith_tac may allow us to prove *)
- (* some goals that fast_arith_tac alone would fail on. *)
+ (* Therefore splitting outside of simple_tac may allow us to prove *)
+ (* some goals that simple_tac alone would fail on. *)
(REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt)))
- (fast_ex_arith_tac ctxt ex);
+ (lin_arith_tac ctxt ex);
in
-fun gen_linear_arith_tac ex ctxt = FIRST' [fast_arith_tac ctxt,
- ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt ex];
+fun gen_tac ex ctxt = FIRST' [simple_tac ctxt,
+ ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
-val linear_arith_tac = gen_linear_arith_tac true;
+val tac = gen_tac true;
end;
@@ -903,7 +883,13 @@
val setup =
init_arith_data #>
- Simplifier.map_ss (fn ss => ss addsimprocs [fast_nat_arith_simproc]
+ Simplifier.map_ss (fn ss => ss addsimprocs [Simplifier.simproc (@{theory}) "fast_nat_arith"
+ ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K simproc)]
+ (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
+ useful to detect inconsistencies among the premises for subgoals which are
+ *not* themselves (in)equalities, because the latter activate
+ fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
+ solver all the time rather than add the additional check. *)
addSolver (mk_solver' "lin_arith"
(add_arith_facts #> Fast_Arith.cut_lin_arith_tac)))
@@ -915,10 +901,7 @@
(Args.bang_facts >> (fn prems => fn ctxt =>
METHOD (fn facts =>
HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
- THEN' linear_arith_tac ctxt)))) "linear arithmetic" #>
- Arith_Data.add_tactic "linear arithmetic" gen_linear_arith_tac;
+ THEN' tac ctxt)))) "linear arithmetic" #>
+ Arith_Data.add_tactic "linear arithmetic" gen_tac;
end;
-
-structure Basic_Lin_Arith: BASIC_LIN_ARITH = Lin_Arith;
-open Basic_Lin_Arith;
--- a/src/HOL/Tools/numeral_simprocs.ML Mon May 11 15:18:32 2009 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Mon May 11 15:57:29 2009 +0200
@@ -516,7 +516,7 @@
val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
val pos = less $ zero $ t and neg = less $ t $ zero
fun prove p =
- Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p)
+ Option.map Eq_True_elim (Lin_Arith.simproc ss p)
handle THM _ => NONE
in case prove pos of
SOME th => SOME(th RS pos_th)
--- a/src/HOL/ex/Arith_Examples.thy Mon May 11 15:18:32 2009 +0200
+++ b/src/HOL/ex/Arith_Examples.thy Mon May 11 15:57:29 2009 +0200
@@ -13,18 +13,18 @@
distribution. This file merely contains some additional tests and special
corner cases. Some rather technical remarks:
- @{ML fast_arith_tac} is a very basic version of the tactic. It performs no
+ @{ML Lin_Arith.simple_tac} is a very basic version of the tactic. It performs no
meta-to-object-logic conversion, and only some splitting of operators.
- @{ML linear_arith_tac} performs meta-to-object-logic conversion, full
+ @{ML Lin_Arith.tac} performs meta-to-object-logic conversion, full
splitting of operators, and NNF normalization of the goal. The @{text arith}
method combines them both, and tries other methods (e.g.~@{text presburger})
as well. This is the one that you should use in your proofs!
An @{text arith}-based simproc is available as well (see @{ML
- Lin_Arith.lin_arith_simproc}), which---for performance
- reasons---however does even less splitting than @{ML fast_arith_tac}
+ Lin_Arith.simproc}), which---for performance
+ reasons---however does even less splitting than @{ML Lin_Arith.simple_tac}
at the moment (namely inequalities only). (On the other hand, it
- does take apart conjunctions, which @{ML fast_arith_tac} currently
+ does take apart conjunctions, which @{ML Lin_Arith.simple_tac} currently
does not do.)
*}
@@ -208,13 +208,13 @@
(* preprocessing negates the goal and tries to compute its negation *)
(* normal form, which creates lots of separate cases for this *)
(* disjunction of conjunctions *)
-(* by (tactic {* linear_arith_tac 1 *}) *)
+(* by (tactic {* Lin_Arith.tac 1 *}) *)
oops
lemma "2 * (x::nat) ~= 1"
(* FIXME: this is beyond the scope of the decision procedure at the moment, *)
(* because its negation is satisfiable in the rationals? *)
-(* by (tactic {* fast_arith_tac 1 *}) *)
+(* by (tactic {* Lin_Arith.simple_tac 1 *}) *)
oops
text {* Constants. *}