Theory Transport_Functions_Monotone

✐‹creator "Kevin Kappelmann"›
subsection ‹Monotonicity›
theory Transport_Functions_Monotone
  imports
    Transport_Functions_Base
begin

paragraph ‹Dependent Function Relator›

context transport_Dep_Fun_Rel
begin

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

lemma mono_wrt_rel_leftI:
  assumes mono_r1: "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and mono_l2: "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹
    ((≤⇘L2 (r1 x1') (r1 x2')⇙) ⇒ (≤⇘R2 (ε⇩1 x1') x2'⇙)) (l2⇘x2' (r1 x1')⇙)"
  and R2_le1: "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 (ε⇩1 x1') x2'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and R2_l2_le1: "⋀x1' x2' y. x1' ≤⇘R1⇙ x2' ⟹ in_dom (≤⇘L2 (r1 x1') (r1 x2')⇙) y ⟹
    (≤⇘R2 x1' x2'⇙) (l2⇘x2' (r1 x1')⇙ y) ≤ (≤⇘R2 x1' x2'⇙) (l2⇘x1' (r1 x1')⇙ y)"
  and ge_R2_l2_le2: "⋀x1' x2' y. x1' ≤⇘R1⇙ x2' ⟹ in_codom (≤⇘L2 (r1 x1') (r1 x2')⇙) y ⟹
    (≥⇘R2 x1' x2'⇙) (l2⇘x2' (r1 x1')⇙ y) ≤ (≥⇘R2 x1' x2'⇙) (l2⇘x2' (r1 x2')⇙ y)"
  shows "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
proof (intro mono_wrt_relI flip.left_relI)
  fix f1 f2 x1' x2' assume [iff]: "x1' ≤⇘R1⇙ x2'"
  with mono_r1 have "r1 x1' ≤⇘L1⇙ r1 x2'" (is "?x1 ≤⇘L1⇙ ?x2") by blast
  moreover assume "f1 ≤⇘L⇙ f2"
  ultimately have "f1 ?x1 ≤⇘L2 ?x1 ?x2⇙ f2 ?x2" (is "?y1 ≤⇘L2 ?x1 ?x2⇙ ?y2") by blast
  with mono_l2 have "l2⇘x2' ?x1⇙ ?y1 ≤⇘R2 (ε⇩1 x1') x2'⇙ l2⇘x2' ?x1⇙ ?y2" by blast
  with R2_le1 have "l2⇘x2' ?x1⇙ ?y1 ≤⇘R2 x1' x2'⇙ l2⇘x2' ?x1⇙ ?y2" by blast
  with R2_l2_le1 have "l2⇘x1' ?x1⇙ ?y1 ≤⇘R2 x1' x2'⇙ l2⇘x2' ?x1⇙ ?y2"
    using ‹?y1 ≤⇘L2 ?x1 ?x2⇙ _›  by blast
  with ge_R2_l2_le2 have "l2⇘x1' ?x1⇙ ?y1 ≤⇘R2 x1' x2'⇙ l2⇘x2' ?x2⇙ ?y2"
    using ‹_ ≤⇘L2 ?x1 ?x2⇙ ?y2›  by blast
  then show "l f1 x1' ≤⇘R2 x1' x2'⇙ l f2 x2'" by simp
qed

lemma mono_wrt_rel_left_in_dom_mono_left_assm:
  assumes "(in_dom (≤⇘L2 (r1 x1') (r1 x2')⇙) ⇛ (≤⇘R2 x1' x2'⇙)) (l2⇘x1' (r1 x1')⇙) (l2⇘x2' (r1 x1')⇙)"
  and "transitive (≤⇘R2 x1' x2'⇙)"
  and "x1' ≤⇘R1⇙ x2'"
  and "in_dom (≤⇘L2 (r1 x1') (r1 x2')⇙) y"
  shows "(≤⇘R2 x1' x2'⇙) (l2⇘x2' (r1 x1')⇙ y) ≤ (≤⇘R2 x1' x2'⇙) (l2⇘x1' (r1 x1')⇙ y)"
  using assms by blast

lemma mono_wrt_rel_left_in_codom_mono_left_assm:
  assumes "(in_codom (≤⇘L2 (r1 x1') (r1 x2')⇙) ⇛ (≤⇘R2 x1' x2'⇙)) (l2⇘x2' (r1 x1')⇙) (l2⇘x2' (r1 x2')⇙)"
  and "transitive (≤⇘R2 x1' x2'⇙)"
  and "x1' ≤⇘R1⇙ x2'"
  and "in_codom (≤⇘L2 (r1 x1') (r1 x2')⇙) y"
  shows "(≥⇘R2 x1' x2'⇙) (l2⇘x2' (r1 x1')⇙ y) ≤ (≥⇘R2 x1' x2'⇙) (l2⇘x2' (r1 x2')⇙ y)"
  using assms by blast

lemma mono_wrt_rel_left_if_transitiveI:
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹
    ((≤⇘L2 (r1 x1') (r1 x2')⇙) ⇒ (≤⇘R2 (ε⇩1 x1') x2'⇙)) (l2⇘x2' (r1 x1')⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 (ε⇩1 x1') x2'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹
    (in_dom (≤⇘L2 (r1 x1') (r1 x2')⇙) ⇛ (≤⇘R2 x1' x2'⇙)) (l2⇘x1' (r1 x1')⇙) (l2⇘x2' (r1 x1')⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹
    (in_codom (≤⇘L2 (r1 x1') (r1 x2')⇙) ⇛ (≤⇘R2 x1' x2'⇙)) (l2⇘x2' (r1 x1')⇙) (l2⇘x2' (r1 x2')⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ transitive (≤⇘R2 x1' x2'⇙)"
  shows "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  using assms by (intro mono_wrt_rel_leftI
    mono_wrt_rel_left_in_dom_mono_left_assm
    mono_wrt_rel_left_in_codom_mono_left_assm)
  auto

lemma mono_wrt_rel_left2_if_mono_wrt_rel_left2_if_left_GaloisI:
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ⇒ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙)"
  shows "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹
    ((≤⇘L2 (r1 x1') (r1 x2')⇙) ⇒ (≤⇘R2 (ε⇩1 x1') x2'⇙)) (l2⇘x2' (r1 x1')⇙)"
  using assms by (intro mono_wrt_relI) fastforce

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

lemma mono_wrt_rel_rightI:
  assumes "((≤⇘L1⇙) ⇒ (≤⇘R1⇙)) l1"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ ((≤⇘R2 (l1 x1) (l1 x2)⇙) ⇒ (≤⇘L2 x1 (η⇩1 x2)⇙)) (r2⇘x1 (l1 x2)⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2 y'. x1 ≤⇘L1⇙ x2 ⟹ in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙) y' ⟹
    (≥⇘L2 x1 x2⇙) (r2⇘x1 (l1 x2)⇙ y') ≤ (≥⇘L2 x1 x2⇙) (r2⇘x2 (l1 x2)⇙ y')"
  and "⋀x1 x2 y'. x1 ≤⇘L1⇙ x2 ⟹ in_dom (≤⇘R2 (l1 x1) (l1 x2)⇙) y' ⟹
    (≤⇘L2 x1 x2⇙) (r2⇘x1 (l1 x2)⇙ y') ≤ (≤⇘L2 x1 x2⇙) (r2⇘x1 (l1 x1)⇙ y')"
  shows "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  using assms by (intro flip_inv.mono_wrt_rel_leftI[simplified rel_inv_iff_rel])

lemma mono_wrt_rel_right_if_transitiveI:
  assumes "((≤⇘L1⇙) ⇒ (≤⇘R1⇙)) l1"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ ((≤⇘R2 (l1 x1) (l1 x2)⇙) ⇒ (≤⇘L2 x1 (η⇩1 x2)⇙)) (r2⇘x1 (l1 x2)⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙) ⇛ (≤⇘L2 x1 x2⇙)) (r2⇘x1 (l1 x2)⇙) (r2⇘x2 (l1 x2)⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (in_dom (≤⇘R2 (l1 x1) (l1 x2)⇙) ⇛ (≤⇘L2 x1 x2⇙)) (r2⇘x1 (l1 x1)⇙) (r2⇘x1 (l1 x2)⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  shows "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  using assms by (intro flip_inv.mono_wrt_rel_left_if_transitiveI
    [simplified rel_inv_iff_rel])

lemma mono_wrt_rel_right2_if_mono_wrt_rel_right2_if_left_GaloisI:
  assumes assms1: "((≤⇘L1⇙) ⇒ (≤⇘R1⇙)) l1" "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and mono_r2: "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘R2 (l1 x) x'⇙) ⇒ (≤⇘L2 x (r1 x')⇙)) (r2⇘x x'⇙)"
  shows "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ ((≤⇘R2 (l1 x1) (l1 x2)⇙) ⇒ (≤⇘L2 x1 (η⇩1 x2)⇙)) (r2⇘x1 (l1 x2)⇙)"
proof -
  show "((≤⇘R2 (l1 x1) (l1 x2)⇙) ⇒ (≤⇘L2 x1 (η⇩1 x2)⇙)) (r2⇘x1 (l1 x2)⇙)" if "x1 ≤⇘L1⇙ x2" for x1 x2
  proof -
    from ‹x1 ≤⇘L1⇙ x2› have "x1 ⇘L1⇙⪅ l1 x2"
      using assms1 by (intro t1.left_Galois_left_if_left_relI) blast
    with mono_r2 show ?thesis by auto
  qed
qed

end


paragraph ‹Function Relator›

context transport_Fun_Rel
begin

lemma mono_wrt_rel_leftI:
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹((≤⇘L2⇙) ⇒ (≤⇘R2⇙)) l2"
  shows "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  using assms by (intro tdfr.mono_wrt_rel_leftI) simp_all

end


paragraph ‹Monotone Dependent Function Relator›

context transport_Mono_Dep_Fun_Rel
begin

lemmas mono_wrt_rel_leftI = mono_wrt_rel_Refl_Rel_Refl_Rel_if_mono_wrt_rel
  [of tdfr.L tdfr.R l, folded transport_defs]

end

paragraph ‹Monotone Function Relator›

context transport_Mono_Fun_Rel
begin

lemmas mono_wrt_rel_leftI = tmdfr.mono_wrt_rel_leftI[OF tfr.mono_wrt_rel_leftI]

end


end