如何通过案例分析证明Isabelle/HOL中的逻辑条件为真或为假？

Question

我知道伊莎贝尔可以通过构造函数（例如列表）进行案例分析，但是

\n

有没有办法根据条件是真还是假来划分案例？

\n

例如，在证明以下引理时，我的逻辑（如以下无效语法中的无效证明所示）是，如果条件“x \xe2\x88\x88 A”为真，则证明会简化为微不足道的东西；当条件为假时（即“x \xe2\x88\x89 A”），它也会简化：

\n

lemma "(x \xe2\x88\x88 A \xe2\x88\xa8 x \xe2\x88\x88 B) \xe2\x88\xa7 (x \xe2\x88\x88 A \xe2\x88\xa8 x \xe2\x88\x88 C) \xe2\x9f\xb9 x \xe2\x88\x88 A \xe2\x88\xa8 (x \xe2\x88\x88 B \xe2\x88\xa7 x \xe2\x88\x88 C)"\nproof (case "x \xe2\x88\x88 A")\n  (* ... case true *)\n  show "x \xe2\x88\x88 A \xe2\x88\xa8 (x \xe2\x88\x88 B \xe2\x88\xa7 x \xe2\x88\x88 C)" by (rule disjI1)\nnext (* ... case false *)\n  have "x \xe2\x88\x88 B \xe2\x88\xa7 x \xe2\x88\x88 C" by simp\n  show "x \xe2\x88\x88 A \xe2\x88\xa8 (x \xe2\x88\x88 B \xe2\x88\xa7 x \xe2\x88\x88 C)" by (rule disjI2)\n

\n

但我不知道如何将英文的“案例分析”翻译成Isabelle。

\n

Isabelle/HOL中有没有办法通过条件的真假来表达这种案例分析？（截至 2021 年伊莎贝尔）

\n

（或者它是否需要额外的公理，例如排中律？）

\n

Answer 1

您几乎正确地猜出了语法，您可以为具有语法 的任何谓词编写案例证明proof (cases "<pred>")。

\n

对于您提供的示例：

\n

lemma "(x \xe2\x88\x88 A \xe2\x88\xa8 x \xe2\x88\x88 B) \xe2\x88\xa7 (x \xe2\x88\x88 A \xe2\x88\xa8 x \xe2\x88\x88 C) \xe2\x9f\xb9 x \xe2\x88\x88 A \xe2\x88\xa8 (x \xe2\x88\x88 B \xe2\x88\xa7 x \xe2\x88\x88 C)"\nproof (cases "x \xe2\x88\x88 A")\n  (* ... case true *)\n  case True\n  then show "x \xe2\x88\x88 A \xe2\x88\xa8 (x \xe2\x88\x88 B \xe2\x88\xa7 x \xe2\x88\x88 C)" by (rule disjI1)\nnext (* ... case false *)\n  case False\n  then have "x \xe2\x88\x88 B \xe2\x88\xa7 x \xe2\x88\x88 C" sorry (* by simp*)\n  then show "x \xe2\x88\x88 A \xe2\x88\xa8 (x \xe2\x88\x88 B \xe2\x88\xa7 x \xe2\x88\x88 C)" by (rule disjI2)\n

\n