wenzelm@35100: (*  Title:      HOL/Library/Quotient_Type.thy
wenzelm@10483:     Author:     Markus Wenzel, TU Muenchen
wenzelm@10250: *)
wenzelm@10250: 
wenzelm@14706: header {* Quotient types *}
wenzelm@10250: 
wenzelm@35100: theory Quotient_Type
haftmann@30738: imports Main
nipkow@15131: begin
wenzelm@10250: 
wenzelm@10250: text {*
wenzelm@10285:  We introduce the notion of quotient types over equivalence relations
haftmann@22390:  via 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: 
haftmann@29608: class eqv =
haftmann@25062:   fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<sim>" 50)
wenzelm@10250: 
haftmann@22390: class equiv = eqv +
haftmann@25062:   assumes equiv_refl [intro]: "x \<sim> x"
haftmann@25062:   assumes equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z"
haftmann@25062:   assumes equiv_sym [sym]: "x \<sim> y \<Longrightarrow> 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@23373:   assume "\<not> (x \<sim> y)" then show "\<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@23373:   assume "\<not> (x \<sim> y)" and "y \<sim> z"
wenzelm@10477:   show "\<not> (x \<sim> z)"
wenzelm@10477:   proof
wenzelm@10477:     assume "x \<sim> z"
wenzelm@23373:     also from `y \<sim> z` have "z \<sim> y" ..
wenzelm@10477:     finally have "x \<sim> y" .
wenzelm@23373:     with `\<not> (x \<sim> y)` show 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@23373:   assume "\<not> (y \<sim> z)" then have "\<not> (z \<sim> y)" ..
wenzelm@23373:   also assume "x \<sim> y" then have "y \<sim> x" ..
wenzelm@23373:   finally have "\<not> (z \<sim> x)" . then show "(\<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@45694: definition "quot = {{x. a \<sim> x} | a::'a::eqv. True}"
wenzelm@45694: 
wenzelm@49834: typedef 'a quot = "quot :: 'a::eqv set set"
wenzelm@45694:   unfolding quot_def by blast
wenzelm@10250: 
wenzelm@10250: lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
wenzelm@18730:   unfolding quot_def by blast
wenzelm@10250: 
wenzelm@10250: lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
wenzelm@18730:   unfolding quot_def by 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@19086: definition
wenzelm@21404:   "class" :: "'a::equiv => 'a quot"  ("\<lfloor>_\<rfloor>") where
wenzelm@19086:   "\<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@23373:   assume "R \<in> quot" then have "\<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@23373:   then show ?thesis unfolding class_def .
wenzelm@10250: qed
wenzelm@10250: 
wenzelm@10311: lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
wenzelm@18730:   using quot_exhaust by 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@23373:     then have "b \<sim> a" by blast
wenzelm@23373:     then show ?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@23373:     then show ?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@19086: definition
wenzelm@21404:   pick :: "'a::equiv quot => 'a" where
wenzelm@19086:   "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@23373:     then have "a \<sim> x" .. then show "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@23373:   then have "pick A \<sim> a" by (simp only: pick_equiv)
wenzelm@23373:   then have "\<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@18372:   assumes eq: "!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)"
wenzelm@18372:     and cong: "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
wenzelm@18372:       ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
wenzelm@18372:     and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
wenzelm@18372:   shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
wenzelm@10473: proof -
wenzelm@18372:   from eq and P have "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@23373:     show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" by (rule P)
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@18372:   assumes "!!X Y. f X Y == g (pick X) (pick Y)"
wenzelm@18372:     and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
wenzelm@18372:   shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
wenzelm@23394:   using assms and TrueI
wenzelm@18372:   by (rule quot_cond_function)
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"
wenzelm@18372:   by (rule quot_function) (simp_all only: quot_equality)
bauerg@10499: 
wenzelm@10250: end