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 rhs/sigma.

Does Isabelle's simplifier use a similar strategy?

Yes.

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?

Eg:
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.?

No.

Tobias






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