*** empty log message ***
authornipkow
Sun Apr 06 10:08:52 2003 +0200 (2003-04-06)
changeset 1389912c7029d278b
parent 13898 9410d2eb9563
child 13900 0cfdeb44621e
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Sat Apr 05 22:14:04 2003 +0200
     1.2 +++ b/NEWS	Sun Apr 06 10:08:52 2003 +0200
     1.3 @@ -103,6 +103,25 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* arith(_tac)
     1.8 +
     1.9 + - Produces a counter example if it cannot prove a goal.
    1.10 +   Note that the counter example may be spurious if the goal is not a formula
    1.11 +   of quantifier-free linear arithmetic.
    1.12 +   In ProofGeneral the counter example appears in the trace buffer.
    1.13 +
    1.14 + - Knows about div k and mod k where k is a numeral of type nat or int.
    1.15 +
    1.16 + - Calls full Presburger arithmetic (by Amine Chaieb) if quantifier-free
    1.17 +   linear arithmetic fails. This takes account of quantifiers and divisibility.
    1.18 +   Presburger arithmetic can also be called explicitly via presburger(_tac). 
    1.19 +
    1.20 +* simp's arithmetic capabilities have been enhanced a bit: it now
    1.21 +takes ~= in premises into account (by performing a case split);
    1.22 +
    1.23 +* simp reduces "m*(n div m) + n mod m" to n, even if the two summands
    1.24 +are distributed over a sum of terms;
    1.25 +
    1.26  * New tactic "trans_tac" and method "trans" instantiate
    1.27  Provers/linorder.ML for axclasses "order" and "linorder" (predicates
    1.28  "<=", "<" and "="). 
    1.29 @@ -119,32 +138,13 @@
    1.30  * attribute [symmetric] now works for relations as well; it turns
    1.31  (x,y) : R^-1 into (y,x) : R, and vice versa;
    1.32  
    1.33 -* arith(_tac) now produces a counter example if it cannot prove a theorem.
    1.34 -  In ProofGeneral the counter example appears in the trace buffer.
    1.35 -
    1.36 -* arith(_tac) does now know about div k and mod k where k is a numeral
    1.37 -of type nat or int. It can solve simple goals like
    1.38 -
    1.39 -  "0 < n ==> n div 2 < (n::nat)"
    1.40 -
    1.41 -but fails if divisibility plays a role like in
    1.42 -
    1.43 -  "n div 2 + (n+1) div 2 = (n::nat)"
    1.44 -
    1.45 -* New method / tactic presburger(_tac) for full Presburger arithmetic
    1.46 -  (by Amine Chaieb). Integrated with arith(_tac), i.e. presburger(_tac)
    1.47 -  is called automatically by arith(_tac), if the decision procedure for
    1.48 -  simple arithmetic fails to solve the goal.
    1.49 -
    1.50 -* simp's arithmetic capabilities have been enhanced a bit: it now
    1.51 -takes ~= in premises into account (by performing a case split);
    1.52 -
    1.53 -* simp reduces "m*(n div m) + n mod m" to n, even if the two summands
    1.54 -are distributed over a sum of terms;
    1.55 -
    1.56  * induct over a !!-quantified statement (say !!x1..xn):
    1.57    each "case" automatically performs "fix x1 .. xn" with exactly those names.
    1.58  
    1.59 +* Map: `empty' is no longer a constant but a syntactic abbreviation for
    1.60 +%x. None. Warning: empty_def now refers to the previously hidden definition
    1.61 +of the empty set.
    1.62 +
    1.63  * Real/HahnBanach: updated and adapted to locales;
    1.64  
    1.65  * GroupTheory: converted to Isar theories, using locales with implicit