moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
authorhaftmann
Mon Mar 23 19:01:16 2009 +0100 (2009-03-23)
changeset 3068647a32dd1b86e
parent 30685 dd5fe091ff04
child 30687 16f6efd4e599
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
doc-src/HOL/HOL.tex
src/HOL/HoareParallel/OG_Examples.thy
src/HOL/Nat.thy
src/HOL/Presburger.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/arith_data.ML
src/HOL/Tools/function_package/scnp_reconstruct.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Word/WordArith.thy
src/HOL/ex/Arith_Examples.thy
     1.1 --- a/doc-src/HOL/HOL.tex	Mon Mar 23 19:01:15 2009 +0100
     1.2 +++ b/doc-src/HOL/HOL.tex	Mon Mar 23 19:01:16 2009 +0100
     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{arith_tac} explicitly.  It copes with arbitrary
     1.8 +full procedure \ttindex{linear_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{arith_tac} may take
    1.17 +If the formula involves explicit quantifiers, \texttt{linear_arith_tac} may take
    1.18  super-exponential time and space.
    1.19  
    1.20 -If \texttt{arith_tac} fails, try to find relevant arithmetic results in
    1.21 +If \texttt{linear_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 Mar 23 19:01:15 2009 +0100
     2.2 +++ b/src/HOL/HoareParallel/OG_Examples.thy	Mon Mar 23 19:01:16 2009 +0100
     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 (simple_arith_tac @{context}) *})
     2.8 +apply(tactic {* TRYALL (linear_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/Nat.thy	Mon Mar 23 19:01:15 2009 +0100
     3.2 +++ b/src/HOL/Nat.thy	Mon Mar 23 19:01:16 2009 +0100
     3.3 @@ -63,9 +63,8 @@
     3.4  end
     3.5  
     3.6  lemma Suc_not_Zero: "Suc m \<noteq> 0"
     3.7 -  apply (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def]
     3.8 +  by (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def]
     3.9      Rep_Nat [unfolded mem_def] Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def])
    3.10 -  done
    3.11  
    3.12  lemma Zero_not_Suc: "0 \<noteq> Suc m"
    3.13    by (rule not_sym, rule Suc_not_Zero not_sym)
    3.14 @@ -82,7 +81,7 @@
    3.15    done
    3.16  
    3.17  lemma nat_induct [case_names 0 Suc, induct type: nat]:
    3.18 -  -- {* for backward compatibility -- naming of variables differs *}
    3.19 +  -- {* for backward compatibility -- names of variables differ *}
    3.20    fixes n
    3.21    assumes "P 0"
    3.22      and "\<And>n. P n \<Longrightarrow> P (Suc n)"
    3.23 @@ -1345,19 +1344,13 @@
    3.24    shows "u = s"
    3.25    using 2 1 by (rule trans)
    3.26  
    3.27 +setup Arith_Data.setup
    3.28 +
    3.29  use "Tools/nat_arith.ML"
    3.30  declaration {* K Nat_Arith.setup *}
    3.31  
    3.32 -ML{*
    3.33 -structure ArithFacts =
    3.34 -  NamedThmsFun(val name = "arith"
    3.35 -               val description = "arith facts - only ground formulas");
    3.36 -*}
    3.37 -
    3.38 -setup ArithFacts.setup
    3.39 -
    3.40  use "Tools/lin_arith.ML"
    3.41 -declaration {* K LinArith.setup *}
    3.42 +declaration {* K Lin_Arith.setup *}
    3.43  
    3.44  lemmas [arith_split] = nat_diff_split split_min split_max
    3.45  
     4.1 --- a/src/HOL/Presburger.thy	Mon Mar 23 19:01:15 2009 +0100
     4.2 +++ b/src/HOL/Presburger.thy	Mon Mar 23 19:01:16 2009 +0100
     4.3 @@ -439,12 +439,7 @@
     4.4  
     4.5  use "Tools/Qelim/presburger.ML"
     4.6  
     4.7 -declaration {* fn _ =>
     4.8 -  arith_tactic_add
     4.9 -    (mk_arith_tactic "presburger" (fn ctxt => fn i => fn st =>
    4.10 -       (warning "Trying Presburger arithmetic ...";   
    4.11 -    Presburger.cooper_tac true [] [] ctxt i st)))
    4.12 -*}
    4.13 +setup {* Arith_Data.add_tactic "Presburger arithmetic" (K (Presburger.cooper_tac true [] [])) *}
    4.14  
    4.15  method_setup presburger = {*
    4.16  let
     5.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon Mar 23 19:01:15 2009 +0100
     5.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Mar 23 19:01:16 2009 +0100
     5.3 @@ -172,7 +172,7 @@
     5.4  
     5.5      (* Canonical linear form for terms, formulae etc.. *)
     5.6  fun provelin ctxt t = Goal.prove ctxt [] [] t 
     5.7 -  (fn _ => EVERY [simp_tac lin_ss 1, TRY (simple_arith_tac ctxt 1)]);
     5.8 +  (fn _ => EVERY [simp_tac lin_ss 1, TRY (linear_arith_tac ctxt 1)]);
     5.9  fun linear_cmul 0 tm = zero 
    5.10    | linear_cmul n tm = case tm of  
    5.11        Const (@{const_name HOL.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
     6.1 --- a/src/HOL/Tools/TFL/post.ML	Mon Mar 23 19:01:15 2009 +0100
     6.2 +++ b/src/HOL/Tools/TFL/post.ML	Mon Mar 23 19:01:16 2009 +0100
     6.3 @@ -55,7 +55,7 @@
     6.4    Prim.postprocess strict
     6.5     {wf_tac     = REPEAT (ares_tac wfs 1),
     6.6      terminator = asm_simp_tac ss 1
     6.7 -                 THEN TRY (silent_arith_tac (Simplifier.the_context ss) 1 ORELSE
     6.8 +                 THEN TRY (Arith_Data.arith_tac (Simplifier.the_context ss) 1 ORELSE
     6.9                             fast_tac (cs addSDs [@{thm not0_implies_Suc}] addss ss) 1),
    6.10      simplifier = Rules.simpl_conv ss []};
    6.11  
     7.1 --- a/src/HOL/Tools/arith_data.ML	Mon Mar 23 19:01:15 2009 +0100
     7.2 +++ b/src/HOL/Tools/arith_data.ML	Mon Mar 23 19:01:16 2009 +0100
     7.3 @@ -6,6 +6,11 @@
     7.4  
     7.5  signature ARITH_DATA =
     7.6  sig
     7.7 +  val arith_tac: Proof.context -> int -> tactic
     7.8 +  val verbose_arith_tac: Proof.context -> int -> tactic
     7.9 +  val add_tactic: string -> (bool -> Proof.context -> int -> tactic) -> theory -> theory
    7.10 +  val get_arith_facts: Proof.context -> thm list
    7.11 +
    7.12    val prove_conv_nohyps: tactic list -> Proof.context -> term * term -> thm option
    7.13    val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
    7.14    val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
    7.15 @@ -14,11 +19,54 @@
    7.16    val trans_tac: thm option -> tactic
    7.17    val prep_simproc: string * string list * (theory -> simpset -> term -> thm option)
    7.18      -> simproc
    7.19 +
    7.20 +  val setup: theory -> theory
    7.21  end;
    7.22  
    7.23  structure Arith_Data: ARITH_DATA =
    7.24  struct
    7.25  
    7.26 +(* slots for pluging in arithmetic facts and tactics *)
    7.27 +
    7.28 +structure Arith_Facts = NamedThmsFun(
    7.29 +  val name = "arith"
    7.30 +  val description = "arith facts - only ground formulas"
    7.31 +);
    7.32 +
    7.33 +val get_arith_facts = Arith_Facts.get;
    7.34 +
    7.35 +structure Arith_Tactics = TheoryDataFun
    7.36 +(
    7.37 +  type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list;
    7.38 +  val empty = [];
    7.39 +  val copy = I;
    7.40 +  val extend = I;
    7.41 +  fun merge _ = AList.merge (op =) (K true);
    7.42 +);
    7.43 +
    7.44 +fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac)));
    7.45 +
    7.46 +fun gen_arith_tac verbose ctxt =
    7.47 +  let
    7.48 +    val tactics = (Arith_Tactics.get o ProofContext.theory_of) ctxt
    7.49 +    fun invoke (_, (name, tac)) k st = (if verbose
    7.50 +      then warning ("Trying " ^ name ^ "...") else ();
    7.51 +      tac verbose ctxt k st);
    7.52 +  in FIRST' (map invoke (rev tactics)) end;
    7.53 +
    7.54 +val arith_tac = gen_arith_tac false;
    7.55 +val verbose_arith_tac = gen_arith_tac true;
    7.56 +
    7.57 +val arith_method = Args.bang_facts >> (fn prems => fn ctxt =>
    7.58 +  METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts)
    7.59 +    THEN' verbose_arith_tac ctxt)));
    7.60 +
    7.61 +val setup = Arith_Facts.setup
    7.62 +  #> Method.setup @{binding arith} arith_method "various arithmetic decision procedures";
    7.63 +
    7.64 +
    7.65 +(* various auxiliary and legacy *)
    7.66 +
    7.67  fun prove_conv_nohyps tacs ctxt (t, u) =
    7.68    if t aconv u then NONE
    7.69    else let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
     8.1 --- a/src/HOL/Tools/function_package/scnp_reconstruct.ML	Mon Mar 23 19:01:15 2009 +0100
     8.2 +++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML	Mon Mar 23 19:01:16 2009 +0100
     8.3 @@ -197,7 +197,7 @@
     8.4                else if b <= a then @{thm pair_leqI2} else @{thm pair_leqI1}
     8.5            in
     8.6              rtac rule 1 THEN PRIMITIVE (Thm.elim_implies stored_thm)
     8.7 -            THEN (if tag_flag then arith_tac ctxt 1 else all_tac)
     8.8 +            THEN (if tag_flag then Arith_Data.verbose_arith_tac ctxt 1 else all_tac)
     8.9            end
    8.10  
    8.11          fun steps_tac MAX strict lq lp =
     9.1 --- a/src/HOL/Tools/lin_arith.ML	Mon Mar 23 19:01:15 2009 +0100
     9.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon Mar 23 19:01:16 2009 +0100
     9.3 @@ -6,13 +6,9 @@
     9.4  
     9.5  signature BASIC_LIN_ARITH =
     9.6  sig
     9.7 -  type arith_tactic
     9.8 -  val mk_arith_tactic: string -> (Proof.context -> int -> tactic) -> arith_tactic
     9.9 -  val eq_arith_tactic: arith_tactic * arith_tactic -> bool
    9.10    val arith_split_add: attribute
    9.11    val arith_discrete: string -> Context.generic -> Context.generic
    9.12    val arith_inj_const: string * typ -> Context.generic -> Context.generic
    9.13 -  val arith_tactic_add: arith_tactic -> Context.generic -> Context.generic
    9.14    val fast_arith_split_limit: int Config.T
    9.15    val fast_arith_neq_limit: int Config.T
    9.16    val lin_arith_pre_tac: Proof.context -> int -> tactic
    9.17 @@ -21,9 +17,7 @@
    9.18    val trace_arith: bool ref
    9.19    val lin_arith_simproc: simpset -> term -> thm option
    9.20    val fast_nat_arith_simproc: simproc
    9.21 -  val simple_arith_tac: Proof.context -> int -> tactic
    9.22 -  val arith_tac: Proof.context -> int -> tactic
    9.23 -  val silent_arith_tac: Proof.context -> int -> tactic
    9.24 +  val linear_arith_tac: Proof.context -> int -> tactic
    9.25  end;
    9.26  
    9.27  signature LIN_ARITH =
    9.28 @@ -39,7 +33,7 @@
    9.29    val setup: Context.generic -> Context.generic
    9.30  end;
    9.31  
    9.32 -structure LinArith: LIN_ARITH =
    9.33 +structure Lin_Arith: LIN_ARITH =
    9.34  struct
    9.35  
    9.36  (* Parameters data for general linear arithmetic functor *)
    9.37 @@ -72,7 +66,7 @@
    9.38    let val _ $ t = Thm.prop_of thm
    9.39    in t = Const("False",HOLogic.boolT) end;
    9.40  
    9.41 -fun is_nat(t) = fastype_of1 t = HOLogic.natT;
    9.42 +fun is_nat t = (fastype_of1 t = HOLogic.natT);
    9.43  
    9.44  fun mk_nat_thm sg t =
    9.45    let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
    9.46 @@ -83,49 +77,35 @@
    9.47  
    9.48  (* arith context data *)
    9.49  
    9.50 -datatype arith_tactic =
    9.51 -  ArithTactic of {name: string, tactic: Proof.context -> int -> tactic, id: stamp};
    9.52 -
    9.53 -fun mk_arith_tactic name tactic = ArithTactic {name = name, tactic = tactic, id = stamp ()};
    9.54 -
    9.55 -fun eq_arith_tactic (ArithTactic {id = id1, ...}, ArithTactic {id = id2, ...}) = (id1 = id2);
    9.56 -
    9.57  structure ArithContextData = GenericDataFun
    9.58  (
    9.59    type T = {splits: thm list,
    9.60              inj_consts: (string * typ) list,
    9.61 -            discrete: string list,
    9.62 -            tactics: arith_tactic list};
    9.63 -  val empty = {splits = [], inj_consts = [], discrete = [], tactics = []};
    9.64 +            discrete: string list};
    9.65 +  val empty = {splits = [], inj_consts = [], discrete = []};
    9.66    val extend = I;
    9.67    fun merge _
    9.68 -   ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1},
    9.69 -    {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) : T =
    9.70 +   ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1},
    9.71 +    {splits= splits2, inj_consts= inj_consts2, discrete= discrete2}) : T =
    9.72     {splits = Library.merge Thm.eq_thm_prop (splits1, splits2),
    9.73      inj_consts = Library.merge (op =) (inj_consts1, inj_consts2),
    9.74 -    discrete = Library.merge (op =) (discrete1, discrete2),
    9.75 -    tactics = Library.merge eq_arith_tactic (tactics1, tactics2)};
    9.76 +    discrete = Library.merge (op =) (discrete1, discrete2)};
    9.77  );
    9.78  
    9.79  val get_arith_data = ArithContextData.get o Context.Proof;
    9.80  
    9.81  val arith_split_add = Thm.declaration_attribute (fn thm =>
    9.82 -  ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
    9.83 +  ArithContextData.map (fn {splits, inj_consts, discrete} =>
    9.84      {splits = update Thm.eq_thm_prop thm splits,
    9.85 -     inj_consts = inj_consts, discrete = discrete, tactics = tactics}));
    9.86 -
    9.87 -fun arith_discrete d = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
    9.88 -  {splits = splits, inj_consts = inj_consts,
    9.89 -   discrete = update (op =) d discrete, tactics = tactics});
    9.90 +     inj_consts = inj_consts, discrete = discrete}));
    9.91  
    9.92 -fun arith_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
    9.93 -  {splits = splits, inj_consts = update (op =) c inj_consts,
    9.94 -   discrete = discrete, tactics= tactics});
    9.95 +fun arith_discrete d = ArithContextData.map (fn {splits, inj_consts, discrete} =>
    9.96 +  {splits = splits, inj_consts = inj_consts,
    9.97 +   discrete = update (op =) d discrete});
    9.98  
    9.99 -fun arith_tactic_add tac = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
   9.100 -  {splits = splits, inj_consts = inj_consts, discrete = discrete,
   9.101 -   tactics = update eq_arith_tactic tac tactics});
   9.102 -
   9.103 +fun arith_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete} =>
   9.104 +  {splits = splits, inj_consts = update (op =) c inj_consts,
   9.105 +   discrete = discrete});
   9.106  
   9.107  val (fast_arith_split_limit, setup1) = Attrib.config_int "fast_arith_split_limit" 9;
   9.108  val (fast_arith_neq_limit, setup2) = Attrib.config_int "fast_arith_neq_limit" 9;
   9.109 @@ -794,7 +774,7 @@
   9.110     Most of the work is done by the cancel tactics. *)
   9.111  
   9.112  val init_arith_data =
   9.113 - Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
   9.114 + map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
   9.115     {add_mono_thms = add_mono_thms @
   9.116      @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field},
   9.117      mult_mono_thms = mult_mono_thms,
   9.118 @@ -815,7 +795,7 @@
   9.119    arith_discrete "nat";
   9.120  
   9.121  fun add_arith_facts ss =
   9.122 -  add_prems (ArithFacts.get (MetaSimplifier.the_context ss)) ss;
   9.123 +  add_prems (Arith_Data.get_arith_facts (MetaSimplifier.the_context ss)) ss;
   9.124  
   9.125  val lin_arith_simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
   9.126  
   9.127 @@ -895,27 +875,16 @@
   9.128      (REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt)))
   9.129      (fast_ex_arith_tac ctxt ex);
   9.130  
   9.131 -fun more_arith_tacs ctxt =
   9.132 -  let val tactics = #tactics (get_arith_data ctxt)
   9.133 -  in FIRST' (map (fn ArithTactic {tactic, ...} => tactic ctxt) tactics) end;
   9.134 -
   9.135  in
   9.136  
   9.137 -fun simple_arith_tac ctxt = FIRST' [fast_arith_tac ctxt,
   9.138 -  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt true];
   9.139 -
   9.140 -fun arith_tac ctxt = FIRST' [fast_arith_tac ctxt,
   9.141 -  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt true,
   9.142 -  more_arith_tacs ctxt];
   9.143 +fun gen_linear_arith_tac ex ctxt = FIRST' [fast_arith_tac ctxt,
   9.144 +  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt ex];
   9.145  
   9.146 -fun silent_arith_tac ctxt = FIRST' [fast_arith_tac ctxt,
   9.147 -  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt false,
   9.148 -  more_arith_tacs ctxt];
   9.149 +val linear_arith_tac = gen_linear_arith_tac true;
   9.150  
   9.151 -val arith_method = Args.bang_facts >>
   9.152 -  (fn prems => fn ctxt => METHOD (fn facts =>
   9.153 -      HEADGOAL (Method.insert_tac (prems @ ArithFacts.get ctxt @ facts)
   9.154 -      THEN' arith_tac ctxt)));
   9.155 +val linarith_method = Args.bang_facts >> (fn prems => fn ctxt =>
   9.156 +  METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
   9.157 +    THEN' linear_arith_tac ctxt)));
   9.158  
   9.159  end;
   9.160  
   9.161 @@ -929,11 +898,12 @@
   9.162        (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) #>
   9.163    Context.mapping
   9.164     (setup_options #>
   9.165 -    Method.setup @{binding arith} arith_method "decide linear arithmetic" #>
   9.166 +    Arith_Data.add_tactic "linear arithmetic" gen_linear_arith_tac #>
   9.167 +    Method.setup @{binding linarith} linarith_method "linear arithmetic" #>
   9.168      Attrib.setup @{binding arith_split} (Scan.succeed arith_split_add)
   9.169        "declaration of split rules for arithmetic procedure") I;
   9.170  
   9.171  end;
   9.172  
   9.173 -structure BasicLinArith: BASIC_LIN_ARITH = LinArith;
   9.174 -open BasicLinArith;
   9.175 +structure Basic_Lin_Arith: BASIC_LIN_ARITH = Lin_Arith;
   9.176 +open Basic_Lin_Arith;
    10.1 --- a/src/HOL/Word/WordArith.thy	Mon Mar 23 19:01:15 2009 +0100
    10.2 +++ b/src/HOL/Word/WordArith.thy	Mon Mar 23 19:01:16 2009 +0100
    10.3 @@ -512,7 +512,7 @@
    10.4  
    10.5  fun uint_arith_tacs ctxt = 
    10.6    let
    10.7 -    fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty;
    10.8 +    fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
    10.9      val cs = local_claset_of ctxt;
   10.10      val ss = local_simpset_of ctxt;
   10.11    in 
   10.12 @@ -1075,7 +1075,7 @@
   10.13  
   10.14  fun unat_arith_tacs ctxt =   
   10.15    let
   10.16 -    fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty;
   10.17 +    fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
   10.18      val cs = local_claset_of ctxt;
   10.19      val ss = local_simpset_of ctxt;
   10.20    in 
    11.1 --- a/src/HOL/ex/Arith_Examples.thy	Mon Mar 23 19:01:15 2009 +0100
    11.2 +++ b/src/HOL/ex/Arith_Examples.thy	Mon Mar 23 19:01:16 2009 +0100
    11.3 @@ -1,5 +1,4 @@
    11.4  (*  Title:  HOL/ex/Arith_Examples.thy
    11.5 -    ID:     $Id$
    11.6      Author: Tjark Weber
    11.7  *)
    11.8  
    11.9 @@ -14,13 +13,13 @@
   11.10  
   11.11    @{ML fast_arith_tac} is a very basic version of the tactic.  It performs no
   11.12    meta-to-object-logic conversion, and only some splitting of operators.
   11.13 -  @{ML simple_arith_tac} performs meta-to-object-logic conversion, full
   11.14 +  @{ML linear_arith_tac} performs meta-to-object-logic conversion, full
   11.15    splitting of operators, and NNF normalization of the goal.  The @{text arith}
   11.16    method combines them both, and tries other methods (e.g.~@{text presburger})
   11.17    as well.  This is the one that you should use in your proofs!
   11.18  
   11.19    An @{text arith}-based simproc is available as well (see @{ML
   11.20 -  LinArith.lin_arith_simproc}), which---for performance
   11.21 +  Lin_Arith.lin_arith_simproc}), which---for performance
   11.22    reasons---however does even less splitting than @{ML fast_arith_tac}
   11.23    at the moment (namely inequalities only).  (On the other hand, it
   11.24    does take apart conjunctions, which @{ML fast_arith_tac} currently
   11.25 @@ -83,7 +82,7 @@
   11.26    by (tactic {* fast_arith_tac @{context} 1 *})
   11.27  
   11.28  lemma "!!x. ((x::nat) <= y) = (x - y = 0)"
   11.29 -  by (tactic {* simple_arith_tac @{context} 1 *})
   11.30 +  by (tactic {* linear_arith_tac @{context} 1 *})
   11.31  
   11.32  lemma "[| (x::nat) < y; d < 1 |] ==> x - y = d"
   11.33    by (tactic {* fast_arith_tac @{context} 1 *})
   11.34 @@ -140,34 +139,34 @@
   11.35  subsection {* Meta-Logic *}
   11.36  
   11.37  lemma "x < Suc y == x <= y"
   11.38 -  by (tactic {* simple_arith_tac @{context} 1 *})
   11.39 +  by (tactic {* linear_arith_tac @{context} 1 *})
   11.40  
   11.41  lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y"
   11.42 -  by (tactic {* simple_arith_tac @{context} 1 *})
   11.43 +  by (tactic {* linear_arith_tac @{context} 1 *})
   11.44  
   11.45  
   11.46  subsection {* Various Other Examples *}
   11.47  
   11.48  lemma "(x < Suc y) = (x <= y)"
   11.49 -  by (tactic {* simple_arith_tac @{context} 1 *})
   11.50 +  by (tactic {* linear_arith_tac @{context} 1 *})
   11.51  
   11.52  lemma "[| (x::nat) < y; y < z |] ==> x < z"
   11.53    by (tactic {* fast_arith_tac @{context} 1 *})
   11.54  
   11.55  lemma "(x::nat) < y & y < z ==> x < z"
   11.56 -  by (tactic {* simple_arith_tac @{context} 1 *})
   11.57 +  by (tactic {* linear_arith_tac @{context} 1 *})
   11.58  
   11.59  text {* This example involves no arithmetic at all, but is solved by
   11.60    preprocessing (i.e. NNF normalization) alone. *}
   11.61  
   11.62  lemma "(P::bool) = Q ==> Q = P"
   11.63 -  by (tactic {* simple_arith_tac @{context} 1 *})
   11.64 +  by (tactic {* linear_arith_tac @{context} 1 *})
   11.65  
   11.66  lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> min (x::nat) y = 0"
   11.67 -  by (tactic {* simple_arith_tac @{context} 1 *})
   11.68 +  by (tactic {* linear_arith_tac @{context} 1 *})
   11.69  
   11.70  lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> max (x::nat) y = x + y"
   11.71 -  by (tactic {* simple_arith_tac @{context} 1 *})
   11.72 +  by (tactic {* linear_arith_tac @{context} 1 *})
   11.73  
   11.74  lemma "[| (x::nat) ~= y; a + 2 = b; a < y; y < b; a < x; x < b |] ==> False"
   11.75    by (tactic {* fast_arith_tac @{context} 1 *})
   11.76 @@ -185,7 +184,7 @@
   11.77    by (tactic {* fast_arith_tac @{context} 1 *})
   11.78  
   11.79  lemma "[| (x::nat) < y; P (x - y) |] ==> P 0"
   11.80 -  by (tactic {* simple_arith_tac @{context} 1 *})
   11.81 +  by (tactic {* linear_arith_tac @{context} 1 *})
   11.82  
   11.83  lemma "(x - y) - (x::nat) = (x - x) - y"
   11.84    by (tactic {* fast_arith_tac @{context} 1 *})
   11.85 @@ -207,7 +206,7 @@
   11.86  (*        preprocessing negates the goal and tries to compute its negation *)
   11.87  (*        normal form, which creates lots of separate cases for this       *)
   11.88  (*        disjunction of conjunctions                                      *)
   11.89 -(* by (tactic {* simple_arith_tac 1 *}) *)
   11.90 +(* by (tactic {* linear_arith_tac 1 *}) *)
   11.91  oops
   11.92  
   11.93  lemma "2 * (x::nat) ~= 1"