Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] disable the simplication rule


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

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

view this post on Zulip 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: Mar 28 2024 at 20:16 UTC