Re: [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
Does Isabelle's simplifier use a similar strategy?
If so, how does it
handle free variables in hypotheses?
They can be instantiated by matching with assumptions.
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?
ML"simp_depth_limit := 5"
Is there a way
to write syntactic conditions as hypotheses, e.g., apply unless some
variable has literally matched "0", etc.?
This archive was generated by a fusion of
Pipermail (Mailman edition) and