wenzelm@10250: (*  Title:      HOL/Library/Quotient.thy
wenzelm@10250:     ID:         $Id$
wenzelm@10250:     Author:     Gertrud Bauer and Markus Wenzel, TU Muenchen
wenzelm@10250: *)
wenzelm@10250: 
wenzelm@10250: header {*
wenzelm@10250:   \title{Quotients}
wenzelm@10250:   \author{Gertrud Bauer and Markus Wenzel}
wenzelm@10250: *}
wenzelm@10250: 
wenzelm@10250: theory Quotient = Main:
wenzelm@10250: 
wenzelm@10250: text {*
wenzelm@10250:  Higher-order quotients are defined over partial equivalence relations
wenzelm@10250:  (PERs) instead of total ones.  We provide axiomatic type classes
wenzelm@10250:  @{text "equiv < partial_equiv"} and a type constructor
wenzelm@10250:  @{text "'a quot"} with basic operations.  Note that conventional
wenzelm@10250:  quotient constructions emerge as a special case.  This development is
wenzelm@10250:  loosely based on \cite{Slotosch:1997}.
wenzelm@10250: *}
wenzelm@10250: 
wenzelm@10250: 
wenzelm@10250: subsection {* Equivalence relations *}
wenzelm@10250: 
wenzelm@10250: subsubsection {* Partial equivalence *}
wenzelm@10250: 
wenzelm@10250: text {*
wenzelm@10250:  Type class @{text partial_equiv} models partial equivalence relations
wenzelm@10250:  (PERs) using the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation,
wenzelm@10250:  which is required to be symmetric and transitive, but not necessarily
wenzelm@10250:  reflexive.
wenzelm@10250: *}
wenzelm@10250: 
wenzelm@10250: consts
wenzelm@10250:   eqv :: "'a => 'a => bool"    (infixl "\<sim>" 50)
wenzelm@10250: 
wenzelm@10250: axclass partial_equiv < "term"
wenzelm@10250:   eqv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
wenzelm@10250:   eqv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
wenzelm@10250: 
wenzelm@10250: text {*
wenzelm@10250:  \medskip The domain of a partial equivalence relation is the set of
wenzelm@10250:  reflexive elements.  Due to symmetry and transitivity this
wenzelm@10250:  characterizes exactly those elements that are connected with
wenzelm@10250:  \emph{any} other one.
wenzelm@10250: *}
wenzelm@10250: 
wenzelm@10250: constdefs
wenzelm@10250:   domain :: "'a::partial_equiv set"
wenzelm@10250:   "domain == {x. x \<sim> x}"
wenzelm@10250: 
wenzelm@10250: lemma domainI [intro]: "x \<sim> x ==> x \<in> domain"
wenzelm@10250:   by (unfold domain_def) blast
wenzelm@10250: 
wenzelm@10250: lemma domainD [dest]: "x \<in> domain ==> x \<sim> x"
wenzelm@10250:   by (unfold domain_def) blast
wenzelm@10250: 
wenzelm@10250: theorem domainI' [elim?]: "x \<sim> y ==> x \<in> domain"
wenzelm@10250: proof
wenzelm@10250:   assume xy: "x \<sim> y"
wenzelm@10250:   also from xy have "y \<sim> x" ..
wenzelm@10250:   finally show "x \<sim> x" .
wenzelm@10250: qed
wenzelm@10250: 
wenzelm@10250: 
wenzelm@10250: subsubsection {* Equivalence on function spaces *}
wenzelm@10250: 
wenzelm@10250: text {*
wenzelm@10250:  The @{text \<sim>} relation is lifted to function spaces.  It is
wenzelm@10250:  important to note that this is \emph{not} the direct product, but a
wenzelm@10250:  structural one corresponding to the congruence property.
wenzelm@10250: *}
wenzelm@10250: 
wenzelm@10250: defs (overloaded)
wenzelm@10250:   eqv_fun_def: "f \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y --> f x \<sim> g y"
wenzelm@10250: 
wenzelm@10250: lemma partial_equiv_funI [intro?]:
wenzelm@10250:     "(!!x y. x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y) ==> f \<sim> g"
wenzelm@10250:   by (unfold eqv_fun_def) blast
wenzelm@10250: 
wenzelm@10250: lemma partial_equiv_funD [dest?]:
wenzelm@10250:     "f \<sim> g ==> x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y"
wenzelm@10250:   by (unfold eqv_fun_def) blast
wenzelm@10250: 
wenzelm@10250: text {*
wenzelm@10250:  The class of partial equivalence relations is closed under function
wenzelm@10250:  spaces (in \emph{both} argument positions).
wenzelm@10250: *}
wenzelm@10250: 
wenzelm@10250: instance fun :: (partial_equiv, partial_equiv) partial_equiv
wenzelm@10250: proof intro_classes
wenzelm@10250:   fix f g h :: "'a::partial_equiv => 'b::partial_equiv"
wenzelm@10250:   assume fg: "f \<sim> g"
wenzelm@10250:   show "g \<sim> f"
wenzelm@10250:   proof
wenzelm@10250:     fix x y :: 'a
wenzelm@10250:     assume x: "x \<in> domain" and y: "y \<in> domain"
wenzelm@10250:     assume "x \<sim> y" hence "y \<sim> x" ..
wenzelm@10250:     with fg y x have "f y \<sim> g x" ..
wenzelm@10250:     thus "g x \<sim> f y" ..
wenzelm@10250:   qed
wenzelm@10250:   assume gh: "g \<sim> h"
wenzelm@10250:   show "f \<sim> h"
wenzelm@10250:   proof
wenzelm@10250:     fix x y :: 'a
wenzelm@10250:     assume x: "x \<in> domain" and y: "y \<in> domain" and "x \<sim> y"
wenzelm@10250:     with fg have "f x \<sim> g y" ..
wenzelm@10250:     also from y have "y \<sim> y" ..
wenzelm@10250:     with gh y y have "g y \<sim> h y" ..
wenzelm@10250:     finally show "f x \<sim> h y" .
wenzelm@10250:   qed
wenzelm@10250: qed
wenzelm@10250: 
wenzelm@10250: 
wenzelm@10250: subsubsection {* Total equivalence *}
wenzelm@10250: 
wenzelm@10250: text {*
wenzelm@10250:  The class of total equivalence relations on top of PERs.  It
wenzelm@10250:  coincides with the standard notion of equivalence, i.e.\
wenzelm@10250:  @{text "\<sim> :: 'a => 'a => bool"} is required to be reflexive, transitive
wenzelm@10250:  and symmetric.
wenzelm@10250: *}
wenzelm@10250: 
wenzelm@10250: axclass equiv < partial_equiv
wenzelm@10250:   eqv_refl [intro]: "x \<sim> x"
wenzelm@10250: 
wenzelm@10250: text {*
wenzelm@10250:  On total equivalences all elements are reflexive, and congruence
wenzelm@10250:  holds unconditionally.
wenzelm@10250: *}
wenzelm@10250: 
wenzelm@10250: theorem equiv_domain [intro]: "(x::'a::equiv) \<in> domain"
wenzelm@10250: proof
wenzelm@10250:   show "x \<sim> x" ..
wenzelm@10250: qed
wenzelm@10250: 
wenzelm@10250: theorem equiv_cong [dest?]: "f \<sim> g ==> x \<sim> y ==> f x \<sim> g (y::'a::equiv)"
wenzelm@10250: proof -
wenzelm@10250:   assume "f \<sim> g"
wenzelm@10250:   moreover have "x \<in> domain" ..
wenzelm@10250:   moreover have "y \<in> domain" ..
wenzelm@10250:   moreover assume "x \<sim> y"
wenzelm@10250:   ultimately show ?thesis ..
wenzelm@10250: qed
wenzelm@10250: 
wenzelm@10250: 
wenzelm@10250: subsection {* Quotient types *}
wenzelm@10250: 
wenzelm@10250: subsubsection {* General quotients and equivalence classes *}
wenzelm@10250: 
wenzelm@10250: text {*
wenzelm@10250:  The quotient type @{text "'a quot"} consists of all \emph{equivalence
wenzelm@10250:  classes} over elements of the base type @{typ 'a}.
wenzelm@10250: *}
wenzelm@10250: 
wenzelm@10250: typedef 'a quot = "{{x. a \<sim> x}| a::'a. True}"
wenzelm@10250:   by blast
wenzelm@10250: 
wenzelm@10250: lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
wenzelm@10250:   by (unfold quot_def) blast
wenzelm@10250: 
wenzelm@10250: lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
wenzelm@10250:   by (unfold quot_def) blast
wenzelm@10250: 
wenzelm@10250: text {*
wenzelm@10250:  \medskip Abstracted equivalence classes are the canonical
wenzelm@10250:  representation of elements of a quotient type.
wenzelm@10250: *}
wenzelm@10250: 
wenzelm@10250: constdefs
wenzelm@10250:   eqv_class :: "('a::partial_equiv) => 'a quot"    ("\<lfloor>_\<rfloor>")
wenzelm@10250:   "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
wenzelm@10250: 
wenzelm@10250: theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>"
wenzelm@10278: proof (cases A)
wenzelm@10278:   fix R assume R: "A = Abs_quot R"
wenzelm@10278:   assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast
wenzelm@10278:   with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
wenzelm@10278:   thus ?thesis by (unfold eqv_class_def)
wenzelm@10250: qed
wenzelm@10250: 
wenzelm@10250: lemma quot_cases [case_names rep, cases type: quot]:
wenzelm@10250:     "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
wenzelm@10250:   by (insert quot_rep) blast
wenzelm@10250: 
wenzelm@10250: 
wenzelm@10250: subsubsection {* Equality on quotients *}
wenzelm@10250: 
wenzelm@10250: text {*
wenzelm@10250:  Equality of canonical quotient elements corresponds to the original
wenzelm@10250:  relation as follows.
wenzelm@10250: *}
wenzelm@10250: 
wenzelm@10250: theorem eqv_class_eqI [intro]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
wenzelm@10250: proof -
wenzelm@10250:   assume ab: "a \<sim> b"
wenzelm@10250:   have "{x. a \<sim> x} = {x. b \<sim> x}"
wenzelm@10250:   proof (rule Collect_cong)
wenzelm@10250:     fix x show "(a \<sim> x) = (b \<sim> x)"
wenzelm@10250:     proof
wenzelm@10250:       from ab have "b \<sim> a" ..
wenzelm@10250:       also assume "a \<sim> x"
wenzelm@10250:       finally show "b \<sim> x" .
wenzelm@10250:     next
wenzelm@10250:       note ab
wenzelm@10250:       also assume "b \<sim> x"
wenzelm@10250:       finally show "a \<sim> x" .
wenzelm@10250:     qed
wenzelm@10250:   qed
wenzelm@10250:   thus ?thesis by (simp only: eqv_class_def)
wenzelm@10250: qed
wenzelm@10250: 
wenzelm@10250: theorem eqv_class_eqD' [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<in> domain ==> a \<sim> b"  (* FIXME [dest] would cause trouble with blast due to overloading *)
wenzelm@10250: proof (unfold eqv_class_def)
wenzelm@10250:   assume "Abs_quot {x. a \<sim> x} = Abs_quot {x. b \<sim> x}"
wenzelm@10250:   hence "{x. a \<sim> x} = {x. b \<sim> x}" by (simp only: Abs_quot_inject quotI)
wenzelm@10250:   moreover assume "a \<in> domain" hence "a \<sim> a" ..
wenzelm@10250:   ultimately have "a \<in> {x. b \<sim> x}" by blast
wenzelm@10250:   hence "b \<sim> a" by blast
wenzelm@10250:   thus "a \<sim> b" ..
wenzelm@10250: qed
wenzelm@10250: 
wenzelm@10250: theorem eqv_class_eqD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<sim> (b::'a::equiv)"  (* FIXME [dest] would cause trouble with blast due to overloading *)
wenzelm@10250: proof (rule eqv_class_eqD')
wenzelm@10250:   show "a \<in> domain" ..
wenzelm@10250: qed
wenzelm@10250: 
wenzelm@10250: lemma eqv_class_eq' [simp]: "a \<in> domain ==> (\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
wenzelm@10250:   by (insert eqv_class_eqI eqv_class_eqD') blast
wenzelm@10250: 
wenzelm@10250: lemma eqv_class_eq [simp]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> (b::'a::equiv))"
wenzelm@10250:   by (insert eqv_class_eqI eqv_class_eqD) blast
wenzelm@10250: 
wenzelm@10250: 
wenzelm@10250: subsubsection {* Picking representing elements *}
wenzelm@10250: 
wenzelm@10250: constdefs
wenzelm@10250:   pick :: "'a::partial_equiv quot => 'a"
wenzelm@10250:   "pick A == SOME a. A = \<lfloor>a\<rfloor>"
wenzelm@10250: 
wenzelm@10250: theorem pick_eqv' [intro?, simp]: "a \<in> domain ==> pick \<lfloor>a\<rfloor> \<sim> a" (* FIXME [intro] !? *)
wenzelm@10250: proof (unfold pick_def)
wenzelm@10250:   assume a: "a \<in> domain"
wenzelm@10250:   show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"
wenzelm@10250:   proof (rule someI2)
wenzelm@10250:     show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
wenzelm@10250:     fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
wenzelm@10250:     hence "a \<sim> x" ..
wenzelm@10250:     thus "x \<sim> a" ..
wenzelm@10250:   qed
wenzelm@10250: qed
wenzelm@10250: 
wenzelm@10250: theorem pick_eqv [intro, simp]: "pick \<lfloor>a\<rfloor> \<sim> (a::'a::equiv)"
wenzelm@10250: proof (rule pick_eqv')
wenzelm@10250:   show "a \<in> domain" ..
wenzelm@10250: qed
wenzelm@10250: 
wenzelm@10278: theorem pick_inverse: "\<lfloor>pick A\<rfloor> = (A::'a::equiv quot)"
wenzelm@10250: proof (cases A)
wenzelm@10250:   fix a assume a: "A = \<lfloor>a\<rfloor>"
wenzelm@10278:   hence "pick A \<sim> a" by simp
wenzelm@10250:   hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" by simp
wenzelm@10250:   with a show ?thesis by simp
wenzelm@10250: qed
wenzelm@10250: 
wenzelm@10250: end