在Isabelle/HOL中，如何通过案例分析证明逻辑条件是正确的还是错误的？
在Isabelle/HOL中，如何通过案例分析证明逻辑条件是正确的还是错误的？
提问于 2021-04-04 15:24:20
我知道伊莎贝尔可以通过构造函数(例如列表)进行案例分析，但是
是否有一种方法可以根据某一条件的真假分为几种情况？
例如，在证明以下引理时，我的逻辑(如下无效语法中的无效证明所示)是，如果条件"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)但我不知道如何把英语中的“案例分析”翻译成伊莎贝尔。
伊莎贝尔/霍尔是否有办法用一个条件的真伪来表达这种案例分析？(截至伊莎贝尔2021年)
(或者它是否需要附加的公理，如排除的中间定律？)
回答 1
Stack Overflow用户
回答已采纳
发布于 2021-04-05 03:56:57
您几乎正确地猜到了语法，您可以为语法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)页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/66942832
复制相关文章
相似问题
腾讯云开发者
