Stream: Beginner Questions

Topic: unfold, but just once


view this post on Zulip 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?

view this post on Zulip Mathias Fleury (Feb 06 2021 at 06:20):

apply (subst n)

view this post on Zulip Mathias Fleury (Feb 06 2021 at 06:22):

if you need to direct it more:

apply (subst [(asm)][(position)] n)

(asm) = substitute in assumpition
(position) = substitute at position e.g. (1), (10), ...

view this post on Zulip 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: Sep 25 2022 at 23:25 UTC