equal
deleted
inserted
replaced
42 reflexive elements. Due to symmetry and transitivity this |
42 reflexive elements. Due to symmetry and transitivity this |
43 characterizes exactly those elements that are connected with |
43 characterizes exactly those elements that are connected with |
44 \emph{any} other one. |
44 \emph{any} other one. |
45 *} |
45 *} |
46 |
46 |
47 constdefs |
47 definition |
48 domain :: "'a::partial_equiv set" |
48 "domain" :: "'a::partial_equiv set" |
49 "domain == {x. x \<sim> x}" |
49 "domain = {x. x \<sim> x}" |
50 |
50 |
51 lemma domainI [intro]: "x \<sim> x ==> x \<in> domain" |
51 lemma domainI [intro]: "x \<sim> x ==> x \<in> domain" |
52 by (unfold domain_def) blast |
52 by (unfold domain_def) blast |
53 |
53 |
54 lemma domainD [dest]: "x \<in> domain ==> x \<sim> x" |
54 lemma domainD [dest]: "x \<in> domain ==> x \<sim> x" |
162 text {* |
162 text {* |
163 \medskip Abstracted equivalence classes are the canonical |
163 \medskip Abstracted equivalence classes are the canonical |
164 representation of elements of a quotient type. |
164 representation of elements of a quotient type. |
165 *} |
165 *} |
166 |
166 |
167 constdefs |
167 definition |
168 eqv_class :: "('a::partial_equiv) => 'a quot" ("\<lfloor>_\<rfloor>") |
168 eqv_class :: "('a::partial_equiv) => 'a quot" ("\<lfloor>_\<rfloor>") |
169 "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}" |
169 "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}" |
170 |
170 |
171 theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>" |
171 theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>" |
172 proof (cases A) |
172 proof (cases A) |
173 fix R assume R: "A = Abs_quot R" |
173 fix R assume R: "A = Abs_quot R" |
174 assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast |
174 assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast |
229 by (insert eqv_class_eqI eqv_class_eqD) blast |
229 by (insert eqv_class_eqI eqv_class_eqD) blast |
230 |
230 |
231 |
231 |
232 subsection {* Picking representing elements *} |
232 subsection {* Picking representing elements *} |
233 |
233 |
234 constdefs |
234 definition |
235 pick :: "'a::partial_equiv quot => 'a" |
235 pick :: "'a::partial_equiv quot => 'a" |
236 "pick A == SOME a. A = \<lfloor>a\<rfloor>" |
236 "pick A = (SOME a. A = \<lfloor>a\<rfloor>)" |
237 |
237 |
238 theorem pick_eqv' [intro?, simp]: "a \<in> domain ==> pick \<lfloor>a\<rfloor> \<sim> a" |
238 theorem pick_eqv' [intro?, simp]: "a \<in> domain ==> pick \<lfloor>a\<rfloor> \<sim> a" |
239 proof (unfold pick_def) |
239 proof (unfold pick_def) |
240 assume a: "a \<in> domain" |
240 assume a: "a \<in> domain" |
241 show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a" |
241 show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a" |