Stream: Beginner Questions

Topic: limit number of rewrites in simplifier


view this post on Zulip Jason Hu (Sep 06 2022 at 20:39):

how do I ask a recursive simplification lemma to be used only once (or other specified number of times) in the simplifier?

I have a goal at this moment which requires rewrites from X to Y, unfortunately, Y contains a subterm that can again be simplified, which can then be simplified, and then ... it never finishes. I would like to cut off the process in the first step.

a dumb example (not exactly mine) is that I want to rewrite 2 to 1 + 2 - 1, but not 1 + 1 + 1 + ... - 1 - 1 - 1. Is that possible to do this?

view this post on Zulip Wenda Li (Sep 07 2022 at 04:10):

How about the subst tactic?

lemma foo:"(2::int) = 1 + 2 - 1" by auto

lemma "(1+2-1) + 1 = (2::int) +1"
  apply (subst (2) foo)
  by (rule refl)

where the argument '(2)' after subst indicates that the second match (within the goal) of the LHS of foo will be replaced with the RHS.

view this post on Zulip Lukas Stevens (Sep 07 2022 at 07:58):

In this case subst is probably sufficient but note that there is also rewrite which has a more fine-grained interface. You can look at the examples in $ISABELLE_HOME/src/HOL/ex/Rewrite_Examples.thy.

view this post on Zulip Jason Hu (Sep 10 2022 at 03:25):

I am not sure why subst (1) doesn't really rewrite the outermost expression, but rewrite does do the work. thx a lot


Last updated: Mar 29 2024 at 12:28 UTC