equal
deleted
inserted
replaced
52 |
52 |
53 constdefs |
53 constdefs |
54 equivalence_class :: "'a::equiv => 'a quot" ("\<lfloor>_\<rfloor>") |
54 equivalence_class :: "'a::equiv => 'a quot" ("\<lfloor>_\<rfloor>") |
55 "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}" |
55 "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}" |
56 |
56 |
57 theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>" |
57 theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>" |
58 proof (cases A) |
58 proof (cases A) |
59 fix R assume R: "A = Abs_quot R" |
59 fix R assume R: "A = Abs_quot R" |
60 assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast |
60 assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast |
61 with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast |
61 with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast |
62 thus ?thesis by (unfold equivalence_class_def) |
62 thus ?thesis by (unfold equivalence_class_def) |
63 qed |
63 qed |
64 |
64 |
65 lemma quot_cases [case_names rep, cases type: quot]: |
65 lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C" |
66 "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C" |
66 by (insert quot_exhaust) blast |
67 by (insert quot_rep) blast |
|
68 |
67 |
69 |
68 |
70 subsection {* Equality on quotients *} |
69 subsection {* Equality on quotients *} |
71 |
70 |
72 text {* |
71 text {* |