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

【问题标题】：How to prove by case analysis on a logical condition being either true or false in Isabelle/HOL?如何通过案例分析证明 Isabelle/HOL 中的逻辑条件是真还是假？
【发布时间】：2021-04-04 15:24:20
【问题描述】：

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

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

例如，在证明以下引理时，我的逻辑（如以下无效语法中的无效证明所示）是，如果条件“x ∈ A”为真，则证明简化为微不足道的事情；它还简化了条件为假时（即“x ∉ A”）：

lemma "(x ∈ A ∨ x ∈ B) ∧ (x ∈ A ∨ x ∈ C) ⟹ x ∈ A ∨ (x ∈ B ∧ x ∈ C)"
proof (case "x ∈ A")
  (* ... case true *)
  show "x ∈ A ∨ (x ∈ B ∧ x ∈ C)" by (rule disjI1)
next (* ... case false *)
  have "x ∈ B ∧ x ∈ C" by simp
  show "x ∈ A ∨ (x ∈ B ∧ x ∈ C)" by (rule disjI2)

但是我不知道怎么把这个英文“案例分析”翻译成Isabelle。

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

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

【问题讨论】：

请注意，之前有人问过非常相似的问题：例如，请参阅stackoverflow.com/questions/13751358/case-analysis-in-isabelle 和stackoverflow.com/questions/60683091/…。我不会将此问题标记为重复，因为它添加了更多详细信息和明确的示例。尽管如此，我们还是鼓励您在发布新问题之前仔细阅读之前的问答。
@user9716869 谢谢。我实际上已经阅读了第一篇文章，它是关于列表构造函数的案例（如我的问题中所述）。我在这里问的是一个逻辑条件。我不确定第二个。它似乎与函数定义有关。我会阅读更多关于它的内容。

标签： isabelle

【解决方案1】：

您几乎猜对了语法，您可以为语法为proof (cases "<pred>") 的任何谓词编写逐例证明。

对于您提供的示例：

lemma "(x ∈ A ∨ x ∈ B) ∧ (x ∈ A ∨ x ∈ C) ⟹ x ∈ A ∨ (x ∈ B ∧ x ∈ C)"
proof (cases "x ∈ A")
  (* ... case true *)
  case True
  then show "x ∈ A ∨ (x ∈ B ∧ x ∈ C)" by (rule disjI1)
next (* ... case false *)
  case False
  then have "x ∈ B ∧ x ∈ C" sorry (* by simp*)
  then show "x ∈ A ∨ (x ∈ B ∧ x ∈ C)" by (rule disjI2)

【讨论】：

附录：对于 Isabelle2021，方法 cases 在 Isabelle/Isar 参考手册 (Isar-ref) 的第 6.5.2 节中进行了说明。