summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | berghofe |

Tue, 01 Oct 2002 15:03:28 +0200 | |

changeset 13618 | 12290bdce807 |

parent 13617 | 1430360d9782 |

child 13619 | 584291949c23 |

Added some comments on new simplifier.

--- a/NEWS Tue Oct 01 14:45:28 2002 +0200 +++ b/NEWS Tue Oct 01 15:03:28 2002 +0200 @@ -6,6 +6,38 @@ *** General *** +* Provers/simplifier: + + - Completely reimplemented Asm_full_simp_tac: + Assumptions are now subject to complete mutual simplification, + not just from left to right. The simplifier now preserves + the order of assumptions. + + Potential INCOMPATIBILITY: + + -- Asm_full_simp_tac sometimes diverges where the old version did + not, e.g. invoking Asm_full_simp_tac on the goal + + [| P (f x); y = x; f x = f y |] ==> Q + + now gives rise to the infinite reduction sequence + + P (f x) --(f x = f y)--> P (f y) --(y = x)--> P (f x) --(f x = f y)--> ... + + Using Asm_lr_simp_tac (or "simp (asm_lr)" in Isabelle/Isar) instead + often solves this kind of problem. + + -- Tactics combining classical reasoner and simplification (such + as auto) are also affected by this change, because many of them + rely on Asm_full_simp_tac. They may sometimes diverge as well + or yield a different numbers of subgoals. Try to use e.g. force, + fastsimp, or safe instead of auto in case of problems. Sometimes + subsequent calls to the classical reasoner will fail because a + preceeding call to the simplifier too eagerly simplified the + goal, e.g. deleted redundant premises. + + - The simplifier trace now shows the names of the applied rewrite rules + * Pure: locale specifications now produce predicate definitions according to the body of text (covering assumptions modulo local definitions); predicate "loc_axioms" covers newly introduced text, @@ -72,8 +104,6 @@ * simp reduces "m*(n div m) + n mod m" to n, even if the two summands are distributed over a sum of terms; -* the simplifier trace now shows the names of the applied rewrite rules - * induct over a !!-quantified statement (say !!x1..xn): each "case" automatically performs "fix x1 .. xn" with exactly those names.