src/HOL/Equiv_Relations.thy
changeset 15302 a643fcbc3468
parent 15300 7dd5853a4812
child 15303 eedbb8d22ca2
     1.1 --- a/src/HOL/Equiv_Relations.thy	Fri Nov 19 17:52:07 2004 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Sun Nov 21 12:52:03 2004 +0100
     1.3 @@ -143,6 +143,15 @@
     1.4  by(simp add: quotient_def)
     1.5  
     1.6  
     1.7 +lemma singleton_quotient: "{x}//r = {r `` {x}}"
     1.8 +by(simp add:quotient_def)
     1.9 +
    1.10 +lemma quotient_diff1:
    1.11 +  "\<lbrakk> inj_on (%a. {a}//r) A; a \<in> A \<rbrakk> \<Longrightarrow> (A - {a})//r = A//r - {a}//r"
    1.12 +apply(simp add:quotient_def inj_on_def)
    1.13 +apply blast
    1.14 +done
    1.15 +
    1.16  subsection {* Defining unary operations upon equivalence classes *}
    1.17  
    1.18  text{*A congruence-preserving function*}