Theory Transport_Compositions_Generic_Base

✐‹creator "Kevin Kappelmann"›
section ‹Generic Compositions›
subsection ‹Basic Setup›
theory Transport_Compositions_Generic_Base
  imports
    Equivalence_Relations
    Transport_Base
begin

locale transport_comp =
  t1 : transport L1 R1 l1 r1 + t2 : transport L2 R2 l2 r2
  for L1 :: "'a ⇒ 'a ⇒ bool"
  and R1 :: "'b ⇒ 'b ⇒ bool"
  and l1 :: "'a ⇒ 'b"
  and r1 :: "'b ⇒ 'a"
  and L2 :: "'b ⇒ 'b ⇒ bool"
  and R2 :: "'c ⇒ 'c ⇒ bool"
  and l2 :: "'b ⇒ 'c"
  and r2 :: "'c ⇒ 'b"
begin

text ‹This locale collects results about the composition of transportable
components under some generic compatibility conditions on @{term "R1"} and
@{term "L2"} (cf. below). The composition is rather subtle, but in return can
cover quite general cases.

Explanations and intuition about the construction can be found in \<^cite>‹"transport"›.›

notation L1 (infix "≤⇘L1⇙" 50)
notation R1 (infix "≤⇘R1⇙" 50)
notation L2 (infix "≤⇘L2⇙" 50)
notation R2 (infix "≤⇘R2⇙" 50)

notation t1.ge_left (infix "≥⇘L1⇙" 50)
notation t1.ge_right (infix "≥⇘R1⇙" 50)
notation t2.ge_left (infix "≥⇘L2⇙" 50)
notation t2.ge_right (infix "≥⇘R2⇙" 50)

notation t1.left_Galois (infix "⇘L1⇙⪅" 50)
notation t1.right_Galois (infix "⇘R1⇙⪅" 50)
notation t2.left_Galois (infix "⇘L2⇙⪅" 50)
notation t2.right_Galois (infix "⇘R2⇙⪅" 50)

notation t1.ge_Galois_left (infix "⪆⇘L1⇙" 50)
notation t1.ge_Galois_right (infix "⪆⇘R1⇙" 50)
notation t2.ge_Galois_left (infix "⪆⇘L2⇙" 50)
notation t2.ge_Galois_right (infix "⪆⇘R2⇙" 50)

notation t1.right_ge_Galois (infix "⇘R1⇙⪆" 50)
notation t1.Galois_right (infix "⪅⇘R1⇙" 50)
notation t2.right_ge_Galois (infix "⇘R2⇙⪆" 50)
notation t2.Galois_right (infix "⪅⇘R2⇙" 50)

notation t1.left_ge_Galois (infix "⇘L1⇙⪆" 50)
notation t1.Galois_left (infix "⪅⇘L1⇙" 50)
notation t2.left_ge_Galois (infix "⇘L2⇙⪆" 50)
notation t2.Galois_left (infix "⪅⇘L2⇙" 50)

notation t1.unit ("η⇩1")
notation t1.counit ("ε⇩1")
notation t2.unit ("η⇩2")
notation t2.counit ("ε⇩2")

definition "L ≡ (⇘L1⇙⪅) ∘∘ (≤⇘L2⇙) ∘∘ (⇘R1⇙⪅)"

lemma left_rel_eq_comp: "L = (⇘L1⇙⪅) ∘∘ (≤⇘L2⇙) ∘∘ (⇘R1⇙⪅)"
  unfolding L_def ..

definition "l ≡ l2 ∘ l1"

lemma left_eq_comp: "l = l2 ∘ l1"
  unfolding l_def ..

lemma left_eq [simp]: "l x = l2 (l1 x)"
  unfolding left_eq_comp by simp

context
begin

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

abbreviation "R ≡ flip.L"
abbreviation "r ≡ flip.l"

lemma right_rel_eq_comp: "R = (⇘R2⇙⪅) ∘∘ (≤⇘R1⇙) ∘∘ (⇘L2⇙⪅)"
  unfolding flip.L_def ..

lemma right_eq_comp: "r = r1 ∘ r2"
  unfolding flip.l_def ..

lemma right_eq [simp]: "r z = r1 (r2 z)"
  unfolding right_eq_comp by simp

lemmas transport_defs = left_rel_eq_comp left_eq_comp right_rel_eq_comp right_eq_comp

end

sublocale transport L R l r .

(*FIXME: somehow the notation for the fixed parameters L and R, defined in
Order_Functions_Base.thy, is lost. We hence re-declare it here.*)
notation L (infix "≤⇘L⇙" 50)
notation R (infix "≤⇘R⇙" 50)

lemma left_relI [intro]:
  assumes "x ⇘L1⇙⪅ y"
  and "y ≤⇘L2⇙ y'"
  and "y' ⇘R1⇙⪅ x'"
  shows "x ≤⇘L⇙ x'"
  unfolding left_rel_eq_comp using assms by blast

lemma left_relE [elim]:
  assumes "x ≤⇘L⇙ x'"
  obtains y y' where "x ⇘L1⇙⪅ y" "y ≤⇘L2⇙ y'" "y' ⇘R1⇙⪅ x'"
  using assms unfolding left_rel_eq_comp by blast

context
begin

interpretation flip : transport_comp R2 L2 r2 l2 R1 L1 r1 l1 .
interpretation inv : transport_comp "(≥⇘L1⇙)" "(≥⇘R1⇙)" l1 r1 "(≥⇘L2⇙)" "(≥⇘R2⇙)" l2 r2 .

lemma ge_left_rel_eq_left_rel_inv_if_galois_prop [simp]:
  assumes "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1" "((≤⇘R1⇙) ⊴ (≤⇘L1⇙)) r1 l1"
  shows "(≥⇘L⇙) = transport_comp.L (≥⇘L1⇙) (≥⇘R1⇙) l1 r1 (≥⇘L2⇙)"
  using assms unfolding left_rel_eq_comp inv.left_rel_eq_comp
  by (simp add: rel_comp_assoc)

corollary left_rel_inv_iff_left_rel_if_galois_prop [iff]:
  assumes "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1" "((≤⇘R1⇙) ⊴ (≤⇘L1⇙)) r1 l1"
  shows "(transport_comp.L (≥⇘L1⇙) (≥⇘R1⇙) l1 r1 (≥⇘L2⇙)) x x' ⟷ x' ≤⇘L⇙ x"
  using assms by (simp flip: ge_left_rel_eq_left_rel_inv_if_galois_prop)


subsubsection ‹Simplification of Relations›

lemma left_rel_le_left_rel1I:
  assumes "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and "((≤⇘R1⇙) ⇩h⊴ (≤⇘L1⇙)) r1 l1"
  and trans_L1: "transitive (≤⇘L1⇙)"
  and mono_l1: "((≤⇘L⇙) ⇛⇩m ((≤⇘R1⇙) ∘∘ (≤⇘R1⇙))) l1"
  shows "(≤⇘L⇙) ≤ (≤⇘L1⇙)"
proof (rule le_relI)
  fix x x' assume "x ≤⇘L⇙ x'"
  with mono_l1 obtain y where "l1 x ≤⇘R1⇙ y" "y ≤⇘R1⇙ l1 x'" by blast
  with ‹((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1› ‹x ≤⇘L⇙ x'› have "x ≤⇘L1⇙ r1 y" by blast
  moreover from ‹((≤⇘R1⇙) ⇩h⊴ (≤⇘L1⇙)) r1 l1› ‹y ≤⇘R1⇙ l1 x'› ‹x ≤⇘L⇙ x'›
    have "... ≤⇘L1⇙ x'" by blast
  ultimately show "x ≤⇘L1⇙ x'" using trans_L1 by blast
qed

lemma left_rel1_le_left_relI:
  assumes "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and mono_l1: "((≤⇘L1⇙) ⇛⇩m ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙))) l1"
  shows "(≤⇘L1⇙) ≤ (≤⇘L⇙)"
proof (rule le_relI)
  fix x x' assume "x ≤⇘L1⇙ x'"
  with mono_l1 obtain y y' where
    "l1 x ≤⇘R1⇙ y" "y ≤⇘L2⇙ y'" "y' ≤⇘R1⇙ l1 x'" by blast
  with ‹((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1› ‹x ≤⇘L1⇙ x'› have "x ⇘L1⇙⪅ y" by blast
  moreover note ‹y ≤⇘L2⇙ y'›
  moreover from ‹y' ≤⇘R1⇙ l1 x'› ‹x ≤⇘L1⇙ x'› have "y' ⇘R1⇙⪅ x'" by blast
  ultimately show "x ≤⇘L⇙ x'" by blast
qed

corollary left_rel_eq_left_rel1I:
  assumes "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and "((≤⇘R1⇙) ⇩h⊴ (≤⇘L1⇙)) r1 l1"
  and "transitive (≤⇘L1⇙)"
  and "((≤⇘L⇙) ⇛⇩m ((≤⇘R1⇙) ∘∘ (≤⇘R1⇙))) l1"
  and "((≤⇘L1⇙) ⇛⇩m ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙))) l1"
  shows "(≤⇘L⇙) = (≤⇘L1⇙)"
  using assms by (intro antisym left_rel_le_left_rel1I left_rel1_le_left_relI)

text ‹Note that we may not necessarily have @{term "(≤⇘L⇙) = (≤⇘L1⇙)"}, even in
case of equivalence relations. Depending on the use case, one thus may wish to
use an alternative composition operation.›

lemma ex_order_equiv_left_rel_neq_left_rel1:
  "∃(L1 :: bool ⇒ _) (R1 :: bool ⇒ _) l1 r1
    (L2 :: bool ⇒ _) (R2 :: bool ⇒ _) l2 r2.
    (L1 ≡⇩o R1) l1 r1
    ∧ equivalence_rel L1 ∧ equivalence_rel R1
    ∧ (L2 ≡⇩o R2) l2 r2
    ∧ equivalence_rel L2 ∧ equivalence_rel R2
    ∧ transport_comp.L L1 R1 l1 r1 L2 ≠ L1"
proof (intro exI conjI)
  let ?L1 = "(=) :: bool ⇒ _" let ?R1 = ?L1 let ?l1 = id let ?r1 = ?l1
  let ?L2 = "⊤ :: bool ⇒ bool ⇒ bool" let ?R2 = ?L2 let ?l2 = id let ?r2 = ?l2
  interpret tc : transport_comp ?L1 ?R1 ?l1 ?r1 ?L2 ?R2 ?l2 ?r2 .
  show "(?L1 ≡⇩o ?R1) ?l1 ?r1" by fastforce
  show "equivalence_rel ?L1" "equivalence_rel ?R1" by (fact equivalence_eq)+
  show "(?L2 ≡⇩o ?R2) ?l2 ?r2" by fastforce
  show "equivalence_rel ?L2" "equivalence_rel ?R2" by (fact equivalence_top)+
  show "tc.L ≠ ?L1"
  proof -
    have "¬(?L1 False True)" by blast
    moreover have "tc.L False True" by (intro tc.left_relI) auto
    ultimately show ?thesis by auto
  qed
qed

end


subsubsection ‹Generic Left to Right Introduction Rules›

text ‹The following lemmas generalise the proof outline used, for example,
when proving monotonicity and the Galois property (cf. the paper \<^cite>‹"transport"›).›

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

lemma right_rel_if_left_relI:
  assumes "x ≤⇘L⇙ x'"
  and l1_R1_if_L1_r1: "⋀y. in_codom (≤⇘R1⇙) y ⟹ x ≤⇘L1⇙ r1 y ⟹ l1 x ≤⇘R1⇙ y"
  and t_R1_if_l1_R1: "⋀y. l1 x ≤⇘R1⇙ y ⟹ t y ≤⇘R1⇙ y"
  and R2_l2_if_t_L2_if_l1_R1:
    "⋀y y'. l1 x ≤⇘R1⇙ y ⟹ t y ≤⇘L2⇙ y' ⟹ z ≤⇘R2⇙ l2 y'"
  and R1_b_if_R1_l1_if_R1_l1:
    "⋀y y'. y ≤⇘R1⇙ l1 x' ⟹ y' ≤⇘R1⇙ l1 x' ⟹ y' ≤⇘R1⇙ b y"
  and b_L2_r2_if_in_codom_L2_b_if_R1_l1:
    "⋀y. y ≤⇘R1⇙ l1 x' ⟹ in_codom (≤⇘L2⇙) (b y) ⟹ b y ≤⇘L2⇙ r2 z'"
  and in_codom_R2_if_in_codom_L2_b_if_R1_l1:
    "⋀y. y ≤⇘R1⇙ l1 x' ⟹ in_codom (≤⇘L2⇙) (b y) ⟹ in_codom (≤⇘R2⇙) z'"
  and rel_comp_le: "(≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ≤ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)"
  and in_codom_rel_comp_le: "in_codom ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ in_codom (≤⇘L2⇙)"
  shows "z ≤⇘R⇙ z'"
proof -
  from ‹x ≤⇘L⇙ x'› obtain yl yl' where "l1 x ≤⇘R1⇙ yl" "yl ≤⇘L2⇙ yl'" "yl' ≤⇘R1⇙ l1 x'"
    using l1_R1_if_L1_r1 by blast
  moreover then have "t yl ≤⇘R1⇙ yl" by (intro t_R1_if_l1_R1)
  ultimately have "((≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) (t yl) (l1 x')" using rel_comp_le by blast
  then obtain y where "t yl ≤⇘L2⇙ y" "y ≤⇘R1⇙ l1 x'" by blast
  show "z ≤⇘R⇙ z'"
  proof (rule flip.left_relI)
    from ‹t yl ≤⇘L2⇙ y› ‹l1 x ≤⇘R1⇙ yl› show "z ⇘R2⇙⪅ y"
      by (auto intro: R2_l2_if_t_L2_if_l1_R1)
    from ‹yl' ≤⇘R1⇙ l1 x'› ‹y ≤⇘R1⇙ l1 x'› show "y ≤⇘R1⇙ b yl'"
      by (rule R1_b_if_R1_l1_if_R1_l1)
    show "b yl' ⇘L2⇙⪅ z'"
    proof (rule t2.left_GaloisI)
      from ‹yl' ≤⇘R1⇙ l1 x'› have "yl' ≤⇘R1⇙ b yl'"
        by (intro R1_b_if_R1_l1_if_R1_l1)
      with ‹l1 x ≤⇘R1⇙ yl› ‹yl ≤⇘L2⇙ yl'› in_codom_rel_comp_le
        have "in_codom (≤⇘L2⇙) (b yl')" by blast
      with ‹yl' ≤⇘R1⇙ l1 x'› show "b yl' ≤⇘L2⇙ r2 z'" "in_codom (≤⇘R2⇙) z'"
        by (auto intro: b_L2_r2_if_in_codom_L2_b_if_R1_l1
          in_codom_R2_if_in_codom_L2_b_if_R1_l1)
    qed
  qed
qed

lemma right_rel_if_left_relI':
  assumes "x ≤⇘L⇙ x'"
  and l1_R1_if_L1_r1: "⋀y. in_codom (≤⇘R1⇙) y ⟹ x ≤⇘L1⇙ r1 y ⟹ l1 x ≤⇘R1⇙ y"
  and R1_b_if_R1_l1: "⋀y. y ≤⇘R1⇙ l1 x' ⟹ y ≤⇘R1⇙ b y"
  and L2_r2_if_L2_b_if_R1_l1:
    "⋀y y'. y ≤⇘R1⇙ l1 x' ⟹ y' ≤⇘L2⇙ b y ⟹ y' ≤⇘L2⇙ r2 z'"
  and in_codom_R2_if_L2_b_if_R1_l1:
    "⋀y y'. y ≤⇘R1⇙ l1 x' ⟹ y' ≤⇘L2⇙ b y ⟹ in_codom (≤⇘R2⇙) z'"
  and t_R1_if_R1_l1_if_l1_R1:
    "⋀y y' y''. l1 x ≤⇘R1⇙ y ⟹ l1 x ≤⇘R1⇙ y' ⟹ t y ≤⇘R1⇙ y'"
  and R2_l2_t_if_in_dom_L2_t_if_l1_R1:
    "⋀y y'. l1 x ≤⇘R1⇙ y ⟹ in_dom (≤⇘L2⇙) (t y) ⟹ z ≤⇘R2⇙ l2 (t y)"
  and in_codom_L2_t_if_in_dom_L2_t_if_l1_R1:
    "⋀y y'. l1 x ≤⇘R1⇙ y ⟹ in_dom (≤⇘L2⇙) (t y) ⟹ in_codom (≤⇘L2⇙) (t y)"
  and rel_comp_le: "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙))"
  and in_dom_rel_comp_le: "in_dom ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ in_dom (≤⇘L2⇙)"
  shows "z ≤⇘R⇙ z'"
proof -
  from ‹x ≤⇘L⇙ x'› obtain yl yl' where "l1 x ≤⇘R1⇙ yl" "yl ≤⇘L2⇙ yl'" "yl' ≤⇘R1⇙ l1 x'"
    using l1_R1_if_L1_r1 by blast
  moreover then have "yl' ≤⇘R1⇙ b yl'" by (intro R1_b_if_R1_l1)
  ultimately have "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) (l1 x) (b yl')" using rel_comp_le by blast
  then obtain y where "l1 x ≤⇘R1⇙ y" "y ≤⇘L2⇙ b yl'" by blast
  show "z ≤⇘R⇙ z'"
  proof (rule flip.left_relI)
    from ‹yl' ≤⇘R1⇙ l1 x'› ‹y ≤⇘L2⇙ b yl'›
      have "in_codom (≤⇘R2⇙) z'" "y ≤⇘L2⇙ r2 z'"
      by (auto intro: in_codom_R2_if_L2_b_if_R1_l1 L2_r2_if_L2_b_if_R1_l1)
    then show "y ⇘L2⇙⪅ z'" by blast
    from ‹l1 x ≤⇘R1⇙ yl› ‹l1 x ≤⇘R1⇙ y› show "t yl ≤⇘R1⇙ y" by (rule t_R1_if_R1_l1_if_l1_R1)
    show "z ⇘R2⇙⪅ t yl"
    proof (rule flip.t1.left_GaloisI)
      from ‹l1 x ≤⇘R1⇙ yl› have "t yl ≤⇘R1⇙ yl" by (intro t_R1_if_R1_l1_if_l1_R1)
      with ‹yl ≤⇘L2⇙ yl'› ‹yl' ≤⇘R1⇙ l1 x'› in_dom_rel_comp_le have "in_dom (≤⇘L2⇙) (t yl)"
        by blast
      with ‹l1 x ≤⇘R1⇙ yl›
        show "z ≤⇘R2⇙ l2 (t yl)" "in_codom (≤⇘L2⇙) (t yl)" by (auto intro:
          R2_l2_t_if_in_dom_L2_t_if_l1_R1 in_codom_L2_t_if_in_dom_L2_t_if_l1_R1)
    qed
  qed
qed


subsubsection ‹Simplification of Monotonicity Assumptions›

text ‹Some sufficient conditions for monotonicity assumptions that repeatedly
arise in various places.›

lemma mono_in_dom_left_rel_left1_if_in_dom_rel_comp_le:
  assumes "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and "in_dom ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ in_dom (≤⇘L2⇙)"
  shows "(in_dom (≤⇘L⇙) ⇛⇩m in_dom (≤⇘L2⇙)) l1"
  using assms by (intro mono_wrt_predI) blast

lemma mono_in_codom_left_rel_left1_if_in_codom_rel_comp_le:
  assumes "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and "in_codom ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ in_codom (≤⇘L2⇙)"
  shows "(in_codom (≤⇘L⇙) ⇛⇩m in_codom (≤⇘L2⇙)) l1"
  using assms by (intro mono_wrt_predI) blast


subsubsection ‹Simplification of Compatibility Conditions›

text ‹Most results will depend on certain compatibility conditions between
@{term "(≤⇘R1⇙)"} and @{term "(≤⇘L2⇙)"}. We next derive some sufficient assumptions
for these conditions.›

end

lemma rel_comp_comp_le_rel_comp_if_rel_comp_comp_if_in_dom_leI:
  assumes trans_R: "transitive R"
  and refl_S: "reflexive_on P S"
  and in_dom_le: "in_dom (R ∘∘ S ∘∘ R) ≤ P"
  and rel_comp_le: "(S ∘∘ R ∘∘ S) ≤ (S ∘∘ R)"
  shows "(R ∘∘ S ∘∘ R) ≤ (S ∘∘ R)"
proof (intro le_relI)
  fix x y assume "(R ∘∘ S ∘∘ R) x y"
  moreover with in_dom_le refl_S have "S x x" by blast
  ultimately have "((S ∘∘ R ∘∘ S) ∘∘ R) x y" by blast
  with rel_comp_le have "(S ∘∘ R ∘∘ R) x y" by blast
  with trans_R show "(S ∘∘ R) x y" by blast
qed

lemma rel_comp_comp_le_rel_comp_if_rel_comp_comp_if_in_codom_leI:
  assumes trans_R: "transitive R"
  and refl_S: "reflexive_on P S"
  and in_codom_le: "in_codom (R ∘∘ S ∘∘ R) ≤ P"
  and rel_comp_le: "(S ∘∘ R ∘∘ S) ≤ (R ∘∘ S)"
  shows "(R ∘∘ S ∘∘ R) ≤ (R ∘∘ S)"
proof (intro le_relI)
  fix x y assume "(R ∘∘ S ∘∘ R) x y"
  moreover with in_codom_le refl_S have "S y y" by blast
  ultimately have "(R ∘∘ (S ∘∘ R ∘∘ S)) x y" by blast
  with rel_comp_le have "(R ∘∘ R ∘∘ S) x y" by blast
  with trans_R show "(R ∘∘ S) x y" by blast
qed
thm mono_rel_comp
lemma rel_comp_comp_le_rel_comp_if_rel_comp_le_if_transitive:
  assumes trans_R: "transitive R"
  and R_S_le: "(R ∘∘ S) ≤ (S ∘∘ R)"
  shows "(R ∘∘ S ∘∘ R) ≤ (S ∘∘ R)"
proof -
  from trans_R have R_R_le: "(R ∘∘ R) ≤ R" by (intro rel_comp_le_self_if_transitive)
  have "(R ∘∘ S ∘∘ R) ≤ (S ∘∘ R ∘∘ R)"
    using mono_rel_comp R_S_le by blast
  also have "... = S ∘∘ (R ∘∘ R)" by (simp flip: rel_comp_assoc)
  also have "... ≤ (S ∘∘ R)" using mono_rel_comp R_R_le by blast
  finally show ?thesis .
qed

lemma rel_comp_comp_le_rel_comp_if_rel_comp_le_if_transitive':
  assumes trans_R: "transitive R"
  and S_R_le: "(S ∘∘ R) ≤ (R ∘∘ S)"
  shows "(R ∘∘ S ∘∘ R) ≤ (R ∘∘ S)"
proof -
  from trans_R have R_R_le: "(R ∘∘ R) ≤ R" by (intro rel_comp_le_self_if_transitive)
  have "(R ∘∘ S ∘∘ R) ≤ (R ∘∘ R ∘∘ S)"
    using mono_rel_comp S_R_le by (auto simp flip: rel_comp_assoc)
  also have "... ≤ (R ∘∘ S)" using mono_rel_comp R_R_le by blast
  finally show ?thesis .
qed

lemma rel_comp_eq_rel_comp_if_le_if_transitive_if_reflexive:
  assumes refl_R: "reflexive_on (in_field S) R"
  and trans_S: "transitive S"
  and R_le: "R ≤ S ⊔ (=)"
  shows "(R ∘∘ S) = (S ∘∘ R)"
proof (intro ext iffI)
  fix x y assume "(R ∘∘ S) x y"
  then obtain z where "R x z" "S z y" by blast
  with R_le have "(S ⊔ (=)) x z" by blast
  with ‹S z y› trans_S have "S x y" by auto
  moreover from ‹S z y› refl_R have "R y y" by blast
  ultimately show "(S ∘∘ R) x y" by blast
next
  fix x y assume "(S ∘∘ R) x y"
  then obtain z where "S x z" "R z y" by blast
  with R_le have "(S ⊔ (=)) z y" by blast
  with ‹S x z› trans_S have "S x y" by auto
  moreover from ‹S x y› refl_R have "R x x" by blast
  ultimately show "(R ∘∘ S) x y" by blast
qed

lemma rel_comp_eq_rel_comp_if_in_field_le_if_le_eq:
  assumes le_eq: "R ≤ (=)"
  and in_field_le: "in_field S ≤ in_field R"
  shows "(R ∘∘ S) = (S ∘∘ R)"
proof (intro ext iffI)
  fix x y assume "(R ∘∘ S) x y"
  then obtain z where "R x z" "S z y" by blast
  with le_eq have "S x y" by blast
  with assms show "(S ∘∘ R) x y" by blast
next
  fix x y assume "(S ∘∘ R) x y"
  then obtain z where "S x z" "R z y" by blast
  with le_eq have "S x y" by blast
  with assms show "(R ∘∘ S) x y" by blast
qed

context transport_comp
begin

lemma left2_right1_left2_le_left2_right1_if_right1_left2_right1_le_left2_right1:
  assumes "reflexive_on (in_codom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "transitive (≤⇘L2⇙)"
  and "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙))"
  and "in_codom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_codom (≤⇘R1⇙)"
  shows "((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙))"
  using assms by (intro rel_comp_comp_le_rel_comp_if_rel_comp_comp_if_in_codom_leI)
  auto

lemma left2_right1_left2_le_right1_left2_if_right1_left2_right1_le_right1_left2I:
  assumes "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "transitive (≤⇘L2⇙)"
  and "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙))"
  and "in_dom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_dom (≤⇘R1⇙)"
  shows "((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙))"
  using assms by (intro rel_comp_comp_le_rel_comp_if_rel_comp_comp_if_in_dom_leI)
  auto

lemma in_dom_right1_left2_right1_le_if_right1_left2_right1_le:
  assumes "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙))"
  shows "in_dom ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ in_dom (≤⇘L2⇙)"
  using monoD[OF mono_in_dom assms] by (auto intro: in_dom_if_in_dom_rel_comp)

lemma in_codom_right1_left2_right1_le_if_right1_left2_right1_le:
  assumes "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙))"
  shows "in_codom ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ in_codom (≤⇘L2⇙)"
  using monoD[OF mono_in_codom assms]
  by (auto intro: in_codom_if_in_codom_rel_comp)

text ‹Our main results will be derivable for two different sets of compatibility
conditions. The next two lemmas show the equivalence between those two sets
under certain assumptions. In cases where these assumptions are met, we will
only state the result for one of the two compatibility conditions. The other one
will then be derivable using one of the following lemmas.›

definition "middle_compatible_dom ≡
  (≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ≤ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)
  ∧ in_dom ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ in_dom (≤⇘L2⇙)
  ∧ ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙))
  ∧ in_dom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_dom (≤⇘R1⇙)"

lemma middle_compatible_domI [intro]:
  assumes "(≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ≤ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)"
  and "in_dom ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ in_dom (≤⇘L2⇙)"
  and "((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙))"
  and "in_dom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_dom (≤⇘R1⇙)"
  shows "middle_compatible_dom"
  unfolding middle_compatible_dom_def using assms by blast

lemma middle_compatible_domE [elim]:
  assumes "middle_compatible_dom"
  obtains "(≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ≤ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)"
  and "in_dom ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ in_dom (≤⇘L2⇙)"
  and "((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙))"
  and "in_dom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_dom (≤⇘R1⇙)"
  using assms unfolding middle_compatible_dom_def by blast

definition "middle_compatible_codom ≡
  ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙))
  ∧ in_codom ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ in_codom (≤⇘L2⇙)
  ∧ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ≤ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)
  ∧ in_codom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_codom (≤⇘R1⇙)"

lemma middle_compatible_codomI [intro]:
  assumes "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙))"
  and "in_codom ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ in_codom (≤⇘L2⇙)"
  and "(≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ≤ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)"
  and "in_codom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_codom (≤⇘R1⇙)"
  shows "middle_compatible_codom"
  unfolding middle_compatible_codom_def using assms by blast

lemma middle_compatible_codomE [elim]:
  assumes "middle_compatible_codom"
  obtains "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙))"
  and "in_codom ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ in_codom (≤⇘L2⇙)"
  and "(≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ≤ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)"
  and "in_codom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_codom (≤⇘R1⇙)"
  using assms unfolding middle_compatible_codom_def by blast

context
begin

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

lemma rel_comp_comp_le_assms_if_in_codom_rel_comp_comp_leI:
  assumes "preorder_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "preorder_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "middle_compatible_codom"
  shows "middle_compatible_dom"
  using assms by (intro middle_compatible_domI)
  (auto intro!:
    left2_right1_left2_le_left2_right1_if_right1_left2_right1_le_left2_right1
    flip.left2_right1_left2_le_left2_right1_if_right1_left2_right1_le_left2_right1
    in_dom_right1_left2_right1_le_if_right1_left2_right1_le
    flip.in_dom_right1_left2_right1_le_if_right1_left2_right1_le
    intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_codom)

lemma rel_comp_comp_le_assms_if_in_dom_rel_comp_comp_leI:
  assumes "preorder_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "preorder_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "middle_compatible_dom"
  shows "middle_compatible_codom"
  using assms by (intro middle_compatible_codomI)
  (auto intro!:
    left2_right1_left2_le_right1_left2_if_right1_left2_right1_le_right1_left2I
    flip.left2_right1_left2_le_right1_left2_if_right1_left2_right1_le_right1_left2I
    in_codom_right1_left2_right1_le_if_right1_left2_right1_le
    flip.in_codom_right1_left2_right1_le_if_right1_left2_right1_le
    intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_dom)

lemma middle_compatible_dom_iff_middle_compatible_codom_if_preorder_on:
  assumes "preorder_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "preorder_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙)"
  shows "middle_compatible_dom ⟷ middle_compatible_codom"
  using assms by (intro iffI rel_comp_comp_le_assms_if_in_codom_rel_comp_comp_leI)
  (auto intro!: rel_comp_comp_le_assms_if_in_dom_rel_comp_comp_leI)

end

text ‹Finally we derive some sufficient assumptions for the compatibility
conditions.›

lemma right1_left2_right1_le_assms_if_right1_left2_eqI:
  assumes "transitive (≤⇘R1⇙)"
  and "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) = ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙))"
  shows "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙))"
  and "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙))"
  using assms rel_comp_comp_le_rel_comp_if_rel_comp_le_if_transitive[of R1 L2]
  by auto

interpretation flip : transport_comp R2 L2 r2 l2 R1 L1 r1 l1
  rewrites "((≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) = ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≡ ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) = ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙))"
  by (simp only: eq_commute)

lemma middle_compatible_codom_if_rel_comp_eq_if_transitive:
  assumes "transitive (≤⇘R1⇙)" "transitive (≤⇘L2⇙)"
  and "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) = ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙))"
  shows "middle_compatible_codom"
  using assms by (intro middle_compatible_codomI
    in_codom_right1_left2_right1_le_if_right1_left2_right1_le
    flip.in_codom_right1_left2_right1_le_if_right1_left2_right1_le
    right1_left2_right1_le_assms_if_right1_left2_eqI
    flip.right1_left2_right1_le_assms_if_right1_left2_eqI)
  auto

lemma middle_compatible_codom_if_right1_le_left2_eqI:
  assumes "preorder_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)" "transitive (≤⇘L2⇙)"
  and "(≤⇘R1⇙) ≤ (≤⇘L2⇙) ⊔ (=)"
  and "in_field (≤⇘L2⇙) ≤ in_field (≤⇘R1⇙)"
  shows "middle_compatible_codom"
  using assms by (intro middle_compatible_codomI
    in_codom_right1_left2_right1_le_if_right1_left2_right1_le
    flip.in_codom_right1_left2_right1_le_if_right1_left2_right1_le
    right1_left2_right1_le_assms_if_right1_left2_eqI
    flip.right1_left2_right1_le_assms_if_right1_left2_eqI
    rel_comp_eq_rel_comp_if_le_if_transitive_if_reflexive)
  (auto intro: reflexive_on_if_le_pred_if_reflexive_on)

lemma middle_compatible_codom_if_right1_le_eqI:
  assumes "(≤⇘R1⇙) ≤ (=)"
  and "transitive (≤⇘L2⇙)"
  and "in_field (≤⇘L2⇙) ≤ in_field (≤⇘R1⇙)"
  shows "middle_compatible_codom"
  using assms by (intro middle_compatible_codomI
    in_codom_right1_left2_right1_le_if_right1_left2_right1_le
    flip.in_codom_right1_left2_right1_le_if_right1_left2_right1_le
    right1_left2_right1_le_assms_if_right1_left2_eqI
    flip.right1_left2_right1_le_assms_if_right1_left2_eqI
    rel_comp_eq_rel_comp_if_in_field_le_if_le_eq)
  auto

end


end