[isabelle] Simplifier questions
Thanks for the help yesterday. Now I have some more questions, mostly about how
to control the rewriter more effectively. I have used ACL2 before, and when I
give it a rule of the form,
[| hyp1 ; ... ; hypN |] ==> lhs = rhs,
its simplifier will basically:
1. Try to match lhs against subterms in the goal, inside-out,
2. Upon finding a match, sigma, instantiate the hyps with sigma and try to
rewrite them to True using other rewrite rules,
3. If all hyps rewrite to True, replace the matched subterm with rhs/sigma.
Does Isabelle's simplifier use a similar strategy? If so, how does it handle
free variables in hypotheses? Also, is there any way to tell the simplifier to
only backwards chain a few times when trying to relieve certain hyps that might
be expensive or trigger looping? Is there a way to write syntactic conditions
as hypotheses, e.g., apply unless some variable has literally matched "0", etc.?
Finally, I've noticed that some theorems in the tutorial are presented with
outermost, universal quantifiers, e.g., they have the form !!x . foo(x,y). Is
there a reason to prefer this to just writing foo(x,y)?
Jared Davis <jared at cs.utexas.edu>
3600 Greystone Drive #604 - Austin, TX 78731
This archive was generated by a fusion of
Pipermail (Mailman edition) and