[isabelle] Fwd: (no subject)
Thanks Konrad and Stephan,
I wasn't aware of the "A Monadic Interpretation of Tactics" paper, it
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-
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
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
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