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?
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), ...
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: Sep 25 2022 at 23:25 UTC