# HG changeset patch # User nipkow # Date 1234214137 -3600 # Node ID 55ddff2ed906ecc56a0ed41d586eb2049a1a5e3d # Parent a7c164e228e1d808bbbeb8ac86e99e2c3e3f5dc2# Parent 14d9891c917b15bbd025f4d40d6d7443bfa3a7e6 merged diff -r a7c164e228e1 -r 55ddff2ed906 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Mon Feb 09 17:25:07 2009 +1100 +++ b/src/HOL/Nat.thy Mon Feb 09 22:15:37 2009 +0100 @@ -1336,12 +1336,19 @@ use "Tools/arith_data.ML" declaration {* K ArithData.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 *} lemmas [arith_split] = nat_diff_split split_min split_max - context order begin diff -r a7c164e228e1 -r 55ddff2ed906 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Mon Feb 09 17:25:07 2009 +1100 +++ b/src/HOL/Tools/lin_arith.ML Mon Feb 09 22:15:37 2009 +0100 @@ -814,11 +814,14 @@ addsimprocs ArithData.nat_cancel_sums_add}) #> arith_discrete "nat"; -val lin_arith_simproc = Fast_Arith.lin_arith_simproc; +fun add_arith_facts ss = + add_prems (ArithFacts.get (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 Fast_Arith.lin_arith_simproc); + ["(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 @@ -912,7 +915,8 @@ fun arith_method src = Method.syntax Args.bang_facts src #> (fn (prems, ctxt) => Method.METHOD (fn facts => - HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac ctxt))); + HEADGOAL (Method.insert_tac (prems @ ArithFacts.get ctxt @ facts) + THEN' arith_tac ctxt))); end; @@ -922,7 +926,8 @@ val setup = init_arith_data #> Simplifier.map_ss (fn ss => ss addsimprocs [fast_nat_arith_simproc] - addSolver (mk_solver' "lin_arith" Fast_Arith.cut_lin_arith_tac)) #> + addSolver (mk_solver' "lin_arith" + (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) #> Context.mapping (setup_options #> Method.add_methods