如何在 Isabelle 中为子集做证明

Question

我正在尝试在 Isabelle 中手动做一些证明，但我正在努力处理以下证明： lemma "(A ∩ B) ∪ C ⊆ A ∪ C "

我正在尝试将其转换为命题逻辑然后证明它。

这就是我的尝试：

 lemma "(A ∩ B) ∪ C ⊆ A  ∪ C "
  apply (subst subset_iff)+
  apply(rule allI)
  apply (rule impI)
 (*here normally we should try to get rid of Union and Inter*)
  apply(subst Un_iff)+ 
  apply(subst  (asm)  Un_iff)+
  apply(subst Inter_iff) (*not working*)

我卡在了最后一步，有人可以帮我完成这个证明并解释如何找到正确的定理直到最后吗？

我使用 find_theorems，但它需要很多时间 + 到目前为止我发现的唯一有用（并且可以理解）的资源是这个 link： https://www.inf.ed.ac.uk/teaching/courses/ar/isabelle/FormalCheatSheet.pdf 和一些非常随机的讲义，内容与上面的 link 几乎相同...

我找到的其他资源有 100 多页，看起来不适合初学者...

提前致谢

Answer 1

先手写这样的证明是没有用的，可以用blast来解决。它主要为高级用户保留。我知道的唯一文档是 the old tutorial，第 5 节

无论如何，你的交集定理是错误的：你想使用 Int_iff。这是完整的证明：


lemma "(A ∩ B) ∪ C ⊆ A  ∪ C "
  apply (subst subset_iff)+
  apply(rule allI)
  apply (rule impI)
    (*here normally we should try to get rid of Union and Inter*)
  apply(subst Un_iff)+ 
  apply(subst  (asm)  Un_iff)
  apply(subst (asm) Int_iff)
  apply (elim disjE)
   apply (elim conjE)
   apply (rule disjI1)
   apply assumption
  apply (rule disjI2)
  apply assumption
  done

我如何找到这样的证据？我熟知关于蕴涵、合取和析取的低级定理 (allI, impI, conjI, conjE, disjE, disjI1,...)。有统一的命名规范（I：介绍规则，E：淘汰规则，D：销毁规则），所以不难记。

对于其余部分，可以使用 find_theorems（或查询面板）进行搜索。

这是我要写的证明（但另一个更适合教学：conjE 比 IntE 重要得多）：

lemma "(A ∩ B) ∪ C ⊆ A  ∪ C "
  apply (rule subset_iff[THEN iffD2])
  apply(intro allI impI)
  apply (elim UnE)
   apply (elim IntE)
   apply (rule UnI1)
   apply assumption
  apply (rule UnI2)
  apply assumption
  done

如何在 Isabelle 中为子集做证明

how to do a proof for subset in Isabelle

set

isabelle

proof