section ‹Partial equivalence relations›
theory PER
imports Main
begin
text ‹
Higher-order quotients are defined over partial equivalence
relations (PERs) instead of total ones. We provide axiomatic type
classes ‹equiv < partial_equiv› and a type constructor
‹'a quot› with basic operations. This development is based
on:
Oscar Slotosch: \emph{Higher Order Quotients and their
Implementation in Isabelle HOL.} Elsa L. Gunter and Amy Felty,
editors, Theorem Proving in Higher Order Logics: TPHOLs '97,
Springer LNCS 1275, 1997.
›
subsection ‹Partial equivalence›
text ‹
Type class ‹partial_equiv› models partial equivalence
relations (PERs) using the polymorphic ‹∼ :: 'a ⇒ 'a ⇒
bool› relation, which is required to be symmetric and transitive,
but not necessarily reflexive.
›
class partial_equiv =
fixes eqv :: "'a ⇒ 'a ⇒ bool" (infixl "∼" 50)
assumes partial_equiv_sym [elim?]: "x ∼ y ⟹ y ∼ x"
assumes partial_equiv_trans [trans]: "x ∼ y ⟹ y ∼ z ⟹ x ∼ z"
text ‹
\medskip The domain of a partial equivalence relation is the set of
reflexive elements. Due to symmetry and transitivity this
characterizes exactly those elements that are connected with
\emph{any} other one.
›
definition
"domain" :: "'a::partial_equiv set" where
"domain = {x. x ∼ x}"
lemma domainI [intro]: "x ∼ x ⟹ x ∈ domain"
unfolding domain_def by blast
lemma domainD [dest]: "x ∈ domain ⟹ x ∼ x"
unfolding domain_def by blast
theorem domainI' [elim?]: "x ∼ y ⟹ x ∈ domain"
proof
assume xy: "x ∼ y"
also from xy have "y ∼ x" ..
finally show "x ∼ x" .
qed
subsection ‹Equivalence on function spaces›
text ‹
The ‹∼› relation is lifted to function spaces. It is
important to note that this is \emph{not} the direct product, but a
structural one corresponding to the congruence property.
›
instantiation "fun" :: (partial_equiv, partial_equiv) partial_equiv
begin
definition "f ∼ g ⟷ (∀x ∈ domain. ∀y ∈ domain. x ∼ y ⟶ f x ∼ g y)"
lemma partial_equiv_funI [intro?]:
"(⋀x y. x ∈ domain ⟹ y ∈ domain ⟹ x ∼ y ⟹ f x ∼ g y) ⟹ f ∼ g"
unfolding eqv_fun_def by blast
lemma partial_equiv_funD [dest?]:
"f ∼ g ⟹ x ∈ domain ⟹ y ∈ domain ⟹ x ∼ y ⟹ f x ∼ g y"
unfolding eqv_fun_def by blast
text ‹
The class of partial equivalence relations is closed under function
spaces (in \emph{both} argument positions).
›
instance proof
fix f g h :: "'a::partial_equiv ⇒ 'b::partial_equiv"
assume fg: "f ∼ g"
show "g ∼ f"
proof
fix x y :: 'a
assume x: "x ∈ domain" and y: "y ∈ domain"
assume "x ∼ y" then have "y ∼ x" ..
with fg y x have "f y ∼ g x" ..
then show "g x ∼ f y" ..
qed
assume gh: "g ∼ h"
show "f ∼ h"
proof
fix x y :: 'a
assume x: "x ∈ domain" and y: "y ∈ domain" and "x ∼ y"
with fg have "f x ∼ g y" ..
also from y have "y ∼ y" ..
with gh y y have "g y ∼ h y" ..
finally show "f x ∼ h y" .
qed
qed
end
subsection ‹Total equivalence›
text ‹
The class of total equivalence relations on top of PERs. It
coincides with the standard notion of equivalence, i.e.\ ‹∼
:: 'a ⇒ 'a ⇒ bool› is required to be reflexive, transitive and
symmetric.
›
class equiv =
assumes eqv_refl [intro]: "x ∼ x"
text ‹
On total equivalences all elements are reflexive, and congruence
holds unconditionally.
›
theorem equiv_domain [intro]: "(x::'a::equiv) ∈ domain"
proof
show "x ∼ x" ..
qed
theorem equiv_cong [dest?]: "f ∼ g ⟹ x ∼ y ⟹ f x ∼ g (y::'a::equiv)"
proof -
assume "f ∼ g"
moreover have "x ∈ domain" ..
moreover have "y ∈ domain" ..
moreover assume "x ∼ y"
ultimately show ?thesis ..
qed
subsection ‹Quotient types›
text ‹
The quotient type ‹'a quot› consists of all
\emph{equivalence classes} over elements of the base type @{typ 'a}.
›
definition "quot = {{x. a ∼ x}| a::'a::partial_equiv. True}"
typedef (overloaded) 'a quot = "quot :: 'a::partial_equiv set set"
unfolding quot_def by blast
lemma quotI [intro]: "{x. a ∼ x} ∈ quot"
unfolding quot_def by blast
lemma quotE [elim]: "R ∈ quot ⟹ (⋀a. R = {x. a ∼ x} ⟹ C) ⟹ C"
unfolding quot_def by blast
text ‹
\medskip Abstracted equivalence classes are the canonical
representation of elements of a quotient type.
›
definition eqv_class :: "('a::partial_equiv) ⇒ 'a quot" ("⌊_⌋")
where "⌊a⌋ = Abs_quot {x. a ∼ x}"
theorem quot_rep: "∃a. A = ⌊a⌋"
proof (cases A)
fix R assume R: "A = Abs_quot R"
assume "R ∈ quot" then have "∃a. R = {x. a ∼ x}" by blast
with R have "∃a. A = Abs_quot {x. a ∼ x}" by blast
then show ?thesis by (unfold eqv_class_def)
qed
lemma quot_cases [cases type: quot]:
obtains (rep) a where "A = ⌊a⌋"
using quot_rep by blast
subsection ‹Equality on quotients›
text ‹
Equality of canonical quotient elements corresponds to the original
relation as follows.
›
theorem eqv_class_eqI [intro]: "a ∼ b ⟹ ⌊a⌋ = ⌊b⌋"
proof -
assume ab: "a ∼ b"
have "{x. a ∼ x} = {x. b ∼ x}"
proof (rule Collect_cong)
fix x show "a ∼ x ⟷ b ∼ x"
proof
from ab have "b ∼ a" ..
also assume "a ∼ x"
finally show "b ∼ x" .
next
note ab
also assume "b ∼ x"
finally show "a ∼ x" .
qed
qed
then show ?thesis by (simp only: eqv_class_def)
qed
theorem eqv_class_eqD' [dest?]: "⌊a⌋ = ⌊b⌋ ⟹ a ∈ domain ⟹ a ∼ b"
proof (unfold eqv_class_def)
assume "Abs_quot {x. a ∼ x} = Abs_quot {x. b ∼ x}"
then have "{x. a ∼ x} = {x. b ∼ x}" by (simp only: Abs_quot_inject quotI)
moreover assume "a ∈ domain" then have "a ∼ a" ..
ultimately have "a ∈ {x. b ∼ x}" by blast
then have "b ∼ a" by blast
then show "a ∼ b" ..
qed
theorem eqv_class_eqD [dest?]: "⌊a⌋ = ⌊b⌋ ⟹ a ∼ (b::'a::equiv)"
proof (rule eqv_class_eqD')
show "a ∈ domain" ..
qed
lemma eqv_class_eq' [simp]: "a ∈ domain ⟹ ⌊a⌋ = ⌊b⌋ ⟷ a ∼ b"
using eqv_class_eqI eqv_class_eqD' by (blast del: eqv_refl)
lemma eqv_class_eq [simp]: "⌊a⌋ = ⌊b⌋ ⟷ a ∼ (b::'a::equiv)"
using eqv_class_eqI eqv_class_eqD by blast
subsection ‹Picking representing elements›
definition pick :: "'a::partial_equiv quot ⇒ 'a"
where "pick A = (SOME a. A = ⌊a⌋)"
theorem pick_eqv' [intro?, simp]: "a ∈ domain ⟹ pick ⌊a⌋ ∼ a"
proof (unfold pick_def)
assume a: "a ∈ domain"
show "(SOME x. ⌊a⌋ = ⌊x⌋) ∼ a"
proof (rule someI2)
show "⌊a⌋ = ⌊a⌋" ..
fix x assume "⌊a⌋ = ⌊x⌋"
from this and a have "a ∼ x" ..
then show "x ∼ a" ..
qed
qed
theorem pick_eqv [intro, simp]: "pick ⌊a⌋ ∼ (a::'a::equiv)"
proof (rule pick_eqv')
show "a ∈ domain" ..
qed
theorem pick_inverse: "⌊pick A⌋ = (A::'a::equiv quot)"
proof (cases A)
fix a assume a: "A = ⌊a⌋"
then have "pick A ∼ a" by simp
then have "⌊pick A⌋ = ⌊a⌋" by simp
with a show ?thesis by simp
qed
end