Theory Transport_Functions_Order_Base

✐‹creator "Kevin Kappelmann"›
subsection ‹Basic Order Properties›
theory Transport_Functions_Order_Base
  imports
    Transport_Functions_Base
begin

paragraph ‹Dependent Function Relator›

context hom_Dep_Fun_Rel_orders
begin

lemma reflexive_on_in_domI:
  assumes refl_L: "reflexive_on (in_codom (≤L)) (≤L)"
  and R_le_R_if_L: "x1 x2. x1L x2  (≤⇘R x2 x2)  (≤⇘R x1 x2)"
  and pequiv_R: "x1 x2. x1L x2  partial_equivalence_rel (≤⇘R x1 x2)"
  shows "reflexive_on (in_dom DFR) DFR"
proof (intro reflexive_onI Dep_Fun_Rel_relI)
  fix f x1 x2
  assume "in_dom DFR f"
  then obtain g where "DFR f g" by auto
  moreover assume "x1L x2"
  moreover with refl_L have "x2L x2" by blast
  ultimately have "f x1 ≤⇘R x1 x2g x2" "f x2 ≤⇘R x1 x2g x2"
    using R_le_R_if_L by auto
  moreover with pequiv_R x1L x2  have "g x2 ≤⇘R x1 x2f x2"
    by (blast dest: symmetricD)
  ultimately show "f x1 ≤⇘R x1 x2f x2" using pequiv_R x1L x2 by blast
qed

lemma reflexive_on_in_codomI:
  assumes refl_L: "reflexive_on (in_dom (≤L)) (≤L)"
  and R_le_R_if_L: "x1 x2. x1L x2  (≤⇘R x1 x1)  (≤⇘R x1 x2)"
  and pequiv_R: "x1 x2. x1L x2  partial_equivalence_rel (≤⇘R x1 x2)"
  shows "reflexive_on (in_codom DFR) DFR"
proof (intro reflexive_onI Dep_Fun_Rel_relI)
  fix f x1 x2
  assume "in_codom DFR f"
  then obtain g where "DFR g f" by auto
  moreover assume "x1L x2"
  moreover with refl_L have "x1L x1" by blast
  ultimately have "g x1 ≤⇘R x1 x2f x2" "g x1 ≤⇘R x1 x2f x1"
    using R_le_R_if_L by auto
  moreover with pequiv_R x1L x2  have "f x1 ≤⇘R x1 x2g x1"
    by (blast dest: symmetricD)
  ultimately show "f x1 ≤⇘R x1 x2f x2" using pequiv_R x1L x2 by blast
qed

corollary reflexive_on_in_fieldI:
  assumes "reflexive_on (in_field (≤L)) (≤L)"
  and "x1 x2. x1L x2  (≤⇘R x2 x2)  (≤⇘R x1 x2)"
  and "x1 x2. x1L x2  (≤⇘R x1 x1)  (≤⇘R x1 x2)"
  and "x1 x2. x1L x2  partial_equivalence_rel (≤⇘R x1 x2)"
  shows "reflexive_on (in_field DFR) DFR"
proof -
  from assms have "reflexive_on (in_dom DFR) DFR"
    by (intro reflexive_on_in_domI)
    (auto intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_codom)
  moreover from assms have "reflexive_on (in_codom DFR) DFR"
    by (intro reflexive_on_in_codomI)
    (auto intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_dom)
  ultimately show ?thesis by (auto iff: in_field_iff_in_dom_or_in_codom)
qed

lemma transitiveI:
  assumes refl_L: "reflexive_on (in_dom (≤L)) (≤L)"
  and R_le_R_if_L: "x1 x2. x1L x2  (≤⇘R x1 x1)  (≤⇘R x1 x2)"
  and trans: "x1 x2. x1L x2  transitive (≤⇘R x1 x2)"
  shows "transitive DFR"
proof (intro transitiveI Dep_Fun_Rel_relI)
  fix f1 f2 f3 x1 x2 assume "x1L x2"
  with refl_L have "x1L x1" by blast
  moreover assume "DFR f1 f2"
  ultimately have "f1 x1 ≤⇘R x1 x1f2 x1" by blast
  with R_le_R_if_L have "f1 x1 ≤⇘R x1 x2f2 x1" using x1L x2 by blast
  assume "DFR f2 f3"
  with x1L x2 have "f2 x1 ≤⇘R x1 x2f3 x2" by blast
  with f1 x1 ≤⇘R x1 x2f2 x1 show "f1 x1 ≤⇘R x1 x2f3 x2"
    using trans x1L x2 by blast
qed

lemma transitiveI':
  assumes refl_L: "reflexive_on (in_codom (≤L)) (≤L)"
  and R_le_R_if_L: "x1 x2. x1L x2  (≤⇘R x2 x2)  (≤⇘R x1 x2)"
  and trans: "x1 x2. x1L x2  transitive (≤⇘R x1 x2)"
  shows "transitive DFR"
proof (intro Binary_Relations_Transitive.transitiveI Dep_Fun_Rel_relI)
  fix f1 f2 f3 x1 x2 assume "DFR f1 f2" "x1L x2"
  then have "f1 x1 ≤⇘R x1 x2f2 x2" by blast
  from x1L x2 refl_L have "x2L x2" by blast
  moreover assume "DFR f2 f3"
  ultimately have "f2 x2 ≤⇘R x2 x2f3 x2" by blast
  with R_le_R_if_L have "f2 x2 ≤⇘R x1 x2f3 x2" using x1L x2 by blast
  with f1 x1 ≤⇘R x1 x2f2 x2 show "f1 x1 ≤⇘R x1 x2f3 x2"
    using trans x1L x2 by blast
qed

lemma preorder_on_in_fieldI:
  assumes "reflexive_on (in_field (≤L)) (≤L)"
  and "x1 x2. x1L x2  (≤⇘R x2 x2)  (≤⇘R x1 x2)"
  and "x1 x2. x1L x2  (≤⇘R x1 x1)  (≤⇘R x1 x2)"
  and pequiv_R: "x1 x2. x1L x2  partial_equivalence_rel (≤⇘R x1 x2)"
  shows "preorder_on (in_field DFR) DFR"
  using assms by (intro preorder_onI reflexive_on_in_fieldI)
  (auto intro!: transitiveI dest: pequiv_R elim!: partial_equivalence_relE)

lemma symmetricI:
  assumes sym_L: "symmetric (≤L)"
  and R_le_R_if_L: "x1 x2. x1L x2  (≤⇘R x1 x2)  (≤⇘R x2 x1)"
  and sym_R: "x1 x2. x1L x2  symmetric (≤⇘R x1 x2)"
  shows "symmetric DFR"
proof (intro symmetricI Dep_Fun_Rel_relI)
  fix f g x y assume "xL y"
  with sym_L have "yL x" by (rule symmetricD)
  moreover assume "DFR f g"
  ultimately have "f y ≤⇘R y xg x" by blast
  with sym_R yL x have "g x ≤⇘R y xf y" by (blast dest: symmetricD)
  with R_le_R_if_L yL x show "g x ≤⇘R x yf y" by blast
qed

corollary partial_equivalence_relI:
  assumes "reflexive_on (in_field (≤L)) (≤L)"
  and sym_L: "symmetric (≤L)"
  and mono_R: "((x1 x2  (≤L))  (x3 x4  (≤L) | x1L x3)  (≤)) R"
  and "x1 x2. x1L x2  partial_equivalence_rel (≤⇘R x1 x2)"
  shows "partial_equivalence_rel DFR"
proof -
  have "(≤⇘R x1 x2)  (≤⇘R x2 x1)" if "x1L x2" for x1 x2
  proof -
    from sym_L x1L x2 have "x2L x1" by (rule symmetricD)
    with mono_R x1L x2 show ?thesis by blast
  qed
  with assms show ?thesis
    by (intro partial_equivalence_relI transitiveI symmetricI)
    (blast elim: partial_equivalence_relE[OF assms(4)])+
qed

end

context transport_Dep_Fun_Rel
begin

lemmas reflexive_on_in_field_leftI = dfro1.reflexive_on_in_fieldI
  [folded left_rel_eq_Dep_Fun_Rel]
lemmas transitive_leftI = dfro1.transitiveI[folded left_rel_eq_Dep_Fun_Rel]
lemmas transitive_leftI' = dfro1.transitiveI'[folded left_rel_eq_Dep_Fun_Rel]
lemmas preorder_on_in_field_leftI = dfro1.preorder_on_in_fieldI
  [folded left_rel_eq_Dep_Fun_Rel]
lemmas symmetric_leftI = dfro1.symmetricI[folded left_rel_eq_Dep_Fun_Rel]
lemmas partial_equivalence_rel_leftI = dfro1.partial_equivalence_relI
  [folded left_rel_eq_Dep_Fun_Rel]


subparagraph ‹Introduction Rules for Assumptions›

lemma transitive_left2_if_transitive_left2_if_left_GaloisI:
  assumes "((≤L1)  (≤R1)) l1"
  and "((≤L1) h (≤R1)) l1 r1"
  and L2_eq: "(≤⇘L2 x1 x2) = (≤⇘L2 x1 (η1 x2))"
  and "x x'. x L1x'  transitive (≤⇘L2 x (r1 x'))"
  and "x1L1 x2"
  shows "transitive (≤⇘L2 x1 x2)"
  by (subst L2_eq) (auto intro!: assms t1.left_Galois_left_if_left_relI)

lemma symmetric_left2_if_symmetric_left2_if_left_GaloisI:
  assumes "((≤L1)  (≤R1)) l1"
  and "((≤L1) h (≤R1)) l1 r1"
  and L2_eq: "(≤⇘L2 x1 x2) = (≤⇘L2 x1 (η1 x2))"
  and "x x'. x L1x'  symmetric (≤⇘L2 x (r1 x'))"
  and "x1L1 x2"
  shows "symmetric (≤⇘L2 x1 x2)"
  by (subst L2_eq) (auto intro!: assms t1.left_Galois_left_if_left_relI)

lemma partial_equivalence_rel_left2_if_partial_equivalence_rel_left2_if_left_GaloisI:
  assumes "((≤L1)  (≤R1)) l1"
  and "((≤L1) h (≤R1)) l1 r1"
  and L2_eq: "(≤⇘L2 x1 x2) = (≤⇘L2 x1 (η1 x2))"
  and "x x'. x L1x'  partial_equivalence_rel (≤⇘L2 x (r1 x'))"
  and "x1L1 x2"
  shows "partial_equivalence_rel (≤⇘L2 x1 x2)"
  by (subst L2_eq) (auto intro!: assms t1.left_Galois_left_if_left_relI)

context
  assumes galois_prop: "((≤L1)  (≤R1)) l1 r1"
begin

interpretation flip_inv :
  transport_Dep_Fun_Rel "(≥R1)" "(≥L1)" r1 l1 "flip2 R2" "flip2 L2" r2 l2
  rewrites "flip_inv.t1.unit  ε1"
  and "R x y. (flip2 R x y)  (R y x)¯"
  and "R S. R¯ = S¯  R = S"
  and "R S. (R¯  S¯)  (R  S)"
  and "x x'. x' R1x  x L1x'"
  and "((≥R1) h (≥L1)) r1 l1  True"
  and "(R :: 'z  'z  bool). transitive R¯  transitive R"
  and "(R :: 'z  'z  bool). symmetric R¯  symmetric R"
  and "(R :: 'z  'z  bool). partial_equivalence_rel R¯  partial_equivalence_rel R"
  and "P. (True  P)  Trueprop P"
  and "P Q. (True  PROP P  PROP Q)  (PROP P  True  PROP Q)"
  using galois_prop
  by (auto intro!: Eq_TrueI simp: t1.flip_unit_eq_counit
    galois_prop.half_galois_prop_right_rel_inv_iff_half_galois_prop_left
    mono_wrt_rel_eq_dep_mono_wrt_rel
    simp del: rel_inv_iff_rel)

lemma transitive_right2_if_transitive_right2_if_left_GaloisI:
  assumes "((≤R1)  (≤L1)) r1"
  and "(≤⇘R2 x1 x2) = (≤⇘R2 (ε1 x1) x2)"
  and "x x'. x L1x'  transitive (≤⇘R2 (l1 x) x')"
  and "x1R1 x2"
  shows "transitive (≤⇘R2 x1 x2)"
  using galois_prop assms
  by (intro flip_inv.transitive_left2_if_transitive_left2_if_left_GaloisI
    [simplified rel_inv_iff_rel, of x1])
  auto

lemma symmetric_right2_if_symmetric_right2_if_left_GaloisI:
  assumes "((≤R1)  (≤L1)) r1"
  and "(≤⇘R2 x1 x2) = (≤⇘R2 (ε1 x1) x2)"
  and "x x'. x L1x'  symmetric (≤⇘R2 (l1 x) x')"
  and "x1R1 x2"
  shows "symmetric (≤⇘R2 x1 x2)"
  using galois_prop assms
  by (intro flip_inv.symmetric_left2_if_symmetric_left2_if_left_GaloisI
    [simplified rel_inv_iff_rel, of x1])
  auto

lemma partial_equivalence_rel_right2_if_partial_equivalence_rel_right2_if_left_GaloisI:
  assumes "((≤R1)  (≤L1)) r1"
  and "(≤⇘R2 x1 x2) = (≤⇘R2 (ε1 x1) x2)"
  and "x x'. x L1x'  partial_equivalence_rel (≤⇘R2 (l1 x) x')"
  and "x1R1 x2"
  shows "partial_equivalence_rel (≤⇘R2 x1 x2)"
  using galois_prop assms
  by (intro flip_inv.partial_equivalence_rel_left2_if_partial_equivalence_rel_left2_if_left_GaloisI
    [simplified rel_inv_iff_rel, of x1])
  auto

end

lemma transitive_left2_if_preorder_equivalenceI:
  assumes pre_equiv1: "((≤L1) ≡pre (≤R1)) l1 r1"
  and "((x1 x2  (≥L1))  (x3 x4  (≤L1) | x1L1 x3)  (≤)) L2"
  and "x x'. x L1x'  ((≤⇘L2 x (r1 x'))pre (≤⇘R2 (l1 x) x')) (l2⇘x' x) (r2⇘x x')"
  and "x1L1 x2"
  shows "transitive (≤⇘L2 x1 x2)"
proof -
  from x1L1 x2 pre_equiv1 have "x2 ≡⇘L1η1 x2"
    by (blast elim: t1.preorder_equivalence_order_equivalenceE
      intro: bi_related_if_rel_equivalence_on)
  with assms have "(≤⇘L2 x1 x2) = (≤⇘L2 x1 (η1 x2))"
    by (intro left2_eq_if_bi_related_if_monoI) blast+
  with assms show ?thesis
    by (intro transitive_left2_if_transitive_left2_if_left_GaloisI[of x1]) blast+
qed

lemma symmetric_left2_if_partial_equivalence_rel_equivalenceI:
  assumes PER_equiv1: "((≤L1) ≡PER (≤R1)) l1 r1"
  and "((x1 x2  (≥L1))  (x3 x4  (≤L1) | x1L1 x3)  (≤)) L2"
  and "x x'. x L1x'  ((≤⇘L2 x (r1 x'))PER (≤⇘R2 (l1 x) x')) (l2⇘x' x) (r2⇘x x')"
  and "x1L1 x2"
  shows "symmetric (≤⇘L2 x1 x2)"
proof -
  from x1L1 x2 PER_equiv1 have "x2 ≡⇘L1η1 x2"
    by (blast elim: t1.preorder_equivalence_order_equivalenceE
      intro: bi_related_if_rel_equivalence_on)
  with assms have "(≤⇘L2 x1 x2) = (≤⇘L2 x1 (η1 x2))"
    by (intro left2_eq_if_bi_related_if_monoI) blast+
  with assms show ?thesis
    by (intro symmetric_left2_if_symmetric_left2_if_left_GaloisI[of x1]) blast+
qed

lemma partial_equivalence_rel_left2_if_partial_equivalence_rel_equivalenceI:
  assumes PER_equiv1: "((≤L1) ≡PER (≤R1)) l1 r1"
  and "((x1 x2  (≥L1))  (x3 x4  (≤L1) | x1L1 x3)  (≤)) L2"
  and "x x'. x L1x'  ((≤⇘L2 x (r1 x'))PER (≤⇘R2 (l1 x) x')) (l2⇘x' x) (r2⇘x x')"
  and "x1L1 x2"
  shows "partial_equivalence_rel (≤⇘L2 x1 x2)"
proof -
  from x1L1 x2 PER_equiv1 have "x2 ≡⇘L1η1 x2"
    by (blast elim: t1.preorder_equivalence_order_equivalenceE
      intro: bi_related_if_rel_equivalence_on)
  with assms have "(≤⇘L2 x1 x2) = (≤⇘L2 x1 (η1 x2))"
    by (intro left2_eq_if_bi_related_if_monoI) blast+
  with assms show ?thesis
    by (intro partial_equivalence_rel_left2_if_partial_equivalence_rel_left2_if_left_GaloisI[of x1])
    blast+
qed

interpretation flip : transport_Dep_Fun_Rel R1 L1 r1 l1 R2 L2 r2 l2
  rewrites "flip.t1.counit  η1" and "flip.t1.unit  ε1"
  by (simp_all only: t1.flip_counit_eq_unit t1.flip_unit_eq_counit)

lemma transitive_right2_if_preorder_equivalenceI:
  assumes pre_equiv1: "((≤L1) ≡pre (≤R1)) l1 r1"
  and "((x1' x2'  (≥R1))  (x3' x4'  (≤R1) | x1'R1 x3')  (≤)) R2"
  and "x x'. x L1x'  ((≤⇘L2 x (r1 x'))pre (≤⇘R2 (l1 x) x')) (l2⇘x' x) (r2⇘x x')"
  and "x1'R1 x2'"
  shows "transitive (≤⇘R2 x1' x2')"
proof -
  from x1'R1 x2' pre_equiv1 have "x1' ≡⇘R1ε1 x1'"
    by (blast elim: t1.preorder_equivalence_order_equivalenceE
      intro: bi_related_if_rel_equivalence_on)
  with assms have "(≤⇘R2 x1' x2') = (≤⇘R2 (ε1 x1') x2')"
    by (intro flip.left2_eq_if_bi_related_if_monoI) blast+
  with assms show ?thesis
    by (intro transitive_right2_if_transitive_right2_if_left_GaloisI[of x1']) blast+
qed

lemma symmetric_right2_if_partial_equivalence_rel_equivalenceI:
  assumes PER_equiv1: "((≤L1) ≡PER (≤R1)) l1 r1"
  and "((x1' x2'  (≥R1))  (x3' x4'  (≤R1) | x1'R1 x3')  (≤)) R2"
  and "x x'. x L1x'  ((≤⇘L2 x (r1 x'))PER (≤⇘R2 (l1 x) x')) (l2⇘x' x) (r2⇘x x')"
  and "x1'R1 x2'"
  shows "symmetric (≤⇘R2 x1' x2')"
proof -
  from x1'R1 x2' PER_equiv1 have "x1' ≡⇘R1ε1 x1'"
    by (blast elim: t1.preorder_equivalence_order_equivalenceE
      intro: bi_related_if_rel_equivalence_on)
  with assms have "(≤⇘R2 x1' x2') = (≤⇘R2 (ε1 x1') x2')"
    by (intro flip.left2_eq_if_bi_related_if_monoI) blast+
  with assms show ?thesis
    by (intro symmetric_right2_if_symmetric_right2_if_left_GaloisI[of x1']) blast+
qed

lemma partial_equivalence_rel_right2_if_partial_equivalence_rel_equivalenceI:
  assumes PER_equiv1: "((≤L1) ≡PER (≤R1)) l1 r1"
  and "((x1' x2'  (≥R1))  (x3' x4'  (≤R1) | x1'R1 x3')  (≤)) R2"
  and "x x'. x L1x'  ((≤⇘L2 x (r1 x'))PER (≤⇘R2 (l1 x) x')) (l2⇘x' x) (r2⇘x x')"
  and "x1'R1 x2'"
  shows "partial_equivalence_rel (≤⇘R2 x1' x2')"
proof -
  from x1'R1 x2' PER_equiv1 have "x1' ≡⇘R1ε1 x1'"
    by (blast elim: t1.preorder_equivalence_order_equivalenceE
      intro: bi_related_if_rel_equivalence_on)
  with assms have "(≤⇘R2 x1' x2') = (≤⇘R2 (ε1 x1') x2')"
    by (intro flip.left2_eq_if_bi_related_if_monoI) blast+
  with assms show ?thesis
    by (intro partial_equivalence_rel_right2_if_partial_equivalence_rel_right2_if_left_GaloisI[of x1'])
    blast+
qed

end

paragraph ‹Function Relator›

context transport_Fun_Rel
begin

lemma reflexive_on_in_field_leftI:
  assumes "reflexive_on (in_field (≤L1)) (≤L1)"
  and "partial_equivalence_rel (≤L2)"
  shows "reflexive_on (in_field (≤L)) (≤L)"
  using assms by (intro tdfr.reflexive_on_in_field_leftI) simp_all

lemma transitive_leftI:
  assumes "reflexive_on (in_dom (≤L1)) (≤L1)"
  and "transitive (≤L2)"
  shows "transitive (≤L)"
  using assms by (intro tdfr.transitive_leftI) simp_all

lemma transitive_leftI':
  assumes "reflexive_on (in_codom (≤L1)) (≤L1)"
  and "transitive (≤L2)"
  shows "transitive (≤L)"
  using assms by (intro tdfr.transitive_leftI') simp_all

lemma preorder_on_in_field_leftI:
  assumes "reflexive_on (in_field (≤L1)) (≤L1)"
  and "partial_equivalence_rel (≤L2)"
  shows "preorder_on (in_field (≤L)) (≤L)"
  using assms by (intro tdfr.preorder_on_in_field_leftI) simp_all

lemma symmetric_leftI:
  assumes "symmetric (≤L1)"
  and "symmetric (≤L2)"
  shows "symmetric (≤L)"
  using assms by (intro tdfr.symmetric_leftI) simp_all

corollary partial_equivalence_rel_leftI:
  assumes "reflexive_on (in_field (≤L1)) (≤L1)"
  and "symmetric (≤L1)"
  and "partial_equivalence_rel (≤L2)"
  shows "partial_equivalence_rel (≤L)"
  using assms by (intro tdfr.partial_equivalence_rel_leftI) auto

end

paragraph ‹Monotone Dependent Function Relator›

context transport_Mono_Dep_Fun_Rel
begin

lemmas reflexive_on_in_field_leftI = Refl_Rel_reflexive_on_in_field[of tdfr.L,
  folded left_rel_eq_tdfr_left_Refl_Rel]
lemmas transitive_leftI = Refl_Rel_transitiveI
  [of tdfr.L, folded left_rel_eq_tdfr_left_Refl_Rel]
lemmas preorder_on_in_field_leftI = Refl_Rel_preorder_on_in_fieldI[of tdfr.L,
  folded left_rel_eq_tdfr_left_Refl_Rel]
lemmas symmetric_leftI = Refl_Rel_symmetricI[of tdfr.L,
  OF tdfr.symmetric_leftI, folded left_rel_eq_tdfr_left_Refl_Rel]
lemmas partial_equivalence_rel_leftI = Refl_Rel_partial_equivalence_relI[of tdfr.L,
  OF tdfr.partial_equivalence_rel_leftI, folded left_rel_eq_tdfr_left_Refl_Rel]

end


paragraph ‹Monotone Function Relator›

context transport_Mono_Fun_Rel
begin

lemma symmetric_leftI:
  assumes "symmetric (≤L1)"
  and "symmetric (≤L2)"
  shows "symmetric (≤L)"
  using assms by (intro tpdfr.symmetric_leftI) auto

lemma partial_equivalence_rel_leftI:
  assumes "reflexive_on (in_field (≤L1)) (≤L1)"
  and "symmetric (≤L1)"
  and "partial_equivalence_rel (≤L2)"
  shows "partial_equivalence_rel (≤L)"
  using assms by (intro tpdfr.partial_equivalence_rel_leftI) auto

end


end