qualified names for Lin_Arith tactics and simprocs
authorhaftmann
Mon May 11 15:57:29 2009 +0200 (2009-05-11)
changeset 3110126c7bb764a38
parent 31100 6a2e67fe4488
child 31102 f1e3100e6c49
qualified names for Lin_Arith tactics and simprocs
doc-src/HOL/HOL.tex
src/HOL/HoareParallel/OG_Examples.thy
src/HOL/NSA/HyperDef.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/int_arith.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/ex/Arith_Examples.thy
     1.1 --- a/doc-src/HOL/HOL.tex	Mon May 11 15:18:32 2009 +0200
     1.2 +++ b/doc-src/HOL/HOL.tex	Mon May 11 15:57:29 2009 +0200
     1.3 @@ -1427,7 +1427,7 @@
     1.4  provides a decision procedure for \emph{linear arithmetic}: formulae involving
     1.5  addition and subtraction. The simplifier invokes a weak version of this
     1.6  decision procedure automatically. If this is not sufficent, you can invoke the
     1.7 -full procedure \ttindex{linear_arith_tac} explicitly.  It copes with arbitrary
     1.8 +full procedure \ttindex{Lin_Arith.tac} explicitly.  It copes with arbitrary
     1.9  formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt
    1.10    min}, {\tt max} and numerical constants. Other subterms are treated as
    1.11  atomic, while subformulae not involving numerical types are ignored. Quantified
    1.12 @@ -1438,10 +1438,10 @@
    1.13  If {\tt k} is a numeral, then {\tt div k}, {\tt mod k} and
    1.14  {\tt k dvd} are also supported. The former two are eliminated
    1.15  by case distinctions, again blowing up the running time.
    1.16 -If the formula involves explicit quantifiers, \texttt{linear_arith_tac} may take
    1.17 +If the formula involves explicit quantifiers, \texttt{Lin_Arith.tac} may take
    1.18  super-exponential time and space.
    1.19  
    1.20 -If \texttt{linear_arith_tac} fails, try to find relevant arithmetic results in
    1.21 +If \texttt{Lin_Arith.tac} fails, try to find relevant arithmetic results in
    1.22  the library.  The theories \texttt{Nat} and \texttt{NatArith} contain
    1.23  theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}.
    1.24  Theory \texttt{Divides} contains theorems about \texttt{div} and
     2.1 --- a/src/HOL/HoareParallel/OG_Examples.thy	Mon May 11 15:18:32 2009 +0200
     2.2 +++ b/src/HOL/HoareParallel/OG_Examples.thy	Mon May 11 15:57:29 2009 +0200
     2.3 @@ -443,7 +443,7 @@
     2.4  --{* 32 subgoals left *}
     2.5  apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
     2.6  
     2.7 -apply(tactic {* TRYALL (linear_arith_tac @{context}) *})
     2.8 +apply(tactic {* TRYALL (Lin_Arith.tac @{context}) *})
     2.9  --{* 9 subgoals left *}
    2.10  apply (force simp add:less_Suc_eq)
    2.11  apply(drule sym)
     3.1 --- a/src/HOL/NSA/HyperDef.thy	Mon May 11 15:18:32 2009 +0200
     3.2 +++ b/src/HOL/NSA/HyperDef.thy	Mon May 11 15:57:29 2009 +0200
     3.3 @@ -351,7 +351,7 @@
     3.4    #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"})
     3.5    #> Simplifier.map_ss (fn simpset => simpset addsimprocs [Simplifier.simproc @{theory}
     3.6        "fast_hypreal_arith" ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
     3.7 -      (K Lin_Arith.lin_arith_simproc)]))
     3.8 +      (K Lin_Arith.simproc)]))
     3.9  *}
    3.10  
    3.11  
     4.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon May 11 15:18:32 2009 +0200
     4.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon May 11 15:57:29 2009 +0200
     4.3 @@ -172,7 +172,7 @@
     4.4  
     4.5      (* Canonical linear form for terms, formulae etc.. *)
     4.6  fun provelin ctxt t = Goal.prove ctxt [] [] t 
     4.7 -  (fn _ => EVERY [simp_tac lin_ss 1, TRY (linear_arith_tac ctxt 1)]);
     4.8 +  (fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]);
     4.9  fun linear_cmul 0 tm = zero 
    4.10    | linear_cmul n tm = case tm of  
    4.11        Const (@{const_name HOL.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
     5.1 --- a/src/HOL/Tools/int_arith.ML	Mon May 11 15:18:32 2009 +0200
     5.2 +++ b/src/HOL/Tools/int_arith.ML	Mon May 11 15:57:29 2009 +0200
     5.3 @@ -82,7 +82,7 @@
     5.4    Simplifier.simproc @{theory} "fast_int_arith"
     5.5       ["(m::'a::{ordered_idom,number_ring}) < n",
     5.6        "(m::'a::{ordered_idom,number_ring}) <= n",
     5.7 -      "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.lin_arith_simproc);
     5.8 +      "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
     5.9  
    5.10  val global_setup = Simplifier.map_simpset
    5.11    (fn simpset => simpset addsimprocs [fast_int_arith_simproc]);
     6.1 --- a/src/HOL/Tools/lin_arith.ML	Mon May 11 15:18:32 2009 +0200
     6.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon May 11 15:57:29 2009 +0200
     6.3 @@ -4,19 +4,12 @@
     6.4  HOL setup for linear arithmetic (see Provers/Arith/fast_lin_arith.ML).
     6.5  *)
     6.6  
     6.7 -signature BASIC_LIN_ARITH =
     6.8 -sig
     6.9 -  val lin_arith_simproc: simpset -> term -> thm option
    6.10 -  val fast_nat_arith_simproc: simproc
    6.11 -  val fast_arith_tac: Proof.context -> int -> tactic
    6.12 -  val fast_ex_arith_tac: Proof.context -> bool -> int -> tactic
    6.13 -  val linear_arith_tac: Proof.context -> int -> tactic
    6.14 -end;
    6.15 -
    6.16  signature LIN_ARITH =
    6.17  sig
    6.18 -  include BASIC_LIN_ARITH
    6.19    val pre_tac: Proof.context -> int -> tactic
    6.20 +  val simple_tac: Proof.context -> int -> tactic
    6.21 +  val tac: Proof.context -> int -> tactic
    6.22 +  val simproc: simpset -> term -> thm option
    6.23    val add_inj_thms: thm list -> Context.generic -> Context.generic
    6.24    val add_lessD: thm -> Context.generic -> Context.generic
    6.25    val add_simps: thm list -> Context.generic -> Context.generic
    6.26 @@ -240,15 +233,12 @@
    6.27  end handle Rat.DIVZERO => NONE;
    6.28  
    6.29  fun of_lin_arith_sort thy U =
    6.30 -  Sign.of_sort thy (U, ["Ring_and_Field.ordered_idom"]);
    6.31 +  Sign.of_sort thy (U, @{sort Ring_and_Field.ordered_idom});
    6.32  
    6.33 -fun allows_lin_arith sg (discrete : string list) (U as Type (D, [])) : bool * bool =
    6.34 -  if of_lin_arith_sort sg U then
    6.35 -    (true, D mem discrete)
    6.36 -  else (* special cases *)
    6.37 -    if D mem discrete then  (true, true)  else  (false, false)
    6.38 -  | allows_lin_arith sg discrete U =
    6.39 -  (of_lin_arith_sort sg U, false);
    6.40 +fun allows_lin_arith thy (discrete : string list) (U as Type (D, [])) : bool * bool =
    6.41 +      if of_lin_arith_sort thy U then (true, member (op =) discrete D)
    6.42 +      else if member (op =) discrete D then (true, true) else (false, false)
    6.43 +  | allows_lin_arith sg discrete U = (of_lin_arith_sort sg U, false);
    6.44  
    6.45  fun decomp_typecheck (thy, discrete, inj_consts) (T : typ, xxx) : decomp option =
    6.46    case T of
    6.47 @@ -284,7 +274,7 @@
    6.48    | domain_is_nat (_ $ (Const ("Not", _) $ (Const (_, T) $ _ $ _))) = nT T
    6.49    | domain_is_nat _                                                 = false;
    6.50  
    6.51 -fun number_of (n, T) = HOLogic.mk_number T n;
    6.52 +val mk_number = HOLogic.mk_number;
    6.53  
    6.54  (*---------------------------------------------------------------------------*)
    6.55  (* the following code performs splitting of certain constants (e.g. min,     *)
    6.56 @@ -779,8 +769,8 @@
    6.57  fun add_simps thms = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimps thms));
    6.58  fun add_simprocs procs = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimprocs procs));
    6.59  
    6.60 -fun fast_arith_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
    6.61 -val fast_ex_arith_tac = Fast_Arith.lin_arith_tac;
    6.62 +fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
    6.63 +val lin_arith_tac = Fast_Arith.lin_arith_tac;
    6.64  val trace = Fast_Arith.trace;
    6.65  val warning_count = Fast_Arith.warning_count;
    6.66  
    6.67 @@ -811,17 +801,7 @@
    6.68  fun add_arith_facts ss =
    6.69    add_prems (Arith_Data.get_arith_facts (MetaSimplifier.the_context ss)) ss;
    6.70  
    6.71 -val lin_arith_simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
    6.72 -
    6.73 -val fast_nat_arith_simproc =
    6.74 -  Simplifier.simproc (the_context ()) "fast_nat_arith"
    6.75 -    ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K lin_arith_simproc);
    6.76 -
    6.77 -(* Because of fast_nat_arith_simproc, the arithmetic solver is really only
    6.78 -useful to detect inconsistencies among the premises for subgoals which are
    6.79 -*not* themselves (in)equalities, because the latter activate
    6.80 -fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
    6.81 -solver all the time rather than add the additional check. *)
    6.82 +val simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
    6.83  
    6.84  
    6.85  (* generic refutation procedure *)
    6.86 @@ -871,7 +851,7 @@
    6.87  
    6.88  local
    6.89  
    6.90 -fun raw_arith_tac ctxt ex =
    6.91 +fun raw_tac ctxt ex =
    6.92    (* FIXME: K true should be replaced by a sensible test (perhaps "isSome o
    6.93       decomp sg"? -- but note that the test is applied to terms already before
    6.94       they are split/normalized) to speed things up in case there are lots of
    6.95 @@ -880,21 +860,21 @@
    6.96       (l <= min m n + k) = (l <= m+k & l <= n+k)
    6.97    *)
    6.98    refute_tac (K true)
    6.99 -    (* Splitting is also done inside fast_arith_tac, but not completely --   *)
   6.100 +    (* Splitting is also done inside simple_tac, but not completely --   *)
   6.101      (* split_tac may use split theorems that have not been implemented in    *)
   6.102 -    (* fast_arith_tac (cf. pre_decomp and split_once_items above), and       *)
   6.103 +    (* simple_tac (cf. pre_decomp and split_once_items above), and       *)
   6.104      (* split_limit may trigger.                                   *)
   6.105 -    (* Therefore splitting outside of fast_arith_tac may allow us to prove   *)
   6.106 -    (* some goals that fast_arith_tac alone would fail on.                   *)
   6.107 +    (* Therefore splitting outside of simple_tac may allow us to prove   *)
   6.108 +    (* some goals that simple_tac alone would fail on.                   *)
   6.109      (REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt)))
   6.110 -    (fast_ex_arith_tac ctxt ex);
   6.111 +    (lin_arith_tac ctxt ex);
   6.112  
   6.113  in
   6.114  
   6.115 -fun gen_linear_arith_tac ex ctxt = FIRST' [fast_arith_tac ctxt,
   6.116 -  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt ex];
   6.117 +fun gen_tac ex ctxt = FIRST' [simple_tac ctxt,
   6.118 +  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
   6.119  
   6.120 -val linear_arith_tac = gen_linear_arith_tac true;
   6.121 +val tac = gen_tac true;
   6.122  
   6.123  end;
   6.124  
   6.125 @@ -903,7 +883,13 @@
   6.126  
   6.127  val setup =
   6.128    init_arith_data #>
   6.129 -  Simplifier.map_ss (fn ss => ss addsimprocs [fast_nat_arith_simproc]
   6.130 +  Simplifier.map_ss (fn ss => ss addsimprocs [Simplifier.simproc (@{theory}) "fast_nat_arith"
   6.131 +    ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K simproc)]
   6.132 +    (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
   6.133 +    useful to detect inconsistencies among the premises for subgoals which are
   6.134 +    *not* themselves (in)equalities, because the latter activate
   6.135 +    fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
   6.136 +    solver all the time rather than add the additional check. *)
   6.137      addSolver (mk_solver' "lin_arith"
   6.138        (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)))
   6.139  
   6.140 @@ -915,10 +901,7 @@
   6.141      (Args.bang_facts >> (fn prems => fn ctxt =>
   6.142        METHOD (fn facts =>
   6.143          HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
   6.144 -          THEN' linear_arith_tac ctxt)))) "linear arithmetic" #>
   6.145 -  Arith_Data.add_tactic "linear arithmetic" gen_linear_arith_tac;
   6.146 +          THEN' tac ctxt)))) "linear arithmetic" #>
   6.147 +  Arith_Data.add_tactic "linear arithmetic" gen_tac;
   6.148  
   6.149  end;
   6.150 -
   6.151 -structure Basic_Lin_Arith: BASIC_LIN_ARITH = Lin_Arith;
   6.152 -open Basic_Lin_Arith;
     7.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Mon May 11 15:18:32 2009 +0200
     7.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Mon May 11 15:57:29 2009 +0200
     7.3 @@ -516,7 +516,7 @@
     7.4        val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
     7.5        val pos = less $ zero $ t and neg = less $ t $ zero
     7.6        fun prove p =
     7.7 -        Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p)
     7.8 +        Option.map Eq_True_elim (Lin_Arith.simproc ss p)
     7.9          handle THM _ => NONE
    7.10      in case prove pos of
    7.11           SOME th => SOME(th RS pos_th)
     8.1 --- a/src/HOL/ex/Arith_Examples.thy	Mon May 11 15:18:32 2009 +0200
     8.2 +++ b/src/HOL/ex/Arith_Examples.thy	Mon May 11 15:57:29 2009 +0200
     8.3 @@ -13,18 +13,18 @@
     8.4    distribution.  This file merely contains some additional tests and special
     8.5    corner cases.  Some rather technical remarks:
     8.6  
     8.7 -  @{ML fast_arith_tac} is a very basic version of the tactic.  It performs no
     8.8 +  @{ML Lin_Arith.simple_tac} is a very basic version of the tactic.  It performs no
     8.9    meta-to-object-logic conversion, and only some splitting of operators.
    8.10 -  @{ML linear_arith_tac} performs meta-to-object-logic conversion, full
    8.11 +  @{ML Lin_Arith.tac} performs meta-to-object-logic conversion, full
    8.12    splitting of operators, and NNF normalization of the goal.  The @{text arith}
    8.13    method combines them both, and tries other methods (e.g.~@{text presburger})
    8.14    as well.  This is the one that you should use in your proofs!
    8.15  
    8.16    An @{text arith}-based simproc is available as well (see @{ML
    8.17 -  Lin_Arith.lin_arith_simproc}), which---for performance
    8.18 -  reasons---however does even less splitting than @{ML fast_arith_tac}
    8.19 +  Lin_Arith.simproc}), which---for performance
    8.20 +  reasons---however does even less splitting than @{ML Lin_Arith.simple_tac}
    8.21    at the moment (namely inequalities only).  (On the other hand, it
    8.22 -  does take apart conjunctions, which @{ML fast_arith_tac} currently
    8.23 +  does take apart conjunctions, which @{ML Lin_Arith.simple_tac} currently
    8.24    does not do.)
    8.25  *}
    8.26  
    8.27 @@ -208,13 +208,13 @@
    8.28  (*        preprocessing negates the goal and tries to compute its negation *)
    8.29  (*        normal form, which creates lots of separate cases for this       *)
    8.30  (*        disjunction of conjunctions                                      *)
    8.31 -(* by (tactic {* linear_arith_tac 1 *}) *)
    8.32 +(* by (tactic {* Lin_Arith.tac 1 *}) *)
    8.33  oops
    8.34  
    8.35  lemma "2 * (x::nat) ~= 1"
    8.36  (* FIXME: this is beyond the scope of the decision procedure at the moment, *)
    8.37  (*        because its negation is satisfiable in the rationals?             *)
    8.38 -(* by (tactic {* fast_arith_tac 1 *}) *)
    8.39 +(* by (tactic {* Lin_Arith.simple_tac 1 *}) *)
    8.40  oops
    8.41  
    8.42  text {* Constants. *}