Jason Hu (Sep 06 2022 at 20:39): 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?
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.
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.
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: Nov 13 2025 at 08:29 UTC