Theory Transport_Functions_Galois_Property

✐‹creator "Kevin Kappelmann"›
subsection ‹Galois Property›
theory Transport_Functions_Galois_Property
  imports
    Transport_Functions_Monotone
begin

paragraph ‹Dependent Function Relator›

context transport_Dep_Fun_Rel
begin

context
begin

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

lemma left_right_rel_if_left_rel_rightI:
  assumes mono_r1: "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and half_galois_prop_left1: "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and refl_R1: "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and half_galois_prop_left2: "⋀x'. x' ≤⇘R1⇙ x' ⟹
    ((≤⇘L2 (r1 x') (r1 x')⇙) ⇩h⊴ (≤⇘R2 (ε⇩1 x') x'⇙)) (l2⇘ x' (r1 x')⇙) (r2⇘(r1 x') x'⇙)"
  and R2_le1: "⋀x'. x' ≤⇘R1⇙ x' ⟹ (≤⇘R2 (ε⇩1 x') x'⇙) ≤ (≤⇘R2 x' x'⇙)"
  and R2_le2: "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 x1' x1'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and ge_L2_r2_le2: "⋀x' y'. x' ≤⇘R1⇙ x' ⟹ in_codom (≤⇘R2 (ε⇩1 x') x'⇙) y' ⟹
    (≥⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') (ε⇩1 x')⇙ y') ≤ (≥⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') x'⇙ y')"
  and trans_R2: "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ transitive (≤⇘R2 x1' x2'⇙)"
  and "g ≤⇘R⇙ g"
  and "f ≤⇘L⇙ r g"
  shows "l f ≤⇘R⇙ g"
proof (rule flip.left_relI)
  fix x1' x2'
  assume [iff]: "x1' ≤⇘R1⇙ x2'"
  with refl_R1 have [iff]: "x1' ≤⇘R1⇙ x1'" by auto
  with mono_r1 half_galois_prop_left1 have [iff]: "ε⇩1 x1' ≤⇘R1⇙ x1'"
    by (intro t1.counit_rel_if_right_rel_if_half_galois_prop_left_if_mono_wrt_rel)
  with refl_R1 have "ε⇩1 x1' ≤⇘R1⇙ ε⇩1 x1'" by blast
  with ‹g ≤⇘R⇙ g› have "g (ε⇩1 x1') ≤⇘R2 (ε⇩1 x1') (ε⇩1 x1')⇙ g (ε⇩1 x1')" by blast
  with R2_le2 have "g (ε⇩1 x1') ≤⇘R2 (ε⇩1 x1') x1'⇙ g (ε⇩1 x1')" by blast

  let ?x1 = "r1 x1'"
  from ‹f ≤⇘L⇙ r g› ‹x1' ≤⇘R1⇙ x1'› have "f ?x1 ≤⇘L2 ?x1 ?x1⇙ r g ?x1" using mono_r1 by blast
  then have "f ?x1 ≤⇘L2 ?x1 ?x1⇙ r2⇘?x1 (ε⇩1 x1')⇙ (g (ε⇩1 x1'))" by simp
  with ge_L2_r2_le2 have "f ?x1 ≤⇘L2 ?x1 ?x1⇙ r2⇘?x1 x1'⇙ (g (ε⇩1 x1'))"
    using ‹_ ≤⇘R2 (ε⇩1 x1') x1'⇙ g (ε⇩1 x1')› by blast
  with half_galois_prop_left2 have "l2⇘ x1' ?x1⇙ (f ?x1) ≤⇘R2 (ε⇩1 x1') x1'⇙ g (ε⇩1 x1')"
    using ‹_ ≤⇘R2 (ε⇩1 x1') x1'⇙ g (ε⇩1 x1')› by auto
  moreover from ‹g ≤⇘R⇙ g› ‹ε⇩1 x1' ≤⇘R1⇙ x1'› have "... ≤⇘R2 (ε⇩1 x1') x1'⇙ g x1'" by blast
  ultimately have "l2⇘ x1' ?x1⇙ (f ?x1) ≤⇘R2 (ε⇩1 x1') x1'⇙ g x1'" using trans_R2 by blast
  with R2_le1 R2_le2 have "l2⇘ x1' ?x1⇙ (f ?x1) ≤⇘R2 x1' x2'⇙ g x1'" by blast
  moreover from ‹g ≤⇘R⇙ g› ‹x1' ≤⇘R1⇙ x2'› have "... ≤⇘R2 x1' x2'⇙ g x2'" by blast
  ultimately have "l2⇘ x1' ?x1⇙ (f ?x1) ≤⇘R2 x1' x2'⇙ g x2'" using trans_R2 by blast
  then show "l f x1' ≤⇘R2 x1' x2'⇙ g x2'" by simp
qed

lemma left_right_rel_if_left_rel_right_ge_left2_assmI:
  assumes mono_r1: "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and "((in_codom (≤⇘R2 (ε⇩1 x') x'⇙)) ⇛ (≤⇘L2 (r1 x') (r1 x')⇙))
    (r2⇘(r1 x') (ε⇩1 x')⇙) (r2⇘(r1 x') x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "x' ≤⇘R1⇙ x'"
  and "in_codom (≤⇘R2 (ε⇩1 x') x'⇙) y'"
  shows "(≥⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') (ε⇩1 x')⇙ y') ≤ (≥⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') x'⇙ y')"
  using mono_wrt_relD[OF mono_r1] assms(2-) by blast

interpretation flip_inv :
  transport_Dep_Fun_Rel "(≥⇘R1⇙)" "(≥⇘L1⇙)" r1 l1 "flip2 R2" "flip2 L2" r2 l2
  rewrites "flip_inv.L ≡ (≥⇘R⇙)" and "flip_inv.R ≡ (≥⇘L⇙)"
  and "flip_inv.t1.counit ≡ η⇩1"
  and "⋀R x y. (flip2 R x y)¯ ≡ R y x"
  and "⋀R. in_dom R¯ ≡ in_codom R"
  and "⋀R x1 x2. in_codom (flip2 R x1 x2) ≡ in_dom (R x2 x1)"
  and "⋀R S. (R¯ ⇒ S¯) ≡ (R ⇒ S)"
  and "⋀R S x1 x2 x1' x2'. (flip2 R x1 x2 ⇩h⊴ flip2 S x1' x2') ≡ (S x2' x1' ⊴⇩h R x2 x1)¯"
  and "⋀R S. (R¯ ⇩h⊴ S¯) ≡ (S ⊴⇩h R)¯"
  and "⋀x1 x2 x3 x4. flip2 L2 x1 x2 ≤ flip2 L2 x3 x4 ≡ (≤⇘L2 x2 x1⇙) ≤ (≤⇘L2 x4 x3⇙)"
  and "⋀(R :: 'z ⇒ 'z ⇒ bool) (P :: 'z ⇒ bool). reflexive_on P R¯ ≡ reflexive_on P R"
  and "⋀R x1 x2. transitive (flip2 R x1 x2 :: 'z ⇒ 'z ⇒ bool) ≡ transitive (R x2 x1)"
  and "⋀x x. ((in_dom (≤⇘L2 x' (η⇩1 x')⇙)) ⇛ flip2 R2 (l1 x') (l1 x'))
    ≡ ((in_dom (≤⇘L2 x' (η⇩1 x')⇙)) ⇛ (≤⇘R2 (l1 x') (l1 x')⇙))¯"
  by (simp_all add: flip_inv_left_eq_ge_right flip_inv_right_eq_ge_left
    t1.flip_counit_eq_unit
    galois_prop.rel_inv_half_galois_prop_right_eq_half_galois_prop_left_rel_inv
    mono_wrt_rel_eq_dep_mono_wrt_rel Fun_Rel_pred_eq_Dep_Fun_Rel_pred)

lemma left_rel_right_if_left_right_relI:
  assumes "((≤⇘L1⇙) ⇒ (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ ((≤⇘L2 x (η⇩1 x)⇙) ⊴⇩h (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) x⇙) (r2⇘x (l1 x)⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ (≤⇘L2 x (η⇩1 x)⇙) ≤ (≤⇘L2 x x⇙)"
  and "⋀x y. x ≤⇘L1⇙ x ⟹ in_dom (≤⇘L2 x (η⇩1 x)⇙) y ⟹
    (≤⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) (η⇩1 x)⇙ y) ≤ (≤⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) x⇙ y)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "f ≤⇘L⇙ f"
  and "l f ≤⇘R⇙ g"
  shows "f ≤⇘L⇙ r g"
  using assms
  by (intro flip_inv.left_right_rel_if_left_rel_rightI[simplified rel_inv_iff_rel])

lemma left_rel_right_if_left_right_rel_le_right2_assmI:
  assumes "((≤⇘L1⇙) ⇒ (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙))¯ r1 l1"
  and "((in_dom (≤⇘L2 x (η⇩1 x)⇙)) ⇛ (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) x⇙) (l2⇘(l1 x) (η⇩1 x)⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ transitive (≤⇘R2 x1' x2'⇙)"
  and "x ≤⇘L1⇙ x"
  and "in_dom (≤⇘L2 x (η⇩1 x)⇙) y"
  shows "(≤⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) (η⇩1 x)⇙ y) ≤ (≤⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) x⇙ y)"
  using assms by (intro flip_inv.left_right_rel_if_left_rel_right_ge_left2_assmI
    [simplified rel_inv_iff_rel])
  auto

end

lemma left_rel_right_iff_left_right_relI:
  assumes "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹
    ((≤⇘L2 (r1 x') (r1 x')⇙) ⇩h⊴ (≤⇘R2 (ε⇩1 x') x'⇙)) (l2⇘ x' (r1 x')⇙) (r2⇘(r1 x') x'⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ ((≤⇘L2 x (η⇩1 x)⇙) ⊴⇩h (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) x⇙) (r2⇘x (l1 x)⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ (≤⇘L2 x (η⇩1 x)⇙) ≤ (≤⇘L2 x x⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹ (≤⇘R2 (ε⇩1 x') x'⇙) ≤ (≤⇘R2 x' x'⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 x1' x1'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x y. x ≤⇘L1⇙ x ⟹ in_dom (≤⇘L2 x (η⇩1 x)⇙) y ⟹
    (≤⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) (η⇩1 x)⇙ y) ≤ (≤⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) x⇙ y)"
  and "⋀x' y'. x' ≤⇘R1⇙ x' ⟹ in_codom (≤⇘R2 (ε⇩1 x') x'⇙) y' ⟹
    (≥⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') (ε⇩1 x')⇙ y') ≤ (≥⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') x'⇙ y')"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ transitive (≤⇘R2 x1' x2'⇙)"
  and "f ≤⇘L⇙ f"
  and "g ≤⇘R⇙ g"
  shows "f ≤⇘L⇙ r g ⟷ l f ≤⇘R⇙ g"
  using assms by (intro iffI left_right_rel_if_left_rel_rightI)
  (auto intro!: left_rel_right_if_left_right_relI)

lemma half_galois_prop_left2_if_half_galois_prop_left2_if_left_GaloisI:
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ⇩h⊴ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "x' ≤⇘R1⇙ x'"
  shows "((≤⇘L2 (r1 x') (r1 x')⇙) ⇩h⊴ (≤⇘R2 (ε⇩1 x') x'⇙)) (l2⇘ x' (r1 x')⇙) (r2⇘(r1 x') x'⇙)"
  using assms by (auto intro: t1.right_left_Galois_if_right_relI)

lemma half_galois_prop_right2_if_half_galois_prop_right2_if_left_GaloisI:
  assumes "((≤⇘L1⇙) ⇒ (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ⊴⇩h (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "x ≤⇘L1⇙ x"
  shows "((≤⇘L2 x (η⇩1 x)⇙) ⊴⇩h (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) x⇙) (r2⇘x (l1 x)⇙)"
  by (auto intro!: assms t1.left_Galois_left_if_left_relI)

lemma left_rel_right_iff_left_right_relI':
  assumes "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and galois_prop2: "⋀x x'. x ⇘L1⇙⪅ x' ⟹
    ((≤⇘L2 x (r1 x')⇙) ⊴ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ (≤⇘L2 x (η⇩1 x)⇙) ≤ (≤⇘L2 x x⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹ (≤⇘R2 (ε⇩1 x') x'⇙) ≤ (≤⇘R2 x' x'⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 x1' x1'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹
    ((in_dom (≤⇘L2 x (η⇩1 x)⇙)) ⇛ (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) x⇙) (l2⇘(l1 x) (η⇩1 x)⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹
    ((in_codom (≤⇘R2 (ε⇩1 x') x'⇙)) ⇛ (≤⇘L2 (r1 x') (r1 x')⇙)) (r2⇘(r1 x') (ε⇩1 x')⇙) (r2⇘(r1 x') x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ transitive (≤⇘R2 x1' x2'⇙)"
  and "f ≤⇘L⇙ f"
  and "g ≤⇘R⇙ g"
  shows "f ≤⇘L⇙ r g ⟷ l f ≤⇘R⇙ g"
proof -
  from galois_prop2 have
    "((≤⇘L2 x (r1 x')⇙) ⇩h⊴ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
    "((≤⇘L2 x (r1 x')⇙) ⊴⇩h (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
    if "x ⇘L1⇙⪅ x'" for x x'
    using ‹x ⇘L1⇙⪅ x'› by blast+
  with assms show ?thesis
    by (intro left_rel_right_iff_left_right_relI
      left_right_rel_if_left_rel_right_ge_left2_assmI
      left_rel_right_if_left_right_rel_le_right2_assmI
      half_galois_prop_left2_if_half_galois_prop_left2_if_left_GaloisI
      half_galois_prop_right2_if_half_galois_prop_right2_if_left_GaloisI)
    auto
qed

lemma left_rel_right_iff_left_right_rel_if_galois_prop_le_assms_leftI:
  assumes galois_conn1: "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and refl_L1: "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and antimono_L2:
    "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | (x2 ≤⇘L1⇙ x3 ∧ x4 ≤⇘L1⇙ η⇩1 x3)) ⇛ (≥)) L2"
  shows "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
proof -
  fix x1 x2 assume "x1 ≤⇘L1⇙ x2"
  with galois_conn1 refl_L1 have "x1 ≤⇘L1⇙ x1" "x2 ≤⇘L1⇙ η⇩1 x2"
    by (blast intro:
      t1.rel_unit_if_left_rel_if_half_galois_prop_right_if_mono_wrt_rel)+
  moreover with refl_L1 have "x2 ≤⇘L1⇙ x2" "η⇩1 x2 ≤⇘L1⇙ η⇩1 x2" by auto
  moreover note dep_mono_wrt_relD[OF antimono_L2 ‹x1 ≤⇘L1⇙ x2›]
    and dep_mono_wrt_relD[OF antimono_L2 ‹x1 ≤⇘L1⇙ x1›]
  ultimately show "(≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)" "(≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
    using ‹x1 ≤⇘L1⇙ x2› by auto
qed

lemma left_rel_right_iff_left_right_rel_if_galois_prop_le_assms_rightI:
  assumes galois_conn1: "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and refl_R1: "reflexive_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and mono_R2:
    "((x1' x2' ∷ (≤⇘R1⇙) | ε⇩1 x2' ≤⇘R1⇙ x1') ⇒ (x3' x4' ∷ (≤⇘R1⇙) | x2' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  shows "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 (ε⇩1 x1') x2'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 x1' x1'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
proof -
  fix x1' x2' assume "x1' ≤⇘R1⇙ x2'"
  with galois_conn1 refl_R1 have "x2' ≤⇘R1⇙ x2'" "ε⇩1 x1' ≤⇘R1⇙ x1'"
    by (blast intro:
      t1.counit_rel_if_right_rel_if_half_galois_prop_left_if_mono_wrt_rel)+
  moreover with refl_R1 have "x1' ≤⇘R1⇙ x1'" "ε⇩1 x1' ≤⇘R1⇙ ε⇩1 x1'" by auto
  moreover note dep_mono_wrt_relD[OF mono_R2 ‹ε⇩1 x1' ≤⇘R1⇙ x1'›]
    and dep_mono_wrt_relD[OF mono_R2 ‹x1' ≤⇘R1⇙ x1'›]
  ultimately show "(≤⇘R2 (ε⇩1 x1') x2'⇙) ≤ (≤⇘R2 x1' x2'⇙)" "(≤⇘R2 x1' x1'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
    using ‹x1' ≤⇘R1⇙ x2'› by auto
qed

corollary left_rel_right_iff_left_right_rel_if_monoI:
  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 "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | (x2 ≤⇘L1⇙ x3 ∧ x4 ≤⇘L1⇙ η⇩1 x3)) ⇛ (≥)) L2"
  and "((x1' x2' ∷ (≤⇘R1⇙) | ε⇩1 x2' ≤⇘R1⇙ x1') ⇒ (x3' x4' ∷ (≤⇘R1⇙) | x2' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "⋀x. x ≤⇘L1⇙ x ⟹
    ((in_dom (≤⇘L2 x (η⇩1 x)⇙)) ⇛ (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) x⇙) (l2⇘(l1 x) (η⇩1 x)⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹
    ((in_codom (≤⇘R2 (ε⇩1 x') x'⇙)) ⇛ (≤⇘L2 (r1 x') (r1 x')⇙)) (r2⇘(r1 x') (ε⇩1 x')⇙) (r2⇘(r1 x') x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ transitive (≤⇘R2 x1' x2'⇙)"
  and "f ≤⇘L⇙ f"
  and "g ≤⇘R⇙ g"
  shows "f ≤⇘L⇙ r g ⟷ l f ≤⇘R⇙ g"
  using assms by (intro left_rel_right_iff_left_right_relI'
    left_rel_right_iff_left_right_rel_if_galois_prop_le_assms_leftI
    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)

end


paragraph ‹Function Relator›

context transport_Fun_Rel
begin

corollary left_right_rel_if_left_rel_rightI:
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ⇩h⊴ (≤⇘R2⇙)) l2 r2"
  and "transitive (≤⇘R2⇙)"
  and "g ≤⇘R⇙ g"
  and "f ≤⇘L⇙ r g"
  shows "l f ≤⇘R⇙ g"
  using assms by (intro tdfr.left_right_rel_if_left_rel_rightI) simp_all

corollary left_rel_right_if_left_right_relI:
  assumes "((≤⇘L1⇙) ⇒ (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "((≤⇘L2⇙) ⊴⇩h (≤⇘R2⇙)) l2 r2"
  and "transitive (≤⇘L2⇙)"
  and "f ≤⇘L⇙ f"
  and "l f ≤⇘R⇙ g"
  shows "f ≤⇘L⇙ r g"
  using assms by (intro tdfr.left_rel_right_if_left_right_relI) simp_all

corollary left_rel_right_iff_left_right_relI:
  assumes "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ⊴ (≤⇘R2⇙)) l2 r2"
  and "transitive (≤⇘L2⇙)"
  and "transitive (≤⇘R2⇙)"
  and "f ≤⇘L⇙ f"
  and "g ≤⇘R⇙ g"
  shows "f ≤⇘L⇙ r g ⟷ l f ≤⇘R⇙ g"
  using assms by (intro tdfr.left_rel_right_iff_left_right_relI) auto

end


paragraph ‹Monotone Dependent Function Relator›

context transport_Mono_Dep_Fun_Rel
begin

lemma half_galois_prop_left_left_rightI:
  assumes "(tdfr.L ⇒ tdfr.R) l"
  and "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹
    ((≤⇘L2 (r1 x') (r1 x')⇙) ⇩h⊴ (≤⇘R2 (ε⇩1 x') x'⇙)) (l2⇘ x' (r1 x')⇙) (r2⇘(r1 x') x'⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹ (≤⇘R2 (ε⇩1 x') x'⇙) ≤ (≤⇘R2 x' x'⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 x1' x1'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x' y'. x' ≤⇘R1⇙ x' ⟹ in_codom (≤⇘R2 (ε⇩1 x') x'⇙) y' ⟹
    (≥⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') (ε⇩1 x')⇙ y') ≤ (≥⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') x'⇙ y')"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ transitive (≤⇘R2 x1' x2'⇙)"
  shows "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  unfolding left_rel_eq_tdfr_left_Refl_Rel right_rel_eq_tdfr_right_Refl_Rel using assms
  by (intro
    half_galois_prop_leftI[unfolded left_rel_eq_tdfr_left_Refl_Rel right_rel_eq_tdfr_right_Refl_Rel]
    Refl_Rel_app_leftI[where ?f=l]
    tdfr.left_right_rel_if_left_rel_rightI)
  (auto elim!: galois_rel.left_GaloisE)

lemma half_galois_prop_right_left_rightI:
  assumes "(tdfr.R ⇒ tdfr.L) r"
  and "((≤⇘L1⇙) ⇒ (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ ((≤⇘L2 x (η⇩1 x)⇙) ⊴⇩h (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) x⇙) (r2⇘x (l1 x)⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ (≤⇘L2 x (η⇩1 x)⇙) ≤ (≤⇘L2 x x⇙)"
  and "⋀x y. x ≤⇘L1⇙ x ⟹ in_dom (≤⇘L2 x (η⇩1 x)⇙) y ⟹
    (≤⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) (η⇩1 x)⇙ y) ≤ (≤⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) x⇙ y)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  shows "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  unfolding left_rel_eq_tdfr_left_Refl_Rel right_rel_eq_tdfr_right_Refl_Rel using assms
  by (intro
    half_galois_prop_rightI[unfolded left_rel_eq_tdfr_left_Refl_Rel right_rel_eq_tdfr_right_Refl_Rel]
    Refl_Rel_app_rightI[where ?f=r]
    tdfr.left_rel_right_if_left_right_relI)
  (auto elim!: galois_rel.left_GaloisE in_codomE Refl_RelE intro!: in_fieldI)

corollary galois_prop_left_rightI:
  assumes "(tdfr.L ⇒ tdfr.R) l" and "(tdfr.R ⇒ tdfr.L) r"
  and "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹
    ((≤⇘L2 (r1 x') (r1 x')⇙) ⇩h⊴ (≤⇘R2 (ε⇩1 x') x'⇙)) (l2⇘ x' (r1 x')⇙) (r2⇘(r1 x') x'⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ ((≤⇘L2 x (η⇩1 x)⇙) ⊴⇩h (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) x⇙) (r2⇘x (l1 x)⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ (≤⇘L2 x (η⇩1 x)⇙) ≤ (≤⇘L2 x x⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹ (≤⇘R2 (ε⇩1 x') x'⇙) ≤ (≤⇘R2 x' x'⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 x1' x1'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x y. x ≤⇘L1⇙ x ⟹ in_dom (≤⇘L2 x (η⇩1 x)⇙) y ⟹
    (≤⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) (η⇩1 x)⇙ y) ≤ (≤⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) x⇙ y)"
  and "⋀x' y'. x' ≤⇘R1⇙ x' ⟹ in_codom (≤⇘R2 (ε⇩1 x') x'⇙) y' ⟹
    (≥⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') (ε⇩1 x')⇙ y') ≤ (≥⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') x'⇙ y')"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ transitive (≤⇘R2 x1' x2'⇙)"
  shows "((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
  using assms by (intro galois_propI half_galois_prop_left_left_rightI
    half_galois_prop_right_left_rightI)
  auto

corollary galois_prop_left_rightI':
  assumes "(tdfr.L ⇒ tdfr.R) l" and "(tdfr.R ⇒ tdfr.L) r"
  and "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and galois_prop2: "⋀x x'. x ⇘L1⇙⪅ x' ⟹
    ((≤⇘L2 x (r1 x')⇙) ⊴ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ (≤⇘L2 x (η⇩1 x)⇙) ≤ (≤⇘L2 x x⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹ (≤⇘R2 (ε⇩1 x') x'⇙) ≤ (≤⇘R2 x' x'⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 x1' x1'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹
    ((in_dom (≤⇘L2 x (η⇩1 x)⇙)) ⇛ (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) x⇙) (l2⇘(l1 x) (η⇩1 x)⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹
    ((in_codom (≤⇘R2 (ε⇩1 x') x'⇙)) ⇛ (≤⇘L2 (r1 x') (r1 x')⇙)) (r2⇘(r1 x') (ε⇩1 x')⇙) (r2⇘(r1 x') x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ transitive (≤⇘R2 x1' x2'⇙)"
  shows "((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
proof -
  from galois_prop2 have
    "((≤⇘L2 x (r1 x')⇙) ⇩h⊴ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
    "((≤⇘L2 x (r1 x')⇙) ⊴⇩h (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
    if "x ⇘L1⇙⪅ x'" for x x'
    using ‹x ⇘L1⇙⪅ x'› by blast+
  with assms show ?thesis by (intro galois_prop_left_rightI
    tdfr.left_right_rel_if_left_rel_right_ge_left2_assmI
    tdfr.left_rel_right_if_left_right_rel_le_right2_assmI
    tdfr.half_galois_prop_left2_if_half_galois_prop_left2_if_left_GaloisI
    tdfr.half_galois_prop_right2_if_half_galois_prop_right2_if_left_GaloisI)
    auto
qed

corollary galois_prop_left_right_if_mono_if_galois_propI:
  assumes "(tdfr.L ⇒ tdfr.R) l" and "(tdfr.R ⇒ tdfr.L) r"
  and "((≤⇘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 "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | (x2 ≤⇘L1⇙ x3 ∧ x4 ≤⇘L1⇙ η⇩1 x3)) ⇛ (≥)) L2"
  and "((x1' x2' ∷ (≤⇘R1⇙) | ε⇩1 x2' ≤⇘R1⇙ x1') ⇒ (x3' x4' ∷ (≤⇘R1⇙) | x2' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "⋀x. x ≤⇘L1⇙ x ⟹
    ((in_dom (≤⇘L2 x (η⇩1 x)⇙)) ⇛ (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) x⇙) (l2⇘(l1 x) (η⇩1 x)⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹
    ((in_codom (≤⇘R2 (ε⇩1 x') x'⇙)) ⇛ (≤⇘L2 (r1 x') (r1 x')⇙)) (r2⇘(r1 x') (ε⇩1 x')⇙) (r2⇘(r1 x') x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ transitive (≤⇘R2 x1' x2'⇙)"
  shows "((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
  using assms by (intro galois_prop_left_rightI'
    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)

text ‹Note that we could further rewrite
@{thm "galois_prop_left_right_if_mono_if_galois_propI"},
as we will do later for Galois connections, by applying
@{thm "tdfr.mono_wrt_rel_leftI"} and @{thm "tdfr.mono_wrt_rel_rightI"} to the
first premises. However, this is not really helpful here.
Moreover, the resulting theorem will not result in a
useful lemma for the flipped instance of @{locale transport_Dep_Fun_Rel}
since @{thm "tdfr.mono_wrt_rel_leftI"} and @{thm "tdfr.mono_wrt_rel_rightI"} are
not flipped dual but only flipped-inversed dual.›

end


paragraph ‹Monotone Function Relator›

context transport_Mono_Fun_Rel
begin

lemma half_galois_prop_left_left_rightI:
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ⇒ (≤⇘R2⇙)) l2"
  and "((≤⇘L2⇙) ⇩h⊴ (≤⇘R2⇙)) l2 r2"
  and "transitive (≤⇘R2⇙)"
  shows "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  using assms by (intro tpdfr.half_galois_prop_left_left_rightI tfr.mono_wrt_rel_leftI)
  simp_all

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

lemma half_galois_prop_right_left_rightI:
  assumes "((≤⇘L1⇙) ⇒ (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "((≤⇘R2⇙) ⇒ (≤⇘L2⇙)) r2"
  and "((≤⇘L2⇙) ⊴⇩h (≤⇘R2⇙)) l2 r2"
  and "transitive (≤⇘L2⇙)"
  shows "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  using assms by (intro tpdfr.half_galois_prop_right_left_rightI flip.tfr.mono_wrt_rel_leftI)
  simp_all

corollary galois_prop_left_rightI:
  assumes "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ⊣ (≤⇘R2⇙)) l2 r2"
  and "transitive (≤⇘L2⇙)"
  and "transitive (≤⇘R2⇙)"
  shows "((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
  using assms by (intro tpdfr.galois_propI
    half_galois_prop_left_left_rightI half_galois_prop_right_left_rightI)
  auto

end


end