
wenzelm@10250: (*  Title:      HOL/Library/Quotient.thy
wenzelm@10250:     ID:         $Id$
wenzelm@10483:     Author:     Markus Wenzel, TU Muenchen
wenzelm@10250: *)
wenzelm@10250: 
wenzelm@14706: header {* Quotient types *}
wenzelm@10250: 
nipkow@15131: theory Quotient
nipkow@15131: import Main
nipkow@15131: begin
wenzelm@10250: 
wenzelm@10250: text {*
wenzelm@10285:  We introduce the notion of quotient types over equivalence relations
wenzelm@10285:  via axiomatic type classes.
wenzelm@10250: *}
wenzelm@10250: 
wenzelm@10285: subsection {* Equivalence relations and quotient types *}
wenzelm@10250: 
wenzelm@10250: text {*
wenzelm@10390:  \medskip Type class @{text equiv} models equivalence relations @{text
wenzelm@10390:  "\<sim> :: 'a => 'a => bool"}.
wenzelm@10250: *}
wenzelm@10250: 
wenzelm@12338: axclass eqv \<subseteq> type
wenzelm@10285: consts
wenzelm@10285:   eqv :: "('a::eqv) => 'a => bool"    (infixl "\<sim>" 50)
wenzelm@10250: 
wenzelm@11099: axclass equiv \<subseteq> eqv
wenzelm@10333:   equiv_refl [intro]: "x \<sim> x"
wenzelm@10333:   equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
wenzelm@12371:   equiv_sym [sym]: "x \<sim> y ==> y \<sim> x"
wenzelm@10250: 
wenzelm@12371: lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
wenzelm@10477: proof -
wenzelm@10477:   assume "\<not> (x \<sim> y)" thus "\<not> (y \<sim> x)"
wenzelm@10477:     by (rule contrapos_nn) (rule equiv_sym)
wenzelm@10477: qed
wenzelm@10477: 
wenzelm@10477: lemma not_equiv_trans1 [trans]: "\<not> (x \<sim> y) ==> y \<sim> z ==> \<not> (x \<sim> (z::'a::equiv))"
wenzelm@10477: proof -
wenzelm@10477:   assume "\<not> (x \<sim> y)" and yz: "y \<sim> z"
wenzelm@10477:   show "\<not> (x \<sim> z)"
wenzelm@10477:   proof
wenzelm@10477:     assume "x \<sim> z"
wenzelm@10477:     also from yz have "z \<sim> y" ..
wenzelm@10477:     finally have "x \<sim> y" .
wenzelm@10477:     thus False by contradiction
wenzelm@10477:   qed
wenzelm@10477: qed
wenzelm@10477: 
wenzelm@10477: lemma not_equiv_trans2 [trans]: "x \<sim> y ==> \<not> (y \<sim> z) ==> \<not> (x \<sim> (z::'a::equiv))"
wenzelm@10477: proof -
wenzelm@10477:   assume "\<not> (y \<sim> z)" hence "\<not> (z \<sim> y)" ..
wenzelm@10477:   also assume "x \<sim> y" hence "y \<sim> x" ..
wenzelm@10477:   finally have "\<not> (z \<sim> x)" . thus "(\<not> x \<sim> z)" ..
wenzelm@10477: qed
wenzelm@10477: 
wenzelm@10250: text {*
wenzelm@10285:  \medskip The quotient type @{text "'a quot"} consists of all
wenzelm@10285:  \emph{equivalence classes} over elements of the base type @{typ 'a}.
wenzelm@10250: *}
wenzelm@10250: 
wenzelm@10392: typedef 'a quot = "{{x. a \<sim> x} | a::'a::eqv. 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@10551:   class :: "'a::equiv => 'a quot"    ("\<lfloor>_\<rfloor>")
wenzelm@10250:   "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
wenzelm@10250: 
wenzelm@10311: theorem quot_exhaust: "\<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@10551:   thus ?thesis by (unfold class_def)
wenzelm@10250: qed
wenzelm@10250: 
wenzelm@10311: lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
wenzelm@10311:   by (insert quot_exhaust) blast
wenzelm@10250: 
wenzelm@10250: 
wenzelm@10285: subsection {* Equality on quotients *}
wenzelm@10250: 
wenzelm@10250: text {*
wenzelm@10286:  Equality of canonical quotient elements coincides with the original
wenzelm@10286:  relation.
wenzelm@10250: *}
wenzelm@10250: 
wenzelm@12371: theorem quot_equality [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
wenzelm@10285: proof
wenzelm@10285:   assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
wenzelm@10285:   show "a \<sim> b"
wenzelm@10285:   proof -
wenzelm@10285:     from eq have "{x. a \<sim> x} = {x. b \<sim> x}"
wenzelm@10551:       by (simp only: class_def Abs_quot_inject quotI)
wenzelm@10285:     moreover have "a \<sim> a" ..
wenzelm@10285:     ultimately have "a \<in> {x. b \<sim> x}" by blast
wenzelm@10285:     hence "b \<sim> a" by blast
wenzelm@10285:     thus ?thesis ..
wenzelm@10285:   qed
wenzelm@10285: next
wenzelm@10250:   assume ab: "a \<sim> b"
wenzelm@10285:   show "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
wenzelm@10285:   proof -
wenzelm@10285:     have "{x. a \<sim> x} = {x. b \<sim> x}"
wenzelm@10285:     proof (rule Collect_cong)
wenzelm@10285:       fix x show "(a \<sim> x) = (b \<sim> x)"
wenzelm@10285:       proof
wenzelm@10285:         from ab have "b \<sim> a" ..
wenzelm@10285:         also assume "a \<sim> x"
wenzelm@10285:         finally show "b \<sim> x" .
wenzelm@10285:       next
wenzelm@10285:         note ab
wenzelm@10285:         also assume "b \<sim> x"
wenzelm@10285:         finally show "a \<sim> x" .
wenzelm@10285:       qed
wenzelm@10250:     qed
wenzelm@10551:     thus ?thesis by (simp only: class_def)
wenzelm@10250:   qed
wenzelm@10250: qed
wenzelm@10250: 
wenzelm@10250: 
wenzelm@10285: subsection {* Picking representing elements *}
wenzelm@10250: 
wenzelm@10250: constdefs
wenzelm@10285:   pick :: "'a::equiv quot => 'a"
wenzelm@10250:   "pick A == SOME a. A = \<lfloor>a\<rfloor>"
wenzelm@10250: 
wenzelm@10285: theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"
wenzelm@10250: proof (unfold pick_def)
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@10285:     hence "a \<sim> x" .. thus "x \<sim> a" ..
wenzelm@10250:   qed
wenzelm@10250: qed
wenzelm@10250: 
wenzelm@10483: theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A"
wenzelm@10250: proof (cases A)
wenzelm@10250:   fix a assume a: "A = \<lfloor>a\<rfloor>"
wenzelm@10285:   hence "pick A \<sim> a" by (simp only: pick_equiv)
wenzelm@10285:   hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..
wenzelm@10250:   with a show ?thesis by simp
wenzelm@10250: qed
wenzelm@10250: 
wenzelm@10285: text {*
wenzelm@10285:  \medskip The following rules support canonical function definitions
wenzelm@10483:  on quotient types (with up to two arguments).  Note that the
wenzelm@10483:  stripped-down version without additional conditions is sufficient
wenzelm@10483:  most of the time.
wenzelm@10285: *}
wenzelm@10285: 
wenzelm@10483: theorem quot_cond_function:
wenzelm@10491:   "(!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)) ==>
wenzelm@10491:     (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
wenzelm@10491:       ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>
wenzelm@10491:     P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
wenzelm@10491:   (is "PROP ?eq ==> PROP ?cong ==> _ ==> _")
wenzelm@10473: proof -
wenzelm@10491:   assume cong: "PROP ?cong"
wenzelm@10491:   assume "PROP ?eq" and "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
wenzelm@10491:   hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
wenzelm@10505:   also have "... = g a b"
wenzelm@10491:   proof (rule cong)
wenzelm@10483:     show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" ..
wenzelm@10483:     moreover
wenzelm@10483:     show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" ..
wenzelm@10491:     moreover
wenzelm@10491:     show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" .
wenzelm@10491:     ultimately show "P \<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> \<lfloor>pick \<lfloor>b\<rfloor>\<rfloor>" by (simp only:)
wenzelm@10285:   qed
wenzelm@10285:   finally show ?thesis .
wenzelm@10285: qed
wenzelm@10285: 
wenzelm@10483: theorem quot_function:
wenzelm@10473:   "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
wenzelm@10483:     (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>
wenzelm@10473:     f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
wenzelm@10473: proof -
wenzelm@11549:   case rule_context from this TrueI
wenzelm@10483:   show ?thesis by (rule quot_cond_function)
wenzelm@10285: qed
wenzelm@10285: 
bauerg@10499: theorem quot_function':
bauerg@10499:   "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
bauerg@10499:     (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==>
bauerg@10499:     f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
bauerg@10499:   by  (rule quot_function) (simp only: quot_equality)+
bauerg@10499: 
wenzelm@10250: end




