Theory Transport_Compositions_Generic_Order_Base

✐‹creator "Kevin Kappelmann"›
subsection ‹Basic Order Properties›
theory Transport_Compositions_Generic_Order_Base
  imports
   Transport_Compositions_Generic_Base
begin

context transport_comp
begin

interpretation flip1 : galois R1 L1 r1 l1 .

subsubsection ‹Reflexivity›

lemma reflexive_on_in_dom_leftI:
  assumes galois_prop: "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and in_dom_L1_le: "in_dom (≤⇘L1⇙) ≤ in_codom (≤⇘L1⇙)"
  and refl_R1: "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and refl_L2: "reflexive_on (in_dom (≤⇘L2⇙)) (≤⇘L2⇙)"
  and mono_in_dom_l1: "(in_dom (≤⇘L⇙) ⇛⇩m in_dom (≤⇘L2⇙)) l1"
  shows "reflexive_on (in_dom (≤⇘L⇙)) (≤⇘L⇙)"
proof (rule reflexive_onI)
  fix x assume "in_dom (≤⇘L⇙) x"
  then obtain x' where "x ≤⇘L⇙ x'" "in_dom (≤⇘L1⇙) x" by blast
  show "x ≤⇘L⇙ x"
  proof (rule left_relI)
    from refl_R1 have "l1 x ≤⇘R1⇙ l1 x"
    proof (rule reflexive_onD)
      from ‹x ≤⇘L⇙ x'› galois_prop show "in_dom (≤⇘R1⇙) (l1 x)" by blast
    qed
    then show "x ⇘L1⇙⪅ l1 x"
    proof (intro t1.left_GaloisI)
      from galois_prop ‹in_dom (≤⇘L1⇙) x› ‹l1 x ≤⇘R1⇙ l1 x› show "x ≤⇘L1⇙ r1 (l1 x)" by blast
    qed blast
    from refl_L2 show "l1 x ≤⇘L2⇙ l1 x"
    proof (rule reflexive_onD)
      from mono_in_dom_l1 ‹x ≤⇘L⇙ x'› show "in_dom (≤⇘L2⇙) (l1 x)" by blast
    qed
    from ‹l1 x ≤⇘R1⇙ l1 x› show "l1 x ⇘R1⇙⪅ x"
    proof (intro flip1.left_GaloisI)
      from ‹in_dom (≤⇘L1⇙) x› in_dom_L1_le show "in_codom (≤⇘L1⇙) x" by blast
    qed
  qed
qed

lemma reflexive_on_in_codom_leftI:
  assumes L1_r1_l1I: "⋀x. in_dom (≤⇘L1⇙) x ⟹ l1 x ≤⇘R1⇙ l1 x ⟹ x ≤⇘L1⇙ r1 (l1 x)"
  and in_codom_L1_le: "in_codom (≤⇘L1⇙) ≤ in_dom (≤⇘L1⇙)"
  and refl_R1: "reflexive_on (in_codom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and refl_L2: "reflexive_on (in_codom (≤⇘L2⇙)) (≤⇘L2⇙)"
  and mono_in_codom_l1: "(in_codom (≤⇘L⇙) ⇛⇩m in_codom (≤⇘L2⇙)) l1"
  shows "reflexive_on (in_codom (≤⇘L⇙)) (≤⇘L⇙)"
proof (rule reflexive_onI)
  fix x assume "in_codom (≤⇘L⇙) x"
  then obtain x' where "x' ≤⇘L⇙ x" "in_codom (≤⇘L1⇙) x" "in_codom (≤⇘R1⇙) (l1 x)"
    by blast
  show "x ≤⇘L⇙ x"
  proof (rule left_relI)
    from refl_R1 ‹in_codom (≤⇘R1⇙) (l1 x)› have "l1 x ≤⇘R1⇙ l1 x" by blast
    show "x ⇘L1⇙⪅ l1 x"
    proof (rule t1.left_GaloisI)
      from in_codom_L1_le ‹in_codom (≤⇘L1⇙) x› have "in_dom (≤⇘L1⇙) x" by blast
      with ‹l1 x ≤⇘R1⇙ l1 x› show "x ≤⇘L1⇙ r1 (l1 x)" by (intro L1_r1_l1I)
    qed fact
    from refl_L2 show "l1 x ≤⇘L2⇙ l1 x"
    proof (rule reflexive_onD)
      from mono_in_codom_l1 ‹x' ≤⇘L⇙ x› show "in_codom (≤⇘L2⇙) (l1 x)" by blast
    qed
    show "l1 x ⇘R1⇙⪅ x" by (rule flip1.left_GaloisI) fact+
  qed
qed

corollary reflexive_on_in_field_leftI:
  assumes "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and "in_codom (≤⇘L1⇙) = in_dom (≤⇘L1⇙)"
  and "reflexive_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "reflexive_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "(in_field (≤⇘L⇙) ⇛⇩m in_field (≤⇘L2⇙)) l1"
  shows "reflexive_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
proof -
  from assms have "reflexive_on (in_dom (≤⇘L⇙)) (≤⇘L⇙)"
    by (intro reflexive_on_in_dom_leftI)
    (auto 0 5 intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_dom)
  moreover from assms have "reflexive_on (in_codom (≤⇘L⇙)) (≤⇘L⇙)"
    by (intro reflexive_on_in_codom_leftI)
    (auto 0 5 intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_codom)
  ultimately show ?thesis by (auto iff: in_field_iff_in_dom_or_in_codom)
qed


subsubsection ‹Transitivity›

text‹There are many similar proofs for transitivity. They slightly differ in
their assumptions, particularly which of @{term "(≤⇘R1⇙)"} and @{term "(≤⇘L2⇙)"} has
to be transitive and the order of commutativity for the relations.

In the following, we just give two of them that suffice for many purposes.›

lemma transitive_leftI:
  assumes "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and trans_L2: "transitive (≤⇘L2⇙)"
  and R1_L2_R1_le: "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙))"
  shows "transitive (≤⇘L⇙)"
proof (rule transitiveI)
  fix x1 x2 x3 assume "x1 ≤⇘L⇙ x2" "x2 ≤⇘L⇙ x3"
  from ‹x1 ≤⇘L⇙ x2› obtain y1 y2 where "x1 ⇘L1⇙⪅ y1" "y1 ≤⇘L2⇙ y2" "y2 ≤⇘R1⇙ l1 x2"
    by blast
  from ‹x2 ≤⇘L⇙ x3› ‹((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1› obtain y3 y4 where
    "l1 x2 ≤⇘R1⇙ y3" "y3 ≤⇘L2⇙ y4" "y4 ≤⇘R1⇙ l1 x3" "in_codom (≤⇘L1⇙) x3" by blast
  with R1_L2_R1_le have "((≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) (l1 x2) (l1 x3)" by blast
  then obtain y where "l1 x2 ≤⇘L2⇙ y" "y ≤⇘R1⇙ l1 x3" by blast
  with ‹y2 ≤⇘R1⇙ l1 x2› R1_L2_R1_le have "((≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) y2 (l1 x3)" by blast
  then obtain y' where "y2 ≤⇘L2⇙ y'" "y' ≤⇘R1⇙ l1 x3" by blast
  with ‹y1 ≤⇘L2⇙ y2› have "y1 ≤⇘L2⇙ y'" using trans_L2 by blast
  show "x1 ≤⇘L⇙ x3"
  proof (rule left_relI)
    show "x1 ⇘L1⇙⪅ y1" "y1 ≤⇘L2⇙ y'" by fact+
    show "y' ⇘R1⇙⪅ x3" by (rule flip1.left_GaloisI) fact+
  qed
qed

lemma transitive_leftI':
  assumes galois_prop: "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and trans_L2: "transitive (≤⇘L2⇙)"
  and R1_L2_R1_le: "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙))"
  shows "transitive (≤⇘L⇙)"
proof (rule transitiveI)
  fix x1 x2 x3 assume "x1 ≤⇘L⇙ x2" "x2 ≤⇘L⇙ x3"
  from ‹x1 ≤⇘L⇙ x2› galois_prop obtain y1 y2 where
    "in_dom (≤⇘L1⇙) x1" "l1 x1 ≤⇘R1⇙ y1" "y1 ≤⇘L2⇙ y2" "y2 ≤⇘R1⇙ l1 x2" by blast
  with R1_L2_R1_le have "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) (l1 x1) (l1 x2)" by blast
  then obtain y where "l1 x1 ≤⇘R1⇙ y" "y ≤⇘L2⇙ l1 x2" by blast
  moreover from ‹x2 ≤⇘L⇙ x3› galois_prop obtain y3 y4 where
    "l1 x2 ≤⇘R1⇙ y3" "y3 ≤⇘L2⇙ y4" "y4 ⇘R1⇙⪅ x3" by blast
  moreover note R1_L2_R1_le
  ultimately have "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) (l1 x1) y3" by blast
  then obtain y' where "l1 x1 ≤⇘R1⇙ y'" "y' ≤⇘L2⇙ y3" by blast
  with ‹y3 ≤⇘L2⇙ y4› have "y' ≤⇘L2⇙ y4" using trans_L2 by blast
  show "x1 ≤⇘L⇙ x3"
  proof (rule left_relI)
    from ‹in_dom (≤⇘L1⇙) x1› ‹l1 x1 ≤⇘R1⇙ y'› galois_prop show "x1 ⇘L1⇙⪅ y'"
      by (intro t1.left_Galois_if_Galois_right_if_half_galois_prop_right t1.left_GaloisI)
      auto
    show "y' ≤⇘L2⇙ y4" by fact
    from ‹y' ≤⇘L2⇙ y4› ‹y4 ⇘R1⇙⪅ x3› show "y4 ⇘R1⇙⪅ x3" by blast
  qed
qed


subsubsection ‹Preorders›

lemma preorder_on_in_field_leftI:
  assumes "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and "in_codom (≤⇘L1⇙) = in_dom (≤⇘L1⇙)"
  and "reflexive_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "preorder_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙)"
  and mono_in_codom_l1: "(in_codom (≤⇘L⇙) ⇛⇩m in_codom (≤⇘L2⇙)) l1"
  and R1_L2_R1_le: "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙))"
  shows "preorder_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
proof -
  have "(in_field (≤⇘L⇙) ⇛⇩m in_field (≤⇘L2⇙)) l1"
  proof -
    from ‹((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1› R1_L2_R1_le
      have "(in_dom (≤⇘L⇙) ⇛⇩m in_dom (≤⇘L2⇙)) l1"
      by (intro mono_in_dom_left_rel_left1_if_in_dom_rel_comp_le
        in_dom_right1_left2_right1_le_if_right1_left2_right1_le)
      auto
    with mono_in_codom_l1 show ?thesis by (intro mono_wrt_predI) blast
  qed
  with assms show ?thesis by (intro preorder_onI)
    (auto intro: reflexive_on_in_field_leftI transitive_leftI)
qed

lemma preorder_on_in_field_leftI':
  assumes "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and "in_codom (≤⇘L1⇙) = in_dom (≤⇘L1⇙)"
  and "reflexive_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "preorder_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙)"
  and mono_in_dom_l1: "(in_dom (≤⇘L⇙) ⇛⇩m in_dom (≤⇘L2⇙)) l1"
  and R1_L2_R1_le: "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙))"
  shows "preorder_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
proof -
  have "(in_field (≤⇘L⇙) ⇛⇩m in_field (≤⇘L2⇙)) l1"
  proof -
    from ‹((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1› R1_L2_R1_le
      have "(in_codom (≤⇘L⇙) ⇛⇩m in_codom (≤⇘L2⇙)) l1"
      by (intro mono_in_codom_left_rel_left1_if_in_codom_rel_comp_le
        in_codom_right1_left2_right1_le_if_right1_left2_right1_le)
      auto
    with mono_in_dom_l1 show ?thesis by (intro mono_wrt_predI) blast
  qed
  with assms show ?thesis by (intro preorder_onI)
    (auto intro: reflexive_on_in_field_leftI transitive_leftI')
qed


subsubsection ‹Symmetry›

lemma symmetric_leftI:
  assumes "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and "in_codom (≤⇘L1⇙) = in_dom (≤⇘L1⇙)"
  and "symmetric (≤⇘R1⇙)"
  and "symmetric (≤⇘L2⇙)"
  shows "symmetric (≤⇘L⇙)"
proof -
  from assms have "(⪆⇘R1⇙) = (⇘L1⇙⪅)" by (intro
    t1.ge_Galois_right_eq_left_Galois_if_symmetric_if_in_codom_eq_in_dom_if_galois_prop)
  moreover then have "(⇘R1⇙⪅) = (⪆⇘L1⇙)"
    by (subst rel_inv_eq_iff_eq[symmetric]) simp
  ultimately show ?thesis using assms unfolding left_rel_eq_comp
    by (subst symmetric_iff_rel_inv_eq_self) (simp add: rel_comp_assoc)
qed

lemma partial_equivalence_rel_leftI:
  assumes "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and "in_codom (≤⇘L1⇙) = in_dom (≤⇘L1⇙)"
  and "symmetric (≤⇘R1⇙)"
  and "partial_equivalence_rel (≤⇘L2⇙)"
  and "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙))"
  shows "partial_equivalence_rel (≤⇘L⇙)"
  using assms by (intro partial_equivalence_relI transitive_leftI symmetric_leftI)
  auto

lemma partial_equivalence_rel_leftI':
  assumes "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and "in_codom (≤⇘L1⇙) = in_dom (≤⇘L1⇙)"
  and "symmetric (≤⇘R1⇙)"
  and "partial_equivalence_rel (≤⇘L2⇙)"
  and "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙))"
  shows "partial_equivalence_rel (≤⇘L⇙)"
  using assms by (intro partial_equivalence_relI transitive_leftI' symmetric_leftI)
  auto

end


end