Theory Transport_Bijections

✐‹creator "Kevin Kappelmann"›
section ‹Transport using Bijections›
theory Transport_Bijections
  imports
    Restricted_Equality
    Functions_Bijection
    Transport_Base
begin

paragraph ‹Summary›
text ‹Setup for Transport using bijective transport functions.›

locale transport_bijection =
  fixes L :: "'a ⇒ 'a ⇒ bool"
  and R :: "'b ⇒ 'b ⇒ bool"
  and l :: "'a ⇒ 'b"
  and r :: "'b ⇒ 'a"
  assumes mono_wrt_rel_left: "(L ⇛⇩m R) l"
  and mono_wrt_rel_right: "(R ⇛⇩m L) r"
  and inverse_left_right: "inverse_on (in_field L) l r"
  and inverse_right_left: "inverse_on (in_field R) r l"
begin

interpretation transport L R l r .
interpretation g_flip_inv : galois "(≥⇘R⇙)" "(≥⇘L⇙)" r l .

lemma bijection_on_in_field: "bijection_on (in_field (≤⇘L⇙)) (in_field (≤⇘R⇙)) l r"
  using mono_wrt_rel_left mono_wrt_rel_right inverse_left_right inverse_right_left
  by (intro bijection_onI in_field_if_in_field_if_mono_wrt_rel)
  auto

lemma half_galois_prop_left: "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  using mono_wrt_rel_left inverse_right_left
  by (intro half_galois_prop_leftI) (fastforce dest: inverse_onD)

lemma half_galois_prop_right: "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  using mono_wrt_rel_right inverse_left_right
  by (intro half_galois_prop_rightI)
  (force dest: in_field_if_in_dom inverse_onD)

lemma galois_prop: "((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
  using half_galois_prop_left half_galois_prop_right
  by (intro galois_propI)

lemma galois_connection: "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  using mono_wrt_rel_left mono_wrt_rel_right galois_prop
  by (intro galois_connectionI)

lemma rel_equivalence_on_unitI:
  assumes "reflexive_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
  shows "rel_equivalence_on (in_field (≤⇘L⇙)) (≤⇘L⇙) η"
  using assms inverse_left_right
  by (subst rel_equivalence_on_unit_iff_reflexive_on_if_inverse_on)

interpretation flip : transport_bijection R L r l
  rewrites "order_functors.unit r l ≡ ε"
  using mono_wrt_rel_left mono_wrt_rel_right inverse_left_right inverse_right_left
  by unfold_locales (simp_all only: flip_unit_eq_counit)

lemma galois_equivalence: "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  using galois_connection flip.galois_prop by (intro galois_equivalenceI)

lemmas rel_equivalence_on_counitI = flip.rel_equivalence_on_unitI

lemma order_equivalenceI:
  assumes "reflexive_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
  and "reflexive_on (in_field (≤⇘R⇙)) (≤⇘R⇙)"
  shows "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  using assms mono_wrt_rel_left mono_wrt_rel_right rel_equivalence_on_unitI
    rel_equivalence_on_counitI
  by (intro order_equivalenceI)

lemma preorder_equivalenceI:
  assumes "preorder_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
  and "preorder_on (in_field (≤⇘R⇙)) (≤⇘R⇙)"
  shows "((≤⇘L⇙) ≡⇘pre⇙ (≤⇘R⇙)) l r"
  using assms by (intro preorder_equivalence_if_galois_equivalenceI
    galois_equivalence)
  simp_all

lemma partial_equivalence_rel_equivalenceI:
  assumes "partial_equivalence_rel (≤⇘L⇙)"
  and "partial_equivalence_rel (≤⇘R⇙)"
  shows "((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r"
  using assms by (intro partial_equivalence_rel_equivalence_if_galois_equivalenceI
    galois_equivalence)
  simp_all

end

locale transport_reflexive_on_in_field_bijection =
  fixes L :: "'a ⇒ 'a ⇒ bool"
  and R :: "'b ⇒ 'b ⇒ bool"
  and l :: "'a ⇒ 'b"
  and r :: "'b ⇒ 'a"
  assumes reflexive_on_in_field_left: "reflexive_on (in_field L) L"
  and reflexive_on_in_field_right: "reflexive_on (in_field R) R"
  and transport_bijection: "transport_bijection L R l r"
begin

sublocale tbij? : transport_bijection L R l r
  rewrites "reflexive_on (in_field L) L ≡ True"
  and "reflexive_on (in_field R) R ≡ True"
  and "⋀P. (True ⟹ P) ≡ Trueprop P"
  using transport_bijection reflexive_on_in_field_left reflexive_on_in_field_right
  by auto

lemmas rel_equivalence_on_unit = rel_equivalence_on_unitI
lemmas rel_equivalence_on_counit = rel_equivalence_on_counitI
lemmas order_equivalence = order_equivalenceI

end

locale transport_preorder_on_in_field_bijection =
  fixes L :: "'a ⇒ 'a ⇒ bool"
  and R :: "'b ⇒ 'b ⇒ bool"
  and l :: "'a ⇒ 'b"
  and r :: "'b ⇒ 'a"
  assumes preorder_on_in_field_left: "preorder_on (in_field L) L"
  and preorder_on_in_field_right: "preorder_on (in_field R) R"
  and transport_bijection: "transport_bijection L R l r"
begin

sublocale trefl_bij? : transport_reflexive_on_in_field_bijection L R l r
  rewrites "preorder_on (in_field L) L ≡ True"
  and "preorder_on (in_field R) R ≡ True"
  and "⋀P. (True ⟹ P) ≡ Trueprop P"
  using transport_bijection
  by (intro transport_reflexive_on_in_field_bijection.intro)
  (insert preorder_on_in_field_left preorder_on_in_field_right, auto)

lemmas preorder_equivalence = preorder_equivalenceI

end

locale transport_partial_equivalence_rel_bijection =
  fixes L :: "'a ⇒ 'a ⇒ bool"
  and R :: "'b ⇒ 'b ⇒ bool"
  and l :: "'a ⇒ 'b"
  and r :: "'b ⇒ 'a"
  assumes partial_equivalence_rel_left: "partial_equivalence_rel L"
  and partial_equivalence_rel_right: "partial_equivalence_rel R"
  and transport_bijection: "transport_bijection L R l r"
begin

sublocale tpre_bij? : transport_preorder_on_in_field_bijection L R l r
  rewrites "partial_equivalence_rel L ≡ True"
  and "partial_equivalence_rel R ≡ True"
  and "⋀P. (True ⟹ P) ≡ Trueprop P"
  using transport_bijection
  by (intro transport_preorder_on_in_field_bijection.intro)
  (insert partial_equivalence_rel_left partial_equivalence_rel_right, auto)

lemmas partial_equivalence_rel_equivalence = partial_equivalence_rel_equivalenceI

end

locale transport_eq_restrict_bijection =
  fixes P :: "'a ⇒ bool"
  and Q :: "'b ⇒ bool"
  and l :: "'a ⇒ 'b"
  and r :: "'b ⇒ 'a"
  assumes bijection_on_in_field:
    "bijection_on (in_field ((=⇘P⇙) :: 'a ⇒ _)) (in_field ((=⇘Q⇙) :: 'b ⇒ _)) l r"
begin

interpretation transport "(=⇘P⇙)" "(=⇘Q⇙)" l r .

sublocale tper_bij? : transport_partial_equivalence_rel_bijection "(=⇘P⇙)" "(=⇘Q⇙)" l r
  using bijection_on_in_field partial_equivalence_rel_eq_restrict
  by unfold_locales
  (auto elim: bijection_onE intro!:
    mono_wrt_rel_left_if_reflexive_on_if_le_eq_if_mono_wrt_in_field[of "in_field (=⇘Q⇙)"]
    flip_of.mono_wrt_rel_left_if_reflexive_on_if_le_eq_if_mono_wrt_in_field[of "in_field (=⇘P⇙)"])

lemma left_Galois_eq_Galois_eq_eq_restrict: "(⇘L⇙⪅) = (galois_rel.Galois (=) (=) r)↾⇘P⇙↿⇘Q⇙"
  by (subst galois_rel.left_Galois_restrict_left_eq_left_Galois_left_restrict_left
    galois_rel.left_Galois_restrict_right_eq_left_Galois_right_restrict_right
    rel_restrict_right_eq rel_inv_eq_self_if_symmetric)+
  auto

end

locale transport_eq_bijection =
  fixes l :: "'a ⇒ 'b"
  and r :: "'b ⇒ 'a"
  assumes bijection_on_in_field:
    "bijection_on (in_field ((=) :: 'a ⇒ _)) (in_field ((=) :: 'b ⇒ _)) l r"
begin

sublocale teq_restr_bij? : transport_eq_restrict_bijection ⊤ ⊤ l r
  rewrites "(=⇘⊤ :: 'a ⇒ bool⇙) = ((=) :: 'a ⇒ _)"
  and "(=⇘⊤ :: 'b ⇒ bool⇙) = ((=) :: 'b ⇒ _)"
  using bijection_on_in_field by unfold_locales simp_all

end


end