如何在伊莎贝尔中证明子集

问题描述

我正在尝试在 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，但它需要很多时间 + 到目前为止我发现的唯一有用（并且可以理解）的资源是这个链接： https://www.inf.ed.ac.uk/teaching/courses/ar/isabelle/FormalCheatSheet.pdf 以及一些包含与上面链接几乎相同内容的随机讲义......

我发现的其他资源有 100 多页，看起来不像是初学者的起点...

提前致谢

解决方法

首先手动编写这种证明是没有用的，因为它可以通过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