Theory Transport_Bijections

✐‹creator "Kevin Kappelmann"›
section ‹Transport using Bijections›
theory Transport_Bijections
  imports
    Restricted_Equality
    Functions_Bijection
    Transport_Base
    Binary_Relations_Asymmetric
    Binary_Relations_Connected
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 ⇒ R) l"
  and mono_wrt_rel_right: "(R ⇒ 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

lemma mono_wrt_rel_if_connected_on_if_asymmetric_if_mono_if_inverse_on:
  assumes conn: "connected_on (in_field L) L"
  and asym: "asymmetric R"
  and monol: "(L ⇒ R) l"
  and monor: "(in_field R ⇒ in_field L) r"
  and inv: "inverse_on (in_field R) r l"
  shows "(R ⇒ L) r"
proof (intro mono_wrt_relI)
  fix x y assume "R x y"
  with monor have "in_field L (r x)" "in_field L (r y)" by blast+
  with conn consider "r x = r y" | "L (r y) (r x)" | "L (r x) (r y)" by blast
  then show "L (r x) (r y)"
  proof cases
    case 1
    moreover from inv have "injective_on (in_field R) r" using injective_on_if_inverse_on by blast
    ultimately have "x = y" using ‹R x y› by (blast dest: injective_onD)
    with asym ‹R x y› show ?thesis by blast
  next
    case 2
    with monol have "R (l (r y)) (l (r x))" by auto
    moreover from inv ‹R x y› have "l (r y) = y" "l (r x) = x" by (blast dest: inverse_onD)+
    ultimately have "R y x" by simp
    with asym ‹R x y› show ?thesis by blast
  qed auto
qed

context galois
begin

lemma transport_bijection_if_asymmetric_if_connected_on_if_mono_if_bijection_on:
  assumes "bijection_on (in_field (≤⇘L⇙)) (in_field (≤⇘R⇙)) l r"
  and "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "connected_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
  and "asymmetric (≤⇘R⇙)"
  shows "transport_bijection (≤⇘L⇙) (≤⇘R⇙) l r"
proof (intro transport_bijection.intro)
  from assms show "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
    by (auto intro: mono_wrt_rel_if_connected_on_if_asymmetric_if_mono_if_inverse_on)
qed (use assms in auto)

lemma inverse_on_if_connected_on_if_asymmetric_if_galois_connection:
  assumes gconn: "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  and conn: "connected_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
  and asym: "asymmetric (≤⇘R⇙)"
  shows "inverse_on (in_field (≤⇘L⇙)) l r"
proof (intro inverse_onI)
  fix x assume "in_field (≤⇘L⇙) x"
  moreover with gconn have "in_field (≤⇘L⇙) (η x)" by force
  ultimately consider "η x ≤⇘L⇙ x ∨ x ≤⇘L⇙ η x" | "η x = x" using conn by blast
  then show "r (l x) = x"
  proof cases
    case 1
    then show ?thesis using gconn asym by (cases rule: disjE) force+
  qed auto
qed

interpretation flip : galois R L r l .

corollary bijection_on_if_connected_on_if_asymmetric_if_galois_equivalence:
  assumes "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  and "asymmetric (≤⇘L⇙)" "asymmetric (≤⇘R⇙)"
  and "connected_on (in_field (≤⇘L⇙)) (≤⇘L⇙)" "connected_on (in_field (≤⇘R⇙)) (≤⇘R⇙)"
  shows "bijection_on (in_field (≤⇘L⇙)) (in_field (≤⇘R⇙)) l r"
  using assms by (intro transport_bijection.bijection_on_in_field transport_bijection.intro
    inverse_on_if_connected_on_if_asymmetric_if_galois_connection
    flip.inverse_on_if_connected_on_if_asymmetric_if_galois_connection)
  auto

end


end