equal
deleted
inserted
replaced
72 text {* |
72 text {* |
73 \medskip Abstracted equivalence classes are the canonical |
73 \medskip Abstracted equivalence classes are the canonical |
74 representation of elements of a quotient type. |
74 representation of elements of a quotient type. |
75 *} |
75 *} |
76 |
76 |
77 constdefs |
77 definition |
78 "class" :: "'a::equiv => 'a quot" ("\<lfloor>_\<rfloor>") |
78 "class" :: "'a::equiv => 'a quot" ("\<lfloor>_\<rfloor>") |
79 "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}" |
79 "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}" |
80 |
80 |
81 theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>" |
81 theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>" |
82 proof (cases A) |
82 proof (cases A) |
83 fix R assume R: "A = Abs_quot R" |
83 fix R assume R: "A = Abs_quot R" |
84 assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast |
84 assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast |
131 qed |
131 qed |
132 |
132 |
133 |
133 |
134 subsection {* Picking representing elements *} |
134 subsection {* Picking representing elements *} |
135 |
135 |
136 constdefs |
136 definition |
137 pick :: "'a::equiv quot => 'a" |
137 pick :: "'a::equiv quot => 'a" |
138 "pick A == SOME a. A = \<lfloor>a\<rfloor>" |
138 "pick A = (SOME a. A = \<lfloor>a\<rfloor>)" |
139 |
139 |
140 theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a" |
140 theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a" |
141 proof (unfold pick_def) |
141 proof (unfold pick_def) |
142 show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a" |
142 show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a" |
143 proof (rule someI2) |
143 proof (rule someI2) |