equal
deleted
inserted
replaced
88 |
88 |
89 theorem eq_equiv_class_iff: |
89 theorem eq_equiv_class_iff: |
90 "equiv A r ==> x \<in> A ==> y \<in> A ==> (r``{x} = r``{y}) = ((x, y) \<in> r)" |
90 "equiv A r ==> x \<in> A ==> y \<in> A ==> (r``{x} = r``{y}) = ((x, y) \<in> r)" |
91 by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type) |
91 by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type) |
92 |
92 |
93 lemma eq_equiv_class_iff2: |
|
94 "\<lbrakk> equiv A r; x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> ({x}//r = {y}//r) = ((x,y) : r)" |
|
95 by(simp add:quotient_def eq_equiv_class_iff) |
|
96 |
|
97 |
93 |
98 subsection {* Quotients *} |
94 subsection {* Quotients *} |
99 |
95 |
100 constdefs |
96 constdefs |
101 quotient :: "['a set, ('a*'a) set] => 'a set set" (infixl "'/'/" 90) |
97 quotient :: "['a set, ('a*'a) set] => 'a set set" (infixl "'/'/" 90) |
133 apply (rule iffI) |
129 apply (rule iffI) |
134 prefer 2 apply (blast del: equalityI intro: quotient_eqI) |
130 prefer 2 apply (blast del: equalityI intro: quotient_eqI) |
135 apply (clarify elim!: quotientE) |
131 apply (clarify elim!: quotientE) |
136 apply (unfold equiv_def sym_def trans_def, blast) |
132 apply (unfold equiv_def sym_def trans_def, blast) |
137 done |
133 done |
|
134 |
|
135 lemma eq_equiv_class_iff2: |
|
136 "\<lbrakk> equiv A r; x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> ({x}//r = {y}//r) = ((x,y) : r)" |
|
137 by(simp add:quotient_def eq_equiv_class_iff) |
138 |
138 |
139 |
139 |
140 lemma quotient_empty [simp]: "{}//r = {}" |
140 lemma quotient_empty [simp]: "{}//r = {}" |
141 by(simp add: quotient_def) |
141 by(simp add: quotient_def) |
142 |
142 |