author haftmann Mon May 11 15:57:29 2009 +0200 (2009-05-11) changeset 31101 26c7bb764a38 parent 31100 6a2e67fe4488 child 31102 f1e3100e6c49
qualified names for Lin_Arith tactics and simprocs
 doc-src/HOL/HOL.tex file | annotate | diff | revisions src/HOL/HoareParallel/OG_Examples.thy file | annotate | diff | revisions src/HOL/NSA/HyperDef.thy file | annotate | diff | revisions src/HOL/Tools/Qelim/cooper.ML file | annotate | diff | revisions src/HOL/Tools/int_arith.ML file | annotate | diff | revisions src/HOL/Tools/lin_arith.ML file | annotate | diff | revisions src/HOL/Tools/numeral_simprocs.ML file | annotate | diff | revisions src/HOL/ex/Arith_Examples.thy file | annotate | diff | revisions
     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.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.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.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. *}