src/HOL/Library/Quotient_Type.thy
 author huffman Fri Mar 30 12:32:35 2012 +0200 (2012-03-30) changeset 47220 52426c62b5d0 parent 45694 4a8743618257 child 49834 b27bbb021df1 permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
1 (*  Title:      HOL/Library/Quotient_Type.thy
2     Author:     Markus Wenzel, TU Muenchen
3 *)
5 header {* Quotient types *}
7 theory Quotient_Type
8 imports Main
9 begin
11 text {*
12  We introduce the notion of quotient types over equivalence relations
13  via type classes.
14 *}
16 subsection {* Equivalence relations and quotient types *}
18 text {*
19  \medskip Type class @{text equiv} models equivalence relations @{text
20  "\<sim> :: 'a => 'a => bool"}.
21 *}
23 class eqv =
24   fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<sim>" 50)
26 class equiv = eqv +
27   assumes equiv_refl [intro]: "x \<sim> x"
28   assumes equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z"
29   assumes equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x"
31 lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
32 proof -
33   assume "\<not> (x \<sim> y)" then show "\<not> (y \<sim> x)"
34     by (rule contrapos_nn) (rule equiv_sym)
35 qed
37 lemma not_equiv_trans1 [trans]: "\<not> (x \<sim> y) ==> y \<sim> z ==> \<not> (x \<sim> (z::'a::equiv))"
38 proof -
39   assume "\<not> (x \<sim> y)" and "y \<sim> z"
40   show "\<not> (x \<sim> z)"
41   proof
42     assume "x \<sim> z"
43     also from y \<sim> z have "z \<sim> y" ..
44     finally have "x \<sim> y" .
45     with \<not> (x \<sim> y) show False by contradiction
46   qed
47 qed
49 lemma not_equiv_trans2 [trans]: "x \<sim> y ==> \<not> (y \<sim> z) ==> \<not> (x \<sim> (z::'a::equiv))"
50 proof -
51   assume "\<not> (y \<sim> z)" then have "\<not> (z \<sim> y)" ..
52   also assume "x \<sim> y" then have "y \<sim> x" ..
53   finally have "\<not> (z \<sim> x)" . then show "(\<not> x \<sim> z)" ..
54 qed
56 text {*
57  \medskip The quotient type @{text "'a quot"} consists of all
58  \emph{equivalence classes} over elements of the base type @{typ 'a}.
59 *}
61 definition "quot = {{x. a \<sim> x} | a::'a::eqv. True}"
63 typedef (open) 'a quot = "quot :: 'a::eqv set set"
64   unfolding quot_def by blast
66 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
67   unfolding quot_def by blast
69 lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
70   unfolding quot_def by blast
72 text {*
73  \medskip Abstracted equivalence classes are the canonical
74  representation of elements of a quotient type.
75 *}
77 definition
78   "class" :: "'a::equiv => 'a quot"  ("\<lfloor>_\<rfloor>") where
79   "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
81 theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
82 proof (cases A)
83   fix R assume R: "A = Abs_quot R"
84   assume "R \<in> quot" then have "\<exists>a. R = {x. a \<sim> x}" by blast
85   with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
86   then show ?thesis unfolding class_def .
87 qed
89 lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
90   using quot_exhaust by blast
93 subsection {* Equality on quotients *}
95 text {*
96  Equality of canonical quotient elements coincides with the original
97  relation.
98 *}
100 theorem quot_equality [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
101 proof
102   assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
103   show "a \<sim> b"
104   proof -
105     from eq have "{x. a \<sim> x} = {x. b \<sim> x}"
106       by (simp only: class_def Abs_quot_inject quotI)
107     moreover have "a \<sim> a" ..
108     ultimately have "a \<in> {x. b \<sim> x}" by blast
109     then have "b \<sim> a" by blast
110     then show ?thesis ..
111   qed
112 next
113   assume ab: "a \<sim> b"
114   show "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
115   proof -
116     have "{x. a \<sim> x} = {x. b \<sim> x}"
117     proof (rule Collect_cong)
118       fix x show "(a \<sim> x) = (b \<sim> x)"
119       proof
120         from ab have "b \<sim> a" ..
121         also assume "a \<sim> x"
122         finally show "b \<sim> x" .
123       next
124         note ab
125         also assume "b \<sim> x"
126         finally show "a \<sim> x" .
127       qed
128     qed
129     then show ?thesis by (simp only: class_def)
130   qed
131 qed
134 subsection {* Picking representing elements *}
136 definition
137   pick :: "'a::equiv quot => 'a" where
138   "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
140 theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"
141 proof (unfold pick_def)
142   show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"
143   proof (rule someI2)
144     show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
145     fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
146     then have "a \<sim> x" .. then show "x \<sim> a" ..
147   qed
148 qed
150 theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A"
151 proof (cases A)
152   fix a assume a: "A = \<lfloor>a\<rfloor>"
153   then have "pick A \<sim> a" by (simp only: pick_equiv)
154   then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..
155   with a show ?thesis by simp
156 qed
158 text {*
159  \medskip The following rules support canonical function definitions
160  on quotient types (with up to two arguments).  Note that the
161  stripped-down version without additional conditions is sufficient
162  most of the time.
163 *}
165 theorem quot_cond_function:
166   assumes eq: "!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)"
167     and cong: "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
168       ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
169     and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
170   shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
171 proof -
172   from eq and P have "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
173   also have "... = g a b"
174   proof (rule cong)
175     show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" ..
176     moreover
177     show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" ..
178     moreover
179     show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" by (rule P)
180     ultimately show "P \<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> \<lfloor>pick \<lfloor>b\<rfloor>\<rfloor>" by (simp only:)
181   qed
182   finally show ?thesis .
183 qed
185 theorem quot_function:
186   assumes "!!X Y. f X Y == g (pick X) (pick Y)"
187     and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
188   shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
189   using assms and TrueI
190   by (rule quot_cond_function)
192 theorem quot_function':
193   "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
194     (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==>
195     f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
196   by (rule quot_function) (simp_all only: quot_equality)
198 end