src/HOL/Arith.ML
changeset 6073 fba734ba6894
parent 6059 aa00e235ea27
child 6075 c148037f53c6
     1.1 --- a/src/HOL/Arith.ML	Fri Jan 08 14:02:04 1999 +0100
     1.2 +++ b/src/HOL/Arith.ML	Sat Jan 09 15:24:11 1999 +0100
     1.3 @@ -855,6 +855,13 @@
     1.4  val not_lessD = leI;
     1.5  val sym = sym;
     1.6  
     1.7 +fun mkEqTrue thm = thm RS (eqTrueI RS eq_reflection);
     1.8 +val mk_Trueprop = HOLogic.mk_Trueprop;
     1.9 +
    1.10 +fun neg_prop(TP$(Const("Not",_)$t)) = (TP$t, true)
    1.11 +  | neg_prop(TP$t) =
    1.12 +      (TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t), false);
    1.13 +
    1.14  (* Turn term into list of summand * multiplicity plus a constant *)
    1.15  fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))
    1.16    | poly(Const("op +",_) $ s $ t, pi) = poly(s,poly(t,pi))
    1.17 @@ -916,9 +923,29 @@
    1.18  
    1.19  structure Fast_Nat_Arith = Fast_Lin_Arith(Nat_LA_Data);
    1.20  
    1.21 -simpset_ref () := (simpset() addSolver Fast_Nat_Arith.cut_lin_arith_tac);
    1.22 +val fast_nat_arith_tac = Fast_Nat_Arith.lin_arith_tac;
    1.23 +
    1.24 +local
    1.25 +fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.boolT);
    1.26 +
    1.27 +val pats = map prep_pat
    1.28 +  ["(m::nat) < n","(m::nat) <= n", "~ (m::nat) < n","~ (m::nat) <= n",
    1.29 +   "(m::nat) = n"]
    1.30  
    1.31 -val fast_nat_arith_tac = Fast_Nat_Arith.lin_arith_tac;
    1.32 +in
    1.33 +val fast_nat_arith_simproc =
    1.34 +  mk_simproc "fast_nat_arith" pats Fast_Nat_Arith.lin_arith_prover;
    1.35 +end;
    1.36 +
    1.37 +Addsimprocs [fast_nat_arith_simproc];
    1.38 +
    1.39 +(* Because of fast_nat_arith_simproc, the arithmetic solver is really only
    1.40 +useful to detect inconsistencies among the premises for subgoals which are
    1.41 +*not* themselves (in)equalities, because the latter activate
    1.42 +fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
    1.43 +solver all the time rather than add the additional check. *)
    1.44 +
    1.45 +simpset_ref () := (simpset() addSolver Fast_Nat_Arith.cut_lin_arith_tac);
    1.46  
    1.47  (* Elimination of `-' on nat due to John Harrison *)
    1.48  Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";