Theory Transport_Base

✐‹creator "Kevin Kappelmann"›
chapter ‹Transport›
section ‹Basic Setup›
theory Transport_Base
  imports
    Galois_Equivalences
    Galois_Relator
begin

paragraph ‹Summary›
text ‹Basic setup for commonly used concepts in Transport, including a suitable
locale.›

locale transport = galois L R l r
  for L :: "'a ⇒ 'a ⇒ bool"
  and R :: "'b ⇒ 'b ⇒ bool"
  and l :: "'a ⇒ 'b"
  and r :: "'b ⇒ 'a"
begin

subsection ‹Ordered Galois Connections›

definition "preorder_galois_connection ≡
  ((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r
  ∧ preorder_on (in_field (≤⇘L⇙)) (≤⇘L⇙)
  ∧ preorder_on (in_field (≤⇘R⇙)) (≤⇘R⇙)"

notation transport.preorder_galois_connection (infix "⊣⇘pre⇙" 50)

lemma preorder_galois_connectionI [intro]:
  assumes "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  and "preorder_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
  and "preorder_on (in_field (≤⇘R⇙)) (≤⇘R⇙)"
  shows "((≤⇘L⇙) ⊣⇘pre⇙ (≤⇘R⇙)) l r"
  unfolding preorder_galois_connection_def using assms by blast

lemma preorder_galois_connectionE [elim]:
  assumes "((≤⇘L⇙) ⊣⇘pre⇙ (≤⇘R⇙)) l r"
  obtains "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r" "preorder_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
    "preorder_on (in_field (≤⇘R⇙)) (≤⇘R⇙)"
  using assms unfolding preorder_galois_connection_def by blast

context
begin

interpretation t : transport S T f g for S T f g .

lemma rel_inv_preorder_galois_connection_eq_preorder_galois_connection_rel_inv [simp]:
  "((≤⇘R⇙) ⊣⇘pre⇙ (≤⇘L⇙))¯ = ((≥⇘L⇙) ⊣⇘pre⇙ (≥⇘R⇙))"
  by (intro ext) (auto intro!: t.preorder_galois_connectionI)

end

corollary preorder_galois_connection_rel_inv_iff_preorder_galois_connection [iff]:
  "((≥⇘L⇙) ⊣⇘pre⇙ (≥⇘R⇙)) l r ⟷ ((≤⇘R⇙) ⊣⇘pre⇙ (≤⇘L⇙)) r l"
  by (simp flip:
    rel_inv_preorder_galois_connection_eq_preorder_galois_connection_rel_inv)

definition "partial_equivalence_rel_galois_connection ≡
  ((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r
  ∧ partial_equivalence_rel (≤⇘L⇙)
  ∧ partial_equivalence_rel (≤⇘R⇙)"

notation transport.partial_equivalence_rel_galois_connection (infix "⊣⇘PER⇙" 50)

lemma partial_equivalence_rel_galois_connectionI [intro]:
  assumes "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  and "partial_equivalence_rel_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
  and "partial_equivalence_rel_on (in_field (≤⇘R⇙)) (≤⇘R⇙)"
  shows "((≤⇘L⇙) ⊣⇘PER⇙ (≤⇘R⇙)) l r"
  unfolding partial_equivalence_rel_galois_connection_def using assms by blast

lemma partial_equivalence_rel_galois_connectionE [elim]:
  assumes "((≤⇘L⇙) ⊣⇘PER⇙ (≤⇘R⇙)) l r"
  obtains "((≤⇘L⇙) ⊣⇘pre⇙ (≤⇘R⇙)) l r" "symmetric (≤⇘L⇙)" "symmetric (≤⇘R⇙)"
  using assms unfolding partial_equivalence_rel_galois_connection_def by blast

context
begin

interpretation t : transport S T f g for S T f g .

lemma rel_inv_partial_equivalence_rel_galois_connection_eq_partial_equivalence_rel_galois_connection_rel_inv
  [simp]: "((≤⇘R⇙) ⊣⇘PER⇙ (≤⇘L⇙))¯ = ((≥⇘L⇙) ⊣⇘PER⇙ (≥⇘R⇙))"
  by (intro ext) blast

end

corollary partial_equivalence_rel_galois_connection_rel_inv_iff_partial_equivalence_rel_galois_connection
  [iff]: "((≥⇘L⇙) ⊣⇘PER⇙ (≥⇘R⇙)) l r ⟷ ((≤⇘R⇙) ⊣⇘PER⇙ (≤⇘L⇙)) r l"
  by (simp flip:
    rel_inv_partial_equivalence_rel_galois_connection_eq_partial_equivalence_rel_galois_connection_rel_inv)

lemma left_Galois_comp_ge_Galois_left_eq_left_if_partial_equivalence_rel_galois_connection:
  assumes "((≤⇘L⇙) ⊣⇘PER⇙ (≤⇘R⇙)) l r"
  shows "((⇘L⇙⪅) ∘∘ (⪆⇘L⇙)) = (≤⇘L⇙)"
proof (intro ext iffI)
  fix x x' assume "((⇘L⇙⪅) ∘∘ (⪆⇘L⇙)) x x'"
  then obtain y where "x ≤⇘L⇙ r y" "r y ≥⇘L⇙ x'" by blast
  with assms show "x ≤⇘L⇙ x'" by (blast dest: symmetricD)
next
  fix x x' assume "x ≤⇘L⇙ x'"
  with assms have "x ⇘L⇙⪅ l x'" "x' ⇘L⇙⪅ l x'"
    by (blast intro: left_Galois_left_if_left_relI)+
  with assms show "((⇘L⇙⪅) ∘∘ (⪆⇘L⇙)) x x'" by auto
qed


subsection ‹Ordered Equivalences›

definition "preorder_equivalence ≡
  ((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r
  ∧ preorder_on (in_field (≤⇘L⇙)) (≤⇘L⇙)
  ∧ preorder_on (in_field (≤⇘R⇙)) (≤⇘R⇙)"

notation transport.preorder_equivalence (infix "≡⇘pre⇙" 50)

lemma preorder_equivalence_if_galois_equivalenceI [intro]:
  assumes "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  and "preorder_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
  and "preorder_on (in_field (≤⇘R⇙)) (≤⇘R⇙)"
  shows "((≤⇘L⇙) ≡⇘pre⇙ (≤⇘R⇙)) l r"
  unfolding preorder_equivalence_def using assms by blast

lemma preorder_equivalence_if_order_equivalenceI:
  assumes "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  and "transitive (≤⇘L⇙)"
  and "transitive (≤⇘R⇙)"
  shows "((≤⇘L⇙) ≡⇘pre⇙ (≤⇘R⇙)) l r"
  unfolding preorder_equivalence_def using assms
  by (blast intro: reflexive_on_in_field_if_transitive_if_rel_equivalence_on
    dest: galois_equivalence_left_right_if_transitive_if_order_equivalence)

lemma preorder_equivalence_galois_equivalenceE [elim]:
  assumes "((≤⇘L⇙) ≡⇘pre⇙ (≤⇘R⇙)) l r"
  obtains "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r" "preorder_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
    "preorder_on (in_field (≤⇘R⇙)) (≤⇘R⇙)"
  using assms unfolding preorder_equivalence_def by blast

lemma preorder_equivalence_order_equivalenceE:
  assumes "((≤⇘L⇙) ≡⇘pre⇙ (≤⇘R⇙)) l r"
  obtains "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r" "preorder_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
    "preorder_on (in_field (≤⇘R⇙)) (≤⇘R⇙)"
  using assms by (blast intro:
    order_equivalence_if_reflexive_on_in_field_if_galois_equivalence)

context
begin

interpretation t : transport S T f g for S T f g .

lemma rel_inv_preorder_equivalence_eq_preorder_equivalence [simp]:
  "((≤⇘R⇙) ≡⇘pre⇙ (≤⇘L⇙))¯ = ((≤⇘L⇙) ≡⇘pre⇙ (≤⇘R⇙))"
  by (intro ext) blast

end

corollary preorder_equivalence_right_left_iff_preorder_equivalence_left_right:
  "((≤⇘R⇙) ≡⇘pre⇙ (≤⇘L⇙)) r l ⟷ ((≤⇘L⇙) ≡⇘pre⇙ (≤⇘R⇙)) l r"
  by (simp flip: rel_inv_preorder_equivalence_eq_preorder_equivalence)

lemma preorder_equivalence_rel_inv_eq_preorder_equivalence [simp]:
  "((≥⇘L⇙) ≡⇘pre⇙ (≥⇘R⇙)) = ((≤⇘L⇙) ≡⇘pre⇙ (≤⇘R⇙))"
  by (intro ext iffI)
  (auto intro!: transport.preorder_equivalence_if_galois_equivalenceI
    elim!: transport.preorder_equivalence_galois_equivalenceE)

definition "partial_equivalence_rel_equivalence ≡
  ((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r
  ∧ partial_equivalence_rel (≤⇘L⇙)
  ∧ partial_equivalence_rel (≤⇘R⇙)"

notation transport.partial_equivalence_rel_equivalence (infix "≡⇘PER⇙" 50)

lemma partial_equivalence_rel_equivalence_if_galois_equivalenceI [intro]:
  assumes "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  and "partial_equivalence_rel (≤⇘L⇙)"
  and "partial_equivalence_rel (≤⇘R⇙)"
  shows "((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r"
  unfolding partial_equivalence_rel_equivalence_def using assms by blast

lemma partial_equivalence_rel_equivalence_if_order_equivalenceI:
  assumes "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  and "partial_equivalence_rel (≤⇘L⇙)"
  and "partial_equivalence_rel (≤⇘R⇙)"
  shows "((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r"
  unfolding partial_equivalence_rel_equivalence_def using assms
  by (blast dest: galois_equivalence_left_right_if_transitive_if_order_equivalence)

lemma partial_equivalence_rel_equivalenceE [elim]:
  assumes "((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r"
  obtains "((≤⇘L⇙) ≡⇘pre⇙ (≤⇘R⇙)) l r" "symmetric (≤⇘L⇙)" "symmetric (≤⇘R⇙)"
  using assms unfolding partial_equivalence_rel_equivalence_def by blast

context
begin

interpretation t : transport S T f g for S T f g .

lemma rel_inv_partial_equivalence_rel_equivalence_eq_partial_equivalence_rel_equivalence [simp]:
  "((≤⇘R⇙) ≡⇘PER⇙ (≤⇘L⇙))¯ = ((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙))"
  by (intro ext) blast

end

corollary partial_equivalence_rel_equivalence_right_left_iff_partial_equivalence_rel_equivalence_left_right:
  "((≤⇘R⇙) ≡⇘PER⇙ (≤⇘L⇙)) r l ⟷ ((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r"
  by (simp flip:
    rel_inv_partial_equivalence_rel_equivalence_eq_partial_equivalence_rel_equivalence)

lemma partial_equivalence_rel_equivalence_rel_inv_eq_partial_equivalence_rel_equivalence
  [simp]: "((≥⇘L⇙) ≡⇘PER⇙ (≥⇘R⇙)) = ((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙))"
  by (intro ext iffI)
  (auto intro!: transport.partial_equivalence_rel_equivalence_if_galois_equivalenceI
    elim!: transport.partial_equivalence_rel_equivalenceE
      transport.preorder_equivalence_galois_equivalenceE
      preorder_on_in_fieldE)

end


end