对包含集合元素的案例进行证明

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) or (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 的源代码中找不到这个常量。我冒昧地猜测了它的含义并提供了我自己的定义（如果我猜错了请告诉我）。
我的证明与您提出的证明不完全相同。但是，希望您能够对其进行修改以满足您的需要。

I am quite new to Isabelle and am not sure what I even would be searching for in the reference to find this.

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

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

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

对包含集合元素的案例进行证明

Proof over cases for which set element is included in

isabelle