# Theory PER

theory PER
imports Main
(*  Title:      HOL/ex/PER.thy    Author:     Oscar Slotosch and Markus Wenzel, TU Muenchen*)header {* Partial equivalence relations *}theory PER imports Main begintext {*  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 blastlemma domainD [dest]: "x ∈ domain ==> x ∼ x"  unfolding domain_def by blasttheorem domainI' [elim?]: "x ∼ y ==> x ∈ domain"proof  assume xy: "x ∼ y"  also from xy have "y ∼ x" ..  finally show "x ∼ x" .qedsubsection {* 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_equivbegindefinition  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 blastlemma partial_equiv_funD [dest?]:    "f ∼ g ==> x ∈ domain ==> y ∈ domain ==> x ∼ y ==> f x ∼ g y"  unfolding eqv_fun_def by blasttext {*  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" .  qedqedendsubsection {* 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" ..qedtheorem 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 ..qedsubsection {* 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 blastlemma quotI [intro]: "{x. a ∼ x} ∈ quot"  unfolding quot_def by blastlemma quotE [elim]: "R ∈ quot ==> (!!a. R = {x. a ∼ x} ==> C) ==> C"  unfolding quot_def by blasttext {*  \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)qedlemma quot_cases [cases type: quot]:  obtains (rep) a where "A = ⌊a⌋"  using quot_rep by blastsubsection {* 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)qedtheorem 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" ..qedtheorem eqv_class_eqD [dest?]: "⌊a⌋ = ⌊b⌋ ==> a ∼ (b::'a::equiv)"proof (rule eqv_class_eqD')  show "a ∈ domain" ..qedlemma 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 blastsubsection {* 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" ..  qedqedtheorem pick_eqv [intro, simp]: "pick ⌊a⌋ ∼ (a::'a::equiv)"proof (rule pick_eqv')  show "a ∈ domain" ..qedtheorem 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 simpqedend