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)  (≤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)  (≤R)) l"
proof (rule mono_wrt_relI)
  fix x x' assume "xL x'"
  then show "l xR l x'"
  proof (rule right_rel_if_left_relI)
    fix y' assume "l1 xL2 y'"
    with ((≤L2)  (≤R2)) l2 show "l xR2 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)  (≤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)  (≤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)  (≤R)) l"
proof (rule mono_wrt_relI)
  fix x x' assume "xL x'"
  then show "l xR l x'"
  proof (rule right_rel_if_left_relI')
    fix y' assume "y'L2 l1 x'"
    moreover with ((≤L2)  (≤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)  (≤R2)) l2 show "l xR2 l2 (l1 x)" by auto
  qed (insert assms, auto)
qed

end


end