(* 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