Proof over cases for which set element is included in

Question

I want to validate the following theorem, for which I already have a proof on paper, in 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

To prove 2 and 3, I would like to make use of a case distinction on which subsets the parties in a given member of the new relation are included in:

(a, b) ∈ (r ∪ r' ∪ {(x, y) | x y. x ∈ X ∧ y ∈ Y}) where (a ∈ X, b ∈ X) or (a ∈ X, b ∈ Y), etc.

For each of the possible cases, I would then like to prove the subgoals.

Is there some kind of automatic proof rule that can help me formalize this? I am quite new to Isabelle and am not sure what I even would be searching for in the reference to find this.

Furthermore, I am unhappy with having to copy "(r ∪ r' ∪ {(x, y) | x y. x ∈ X ∧ y ∈ Y})" all over the place. What is the idiomatic way to extract this new relation into some kind of definition to avoid copying?

user9716869 user9716869 · Accepted Answer · 2020-04-24T11:10:23

Below I provide a code listing that, hopefully, will help you to find answers to most of the problems stated in your question:

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

Side remarks:

I am not certain what exactly is the intended meaning of total_in in the statement of your question. I could not find this constant in the Isabelle/HOL's source code. I took the liberty to guess its meaning and provide my own definition (please let me know if my guess was wrong).
My proof is not entirely identical to the proof that you proposed. However, hopefully, you will be able to modify it to suit your needs.

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

My own starting point for learning Isabelle was the book "Concrete Semantics" by Tobias Nipkow and Gerwin Klein. Once you are comfortable with the basics, the best way to proceed when you start struggling to find information is to search through the official documentation, i.e. the tutorials and the document "isar-ref".

In this particular case, it is likely that you would wish to look at "Section 6: Proofs" in "isar-ref".

Isabelle version: Isabelle2020

Proof over cases for which set element is included in

1 Answers