merged
authornipkow
Mon Feb 09 22:15:37 2009 +0100 (2009-02-09)
changeset 2985155ddff2ed906
parent 29848 a7c164e228e1
parent 29850 14d9891c917b
child 29854 708c1c7c87ec
merged
     1.1 --- a/src/HOL/Nat.thy	Mon Feb 09 17:25:07 2009 +1100
     1.2 +++ b/src/HOL/Nat.thy	Mon Feb 09 22:15:37 2009 +0100
     1.3 @@ -1336,12 +1336,19 @@
     1.4  use "Tools/arith_data.ML"
     1.5  declaration {* K ArithData.setup *}
     1.6  
     1.7 +ML{*
     1.8 +structure ArithFacts =
     1.9 +  NamedThmsFun(val name = "arith"
    1.10 +               val description = "arith facts - only ground formulas");
    1.11 +*}
    1.12 +
    1.13 +setup ArithFacts.setup
    1.14 +
    1.15  use "Tools/lin_arith.ML"
    1.16  declaration {* K LinArith.setup *}
    1.17  
    1.18  lemmas [arith_split] = nat_diff_split split_min split_max
    1.19  
    1.20 -
    1.21  context order
    1.22  begin
    1.23  
     2.1 --- a/src/HOL/Tools/lin_arith.ML	Mon Feb 09 17:25:07 2009 +1100
     2.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon Feb 09 22:15:37 2009 +0100
     2.3 @@ -814,11 +814,14 @@
     2.4        addsimprocs ArithData.nat_cancel_sums_add}) #>
     2.5    arith_discrete "nat";
     2.6  
     2.7 -val lin_arith_simproc = Fast_Arith.lin_arith_simproc;
     2.8 +fun add_arith_facts ss =
     2.9 +  add_prems (ArithFacts.get (MetaSimplifier.the_context ss)) ss;
    2.10 +
    2.11 +val lin_arith_simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
    2.12  
    2.13  val fast_nat_arith_simproc =
    2.14    Simplifier.simproc (the_context ()) "fast_nat_arith"
    2.15 -    ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K Fast_Arith.lin_arith_simproc);
    2.16 +    ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K lin_arith_simproc);
    2.17  
    2.18  (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
    2.19  useful to detect inconsistencies among the premises for subgoals which are
    2.20 @@ -912,7 +915,8 @@
    2.21  fun arith_method src =
    2.22    Method.syntax Args.bang_facts src
    2.23    #> (fn (prems, ctxt) => Method.METHOD (fn facts =>
    2.24 -      HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac ctxt)));
    2.25 +      HEADGOAL (Method.insert_tac (prems @ ArithFacts.get ctxt @ facts)
    2.26 +      THEN' arith_tac ctxt)));
    2.27  
    2.28  end;
    2.29  
    2.30 @@ -922,7 +926,8 @@
    2.31  val setup =
    2.32    init_arith_data #>
    2.33    Simplifier.map_ss (fn ss => ss addsimprocs [fast_nat_arith_simproc]
    2.34 -    addSolver (mk_solver' "lin_arith" Fast_Arith.cut_lin_arith_tac)) #>
    2.35 +    addSolver (mk_solver' "lin_arith"
    2.36 +      (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) #>
    2.37    Context.mapping
    2.38     (setup_options #>
    2.39      Method.add_methods