如何在伊莎贝尔中应用案例分析？我一直在寻找类似于 apply (induct x) (用于归纳)的东西。
最佳答案
案例分析通常使用cases方法进行(另见Isabelle2014的Isabelle/Isar Reference manual索引中的“案例(方法)”)。如果你是初学者，我推荐教程Programming and Proving in Isabelle/HOL .
请注意，自 Isabelle 2014 起，该文档也可以在 Isabelle/jEdit IDE 的“文档”面板中找到。
关于isabelle - 伊莎贝尔案例分析，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/13751358/