[isabelle] Fwd: (no subject)

Thanks Konrad and Stephan,

I wasn't aware of the "A Monadic Interpretation of Tactics" paper, it looks interesting.

Konrad writes:
Backtracking during rewriting seems a nightmare, on
both efficiency and understandability grounds, but maybe you have evidence to the contrary?

The use case for supporting multiple congruence rules per constant that Matt and I have discussing, is to emulate ACL2's equivalence- based rewriting:


ACL2 can support simplifying a subterm with respect to multiple equivalence relations, and uses a separate congruence rule to propagate each equivalence to the appropriate arguments of the subterm.

I don't think that supporting multiple congruence rules per constant would require Isabelle's full prolog-style backtracking across schematic variable bindings. Instead, it would just backtrack in the same way as is done for conditional rewrite rules. If a congruence fails, you try the next congruence. When you find a congruence that succeeds, you just start from the beginning again, using the simplified term.


On Mar 2, 2006, at 1:40 AM, Stefan Berghofer wrote:

John Matthews wrote:
Matt Kaufmann and I are interested in how Isabelle's simplifier handles the case where there are multiple congruence rules that match a particular subterm. Does it try all the rules in some order, or does it just pick one?

The simplifier currently only allows one congruence rule per constant.
See section 10.2.6 of the Isabelle reference manual for more information.


Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.