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?
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:
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).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