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 refl_L1: "reflexive_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and mono_L2: "((x1 : ⊤) ⇛⇩m (x2 x3 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x2) ⇛⇩m (≤)) L2"
  and "x1 ≤⇘L1⇙ x2"
  shows "(≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)"
proof -
  from refl_L1 ‹x1 ≤⇘L1⇙ x2› have "x1 ≤⇘L1⇙ x1" by blast
  with dep_mono_wrt_relD[OF dep_mono_wrt_predD[OF mono_L2] ‹x1 ≤⇘L1⇙ x2›]
    show "(≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)" by auto
qed

lemma reflexive_on_in_field_mono_assm_left2I:
  assumes mono_L2: "((x1 x2 ∷ (≥⇘L1⇙)) ⇛⇩m (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and refl_L1: "reflexive_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙)"
  shows "((x1 : ⊤) ⇛⇩m (x2 x3 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x2) ⇛⇩m (≤)) L2"
proof (intro dep_mono_wrt_predI dep_mono_wrt_relI rel_if_if_impI)
  fix x1 x2 x3 assume "x1 ≤⇘L1⇙ x2" "x2 ≤⇘L1⇙ x3"
  with refl_L1 have "x1 ≥⇘L1⇙ x1" by blast
  from Dep_Fun_Rel_relD[OF dep_mono_wrt_relD[OF mono_L2 ‹x1 ≥⇘L1⇙ x1›]
    ‹x2 ≤⇘L1⇙ x3›] ‹x1 ≤⇘L1⇙ x2›
    show "(≤⇘L2 x1 x2⇙) ≤ (≤⇘L2 x1 x3⇙)" by blast
qed

lemma reflexive_on_in_field_left_if_equivalencesI:
  assumes "((≤⇘L1⇙) ≡⇩G (≤⇘R1⇙)) l1 r1"
  and "preorder_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇛⇩m (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  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⇙)) ⇛⇩m (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 "partial_equivalence_rel (≤⇘L2⇙)"
  shows "(≤⇘L⇙) = tfr.tdfr.L"
  using assms by (intro tpdfr.left_rel_eq_tdfr_leftI) auto

end


end