Re: [isabelle] (no subject)
The HOL-4 simplifier, which is similar to the one in Isabelle, just
picks one of the
matching congruence rules. No backtracking. In the mid-90's I met
(at Oxford) who wanted to make the Isabelle-style simplifier a
Not sure if he ever implemented it ... googling ...
Hmm ... this has a whisper about backtracking and rewriting, but is
tactic algebra and monads. Also, I think I recall Amy Felty having a
rewriter. However I don't remember if her work dealt with congruence
rules. I think it
didn't, having mostly to do with higher order rewriting where there
could be multiple
matches on a single rewrite rule and you might like to backtrack through
the different substitutions. Backtracking during rewriting seems a
both efficiency and understandability grounds, but maybe you have
evidence to the contrary?
On Mar 1, 2006, at 2:11 PM, 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and