Email Gateway (Aug 22 2022 at 17:54): Email Gateway (Aug 22 2022 at 17:54):From: 王淑灵 <wangsl@ios.ac.cn>
Dear Isabelle list,
In Isabelle, I find that the primcorec declarations implicitly introduce the simplication rules. As a result, the definitions of the primcorec functions are always unfolded by default. However, I hope in certain proof the definition of some preimcorec function not be unfolded. How should this be done? Thank you very much for your help.
Best regards,
Shuling Wang
SKLCS, Institute of Software, Chinese Academy of Sciences
Email Gateway (Aug 22 2022 at 17:54):From: Simon Wimmer <wimmersimon@gmail.com>
Hi Shuling,
to delete the simplification rules for primcorec f from the simpset, you
can use:
lemmas [simp del] = f.simps
Simon
Email Gateway (Aug 22 2022 at 17:54):From: 王淑灵 <wangsl@ios.ac.cn>
Hi Simon,
Thank you very much. It works perfectly.
Best,
Shuling
Best regards,
Shuling Wang
SKLCS, Institute of Software, Chinese Academy of Sciences
Last updated: Nov 21 2024 at 12:39 UTC