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 : )  (x2 x3  (≤L1) | x1L1 x2)  (≤)) L2"
  and "x1L1 x2"
  shows "(≤⇘L2 x1 x1)  (≤⇘L2 x1 x2)"
proof -
  from refl_L1 x1L1 x2 have "x1L1 x1" by blast
  with dep_mono_wrt_relD[OF dep_mono_wrt_predD[OF mono_L2] x1L1 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))  (x3 x4  (≤L1) | x1L1 x3)  (≤)) L2"
  and refl_L1: "reflexive_on (in_dom (≤L1)) (≤L1)"
  shows "((x1 : )  (x2 x3  (≤L1) | x1L1 x2)  (≤)) L2"
proof (intro dep_mono_wrt_predI dep_mono_wrt_relI rel_if_if_impI)
  fix x1 x2 x3 assume "x1L1 x2" "x2L1 x3"
  with refl_L1 have "x1L1 x1" by blast
  from Dep_Fun_Rel_relD[OF dep_mono_wrt_relD[OF mono_L2 x1L1 x1]
    x2L1 x3] x1L1 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))  (x3 x4  (≤L1) | x1L1 x3)  (≤)) L2"
  and "x1 x2. x1L1 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. x1L1 x2  (≤⇘L2 x2 x2)  (≤⇘L2 x1 x2)"
  and "x1 x2. x1L1 x2  (≤⇘L2 x1 x1)  (≤⇘L2 x1 x2)"
  and "x1 x2. x1L1 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) | x1L1 x3)  (≤)) L2"
  and "x1 x2. x1L1 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