# HG changeset patch # User haftmann # Date 1237831276 -3600 # Node ID 47a32dd1b86e397edd27862250bd92e398b18d0b # Parent dd5fe091ff0474c743bb49731c358f97c160d8c8 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 diff -r dd5fe091ff04 -r 47a32dd1b86e doc-src/HOL/HOL.tex --- a/doc-src/HOL/HOL.tex Mon Mar 23 19:01:15 2009 +0100 +++ b/doc-src/HOL/HOL.tex Mon Mar 23 19:01:16 2009 +0100 @@ -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{arith_tac} explicitly. It copes with arbitrary +full procedure \ttindex{linear_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{arith_tac} may take +If the formula involves explicit quantifiers, \texttt{linear_arith_tac} may take super-exponential time and space. -If \texttt{arith_tac} fails, try to find relevant arithmetic results in +If \texttt{linear_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 dd5fe091ff04 -r 47a32dd1b86e src/HOL/HoareParallel/OG_Examples.thy --- a/src/HOL/HoareParallel/OG_Examples.thy Mon Mar 23 19:01:15 2009 +0100 +++ b/src/HOL/HoareParallel/OG_Examples.thy Mon Mar 23 19:01:16 2009 +0100 @@ -443,7 +443,7 @@ --{* 32 subgoals left *} apply(tactic {* ALLGOALS (clarify_tac @{claset}) *}) -apply(tactic {* TRYALL (simple_arith_tac @{context}) *}) +apply(tactic {* TRYALL (linear_arith_tac @{context}) *}) --{* 9 subgoals left *} apply (force simp add:less_Suc_eq) apply(drule sym) diff -r dd5fe091ff04 -r 47a32dd1b86e src/HOL/Nat.thy --- a/src/HOL/Nat.thy Mon Mar 23 19:01:15 2009 +0100 +++ b/src/HOL/Nat.thy Mon Mar 23 19:01:16 2009 +0100 @@ -63,9 +63,8 @@ end lemma Suc_not_Zero: "Suc m \ 0" - apply (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def] + by (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def] Rep_Nat [unfolded mem_def] Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def]) - done lemma Zero_not_Suc: "0 \ Suc m" by (rule not_sym, rule Suc_not_Zero not_sym) @@ -82,7 +81,7 @@ done lemma nat_induct [case_names 0 Suc, induct type: nat]: - -- {* for backward compatibility -- naming of variables differs *} + -- {* for backward compatibility -- names of variables differ *} fixes n assumes "P 0" and "\n. P n \ P (Suc n)" @@ -1345,19 +1344,13 @@ shows "u = s" using 2 1 by (rule trans) +setup Arith_Data.setup + use "Tools/nat_arith.ML" declaration {* K Nat_Arith.setup *} -ML{* -structure ArithFacts = - NamedThmsFun(val name = "arith" - val description = "arith facts - only ground formulas"); -*} - -setup ArithFacts.setup - use "Tools/lin_arith.ML" -declaration {* K LinArith.setup *} +declaration {* K Lin_Arith.setup *} lemmas [arith_split] = nat_diff_split split_min split_max diff -r dd5fe091ff04 -r 47a32dd1b86e src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Mon Mar 23 19:01:15 2009 +0100 +++ b/src/HOL/Presburger.thy Mon Mar 23 19:01:16 2009 +0100 @@ -439,12 +439,7 @@ use "Tools/Qelim/presburger.ML" -declaration {* fn _ => - arith_tactic_add - (mk_arith_tactic "presburger" (fn ctxt => fn i => fn st => - (warning "Trying Presburger arithmetic ..."; - Presburger.cooper_tac true [] [] ctxt i st))) -*} +setup {* Arith_Data.add_tactic "Presburger arithmetic" (K (Presburger.cooper_tac true [] [])) *} method_setup presburger = {* let diff -r dd5fe091ff04 -r 47a32dd1b86e src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Mon Mar 23 19:01:15 2009 +0100 +++ b/src/HOL/Tools/Qelim/cooper.ML Mon Mar 23 19:01:16 2009 +0100 @@ -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 (simple_arith_tac ctxt 1)]); + (fn _ => EVERY [simp_tac lin_ss 1, TRY (linear_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 dd5fe091ff04 -r 47a32dd1b86e src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Mon Mar 23 19:01:15 2009 +0100 +++ b/src/HOL/Tools/TFL/post.ML Mon Mar 23 19:01:16 2009 +0100 @@ -55,7 +55,7 @@ Prim.postprocess strict {wf_tac = REPEAT (ares_tac wfs 1), terminator = asm_simp_tac ss 1 - THEN TRY (silent_arith_tac (Simplifier.the_context ss) 1 ORELSE + THEN TRY (Arith_Data.arith_tac (Simplifier.the_context ss) 1 ORELSE fast_tac (cs addSDs [@{thm not0_implies_Suc}] addss ss) 1), simplifier = Rules.simpl_conv ss []}; diff -r dd5fe091ff04 -r 47a32dd1b86e src/HOL/Tools/arith_data.ML --- a/src/HOL/Tools/arith_data.ML Mon Mar 23 19:01:15 2009 +0100 +++ b/src/HOL/Tools/arith_data.ML Mon Mar 23 19:01:16 2009 +0100 @@ -6,6 +6,11 @@ signature ARITH_DATA = sig + val arith_tac: Proof.context -> int -> tactic + val verbose_arith_tac: Proof.context -> int -> tactic + val add_tactic: string -> (bool -> Proof.context -> int -> tactic) -> theory -> theory + val get_arith_facts: Proof.context -> thm list + val prove_conv_nohyps: tactic list -> Proof.context -> term * term -> thm option val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm @@ -14,11 +19,54 @@ val trans_tac: thm option -> tactic val prep_simproc: string * string list * (theory -> simpset -> term -> thm option) -> simproc + + val setup: theory -> theory end; structure Arith_Data: ARITH_DATA = struct +(* slots for pluging in arithmetic facts and tactics *) + +structure Arith_Facts = NamedThmsFun( + val name = "arith" + val description = "arith facts - only ground formulas" +); + +val get_arith_facts = Arith_Facts.get; + +structure Arith_Tactics = TheoryDataFun +( + type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list; + val empty = []; + val copy = I; + val extend = I; + fun merge _ = AList.merge (op =) (K true); +); + +fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac))); + +fun gen_arith_tac verbose ctxt = + let + val tactics = (Arith_Tactics.get o ProofContext.theory_of) ctxt + fun invoke (_, (name, tac)) k st = (if verbose + then warning ("Trying " ^ name ^ "...") else (); + tac verbose ctxt k st); + in FIRST' (map invoke (rev tactics)) end; + +val arith_tac = gen_arith_tac false; +val verbose_arith_tac = gen_arith_tac true; + +val arith_method = Args.bang_facts >> (fn prems => fn ctxt => + METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts) + THEN' verbose_arith_tac ctxt))); + +val setup = Arith_Facts.setup + #> Method.setup @{binding arith} arith_method "various arithmetic decision procedures"; + + +(* various auxiliary and legacy *) + fun prove_conv_nohyps tacs ctxt (t, u) = if t aconv u then NONE else let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)) diff -r dd5fe091ff04 -r 47a32dd1b86e src/HOL/Tools/function_package/scnp_reconstruct.ML --- a/src/HOL/Tools/function_package/scnp_reconstruct.ML Mon Mar 23 19:01:15 2009 +0100 +++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML Mon Mar 23 19:01:16 2009 +0100 @@ -197,7 +197,7 @@ else if b <= a then @{thm pair_leqI2} else @{thm pair_leqI1} in rtac rule 1 THEN PRIMITIVE (Thm.elim_implies stored_thm) - THEN (if tag_flag then arith_tac ctxt 1 else all_tac) + THEN (if tag_flag then Arith_Data.verbose_arith_tac ctxt 1 else all_tac) end fun steps_tac MAX strict lq lp = diff -r dd5fe091ff04 -r 47a32dd1b86e src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Mon Mar 23 19:01:15 2009 +0100 +++ b/src/HOL/Tools/lin_arith.ML Mon Mar 23 19:01:16 2009 +0100 @@ -6,13 +6,9 @@ signature BASIC_LIN_ARITH = sig - type arith_tactic - val mk_arith_tactic: string -> (Proof.context -> int -> tactic) -> arith_tactic - val eq_arith_tactic: arith_tactic * arith_tactic -> bool val arith_split_add: attribute val arith_discrete: string -> Context.generic -> Context.generic val arith_inj_const: string * typ -> Context.generic -> Context.generic - val arith_tactic_add: arith_tactic -> Context.generic -> Context.generic val fast_arith_split_limit: int Config.T val fast_arith_neq_limit: int Config.T val lin_arith_pre_tac: Proof.context -> int -> tactic @@ -21,9 +17,7 @@ val trace_arith: bool ref val lin_arith_simproc: simpset -> term -> thm option val fast_nat_arith_simproc: simproc - val simple_arith_tac: Proof.context -> int -> tactic - val arith_tac: Proof.context -> int -> tactic - val silent_arith_tac: Proof.context -> int -> tactic + val linear_arith_tac: Proof.context -> int -> tactic end; signature LIN_ARITH = @@ -39,7 +33,7 @@ val setup: Context.generic -> Context.generic end; -structure LinArith: LIN_ARITH = +structure Lin_Arith: LIN_ARITH = struct (* Parameters data for general linear arithmetic functor *) @@ -72,7 +66,7 @@ let val _ $ t = Thm.prop_of thm in t = Const("False",HOLogic.boolT) end; -fun is_nat(t) = fastype_of1 t = HOLogic.natT; +fun is_nat t = (fastype_of1 t = HOLogic.natT); fun mk_nat_thm sg t = let val ct = cterm_of sg t and cn = cterm_of sg (Var(("n",0),HOLogic.natT)) @@ -83,49 +77,35 @@ (* arith context data *) -datatype arith_tactic = - ArithTactic of {name: string, tactic: Proof.context -> int -> tactic, id: stamp}; - -fun mk_arith_tactic name tactic = ArithTactic {name = name, tactic = tactic, id = stamp ()}; - -fun eq_arith_tactic (ArithTactic {id = id1, ...}, ArithTactic {id = id2, ...}) = (id1 = id2); - structure ArithContextData = GenericDataFun ( type T = {splits: thm list, inj_consts: (string * typ) list, - discrete: string list, - tactics: arith_tactic list}; - val empty = {splits = [], inj_consts = [], discrete = [], tactics = []}; + discrete: string list}; + val empty = {splits = [], inj_consts = [], discrete = []}; val extend = I; fun merge _ - ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1}, - {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) : T = + ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1}, + {splits= splits2, inj_consts= inj_consts2, discrete= discrete2}) : T = {splits = Library.merge Thm.eq_thm_prop (splits1, splits2), inj_consts = Library.merge (op =) (inj_consts1, inj_consts2), - discrete = Library.merge (op =) (discrete1, discrete2), - tactics = Library.merge eq_arith_tactic (tactics1, tactics2)}; + discrete = Library.merge (op =) (discrete1, discrete2)}; ); val get_arith_data = ArithContextData.get o Context.Proof; val arith_split_add = Thm.declaration_attribute (fn thm => - ArithContextData.map (fn {splits, inj_consts, discrete, tactics} => + ArithContextData.map (fn {splits, inj_consts, discrete} => {splits = update Thm.eq_thm_prop thm splits, - inj_consts = inj_consts, discrete = discrete, tactics = tactics})); - -fun arith_discrete d = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} => - {splits = splits, inj_consts = inj_consts, - discrete = update (op =) d discrete, tactics = tactics}); + inj_consts = inj_consts, discrete = discrete})); -fun arith_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} => - {splits = splits, inj_consts = update (op =) c inj_consts, - discrete = discrete, tactics= tactics}); +fun arith_discrete d = ArithContextData.map (fn {splits, inj_consts, discrete} => + {splits = splits, inj_consts = inj_consts, + discrete = update (op =) d discrete}); -fun arith_tactic_add tac = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} => - {splits = splits, inj_consts = inj_consts, discrete = discrete, - tactics = update eq_arith_tactic tac tactics}); - +fun arith_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete} => + {splits = splits, inj_consts = update (op =) c inj_consts, + discrete = discrete}); val (fast_arith_split_limit, setup1) = Attrib.config_int "fast_arith_split_limit" 9; val (fast_arith_neq_limit, setup2) = Attrib.config_int "fast_arith_neq_limit" 9; @@ -794,7 +774,7 @@ Most of the work is done by the cancel tactics. *) val init_arith_data = - Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} => + map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} => {add_mono_thms = add_mono_thms @ @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field}, mult_mono_thms = mult_mono_thms, @@ -815,7 +795,7 @@ arith_discrete "nat"; fun add_arith_facts ss = - add_prems (ArithFacts.get (MetaSimplifier.the_context ss)) 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; @@ -895,27 +875,16 @@ (REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt))) (fast_ex_arith_tac ctxt ex); -fun more_arith_tacs ctxt = - let val tactics = #tactics (get_arith_data ctxt) - in FIRST' (map (fn ArithTactic {tactic, ...} => tactic ctxt) tactics) end; - in -fun simple_arith_tac ctxt = FIRST' [fast_arith_tac ctxt, - ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt true]; - -fun arith_tac ctxt = FIRST' [fast_arith_tac ctxt, - ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt true, - more_arith_tacs ctxt]; +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 silent_arith_tac ctxt = FIRST' [fast_arith_tac ctxt, - ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt false, - more_arith_tacs ctxt]; +val linear_arith_tac = gen_linear_arith_tac true; -val arith_method = Args.bang_facts >> - (fn prems => fn ctxt => METHOD (fn facts => - HEADGOAL (Method.insert_tac (prems @ ArithFacts.get ctxt @ facts) - THEN' arith_tac ctxt))); +val linarith_method = 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))); end; @@ -929,11 +898,12 @@ (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) #> Context.mapping (setup_options #> - Method.setup @{binding arith} arith_method "decide linear arithmetic" #> + Arith_Data.add_tactic "linear arithmetic" gen_linear_arith_tac #> + Method.setup @{binding linarith} linarith_method "linear arithmetic" #> Attrib.setup @{binding arith_split} (Scan.succeed arith_split_add) "declaration of split rules for arithmetic procedure") I; end; -structure BasicLinArith: BASIC_LIN_ARITH = LinArith; -open BasicLinArith; +structure Basic_Lin_Arith: BASIC_LIN_ARITH = Lin_Arith; +open Basic_Lin_Arith; diff -r dd5fe091ff04 -r 47a32dd1b86e src/HOL/Word/WordArith.thy --- a/src/HOL/Word/WordArith.thy Mon Mar 23 19:01:15 2009 +0100 +++ b/src/HOL/Word/WordArith.thy Mon Mar 23 19:01:16 2009 +0100 @@ -512,7 +512,7 @@ fun uint_arith_tacs ctxt = let - fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty; + fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty; val cs = local_claset_of ctxt; val ss = local_simpset_of ctxt; in @@ -1075,7 +1075,7 @@ fun unat_arith_tacs ctxt = let - fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty; + fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty; val cs = local_claset_of ctxt; val ss = local_simpset_of ctxt; in diff -r dd5fe091ff04 -r 47a32dd1b86e src/HOL/ex/Arith_Examples.thy --- a/src/HOL/ex/Arith_Examples.thy Mon Mar 23 19:01:15 2009 +0100 +++ b/src/HOL/ex/Arith_Examples.thy Mon Mar 23 19:01:16 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/ex/Arith_Examples.thy - ID: $Id$ Author: Tjark Weber *) @@ -14,13 +13,13 @@ @{ML fast_arith_tac} is a very basic version of the tactic. It performs no meta-to-object-logic conversion, and only some splitting of operators. - @{ML simple_arith_tac} performs meta-to-object-logic conversion, full + @{ML linear_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 - LinArith.lin_arith_simproc}), which---for performance + Lin_Arith.lin_arith_simproc}), which---for performance reasons---however does even less splitting than @{ML fast_arith_tac} at the moment (namely inequalities only). (On the other hand, it does take apart conjunctions, which @{ML fast_arith_tac} currently @@ -83,7 +82,7 @@ by (tactic {* fast_arith_tac @{context} 1 *}) lemma "!!x. ((x::nat) <= y) = (x - y = 0)" - by (tactic {* simple_arith_tac @{context} 1 *}) + by (tactic {* linear_arith_tac @{context} 1 *}) lemma "[| (x::nat) < y; d < 1 |] ==> x - y = d" by (tactic {* fast_arith_tac @{context} 1 *}) @@ -140,34 +139,34 @@ subsection {* Meta-Logic *} lemma "x < Suc y == x <= y" - by (tactic {* simple_arith_tac @{context} 1 *}) + by (tactic {* linear_arith_tac @{context} 1 *}) lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y" - by (tactic {* simple_arith_tac @{context} 1 *}) + by (tactic {* linear_arith_tac @{context} 1 *}) subsection {* Various Other Examples *} lemma "(x < Suc y) = (x <= y)" - by (tactic {* simple_arith_tac @{context} 1 *}) + by (tactic {* linear_arith_tac @{context} 1 *}) lemma "[| (x::nat) < y; y < z |] ==> x < z" by (tactic {* fast_arith_tac @{context} 1 *}) lemma "(x::nat) < y & y < z ==> x < z" - by (tactic {* simple_arith_tac @{context} 1 *}) + by (tactic {* linear_arith_tac @{context} 1 *}) text {* This example involves no arithmetic at all, but is solved by preprocessing (i.e. NNF normalization) alone. *} lemma "(P::bool) = Q ==> Q = P" - by (tactic {* simple_arith_tac @{context} 1 *}) + by (tactic {* linear_arith_tac @{context} 1 *}) lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> min (x::nat) y = 0" - by (tactic {* simple_arith_tac @{context} 1 *}) + by (tactic {* linear_arith_tac @{context} 1 *}) lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> max (x::nat) y = x + y" - by (tactic {* simple_arith_tac @{context} 1 *}) + by (tactic {* linear_arith_tac @{context} 1 *}) lemma "[| (x::nat) ~= y; a + 2 = b; a < y; y < b; a < x; x < b |] ==> False" by (tactic {* fast_arith_tac @{context} 1 *}) @@ -185,7 +184,7 @@ by (tactic {* fast_arith_tac @{context} 1 *}) lemma "[| (x::nat) < y; P (x - y) |] ==> P 0" - by (tactic {* simple_arith_tac @{context} 1 *}) + by (tactic {* linear_arith_tac @{context} 1 *}) lemma "(x - y) - (x::nat) = (x - x) - y" by (tactic {* fast_arith_tac @{context} 1 *}) @@ -207,7 +206,7 @@ (* 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 {* simple_arith_tac 1 *}) *) +(* by (tactic {* linear_arith_tac 1 *}) *) oops lemma "2 * (x::nat) ~= 1"