Theory Transport_Compositions_Generic_Monotone

✐‹creator "Kevin Kappelmann"›
subsection ‹Monotonicity›
theory Transport_Compositions_Generic_Monotone
  imports
    Transport_Compositions_Generic_Base
begin

context transport_comp
begin

lemma mono_wrt_rel_leftI:
  assumes "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and "((≤⇘L2⇙) ⇛⇩m (≤⇘R2⇙)) l2"
  and inflationary_unit2: "inflationary_on (in_codom (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙))"
  and "in_codom ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ in_codom (≤⇘L2⇙)"
  shows "((≤⇘L⇙) ⇛⇩m (≤⇘R⇙)) l"
proof (rule mono_wrt_relI)
  fix x x' assume "x ≤⇘L⇙ x'"
  then show "l x ≤⇘R⇙ l x'"
  proof (rule right_rel_if_left_relI)
    fix y' assume "l1 x ≤⇘L2⇙ y'"
    with ‹((≤⇘L2⇙) ⇛⇩m (≤⇘R2⇙)) l2› show "l x ≤⇘R2⇙ l2 y'" by auto
  next
    assume "in_codom (≤⇘L2⇙) (l1 x')"
    with inflationary_unit2 show "l1 x' ≤⇘L2⇙ r2 (l x')" by auto
    from ‹in_codom (≤⇘L2⇙) (l1 x')› ‹((≤⇘L2⇙) ⇛⇩m (≤⇘R2⇙)) l2›
      show "in_codom (≤⇘R2⇙) (l x')" by fastforce
  qed (insert assms, auto)
qed

lemma mono_wrt_rel_leftI':
  assumes "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and "((≤⇘L2⇙) ⇛⇩m (≤⇘R2⇙)) l2"
  and "((≤⇘L2⇙) ⊴⇩h (≤⇘R2⇙)) l2 r2"
  and refl_L2: "reflexive_on (in_dom (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙))"
  and "in_dom ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ in_dom (≤⇘L2⇙)"
  shows "((≤⇘L⇙) ⇛⇩m (≤⇘R⇙)) l"
proof (rule mono_wrt_relI)
  fix x x' assume "x ≤⇘L⇙ x'"
  then show "l x ≤⇘R⇙ l x'"
  proof (rule right_rel_if_left_relI')
    fix y' assume "y' ≤⇘L2⇙ l1 x'"
    moreover with ‹((≤⇘L2⇙) ⇛⇩m (≤⇘R2⇙)) l2› have "l2 y' ≤⇘R2⇙ l x'" by auto
    ultimately show "in_codom (≤⇘R2⇙) (l x')" "y' ≤⇘L2⇙ r2 (l x')"
      using ‹((≤⇘L2⇙) ⊴⇩h (≤⇘R2⇙)) l2 r2› by auto
  next
    assume "in_dom (≤⇘L2⇙) (l1 x)"
    with refl_L2 ‹((≤⇘L2⇙) ⇛⇩m (≤⇘R2⇙)) l2› show "l x ≤⇘R2⇙ l2 (l1 x)" by auto
  qed (insert assms, auto)
qed

end


end