Theory Transport_Functions_Relation_Simplifications

✐‹creator "Kevin Kappelmann"›
subsection ‹Simplification of Left and Right Relations›
theory Transport_Functions_Relation_Simplifications
  imports
    Transport_Functions_Order_Base
    Transport_Functions_Galois_Equivalence
begin

paragraph ‹Dependent Function Relator›

context transport_Dep_Fun_Rel
begin

text ‹Due to
@{thm "transport_Mono_Dep_Fun_Rel.left_rel_eq_tdfr_left_rel_if_reflexive_on"},
we can apply all results from @{locale "transport_Mono_Dep_Fun_Rel"} to
@{locale "transport_Dep_Fun_Rel"} whenever @{term "(≤⇘L⇙)"} and @{term "(≤⇘R⇙)"} are
reflexive.›

lemma reflexive_on_in_field_left_rel2_le_assmI:
  assumes "reflexive_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "((x1 : ⊤) ⇒ ⦇x2 x3 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x2⦈ ⇒ (≤)) L2"
  and "x1 ≤⇘L1⇙ x2"
  shows "(≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)"
  using assms by fastforce

lemma reflexive_on_in_field_mono_assm_left2I:
  assumes "((x1 x2 ∷ (≥⇘L1⇙)) ⇒ ⦇x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3⦈ ⇛ (≤)) L2"
  and "reflexive_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙)"
  shows "((x1 : ⊤) ⇒ ⦇x2 x3 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x2⦈ ⇒ (≤)) L2"
  using assms by fastforce

lemma reflexive_on_in_field_left_if_equivalencesI:
  assumes "((≤⇘L1⇙) ≡⇩G (≤⇘R1⇙)) l1 r1"
  and "preorder_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and mono_cond_left_rel
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ partial_equivalence_rel (≤⇘L2 x1 x2⇙)"
  shows "reflexive_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
  using assms
  by (intro reflexive_on_in_field_leftI
    left_rel_right_iff_left_right_rel_if_galois_prop_le_assms_leftI
    galois_equivalence_if_mono_if_galois_equivalence_mono_assms_leftI
    reflexive_on_in_field_left_rel2_le_assmI
    reflexive_on_in_field_mono_assm_left2I)
  (auto intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_dom)

end


paragraph ‹Monotone Dependent Function Relator›

context transport_Mono_Dep_Fun_Rel
begin

lemma left_rel_eq_tdfr_leftI:
  assumes "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ partial_equivalence_rel (≤⇘L2 x1 x2⇙)"
  shows "(≤⇘L⇙) = tdfr.L"
  using assms by (intro left_rel_eq_tdfr_left_rel_if_reflexive_on
    tdfr.reflexive_on_in_field_leftI)
  auto

lemma left_rel_eq_tdfr_leftI_if_equivalencesI:
  assumes "((≤⇘L1⇙) ≡⇩G (≤⇘R1⇙)) l1 r1"
  and "preorder_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇒ ⦇x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3⦈ ⇛ (≤)) L2"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ partial_equivalence_rel (≤⇘L2 x1 x2⇙)"
  shows "(≤⇘L⇙) = tdfr.L"
  using assms by (intro left_rel_eq_tdfr_left_rel_if_reflexive_on
    tdfr.reflexive_on_in_field_left_if_equivalencesI)
  auto

end


paragraph ‹Monotone Function Relator›

context transport_Mono_Fun_Rel
begin

lemma left_rel_eq_tfr_leftI:
  assumes "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ partial_equivalence_rel (≤⇘L2⇙)"
  shows "(≤⇘L⇙) = tfr.tdfr.L"
  using assms by (intro tmdfr.left_rel_eq_tdfr_leftI) auto

end


end