Theory Transport_Compositions_Agree_Order_Equivalence

✐‹creator "Kevin Kappelmann"›
subsection ‹Order Equivalence›
theory Transport_Compositions_Agree_Order_Equivalence
  imports
    Transport_Compositions_Agree_Monotone
begin

context transport_comp_agree
begin

subsubsection ‹Unit›
paragraph ‹Inflationary›

lemma inflationary_on_unitI:
  assumes mono_l1: "(P ⇛⇩m P') l1"
  and mono_r1: "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and inflationary_unit1: "inflationary_on P (≤⇘L1⇙) η⇩1"
  and trans_L1: "transitive (≤⇘L1⇙)"
  and inflationary_unit2: "inflationary_on P' (≤⇘L2⇙) η⇩2"
  and L2_le_R1: "⋀x. P x ⟹ l1 x ≤⇘L2⇙ r2 (l x) ⟹ l1 x ≤⇘R1⇙ r2 (l x)"
  shows "inflationary_on P (≤⇘L⇙) η"
proof (rule inflationary_onI)
  fix x assume "P x"
  with mono_l1 have "P' (l1 x)" by blast
  with inflationary_unit2 have "l1 x ≤⇘L2⇙ r2 (l x)" by auto
  with L2_le_R1 ‹P x› have "l1 x ≤⇘R1⇙ r2 (l x)" by blast
  with mono_r1 have "η⇩1 x ≤⇘L1⇙ η x" by auto
  moreover from inflationary_unit1 ‹P x› have "x ≤⇘L1⇙ η⇩1 x" by auto
  ultimately show "x ≤⇘L⇙ η x" using trans_L1 by blast
qed

corollary inflationary_on_in_field_unitI:
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘L2⇙)) l1"
  and "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and "inflationary_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and "transitive (≤⇘L1⇙)"
  and "inflationary_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and "⋀x. in_field (≤⇘L1⇙) x ⟹ l1 x ≤⇘L2⇙ r2 (l x) ⟹ l1 x ≤⇘R1⇙ r2 (l x)"
  shows "inflationary_on (in_field (≤⇘L⇙)) (≤⇘L⇙) η"
  using assms by (intro inflationary_on_unitI dep_mono_wrt_predI) (auto 5 0)


paragraph ‹Deflationary›

context
begin

interpretation inv :
  transport_comp_agree "(≥⇘L1⇙)" "(≥⇘R1⇙)" l1 r1 "(≥⇘L2⇙)" "(≥⇘R2⇙)" l2 r2
  rewrites "⋀R S. (R¯ ⇛⇩m S¯) ≡ (R ⇛⇩m S)"
  and "⋀(P :: 'i ⇒ bool) (R :: 'j ⇒ 'i ⇒ bool).
    (inflationary_on P R¯ :: ('i ⇒ 'j) ⇒ bool) ≡ deflationary_on P R"
  and "⋀(R :: 'i ⇒ 'i ⇒ bool). transitive R¯ ≡ transitive R"
  and "⋀R. in_field R¯ ≡ in_field R"
  by (simp_all add: mono_wrt_rel_eq_dep_mono_wrt_rel)

lemma deflationary_on_in_field_unitI:
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘L2⇙)) l1"
  and "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and "deflationary_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and "transitive (≤⇘L1⇙)"
  and "deflationary_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and "⋀x. in_field (≤⇘L1⇙) x ⟹ r2 (l x) ≤⇘L2⇙ l1 x ⟹ r2 (l x) ≤⇘R1⇙ l1 x"
  shows "deflationary_on (in_field (≤⇘L⇙)) (≤⇘L⇙) η"
  using assms by (intro inv.inflationary_on_in_field_unitI[simplified rel_inv_iff_rel])
  auto

end


text ‹Relational Equivalence›

corollary rel_equivalence_on_in_field_unitI:
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘L2⇙)) l1"
  and "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and "rel_equivalence_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and "transitive (≤⇘L1⇙)"
  and "rel_equivalence_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and "⋀x. in_field (≤⇘L1⇙) x ⟹ l1 x ≤⇘L2⇙ r2 (l x) ⟹ l1 x ≤⇘R1⇙ r2 (l x)"
  and "⋀x. in_field (≤⇘L1⇙) x ⟹ r2 (l x) ≤⇘L2⇙ l1 x ⟹ r2 (l x) ≤⇘R1⇙ l1 x"
  shows "rel_equivalence_on (in_field (≤⇘L⇙)) (≤⇘L⇙) η"
  using assms by (intro rel_equivalence_onI
    inflationary_on_in_field_unitI deflationary_on_in_field_unitI)
  auto


subsubsection ‹Counit›

text ‹Corresponding lemmas for the counit can be obtained by flipping the
interpretation of the locale.›


subsubsection ‹Order Equivalence›

interpretation flip : transport_comp_agree R2 L2 r2 l2 R1 L1 r1 l1
  rewrites "flip.g1.unit ≡ ε⇩2" and "flip.g2.unit ≡ ε⇩1" and "flip.unit ≡ ε"
  by (simp_all only: g1.flip_unit_eq_counit g2.flip_unit_eq_counit flip_unit_eq_counit)

lemma order_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇩o (≤⇘R1⇙)) l1 r1"
  and "transitive (≤⇘L1⇙)"
  and "((≤⇘L2⇙) ≡⇩o (≤⇘R2⇙)) l2 r2"
  and "transitive (≤⇘R2⇙)"
  and "⋀x y. x ≤⇘L1⇙ y ⟹ l1 x ≤⇘R1⇙ l1 y ⟹ l1 x ≤⇘L2⇙ l1 y"
  and "⋀x y. x ≤⇘R2⇙ y ⟹ r2 x ≤⇘L2⇙ r2 y ⟹ r2 x ≤⇘R1⇙ r2 y"
  and "⋀x. in_field (≤⇘L1⇙) x ⟹ l1 x ≤⇘L2⇙ r2 (l x) ⟹ l1 x ≤⇘R1⇙ r2 (l x)"
  and "⋀x. in_field (≤⇘L1⇙) x ⟹ r2 (l x) ≤⇘L2⇙ l1 x ⟹ r2 (l x) ≤⇘R1⇙ l1 x"
  and "⋀x. in_field (≤⇘R2⇙) x ⟹ r2 x ≤⇘R1⇙ l1 (r x) ⟹ r2 x ≤⇘L2⇙ l1 (r x)"
  and "⋀x. in_field (≤⇘R2⇙) x ⟹ l1 (r x) ≤⇘R1⇙ r2 x ⟹ l1 (r x) ≤⇘L2⇙ r2 x"
  shows "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  using assms by (intro order_equivalenceI rel_equivalence_on_in_field_unitI
    flip.rel_equivalence_on_in_field_unitI
    mono_wrt_rel_leftI flip.mono_wrt_rel_leftI mono_wrt_relI)
  (auto elim!: g1.order_equivalenceE g2.order_equivalenceE)

end

context transport_comp_same
begin

lemma order_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇩o (≤⇘R1⇙)) l1 r1"
  and "transitive (≤⇘L1⇙)"
  and "((≤⇘R1⇙) ≡⇩o (≤⇘R2⇙)) l2 r2"
  and "transitive (≤⇘R2⇙)"
  shows "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  using assms by (rule order_equivalenceI) auto

end


end