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⇙)) ⇛⇩m (x3 x4 ∷ (≤⇘L1⇙) | (x2 ≤⇘L1⇙ x3 ∧ x4 ≤⇘L1⇙ η⇩1 x3)) ⇛ (≥)) L2"
  and "((x1' x2' ∷ (≤⇘R1⇙) | ε⇩1 x2' ≤⇘R1⇙ x1') ⇛⇩m (x3' _ ∷ (≤⇘R1⇙) | x2' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇛⇩m (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (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⇙)) ⇛⇩m (x3 _ ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1' _ ∷ (≥⇘R1⇙)) ⇛⇩m (x3' _ ∷ (≤⇘R1⇙) | x1' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇛⇩m (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (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⇙)) ⇛⇩m (x3 _ ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1' _ ∷ (≥⇘R1⇙)) ⇛⇩m (x3' _ ∷ (≤⇘R1⇙) | x1' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇛⇩m (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (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 tpdfr.preorder_galois_connectionI
    galois_connection_left_rightI
    tpdfr.preorder_on_in_field_leftI flip.tpdfr.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 tpdfr.preorder_equivalence_if_galois_equivalenceI
    galois_equivalenceI
    tpdfr.preorder_on_in_field_leftI flip.tpdfr.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 tpdfr.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 tpdfr : 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 .

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⇙)) ⇛⇩m (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1' x2' ∷ (≥⇘R1⇙)) ⇛⇩m (x3' x4' ∷ (≤⇘R1⇙) | x1' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇛⇩m (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇛⇩m (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⇙)) = (tpdfr.L ≡⇘PER⇙ tpdfr.R)"
    by (subst tpdfr.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!: tpdfr.partial_equivalence_rel_equivalenceI)
qed

end


paragraph ‹Function Relator›

context transport_Fun_Rel
begin

interpretation tpfr : transport_Mono_Fun_Rel L1 R1 l1 r1 L2 R2 l2 r2 .
interpretation flip_tpfr : 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⇙)) = (tpfr.tpdfr.L ≡⇘PER⇙ tpfr.tpdfr.R)"
    by (subst tpfr.left_rel_eq_tfr_leftI flip_tpfr.left_rel_eq_tfr_leftI; auto)+
  with assms show ?thesis by (auto intro!: tpfr.partial_equivalence_rel_equivalenceI)
qed

end


end