equal
deleted
inserted
replaced
62 |
62 |
63 typedef 'a quot = "{{x. a \<sim> x} | a::'a::eqv. True}" |
63 typedef 'a quot = "{{x. a \<sim> x} | a::'a::eqv. True}" |
64 by blast |
64 by blast |
65 |
65 |
66 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot" |
66 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot" |
67 by (unfold quot_def) blast |
67 unfolding quot_def by blast |
68 |
68 |
69 lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C" |
69 lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C" |
70 by (unfold quot_def) blast |
70 unfolding quot_def by blast |
71 |
71 |
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 *} |
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 |
85 with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast |
85 with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast |
86 thus ?thesis by (unfold class_def) |
86 thus ?thesis unfolding class_def . |
87 qed |
87 qed |
88 |
88 |
89 lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C" |
89 lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C" |
90 by (insert quot_exhaust) blast |
90 using quot_exhaust by blast |
91 |
91 |
92 |
92 |
93 subsection {* Equality on quotients *} |
93 subsection {* Equality on quotients *} |
94 |
94 |
95 text {* |
95 text {* |