Theory Order_Equivalences

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Equivalences›
theory Order_Equivalences
  imports
    Order_Functors_Base
    Partial_Equivalence_Relations
    Preorders
begin

context order_functors
begin

definition "order_equivalence ≡
  ((≤⇘L⇙) ⇛⇩m (≤⇘R⇙)) l ∧
  ((≤⇘R⇙) ⇛⇩m (≤⇘L⇙)) r ∧
  rel_equivalence_on (in_field (≤⇘L⇙)) (≤⇘L⇙) η ∧
  rel_equivalence_on (in_field (≤⇘R⇙)) (≤⇘R⇙) ε"

notation order_functors.order_equivalence (infix "≡⇩o" 50)

lemma order_equivalenceI [intro]:
  assumes "((≤⇘L⇙) ⇛⇩m (≤⇘R⇙)) l"
  and "((≤⇘R⇙) ⇛⇩m (≤⇘L⇙)) r"
  and "rel_equivalence_on (in_field (≤⇘L⇙)) (≤⇘L⇙) η"
  and "rel_equivalence_on (in_field (≤⇘R⇙)) (≤⇘R⇙) ε"
  shows "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  unfolding order_equivalence_def using assms by blast

lemma order_equivalenceE [elim]:
  assumes "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  obtains "((≤⇘L⇙) ⇛⇩m (≤⇘R⇙)) l" "((≤⇘R⇙) ⇛⇩m (≤⇘L⇙)) r"
    "rel_equivalence_on (in_field (≤⇘L⇙)) (≤⇘L⇙) η"
    "rel_equivalence_on (in_field (≤⇘R⇙)) (≤⇘R⇙) ε"
  using assms unfolding order_equivalence_def by blast

interpretation of : order_functors S T f g for S T f g .

lemma rel_inv_order_equivalence_eq_order_equivalence [simp]:
  "((≤⇘R⇙) ≡⇩o (≤⇘L⇙))¯ = ((≤⇘L⇙) ≡⇩o (≤⇘R⇙))"
  by (intro ext) (auto intro!: of.order_equivalenceI simp: of.flip_unit_eq_counit)

corollary order_equivalence_right_left_iff_order_equivalence_left_right:
  "((≤⇘R⇙) ≡⇩o (≤⇘L⇙)) r l ⟷ ((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  by (simp flip: rel_inv_order_equivalence_eq_order_equivalence)

text ‹Due to the symmetry given by
@{thm "order_equivalence_right_left_iff_order_equivalence_left_right"},
for any theorem on @{term "(≤⇘L⇙)"}, we obtain a corresponding theorem on
@{term "(≤⇘R⇙)"} by flipping the roles of the two functors.
As such, in what follows, we do not explicitly state these free theorems but
users can obtain them as needed by creating a flipped interpretation
of @{locale order_functors}.›

lemma order_equivalence_rel_inv_eq_order_equivalence [simp]:
  "((≥⇘L⇙) ≡⇩o (≥⇘R⇙)) = ((≤⇘L⇙) ≡⇩o (≤⇘R⇙))"
  by (intro ext) (auto 0 4 intro!: of.order_equivalenceI)

lemma in_codom_left_eq_in_dom_left_if_order_equivalence:
  assumes "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  shows "in_codom (≤⇘L⇙) = in_dom (≤⇘L⇙)"
  using assms by (elim order_equivalenceE)
  (rule in_codom_eq_in_dom_if_rel_equivalence_on_in_field)

corollary preorder_on_in_field_left_if_transitive_if_order_equivalence:
  assumes "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  and "transitive (≤⇘L⇙)"
  shows "preorder_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
  using assms by (elim order_equivalenceE)
  (rule preorder_on_in_field_if_transitive_if_rel_equivalence_on)

lemma order_equivalence_partial_equivalence_rel_not_reflexive_not_transitive:
  assumes "∃(y :: 'b) y'. y ≠ y'"
  shows "∃(L :: 'a ⇒ 'a ⇒ bool) (R :: 'b ⇒ 'b ⇒ bool) l r.
    (L ≡⇩o R) l r ∧ partial_equivalence_rel L ∧
    ¬(reflexive_on (in_field R) R) ∧ ¬(transitive_on (in_field R) R)"
proof -
  from assms obtain cy cy' where "(cy :: 'b) ≠ cy'" by blast
  let ?cx = "undefined :: 'a"
  let ?L = "λx x'. ?cx = x ∧ x = x'"
  and ?R = "λy y'. (y = cy ∨ y = cy') ∧ (y' = cy ∨ y' = cy') ∧ (y ≠ cy' ∨ y' ≠ cy')"
  and ?l = "λ(a :: 'a). cy"
  and ?r = "λ(b :: 'b). ?cx"
  have "(?L ≡⇩o ?R)?l ?r" using ‹cy ≠ cy'›
    by (intro of.order_equivalenceI) (auto 0 4)
  moreover have "partial_equivalence_rel ?L" by blast
  moreover have
    "¬(transitive_on (in_field ?R) ?R)" and "¬(reflexive_on (in_field ?R) ?R)"
    using ‹cy ≠ cy'› by auto
  ultimately show "?thesis" by blast
qed

end


end