Theory Transport_No_Dep_Fun

✐‹creator "Kevin Kappelmann"›
section ‹Transport for Dependent Function Relator with Non-Dependent Functions›
theory Transport_No_Dep_Fun
  imports
    Transport_Functions
begin

section ‹Transport for Dependent Function Relator with Non-Dependent Functions›
paragraph ‹Summary›
text ‹We introduce a special case of @{locale transport_Dep_Fun_Rel}.
The derived theorem is easier to apply and supported by the current prototype.›

locale transport_Dep_Fun_Rel_no_dep_fun =
  transport_Dep_Fun_Rel_syntax L1 R1 l1 r1 L2 R2 "λ_ _. l2" "λ_ _. r2" +
  tdfr : transport_Dep_Fun_Rel L1 R1 l1 r1 L2 R2 "λ_ _. l2" "λ_ _. r2"
  for L1 :: "'a1 ⇒ 'a1 ⇒ bool"
  and R1 :: "'a2 ⇒ 'a2 ⇒ bool"
  and l1 :: "'a1 ⇒ 'a2"
  and r1 :: "'a2 ⇒ 'a1"
  and L2 :: "'a1 ⇒ 'a1 ⇒ 'b1 ⇒ 'b1 ⇒ bool"
  and R2 :: "'a2 ⇒ 'a2 ⇒ 'b2 ⇒ 'b2 ⇒ bool"
  and l2 :: "'b1 ⇒ 'b2"
  and r2 :: "'b2 ⇒ 'b1"
begin

notation t2.unit (‹η⇩2›)
notation t2.counit (‹ε⇩2›)

abbreviation "L ≡ tdfr.L"
abbreviation "R ≡ tdfr.R"

abbreviation "l ≡ tdfr.l"
abbreviation "r ≡ tdfr.r"

notation tdfr.L (infix ‹≤⇘L⇙› 50)
notation tdfr.R (infix ‹≤⇘R⇙› 50)

notation tdfr.ge_left (infix ‹≥⇘L⇙› 50)
notation tdfr.ge_right (infix ‹≥⇘R⇙› 50)

notation tdfr.unit (‹η›)
notation tdfr.counit (‹ε›)

theorem partial_equivalence_rel_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘PER⇙ (≤⇘R1⇙)) l1 r1"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇘PER⇙ (≤⇘R2 (l1 x) x'⇙)) l2 r2"
  and tdfr.mono_conds_rel
  shows "((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r"
proof -
  from assms have per2I: "((≤⇘L2 x1 (r1 x2')⇙) ≡⇘PER⇙ (≤⇘R2 (l1 x1) x2'⇙)) l2 r2"
    if "x1 ≤⇘L1⇙ x2" "x2 ⇘L1⇙⪅ x1'" "x1' ≤⇘R1⇙ x2'" for x1 x2 x1' x2'
    using that t1.left_Galois_if_left_Galois_if_left_relI
      t1.left_Galois_if_right_rel_if_left_GaloisI
    by fastforce
  have "tdfr.mono_conds_fun"
    by (intro tdfr.mono_conds_funI tdfr.mono_cond_left_funI tdfr.mono_cond_right_funI dep_mono_wrt_relI
      Dep_Fun_Rel_relI Dep_Fun_Rel_predI)
    (auto 0 10 dest!: per2I)
  with assms show ?thesis by (intro tdfr.partial_equivalence_rel_equivalenceI) auto
qed

end

end