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 "?x1L1 ?x2") by blast
  moreover assume "f1L f2"
  ultimately have "f1 ?x1 ≤⇘L2 ?x1 ?x2f2 ?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 L1x'  ((≤⇘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. x1L1 x2  ((≤⇘R2 (l1 x1) (l1 x2))  (≤⇘L2 x1 (η1 x2))) (r2⇘x1 (l1 x2))"
  and "x1 x2. x1L1 x2  (≤⇘L2 x1 (η1 x2))  (≤⇘L2 x1 x2)"
  and "x1 x2 y'. x1L1 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'. x1L1 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. x1L1 x2  ((≤⇘R2 (l1 x1) (l1 x2))  (≤⇘L2 x1 (η1 x2))) (r2⇘x1 (l1 x2))"
  and "x1 x2. x1L1 x2  (≤⇘L2 x1 (η1 x2))  (≤⇘L2 x1 x2)"
  and "x1 x2. x1L1 x2  (in_codom (≤⇘R2 (l1 x1) (l1 x2))  (≤⇘L2 x1 x2)) (r2⇘x1 (l1 x2)) (r2⇘x2 (l1 x2))"
  and "x1 x2. x1L1 x2  (in_dom (≤⇘R2 (l1 x1) (l1 x2))  (≤⇘L2 x1 x2)) (r2⇘x1 (l1 x1)) (r2⇘x1 (l1 x2))"
  and "x1 x2. x1L1 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 L1x'  ((≤⇘R2 (l1 x) x')  (≤⇘L2 x (r1 x'))) (r2⇘x x')"
  shows "x1 x2. x1L1 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 "x1L1 x2" for x1 x2
  proof -
    from x1L1 x2 have "x1 L1l1 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 "((≤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 = tpdfr.mono_wrt_rel_leftI[OF tfr.mono_wrt_rel_leftI]

end


end