# HG changeset patch
# User haftmann
# Date 1242050249 -7200
# Node ID 26c7bb764a389f07cdec209d9a167e1cba334139
# Parent  6a2e67fe448806608e4ecc3341b2b20b90254e39
qualified names for Lin_Arith tactics and simprocs

diff -r 6a2e67fe4488 -r 26c7bb764a38 doc-src/HOL/HOL.tex
--- 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
diff -r 6a2e67fe4488 -r 26c7bb764a38 src/HOL/HoareParallel/OG_Examples.thy
--- 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)
diff -r 6a2e67fe4488 -r 26c7bb764a38 src/HOL/NSA/HyperDef.thy
--- 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)]))
 *}
 
 
diff -r 6a2e67fe4488 -r 26c7bb764a38 src/HOL/Tools/Qelim/cooper.ML
--- 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
diff -r 6a2e67fe4488 -r 26c7bb764a38 src/HOL/Tools/int_arith.ML
--- 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]);
diff -r 6a2e67fe4488 -r 26c7bb764a38 src/HOL/Tools/lin_arith.ML
--- 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;
diff -r 6a2e67fe4488 -r 26c7bb764a38 src/HOL/Tools/numeral_simprocs.ML
--- 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)
diff -r 6a2e67fe4488 -r 26c7bb764a38 src/HOL/ex/Arith_Examples.thy
--- 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. *}