isabelle - 伊莎贝尔案例分析

Question

如何在 Isabelle 中应用案例分析？我正在寻找类似于apply (induct x)（用于归纳）的东西。

Answer 1

案例分析通常使用cases方法进行（另见Isabelle2014的Isabelle/Isar参考手册索引中的“案例（方法）” ）。如果您是初学者，我推荐使用Isabelle/HOL 中的编程和证明教程。

请注意，自 Isabelle 2014 以来，文档也可在文档面板的 Isabelle/jEdit IDE 中找到。