src/HOL/Equiv_Relations.thy
changeset 18493 343da052b961
parent 18490 434e34392c40
child 19323 ec5cd5b1804c
equal deleted inserted replaced
18492:b0fe60800623 18493:343da052b961
    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