[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
(512) 879-3858

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