Jakub Kądziołka (Feb 06 2021 at 00:01): Jakub Kądziołka (Feb 06 2021 at 00:01):I have the following fact in my proof: "n = 2^multiplicity 2 n * k"
Further down, I would like to replace n in a goal with 2^multiplicity 2 n * k. However, both unfolding n and apply (unfold n) go into an infinite loop. How do I avoid that?
Mathias Fleury (Feb 06 2021 at 06:20):apply (subst n)
if you need to direct it more:
apply (subst [(asm)][(position)] n)
(asm) = substitute in assumpition
(position) = substitute at position e.g. (1), (10), ...
Mathias Fleury (Feb 06 2021 at 06:22):Rewrite is nicer to use (you can write a pattern instead of referring to the position), but not part of Main. See https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Rewrite_Examples.html for examples
Last updated: Nov 08 2025 at 08:25 UTC