author | berghofe |

Tue Oct 01 15:03:28 2002 +0200 (2002-10-01) | |

changeset 13618 | 12290bdce807 |

parent 13617 | 1430360d9782 |

child 13619 | 584291949c23 |

Added some comments on new simplifier.

1.1 --- a/NEWS Tue Oct 01 14:45:28 2002 +0200 1.2 +++ b/NEWS Tue Oct 01 15:03:28 2002 +0200 1.3 @@ -6,6 +6,38 @@ 1.4 1.5 *** General *** 1.6 1.7 +* Provers/simplifier: 1.8 + 1.9 + - Completely reimplemented Asm_full_simp_tac: 1.10 + Assumptions are now subject to complete mutual simplification, 1.11 + not just from left to right. The simplifier now preserves 1.12 + the order of assumptions. 1.13 + 1.14 + Potential INCOMPATIBILITY: 1.15 + 1.16 + -- Asm_full_simp_tac sometimes diverges where the old version did 1.17 + not, e.g. invoking Asm_full_simp_tac on the goal 1.18 + 1.19 + [| P (f x); y = x; f x = f y |] ==> Q 1.20 + 1.21 + now gives rise to the infinite reduction sequence 1.22 + 1.23 + P (f x) --(f x = f y)--> P (f y) --(y = x)--> P (f x) --(f x = f y)--> ... 1.24 + 1.25 + Using Asm_lr_simp_tac (or "simp (asm_lr)" in Isabelle/Isar) instead 1.26 + often solves this kind of problem. 1.27 + 1.28 + -- Tactics combining classical reasoner and simplification (such 1.29 + as auto) are also affected by this change, because many of them 1.30 + rely on Asm_full_simp_tac. They may sometimes diverge as well 1.31 + or yield a different numbers of subgoals. Try to use e.g. force, 1.32 + fastsimp, or safe instead of auto in case of problems. Sometimes 1.33 + subsequent calls to the classical reasoner will fail because a 1.34 + preceeding call to the simplifier too eagerly simplified the 1.35 + goal, e.g. deleted redundant premises. 1.36 + 1.37 + - The simplifier trace now shows the names of the applied rewrite rules 1.38 + 1.39 * Pure: locale specifications now produce predicate definitions 1.40 according to the body of text (covering assumptions modulo local 1.41 definitions); predicate "loc_axioms" covers newly introduced text, 1.42 @@ -72,8 +104,6 @@ 1.43 * simp reduces "m*(n div m) + n mod m" to n, even if the two summands 1.44 are distributed over a sum of terms; 1.45 1.46 -* the simplifier trace now shows the names of the applied rewrite rules 1.47 - 1.48 * induct over a !!-quantified statement (say !!x1..xn): 1.49 each "case" automatically performs "fix x1 .. xn" with exactly those names. 1.50