Theory Transport_Partial_Quotient_Types
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