Theory Transport_Partial_Quotient_Types

✐‹creator "Kevin Kappelmann"›
section ‹Transport for Partial Quotient Types›
theory Transport_Partial_Quotient_Types
  imports
    HOL.Lifting
    Transport
begin

paragraph ‹Summary›
text ‹Every partial quotient type @{term Quotient}, as used by the Lifting
package, is transportable.›

context transport
begin

interpretation t : transport L "(=)" l r .

lemma Quotient_T_eq_Galois:
  assumes "Quotient (≤⇘L⇙) l r T"
  shows "T = t.Galois"
proof (intro ext iffI)
  fix x y assume "T x y"
  with assms have "x ≤⇘L⇙ x" "l x = y" using Quotient_cr_rel by auto
  with assms have "r (l x) ≤⇘L⇙ x" "r (l x) ≤⇘L⇙ r y"
    using Quotient_rep_abs Quotient_rep_reflp by auto
  with assms have "x ≤⇘L⇙ r y" using Quotient_part_equivp
    by (blast elim: part_equivpE dest: transpD sympD)
  then show "t.Galois x y" by blast
next
  fix x y assume "t.Galois x y"
  with assms show "T x y" using Quotient_cr_rel Quotient_refl1 Quotient_symp
    by (fastforce intro: Quotient_rel_abs2[symmetric] dest: sympD)
qed

lemma Quotient_if_preorder_equivalence:
  assumes "((≤⇘L⇙) ≡⇘pre⇙ (=)) l r"
  shows "Quotient (≤⇘L⇙) l r t.Galois"
proof (rule QuotientI)
  from assms show g2: "l (r y) = y" for y by fastforce
  from assms show "r y ≤⇘L⇙ r y" for y by blast
  show g1: "x ≤⇘L⇙ x' ⟷ x ≤⇘L⇙ x ∧ x' ≤⇘L⇙ x' ∧ l x = l x'"
    (is "?lhs ⟷ ?rhs") for x x'
  proof (rule iffI)
    assume ?rhs
    with assms have "η x ≤⇘L⇙ η x'" by fastforce
    moreover from ‹?rhs› assms have "x ≤⇘L⇙ η x" "η x' ≤⇘L⇙ x'"
      by (blast elim: t.preorder_equivalence_order_equivalenceE)+
    moreover from assms have "transitive (≤⇘L⇙)" by blast
    ultimately show "x ≤⇘L⇙ x'" by blast
  next
    assume ?lhs
    with assms show ?rhs by blast
  qed
  from assms show "t.Galois = (λx y. x ≤⇘L⇙ x ∧ l x = y)"
    by (intro ext iffI)
    (metis g1 g2 t.left_GaloisE,
      auto intro!: t.left_Galois_left_if_left_rel_if_inflationary_on_in_fieldI
      elim!: t.preorder_equivalence_order_equivalenceE)
qed

lemma partial_equivalence_rel_equivalence_if_Quotient:
  assumes "Quotient (≤⇘L⇙) l r T"
  shows "((≤⇘L⇙) ≡⇘PER⇙ (=)) l r"
proof (rule t.partial_equivalence_rel_equivalence_if_order_equivalenceI)
  from Quotient_part_equivp[OF assms] show "partial_equivalence_rel (≤⇘L⇙)"
    by (blast elim: part_equivpE dest: transpD sympD)
  have "x ≡⇘L⇙ r (l x)" if "in_field (≤⇘L⇙) x" for x
  proof -
    from assms ‹in_field (≤⇘L⇙) x› have "x ≤⇘L⇙ x"
      using Quotient_refl1 Quotient_refl2 by fastforce
    with assms Quotient_rep_abs Quotient_symp show ?thesis
      by (fastforce dest: sympD)
  qed
  with assms show "((≤⇘L⇙) ≡⇩o (=)) l r"
    using Quotient_abs_rep Quotient_rel_abs Quotient_rep_reflp
      Quotient_abs_rep[symmetric]
    by (intro t.order_equivalenceI mono_wrt_relI rel_equivalence_onI
      inflationary_onI deflationary_onI)
    auto
qed auto

corollary Quotient_iff_partial_equivalence_rel_equivalence:
  "Quotient (≤⇘L⇙) l r t.Galois ⟷ ((≤⇘L⇙) ≡⇘PER⇙ (=)) l r"
  using Quotient_if_preorder_equivalence partial_equivalence_rel_equivalence_if_Quotient
  by blast

corollary Quotient_T_eq_ge_Galois_right:
  assumes "Quotient (≤⇘L⇙) l r T"
  shows "T = t.ge_Galois_right"
  using assms
  by (subst t.ge_Galois_right_eq_left_Galois_if_symmetric_if_in_codom_eq_in_dom_if_galois_prop)
  (blast dest: partial_equivalence_rel_equivalence_if_Quotient
  intro: in_codom_eq_in_dom_if_reflexive_on_in_field Quotient_T_eq_Galois)+

end


end