Email Gateway (Aug 18 2022 at 13:06): Email Gateway (Aug 18 2022 at 13:06):From: Tobias Nipkow <nipkow@in.tum.de>
unfold is brute-force unfolding, not stopped by if-then-else.
Please read the section 3.5.3 Simplication in the Tutorial, it explains
how to avoid your simp problems.
Tobias
Email Gateway (Aug 18 2022 at 13:06):From: Brian Huffman <brianh@cs.pdx.edu>
The "unfold" method applies rewrite rules repeatedly, just like simp.
(Internally "unfold" is actually implemented as a call to the
simplifier, but with most of the fancy features disabled.)
To avoid the looping, you can either apply (subst f.simps), to rewrite
exactly one step; or you can use unfold with an instantiated rule,
e.g. apply (unfold f.simps [of n]).
Hope this helps,
Quoting Tim Kremann <twkrema@orion.ncsc.mil>:
Last updated: May 03 2024 at 08:18 UTC