证明包含集合元素的情况

Question

我想在 Isabelle 验证以下定理，我已经在纸上证明了这一点：

theorem 
  assumes "(X :: 'a set) ∩ (Y :: 'a set) = {}"
    and "trans (r :: 'a rel) ∧ total_in X r"
    and "trans (r' :: 'a rel) ∧ total_in Y r'"
  shows "∃ m. m ⊇ (r ∪ r') ∧ trans m ∧ total_in (X ∪ Y) m"
proof
  have 1: "(r ∪ r' ∪ {(x, y) | x y. x ∈ X ∧ y ∈ Y}) ⊇ (r ∪ r')" by simp
  have 2: "trans (r ∪ r' ∪ {(x, y) | x y. x ∈ X ∧ y ∈ Y})" sorry
  have 3: "total_in (X ∪ Y) (r ∪ r' ∪ {(x, y) | x y. x ∈ X ∧ y ∈ Y})" sorry
  from 1 2 3 show "
      r ∪ r' ⊆ (r ∪ r' ∪ {(x, y) | x y. x ∈ X ∧ y ∈ Y}) 
    ∧ trans (r ∪ r' ∪ {(x, y) | x y. x ∈ X ∧ y ∈ Y}) 
    ∧ total_in (X ∪ Y) (r ∪ r' ∪ {(x, y) | x y. x ∈ X ∧ y ∈ Y})" by auto
qed

为了证明 2 和 3，我想利用案例区分新关系的给定成员中的各方包含在哪些子集中：

(a, b) ∈ (r ∪ r' ∪ {(x, y) | x y.x ∈ X ∧ y ∈ Y}) 其中 (a ∈ X, b ∈ X) 或 (a ∈ X, b ∈ Y) 等。

对于每个可能的情况，然后我想证明子目标。

是否有某种自动证明规则可以帮助我将其形式化？我对 Isabelle 很陌生，我什至不确定我什至会在参考中搜索什么来找到这个。

此外，我对不得不到处复制"(r ∪ r' ∪ {(x, y) | x y. x ∈ X ∧ y ∈ Y})" 感到不满。将这种新关系提取到某种定义以避免复制的惯用方法是什么？

Answer 1

下面我提供了一个代码清单，希望能帮助您找到问题中提到的大多数问题的答案：

definition total_in :: "'a set ⇒ 'a rel ⇒ bool"
  where "total_in X r ⟷ total_on X r ∧ r ⊆ X × X"
―‹I could not find the definition of ‹total_in› in the source code of
Isabelle/HOL. Please let me know if my guess is wrong.›

lemma total_inI[intro]:
  assumes "total_on X r" and "r ⊆ X × X"
  shows "total_in X r"
  using assms unfolding total_in_def by simp

lemma total_inE[elim]:
  assumes "total_in X r"
  obtains "total_on X r" and "r ⊆ X × X"
  using assms unfolding total_in_def by simp

lemma my_thm:
   ―‹In this case, there does not seem to be any need to specify the types 
  explicitly: type inference does not seem to struggle to infer the types 
  that you suggested.›
  ―‹There is rarely a need to combine assumptions using HOL's conjunction.›
  ―‹Some of the assumptions seem to be redundant. Of course, given that I
am not certain as to what is the meaning of ‹total_in›, I might be wrong.›
  assumes "total_in X r" and "total_in Y r'"
  shows "∃m. m ⊇ r ∪ r' ∧ trans m ∧ total_in (X ∪ Y) m"
proof(intro exI conjI) 
  ―‹Use the introduction of the existential quantifier and conjunction to
  start the proof.›
  let ?m = "(X ∪ Y) × (X ∪ Y)"
  ―‹Syntactic abbreviation.›
  ―‹Alternatively you can use ‹define› to provide a new definition inside
  the proof context, e.g. ‹define m where "m = (X ∪ Y) × (X ∪ Y)"››
  show "r ∪ r' ⊆ ?m" using assms by auto
  show "trans ?m" by (intro transI) auto
  show "total_in (X ∪ Y) ?m" by (auto simp: total_on_def)
qed

---

旁白：

• 我不确定total_in 在您的问题陈述中究竟是什么意思。我在 Isabelle/HOL 的源代码中找不到这个常量。我冒昧地猜测了它的含义并提供了我自己的定义（如果我的猜测是错误的，请告诉我）。
• 我的证明与您提出的证明并不完全相同。不过，希望您能够根据自己的需要对其进行修改。

---

我对 Isabelle 很陌生，我什至不确定我会成为什么样的人 在参考中搜索以找到此内容。

我自己学习 Isabelle 的起点是 Tobias Nipkow 和 Gerwin Klein 的《"Concrete Semantics"》一书。一旦你熟悉了基础知识，当你开始努力寻找信息时，最好的方法是搜索官方文档，即教程和文档“isar-ref”。

在这种特殊情况下，您可能希望查看“isar-ref”中的“第 6 节：证明”。

---

伊莎贝尔版本：伊莎贝尔2020