(* Title: HOL/ex/PER.thy

Author: Oscar Slotosch and Markus Wenzel, TU Muenchen

*)

header {* 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 @{text "equiv < partial_equiv"} and a type constructor

@{text "'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 @{text partial_equiv} models partial equivalence

relations (PERs) using the polymorphic @{text "∼ :: '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 @{text ∼} 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

eqv_fun_def: "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.\ @{text "∼

:: '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 @{text "'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 '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