Theory Transport_Functions

✐‹creator "Kevin Kappelmann"›
theory Transport_Functions
  imports
    Transport_Functions_Galois_Equivalence
    Transport_Functions_Galois_Relator
    Transport_Functions_Order_Base
    Transport_Functions_Order_Equivalence
    Transport_Functions_Relation_Simplifications
begin

paragraph ‹Summary›
text ‹Composition under (dependent) (monotone) function relators.
Refer to \<^cite>‹"transport"› for more details.›

subsection ‹Summary of Main Results›

text ‹More precise results can be found in the corresponding subtheories.›

paragraph ‹Monotone Dependent Function Relator›

context transport_Mono_Dep_Fun_Rel
begin

interpretation flip : transport_Mono_Dep_Fun_Rel R1 L1 r1 l1 R2 L2 r2 l2
  rewrites "flip.t1.counit ≡ η⇩1" and "flip.t1.unit ≡ ε⇩1"
  by (simp_all only: t1.flip_counit_eq_unit t1.flip_unit_eq_counit)

subparagraph ‹Closure of Order and Galois Concepts›

theorem preorder_galois_connection_if_galois_connectionI:
  assumes "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "reflexive_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ⊣ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "((_ x2 ∷ (≤⇘L1⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | (x2 ≤⇘L1⇙ x3 ∧ x4 ≤⇘L1⇙ η⇩1 x3)) ⇛ (≥)) L2"
  and "((x1' x2' ∷ (≤⇘R1⇙) | ε⇩1 x2' ≤⇘R1⇙ x1') ⇒ (x3' _ ∷ (≤⇘R1⇙) | x2' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ transitive (≤⇘R2 x1' x2'⇙)"
  shows "((≤⇘L⇙) ⊣⇘pre⇙ (≤⇘R⇙)) l r"
  using assms by (intro preorder_galois_connectionI
    galois_connection_left_right_if_mono_if_galois_connectionI'
    preorder_on_in_field_leftI flip.preorder_on_in_field_leftI
    tdfr.transitive_leftI' flip.tdfr.transitive_leftI
    tdfr.left_rel_right_iff_left_right_rel_if_galois_prop_le_assms_leftI
    tdfr.left_rel_right_iff_left_right_rel_if_galois_prop_le_assms_rightI)
  (auto intro: reflexive_on_if_le_pred_if_reflexive_on
      in_field_if_in_dom in_field_if_in_codom)

theorem preorder_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇘pre⇙ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "((x1 _ ∷ (≥⇘L1⇙)) ⇒ (x3 _ ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1' _ ∷ (≥⇘R1⇙)) ⇒ (x3' _ ∷ (≤⇘R1⇙) | x1' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  shows "((≤⇘L⇙) ≡⇘pre⇙ (≤⇘R⇙)) l r"
  using assms by (intro preorder_equivalence_if_galois_equivalenceI
    galois_equivalence_if_mono_if_preorder_equivalenceI'
    preorder_on_in_field_leftI flip.preorder_on_in_field_leftI
    tdfr.transitive_leftI' flip.tdfr.transitive_leftI
    tdfr.transitive_left2_if_preorder_equivalenceI
    tdfr.transitive_right2_if_preorder_equivalenceI
    tdfr.left_rel_right_iff_left_right_rel_if_galois_prop_le_assms_leftI
    tdfr.left_rel_right_iff_left_right_rel_if_galois_prop_le_assms_rightI
    tdfr.galois_equivalence_if_mono_if_galois_equivalence_mono_assms_leftI
    flip.tdfr.galois_equivalence_if_mono_if_galois_equivalence_mono_assms_leftI)
  (auto intro: reflexive_on_if_le_pred_if_reflexive_on
    in_field_if_in_dom in_field_if_in_codom)

theorem partial_equivalence_rel_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘PER⇙ (≤⇘R1⇙)) l1 r1"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇘PER⇙ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "((x1 _ ∷ (≥⇘L1⇙)) ⇒ (x3 _ ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1' _ ∷ (≥⇘R1⇙)) ⇒ (x3' _ ∷ (≤⇘R1⇙) | x1' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  shows "((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r"
  using assms
  by (intro partial_equivalence_rel_equivalence_if_galois_equivalenceI
    galois_equivalence_if_mono_if_preorder_equivalenceI'
    tdfr.transitive_left2_if_preorder_equivalenceI
    tdfr.transitive_right2_if_preorder_equivalenceI
    partial_equivalence_rel_leftI flip.partial_equivalence_rel_leftI
    tdfr.partial_equivalence_rel_left2_if_partial_equivalence_rel_equivalenceI
    tdfr.partial_equivalence_rel_right2_if_partial_equivalence_rel_equivalenceI)
  auto

subparagraph ‹Simplification of Left and Right Relations›

text ‹See @{thm "left_rel_eq_tdfr_leftI_if_equivalencesI"}.›


subparagraph ‹Simplification of Galois relator›

text ‹See
@{thm "left_Galois_eq_Dep_Fun_Rel_left_Galois_restrict_if_mono_if_galois_connectionI"
"left_Galois_eq_Dep_Fun_Rel_left_Galois_restrict_if_preorder_equivalenceI"
"left_Galois_eq_Dep_Fun_Rel_left_Galois_restrict_if_preorder_equivalenceI'"
"Dep_Fun_Rel_left_Galois_restrict_left_right_eq_Dep_Fun_Rel_left_GaloisI"
"Dep_Fun_Rel_left_Galois_restrict_left_right_restrict_left_right_eq"}›

end


paragraph ‹Monotone Function Relator›

context transport_Mono_Fun_Rel
begin

interpretation flip : transport_Mono_Fun_Rel R1 L1 r1 l1 R2 L2 r2 l2 .

subparagraph ‹Closure of Order and Galois Concepts›

lemma preorder_galois_connection_if_galois_connectionI:
  assumes "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)" "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ⊣ (≤⇘R2⇙)) l2 r2"
  and "transitive (≤⇘L2⇙)" "transitive (≤⇘R2⇙)"
  shows "((≤⇘L⇙) ⊣⇘pre⇙ (≤⇘R⇙)) l r"
  using assms by (intro tmdfr.preorder_galois_connectionI
    galois_connection_left_rightI
    tmdfr.preorder_on_in_field_leftI flip.tmdfr.preorder_on_in_field_leftI
    tfr.transitive_leftI' flip.tfr.transitive_leftI)
  auto

theorem preorder_galois_connectionI:
  assumes "((≤⇘L1⇙) ⊣⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "((≤⇘L2⇙) ⊣⇘pre⇙ (≤⇘R2⇙)) l2 r2"
  shows "((≤⇘L⇙) ⊣⇘pre⇙ (≤⇘R⇙)) l r"
  using assms by (intro preorder_galois_connection_if_galois_connectionI)
  (auto intro: reflexive_on_if_le_pred_if_reflexive_on
    in_field_if_in_dom in_field_if_in_codom)

theorem preorder_equivalence_if_galois_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇩G (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)" "reflexive_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ≡⇩G (≤⇘R2⇙)) l2 r2"
  and "transitive (≤⇘L2⇙)" "transitive (≤⇘R2⇙)"
  shows "((≤⇘L⇙) ≡⇘pre⇙ (≤⇘R⇙)) l r"
  using assms by (intro tmdfr.preorder_equivalence_if_galois_equivalenceI
    galois_equivalenceI
    tmdfr.preorder_on_in_field_leftI flip.tmdfr.preorder_on_in_field_leftI
    tfr.transitive_leftI flip.tfr.transitive_leftI)
  (auto intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_dom)

theorem preorder_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "((≤⇘L2⇙) ≡⇘pre⇙ (≤⇘R2⇙)) l2 r2"
  shows "((≤⇘L⇙) ≡⇘pre⇙ (≤⇘R⇙)) l r"
  using assms by (intro preorder_equivalence_if_galois_equivalenceI) auto

theorem partial_equivalence_rel_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘PER⇙ (≤⇘R1⇙)) l1 r1"
  and "((≤⇘L2⇙) ≡⇘PER⇙ (≤⇘R2⇙)) l2 r2"
  shows "((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r"
  using assms by (intro tmdfr.partial_equivalence_rel_equivalence_if_galois_equivalenceI
    galois_equivalenceI
    partial_equivalence_rel_leftI flip.partial_equivalence_rel_leftI)
  auto


subparagraph ‹Simplification of Left and Right Relations›

text ‹See @{thm "left_rel_eq_tfr_leftI"}.›


subparagraph ‹Simplification of Galois relator›

text ‹See @{thm "left_Galois_eq_Fun_Rel_left_Galois_restrictI"
"Fun_Rel_left_Galois_restrict_left_right_eq_Fun_Rel_left_GaloisI"
"Fun_Rel_left_Galois_restrict_left_right_restrict_left_right_eq"}.›

end


paragraph ‹Dependent Function Relator›

text ‹While a general transport of functions is only possible for the monotone
function relator (see above), the locales @{locale "transport_Dep_Fun_Rel"} and
@{locale "transport_Fun_Rel"} contain special cases to transport functions
that are proven to be monotone using the standard function space.

Moreover, in the special case of equivalences on partial equivalence relations,
the standard function space is monotone - see
@{thm "transport_Mono_Dep_Fun_Rel.left_rel_eq_tdfr_leftI_if_equivalencesI"}
As such, we can derive general transport theorems from the monotone cases
above.›

context transport_Dep_Fun_Rel
begin

interpretation tmdfr : transport_Mono_Dep_Fun_Rel L1 R1 l1 r1 L2 R2 l2 r2 .
interpretation flip : transport_Mono_Dep_Fun_Rel R1 L1 r1 l1 R2 L2 r2 l2
  rewrites "flip.t1.counit ≡ η⇩1" and "flip.t1.unit ≡ ε⇩1"
  by (simp_all only: t1.flip_counit_eq_unit t1.flip_unit_eq_counit)

theorem partial_equivalence_rel_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘PER⇙ (≤⇘R1⇙)) l1 r1"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇘PER⇙ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1' x2' ∷ (≥⇘R1⇙)) ⇒ (x3' x4' ∷ (≤⇘R1⇙) | x1' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  shows "((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r"
proof -
  from assms have "((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) = (tmdfr.L ≡⇘PER⇙ tmdfr.R)"
    by (subst tmdfr.left_rel_eq_tdfr_leftI_if_equivalencesI
        flip.left_rel_eq_tdfr_leftI_if_equivalencesI,
      auto intro!: partial_equivalence_rel_left2_if_partial_equivalence_rel_equivalenceI
        partial_equivalence_rel_right2_if_partial_equivalence_rel_equivalenceI
      iff: t1.galois_equivalence_right_left_iff_galois_equivalence_left_right)+
  with assms show ?thesis
    by (auto intro!: tmdfr.partial_equivalence_rel_equivalenceI)
qed

theorem left_Galois_eq_Dep_Fun_Rel_left_Galois_if_partial_equivalence_rel_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘PER⇙ (≤⇘R1⇙)) l1 r1"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇘PER⇙ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1' x2' ∷ (≥⇘R1⇙)) ⇒ (x3' x4' ∷ (≤⇘R1⇙) | x1' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  shows "(⇘L⇙⪅) = ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅))"
proof -
  from assms have rel_eqs: "(≤⇘L⇙) = tmdfr.L" "(≤⇘R⇙) = tmdfr.R"
    by (subst tmdfr.left_rel_eq_tdfr_leftI_if_equivalencesI flip.left_rel_eq_tdfr_leftI_if_equivalencesI,
      auto intro!: partial_equivalence_rel_left2_if_partial_equivalence_rel_equivalenceI
        partial_equivalence_rel_right2_if_partial_equivalence_rel_equivalenceI
      iff: t1.galois_equivalence_right_left_iff_galois_equivalence_left_right)+
  then have "(⇘L⇙⪅) = tmdfr.Galois" by simp
  also with assms have "... = ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅))↾⇘in_dom tmdfr.L⇙↿⇘in_codom tmdfr.R⇙"
    by (intro tmdfr.left_Galois_eq_Dep_Fun_Rel_left_Galois_restrict_if_preorder_equivalenceI
      transitive_left2_if_preorder_equivalenceI)
    (auto 6 2 intro!: partial_equivalence_rel_left2_if_partial_equivalence_rel_equivalenceI)
  also from rel_eqs have "... = ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅))↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙" by simp
  also with assms have "... = ((x x' ∷ (⇘L1⇙⪅)) ⇛ (⇘L2 x x'⇙⪅))"
    by (intro Dep_Fun_Rel_left_Galois_restrict_left_right_eq_Dep_Fun_Rel_left_GaloisI'
      transitive_left2_if_preorder_equivalenceI transitive_right2_if_preorder_equivalenceI
      galois_equivalence_if_mono_if_galois_equivalence_mono_assms_leftI
      flip.tdfr.galois_equivalence_if_mono_if_galois_equivalence_mono_assms_leftI)
    (auto iff: t1.galois_equivalence_right_left_iff_galois_equivalence_left_right, fast?)
  finally show ?thesis .
qed

end

paragraph ‹Function Relator›

context transport_Fun_Rel
begin

interpretation tmfr : transport_Mono_Fun_Rel L1 R1 l1 r1 L2 R2 l2 r2 .
interpretation flip : transport_Mono_Fun_Rel R1 L1 r1 l1 R2 L2 r2 l2 .

theorem partial_equivalence_rel_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘PER⇙ (≤⇘R1⇙)) l1 r1"
  and "((≤⇘L2⇙) ≡⇘PER⇙ (≤⇘R2⇙)) l2 r2"
  shows "((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r"
proof -
  from assms have "((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) = (tmfr.tmdfr.L ≡⇘PER⇙ tmfr.tmdfr.R)"
    by (subst tmfr.left_rel_eq_tfr_leftI flip.left_rel_eq_tfr_leftI; auto)+
  with assms show ?thesis by (auto intro!: tmfr.partial_equivalence_rel_equivalenceI)
qed

theorem left_Galois_eq_Fun_Rel_left_Galois_if_partial_equivalence_rel_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘PER⇙ (≤⇘R1⇙)) l1 r1"
  and "((≤⇘L2⇙) ≡⇘PER⇙ (≤⇘R2⇙)) l2 r2"
  shows "(⇘L⇙⪅) = ((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅))"
proof -
  from assms have rel_eqs: "(≤⇘L⇙) = tmfr.tmdfr.L" "(≤⇘R⇙) = tmfr.tmdfr.R"
    by (subst tmfr.left_rel_eq_tfr_leftI flip.left_rel_eq_tfr_leftI; auto)+
  then have "(⇘L⇙⪅) = tmfr.tmdfr.Galois" by simp
  also with assms have "... = ((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅))↾⇘in_dom tmfr.tmdfr.L⇙↿⇘in_codom tmfr.tmdfr.R⇙"
    by (intro tmfr.left_Galois_eq_Fun_Rel_left_Galois_restrictI)
      (auto intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_dom)
  also from rel_eqs have "... = ((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅))↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙" by simp
  also with assms have "... = ((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅))"
    by (intro Fun_Rel_left_Galois_restrict_left_right_eq_Fun_Rel_left_GaloisI) fastforce+
  finally show ?thesis .
qed

end


end