Theory Relations

theory Relations
  imports Main "HOL-Library.LaTeXsugar" "HOL-Library.OptionalSugar"
begin

section ‹Relations›

subsection ‹Basic Conditions›

text ‹We recall the standard definitions for reflexivity, symmetry, transitivity, preoders,
        equivalence, and inverse relations.›

abbreviation "preorder Rel ≡ preorder_on UNIV Rel"
abbreviation "equivalence Rel ≡ equiv UNIV Rel"

text ‹A symmetric preorder is an equivalence.›

lemma symm_preorder_is_equivalence:
  fixes Rel :: "('a × 'a) set"
  assumes "preorder Rel"
      and "sym Rel"
  shows "equivalence Rel"
      using assms
      unfolding preorder_on_def equiv_def
    by simp

text ‹The symmetric closure of a relation is the union of this relation and its inverse.›

definition symcl :: "('a × 'a) set ⇒ ('a × 'a) set" where
  "symcl Rel = Rel ∪ Rel¯"

text ‹For all (a, b) in R, the symmetric closure of R contains (a, b) as well as (b, a).›

lemma elem_of_symcl:
  fixes Rel :: "('a × 'a) set"
    and a b :: "'a"
  assumes elem: "(a, b) ∈ Rel"
  shows "(a, b) ∈ symcl Rel"
    and "(b, a) ∈ symcl Rel"
    by (auto simp add: elem symcl_def)

text ‹The symmetric closure of a relation is symmetric.›

lemma sym_symcl:
  fixes Rel :: "('a × 'a) set"
  shows "sym (symcl Rel)"
    by (simp add: symcl_def sym_Un_converse)

text ‹The reflexive and symmetric closure of a relation is equal to its symmetric and reflexive
        closure.›

lemma refl_symm_closure_is_symm_refl_closure:
  fixes Rel :: "('a × 'a) set"
  shows "symcl (Rel⇧=) = (symcl Rel)⇧="
    by (auto simp add: symcl_def refl)

text ‹The symmetric closure of a reflexive relation is reflexive.›

lemma refl_symcl_of_refl_rel:
  fixes Rel :: "('a × 'a) set"
    and A   :: "'a set"
  assumes "refl_on A Rel"
  shows "refl_on A (symcl Rel)"
      using assms
    by (auto simp add: refl_on_def' symcl_def)

text ‹Accordingly, the reflexive, symmetric, and transitive closure of a relation is equal to its
        symmetric, reflexive, and transitive closure.›

lemma refl_symm_trans_closure_is_symm_refl_trans_closure:
  fixes Rel :: "('a × 'a) set"
  shows "(symcl (Rel⇧=))⇧+ = (symcl Rel)⇧*"
      using refl_symm_closure_is_symm_refl_closure[where Rel="Rel"]
    by simp

text ‹The reflexive closure of a symmetric relation is symmetric.›

lemma sym_reflcl_of_symm_rel:
  fixes Rel :: "('a × 'a) set"
  assumes "sym Rel"
  shows "sym (Rel⇧=)"
      using assms
    by (simp add: sym_Id sym_Un)

text ‹The reflexive closure of a reflexive relation is the relation itself.›

lemma reflcl_of_refl_rel:
  fixes Rel :: "('a × 'a) set"
  assumes "refl Rel"
  shows "Rel⇧= = Rel"
      using assms
      unfolding refl_on_def
    by auto

text ‹The symmetric closure of a symmetric relation is the relation itself.›

lemma symm_closure_of_symm_rel:
  fixes Rel :: "('a × 'a) set"
  assumes "sym Rel"
  shows "symcl Rel = Rel"
      using assms
      unfolding symcl_def sym_def
    by auto

text ‹The reflexive and transitive closure of a preorder Rel is Rel.›

lemma rtrancl_of_preorder:
  fixes Rel :: "('a × 'a) set"
  assumes "preorder Rel"
  shows "Rel⇧* = Rel"
      using assms reflcl_of_refl_rel[of Rel] trancl_id[of "Rel⇧="] trancl_reflcl[of Rel]
      unfolding preorder_on_def
    by auto

text ‹The reflexive and transitive closure of a relation is a subset of its reflexive, symmetric,
        and transtive closure.›

lemma refl_trans_closure_subset_of_refl_symm_trans_closure:
  fixes Rel :: "('a × 'a) set"
  shows "Rel⇧* ⊆ (symcl (Rel⇧=))⇧+"
proof clarify
  fix a b
  assume "(a, b) ∈ Rel⇧*"
  hence "(a, b) ∈ (symcl Rel)⇧*"
      using in_rtrancl_UnI[of "(a, b)" "Rel" "Rel¯"]
    by (simp add: symcl_def)
  thus "(a, b) ∈ (symcl (Rel⇧=))⇧+"
      using refl_symm_trans_closure_is_symm_refl_trans_closure[of Rel]
    by simp
qed

text ‹If a preorder Rel satisfies the following two conditions, then its symmetric closure is
        transitive:
        (1) If (a, b) and (c, b) in Rel but not (a, c) in Rel, then (b, a) in Rel or (b, c) in Rel.
        (2) If (a, b) and (a, c) in Rel but not (b, c) in Rel, then (b, a) in Rel or (c, a) in Rel.
›

lemma symm_closure_of_preorder_is_trans:
  fixes Rel :: "('a × 'a) set"
  assumes condA: "∀a b c. (a, b) ∈ Rel ∧ (c, b) ∈ Rel ∧ (a, c) ∉ Rel
                  ⟶ (b, a) ∈ Rel ∨ (b, c) ∈ Rel"
      and condB: "∀a b c. (a, b) ∈ Rel ∧ (a, c) ∈ Rel ∧ (b, c) ∉ Rel
                  ⟶ (b, a) ∈ Rel ∨ (c, a) ∈ Rel"
      and reflR: "refl Rel"
      and tranR: "trans Rel"
  shows "trans (symcl Rel)"
    unfolding trans_def
proof clarify
  fix a b c
  have "⟦(a, b) ∈ Rel; (b, c) ∈ Rel⟧ ⟹ (a, c) ∈ symcl Rel"
  proof -
    assume "(a, b) ∈ Rel" and "(b, c) ∈ Rel"
    with tranR have "(a, c) ∈ Rel"
        unfolding trans_def
      by blast
    thus "(a, c) ∈ symcl Rel"
      by (simp add: symcl_def)
  qed
  moreover have "⟦(a, b) ∈ Rel; (c, b) ∈ Rel; (a, c) ∉ Rel⟧ ⟹ (a, c) ∈ symcl Rel"
  proof -
    assume A1: "(a, b) ∈ Rel" and A2: "(c, b) ∈ Rel" and "(a, c) ∉ Rel"
    with condA have "(b, a) ∈ Rel ∨ (b, c) ∈ Rel"
      by blast
    thus "(a, c) ∈ symcl Rel"
    proof auto
      assume "(b, a) ∈ Rel"
      with A2 tranR have "(c, a) ∈ Rel"
          unfolding trans_def
        by blast
      thus "(a, c) ∈ symcl Rel"
        by (simp add: symcl_def)
    next
      assume "(b, c) ∈ Rel"
      with A1 tranR have "(a, c) ∈ Rel"
          unfolding trans_def
        by blast
      thus "(a, c) ∈ symcl Rel"
        by (simp add: symcl_def)
    qed
  qed
  moreover have "⟦(b, a) ∈ Rel; (b, c) ∈ Rel; (a, c) ∉ Rel⟧ ⟹ (a, c) ∈ symcl Rel"
  proof -
    assume B1: "(b, a) ∈ Rel" and B2: "(b, c) ∈ Rel" and "(a, c) ∉ Rel"
    with condB have "(a, b) ∈ Rel ∨ (c, b) ∈ Rel"
      by blast
    thus "(a, c) ∈ symcl Rel"
    proof auto
      assume "(a, b) ∈ Rel"
      with B2 tranR have "(a, c) ∈ Rel"
          unfolding trans_def
        by blast
      thus "(a, c) ∈ symcl Rel"
        by (simp add: symcl_def)
    next
      assume "(c, b) ∈ Rel"
      with B1 tranR have "(c, a) ∈ Rel"
          unfolding trans_def
        by blast
      thus "(a, c) ∈ symcl Rel"
        by (simp add: symcl_def)
    qed
  qed
  moreover have "⟦(b, a) ∈ Rel; (c, b) ∈ Rel⟧ ⟹ (a, c) ∈ symcl Rel"
  proof -
    assume "(c, b) ∈ Rel" and "(b, a) ∈ Rel"
    with tranR have "(c, a) ∈ Rel"
        unfolding trans_def
      by blast
    thus "(a, c) ∈ symcl Rel"
      by (simp add: symcl_def)
  qed
  moreover assume "(a, b) ∈ symcl Rel" and "(b, c) ∈ symcl Rel"
  ultimately show "(a, c) ∈ symcl Rel"
    by (auto simp add: symcl_def)
qed

subsection ‹Preservation, Reflection, and Respection of Predicates›

text ‹A relation R preserves some predicate P if P(a) implies P(b) for all (a, b) in R.›

abbreviation rel_preserves_pred :: "('a × 'a) set ⇒ ('a ⇒ bool) ⇒ bool" where
  "rel_preserves_pred Rel Pred ≡ ∀a b. (a, b) ∈ Rel ∧ Pred a ⟶ Pred b"

abbreviation rel_preserves_binary_pred :: "('a × 'a) set ⇒ ('a ⇒ 'b ⇒ bool) ⇒ bool" where
  "rel_preserves_binary_pred Rel Pred ≡ ∀a b x. (a, b) ∈ Rel ∧ Pred a x ⟶ Pred b x"

text ‹A relation R reflects some predicate P if P(b) implies P(a) for all (a, b) in R.›

abbreviation rel_reflects_pred :: "('a × 'a) set ⇒ ('a ⇒ bool) ⇒ bool" where
  "rel_reflects_pred Rel Pred ≡ ∀a b. (a, b) ∈ Rel ∧ Pred b ⟶ Pred a"

abbreviation rel_reflects_binary_pred :: "('a × 'a) set ⇒ ('a ⇒ 'b ⇒ bool) ⇒ bool" where
  "rel_reflects_binary_pred Rel Pred ≡ ∀a b x. (a, b) ∈ Rel ∧ Pred b x ⟶ Pred a x"

text ‹A relation respects a predicate if it preserves and reflects it.›

abbreviation rel_respects_pred :: "('a × 'a) set ⇒ ('a ⇒ bool) ⇒ bool" where
  "rel_respects_pred Rel Pred ≡ rel_preserves_pred Rel Pred ∧ rel_reflects_pred Rel Pred"

abbreviation rel_respects_binary_pred :: "('a × 'a) set ⇒ ('a ⇒ 'b ⇒ bool) ⇒ bool" where
  "rel_respects_binary_pred Rel Pred ≡
   rel_preserves_binary_pred Rel Pred ∧ rel_reflects_binary_pred Rel Pred"

text ‹For symmetric relations preservation, reflection, and respection of predicates means the
        same.›

lemma symm_relation_impl_preservation_equals_reflection:
  fixes Rel  :: "('a × 'a) set"
    and Pred :: "'a ⇒ bool"
  assumes symm: "sym Rel"
  shows "rel_preserves_pred Rel Pred = rel_reflects_pred Rel Pred"
    and "rel_preserves_pred Rel Pred = rel_respects_pred Rel Pred"
    and "rel_reflects_pred Rel Pred = rel_respects_pred Rel Pred"
      using symm
      unfolding sym_def
    by blast+

lemma symm_relation_impl_preservation_equals_reflection_of_binary_predicates:
  fixes Rel  :: "('a × 'a) set"
    and Pred :: "'a ⇒ 'b ⇒ bool"
  assumes symm: "sym Rel"
  shows "rel_preserves_binary_pred Rel Pred = rel_reflects_binary_pred Rel Pred"
    and "rel_preserves_binary_pred Rel Pred = rel_respects_binary_pred Rel Pred"
    and "rel_reflects_binary_pred Rel Pred = rel_respects_binary_pred Rel Pred"
      using symm
      unfolding sym_def
    by blast+

text ‹If a relation preserves a predicate then so does its reflexive or/and transitive closure.
›

lemma preservation_and_closures:
  fixes Rel  :: "('a × 'a) set"
    and Pred :: "'a ⇒ bool"
  assumes preservation: "rel_preserves_pred Rel Pred"
  shows "rel_preserves_pred (Rel⇧=) Pred"
    and "rel_preserves_pred (Rel⇧+) Pred"
    and "rel_preserves_pred (Rel⇧*) Pred"
proof -
  from preservation show A: "rel_preserves_pred (Rel⇧=) Pred"
    by (auto simp add: refl)
  have B: "⋀Rel. rel_preserves_pred Rel Pred ⟹ rel_preserves_pred (Rel⇧+) Pred"
  proof clarify
    fix Rel a b
    assume "(a, b) ∈ Rel⇧+" and "rel_preserves_pred Rel Pred" and "Pred a"
    thus "Pred b"
      by (induct, blast+)
  qed
  with preservation show "rel_preserves_pred (Rel⇧+) Pred"
    by blast
  from preservation A B[where Rel="Rel⇧="] show "rel_preserves_pred (Rel⇧*) Pred"
      using trancl_reflcl[of Rel]
    by blast
qed

lemma preservation_of_binary_predicates_and_closures:
  fixes Rel  :: "('a × 'a) set"
    and Pred :: "'a ⇒ 'b ⇒ bool"
  assumes preservation: "rel_preserves_binary_pred Rel Pred"
  shows "rel_preserves_binary_pred (Rel⇧=) Pred"
    and "rel_preserves_binary_pred (Rel⇧+) Pred"
    and "rel_preserves_binary_pred (Rel⇧*) Pred"
proof -
  from preservation show A: "rel_preserves_binary_pred (Rel⇧=) Pred"
    by (auto simp add: refl)
  have B: "⋀Rel. rel_preserves_binary_pred Rel Pred
           ⟹ rel_preserves_binary_pred (Rel⇧+) Pred"
  proof clarify
    fix Rel a b x
    assume "(a, b) ∈ Rel⇧+" and "rel_preserves_binary_pred Rel Pred" and "Pred a x"
    thus "Pred b x"
      by (induct, blast+)
  qed
  with preservation show "rel_preserves_binary_pred (Rel⇧+) Pred"
    by blast
  from preservation A B[where Rel="Rel⇧="]
  show "rel_preserves_binary_pred (Rel⇧*) Pred"
      using trancl_reflcl[of Rel]
    by fast
qed

text ‹If a relation reflects a predicate then so does its reflexive or/and transitive closure.›

lemma reflection_and_closures:
  fixes Rel  :: "('a × 'a) set"
    and Pred :: "'a ⇒ bool"
  assumes reflection: "rel_reflects_pred Rel Pred"
  shows "rel_reflects_pred (Rel⇧=) Pred"
    and "rel_reflects_pred (Rel⇧+) Pred"
    and "rel_reflects_pred (Rel⇧*) Pred"
proof -
  from reflection show A: "rel_reflects_pred (Rel⇧=) Pred"
    by (auto simp add: refl)
  have B: "⋀Rel. rel_reflects_pred Rel Pred ⟹ rel_reflects_pred (Rel⇧+) Pred"
  proof clarify
    fix Rel a b
    assume "(a, b) ∈ Rel⇧+" and "rel_reflects_pred Rel Pred" and "Pred b"
    thus "Pred a"
      by (induct, blast+)
  qed
  with reflection show "rel_reflects_pred (Rel⇧+) Pred"
    by blast
  from reflection A B[where Rel="Rel⇧="] show "rel_reflects_pred (Rel⇧*) Pred"
      using trancl_reflcl[of Rel]
    by fast
qed

lemma reflection_of_binary_predicates_and_closures:
  fixes Rel  :: "('a × 'a) set"
    and Pred :: "'a ⇒ 'b ⇒ bool"
  assumes reflection: "rel_reflects_binary_pred Rel Pred"
  shows "rel_reflects_binary_pred (Rel⇧=) Pred"
    and "rel_reflects_binary_pred (Rel⇧+) Pred"
    and "rel_reflects_binary_pred (Rel⇧*) Pred"
proof -
  from reflection show A: "rel_reflects_binary_pred (Rel⇧=) Pred"
    by (auto simp add: refl)
  have B: "⋀Rel. rel_reflects_binary_pred Rel Pred ⟹ rel_reflects_binary_pred (Rel⇧+) Pred"
  proof clarify
    fix Rel a b x
    assume "(a, b) ∈ Rel⇧+" and "rel_reflects_binary_pred Rel Pred" and "Pred b x"
    thus "Pred a x"
      by (induct, blast+)
  qed
  with reflection show "rel_reflects_binary_pred (Rel⇧+) Pred"
    by blast
  from reflection A B[where Rel="Rel⇧="]
  show "rel_reflects_binary_pred (Rel⇧*) Pred"
      using trancl_reflcl[of Rel]
    by fast
qed

text ‹If a relation respects a predicate then so does its reflexive, symmetric, or/and transitive
        closure.›

lemma respection_and_closures:
  fixes Rel  :: "('a × 'a) set"
    and Pred :: "'a ⇒ bool"
  assumes respection: "rel_respects_pred Rel Pred"
  shows "rel_respects_pred (Rel⇧=) Pred"
    and "rel_respects_pred (symcl Rel) Pred"
    and "rel_respects_pred (Rel⇧+) Pred"
    and "rel_respects_pred (symcl (Rel⇧=)) Pred"
    and "rel_respects_pred (Rel⇧*) Pred"
    and "rel_respects_pred ((symcl (Rel⇧=))⇧+) Pred"
proof -
  from respection show A: "rel_respects_pred (Rel⇧=) Pred"
      using preservation_and_closures(1)[where Rel="Rel" and Pred="Pred"]
            reflection_and_closures(1)[where Rel="Rel" and Pred="Pred"]
    by blast
  have B: "⋀Rel. rel_respects_pred Rel Pred ⟹ rel_respects_pred (symcl Rel) Pred"
  proof
    fix Rel
    assume B1: "rel_respects_pred Rel Pred"
    show "rel_preserves_pred (symcl Rel) Pred"
    proof clarify
      fix a b
      assume "(a, b) ∈ symcl Rel"
      hence "(a, b) ∈ Rel ∨ (b, a) ∈ Rel"
        by (simp add: symcl_def)
      moreover assume "Pred a"
      ultimately show "Pred b"
          using B1
        by blast
    qed
  next
    fix Rel  :: "('a × 'a) set"
    and Pred :: "'a ⇒ bool"
    assume B2: "rel_respects_pred Rel Pred"
    show "rel_reflects_pred (symcl Rel) Pred"
    proof clarify
      fix a b
      assume "(a, b) ∈ symcl Rel"
      hence "(a, b) ∈ Rel ∨ (b, a) ∈ Rel"
        by (simp add: symcl_def)
      moreover assume "Pred b"
      ultimately show "Pred a"
          using B2
        by blast
    qed
  qed
  from respection B[where Rel="Rel"] show "rel_respects_pred (symcl Rel) Pred"
    by blast
  have C: "⋀Rel. rel_respects_pred Rel Pred ⟹ rel_respects_pred (Rel⇧+) Pred"
  proof -
    fix Rel
    assume "rel_respects_pred Rel Pred"
    thus "rel_respects_pred (Rel⇧+) Pred"
        using preservation_and_closures(2)[where Rel="Rel" and Pred="Pred"]
              reflection_and_closures(2)[where Rel="Rel" and Pred="Pred"]
      by blast
  qed
  from respection C[where Rel="Rel"] show "rel_respects_pred (Rel⇧+) Pred"
    by blast
  from A B[where Rel="Rel⇧="] show "rel_respects_pred (symcl (Rel⇧=)) Pred"
    by blast
  from A C[where Rel="Rel⇧="] show "rel_respects_pred (Rel⇧*) Pred"
      using trancl_reflcl[of Rel]
    by fast
  from A B[where Rel="Rel⇧="] C[where Rel="symcl (Rel⇧=)"]
  show "rel_respects_pred ((symcl (Rel⇧=))⇧+) Pred"
    by blast
qed

lemma respection_of_binary_predicates_and_closures:
  fixes Rel  :: "('a × 'a) set"
    and Pred :: "'a ⇒ 'b ⇒ bool"
  assumes respection: "rel_respects_binary_pred Rel Pred"
  shows "rel_respects_binary_pred (Rel⇧=) Pred"
    and "rel_respects_binary_pred (symcl Rel) Pred"
    and "rel_respects_binary_pred (Rel⇧+) Pred"
    and "rel_respects_binary_pred (symcl (Rel⇧=)) Pred"
    and "rel_respects_binary_pred (Rel⇧*) Pred"
    and "rel_respects_binary_pred ((symcl (Rel⇧=))⇧+) Pred"
proof -
  from respection show A: "rel_respects_binary_pred (Rel⇧=) Pred"
      using preservation_of_binary_predicates_and_closures(1)[where Rel="Rel" and Pred="Pred"]
            reflection_of_binary_predicates_and_closures(1)[where Rel="Rel" and Pred="Pred"]
    by blast
  have B: "⋀Rel. rel_respects_binary_pred Rel Pred ⟹ rel_respects_binary_pred (symcl Rel) Pred"
  proof
    fix Rel
    assume B1: "rel_respects_binary_pred Rel Pred"
    show "rel_preserves_binary_pred (symcl Rel) Pred"
    proof clarify
      fix a b x
      assume "(a, b) ∈ symcl Rel"
      hence "(a, b) ∈ Rel ∨ (b, a) ∈ Rel"
        by (simp add: symcl_def)
      moreover assume "Pred a x"
      ultimately show "Pred b x"
          using B1
        by blast
    qed
  next
    fix Rel
    assume B2: "rel_respects_binary_pred Rel Pred"
    show "rel_reflects_binary_pred (symcl Rel) Pred"
    proof clarify
      fix a b x
      assume "(a, b) ∈ symcl Rel"
      hence "(a, b) ∈ Rel ∨ (b, a) ∈ Rel"
        by (simp add: symcl_def)
      moreover assume "Pred b x"
      ultimately show "Pred a x"
          using B2
        by blast
    qed
  qed
  from respection B[where Rel="Rel"] show "rel_respects_binary_pred (symcl Rel) Pred"
    by blast
  have C: "⋀Rel. rel_respects_binary_pred Rel Pred ⟹ rel_respects_binary_pred (Rel⇧+) Pred"
  proof -
    fix Rel
    assume "rel_respects_binary_pred Rel Pred"
    thus "rel_respects_binary_pred (Rel⇧+) Pred"
        using preservation_of_binary_predicates_and_closures(2)[where Rel="Rel" and Pred="Pred"]
              reflection_of_binary_predicates_and_closures(2)[where Rel="Rel" and Pred="Pred"]
      by blast
  qed
  from respection C[where Rel="Rel"] show "rel_respects_binary_pred (Rel⇧+) Pred"
    by blast
  from A B[where Rel="Rel⇧="]
  show "rel_respects_binary_pred (symcl (Rel⇧=)) Pred"
    by blast
  from A C[where Rel="Rel⇧="]
  show "rel_respects_binary_pred (Rel⇧*) Pred"
      using trancl_reflcl[of Rel]
    by fast
  from A B[where Rel="Rel⇧="] C[where Rel="symcl (Rel⇧=)"]
  show "rel_respects_binary_pred ((symcl (Rel⇧=))⇧+) Pred"
    by blast
qed

end