summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 13899 | 12c7029d278b |

parent 13881 | f63e2a057fd4 |

child 13938 | b033b53d0c1e |

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