Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Simplifier questions

Email Gateway (Aug 18 2022 at 09:41):

From: Jared Davis <jared@cs.utexas.edu>
Hi,

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)?

Thanks,
Jared

Email Gateway (Aug 18 2022 at 09:41):

From: Tobias Nipkow <nipkow@in.tum.de>

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

Last updated: May 03 2024 at 04:19 UTC