src/HOL/Library/Quotient.thy
changeset 10477 c21bee84cefe
parent 10473 4f15b844fea6
child 10483 eb93ace45a6e
     1.1 --- a/src/HOL/Library/Quotient.thy	Thu Nov 16 19:01:39 2000 +0100
     1.2 +++ b/src/HOL/Library/Quotient.thy	Thu Nov 16 19:03:26 2000 +0100
     1.3 @@ -31,6 +31,31 @@
     1.4    equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
     1.5    equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
     1.6  
     1.7 +lemma not_equiv_sym [elim?]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
     1.8 +proof -
     1.9 +  assume "\<not> (x \<sim> y)" thus "\<not> (y \<sim> x)"
    1.10 +    by (rule contrapos_nn) (rule equiv_sym)
    1.11 +qed
    1.12 +
    1.13 +lemma not_equiv_trans1 [trans]: "\<not> (x \<sim> y) ==> y \<sim> z ==> \<not> (x \<sim> (z::'a::equiv))"
    1.14 +proof -
    1.15 +  assume "\<not> (x \<sim> y)" and yz: "y \<sim> z"
    1.16 +  show "\<not> (x \<sim> z)"
    1.17 +  proof
    1.18 +    assume "x \<sim> z"
    1.19 +    also from yz have "z \<sim> y" ..
    1.20 +    finally have "x \<sim> y" .
    1.21 +    thus False by contradiction
    1.22 +  qed
    1.23 +qed
    1.24 +
    1.25 +lemma not_equiv_trans2 [trans]: "x \<sim> y ==> \<not> (y \<sim> z) ==> \<not> (x \<sim> (z::'a::equiv))"
    1.26 +proof -
    1.27 +  assume "\<not> (y \<sim> z)" hence "\<not> (z \<sim> y)" ..
    1.28 +  also assume "x \<sim> y" hence "y \<sim> x" ..
    1.29 +  finally have "\<not> (z \<sim> x)" . thus "(\<not> x \<sim> z)" ..
    1.30 +qed
    1.31 +
    1.32  text {*
    1.33   \medskip The quotient type @{text "'a quot"} consists of all
    1.34   \emph{equivalence classes} over elements of the base type @{typ 'a}.
    1.35 @@ -73,7 +98,7 @@
    1.36   relation.
    1.37  *}
    1.38  
    1.39 -theorem equivalence_class_iff [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
    1.40 +theorem quot_equality: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
    1.41  proof
    1.42    assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
    1.43    show "a \<sim> b"
    1.44 @@ -106,6 +131,18 @@
    1.45    qed
    1.46  qed
    1.47  
    1.48 +lemma quot_equalI [intro?]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
    1.49 +  by (simp only: quot_equality)
    1.50 +
    1.51 +lemma quot_equalD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<sim> b"
    1.52 +  by (simp only: quot_equality)
    1.53 +
    1.54 +lemma quot_not_equalI [intro?]: "\<not> (a \<sim> b) ==> \<lfloor>a\<rfloor> \<noteq> \<lfloor>b\<rfloor>"
    1.55 +  by (simp add: quot_equality)
    1.56 +
    1.57 +lemma quot_not_equalD [dest?]: "\<lfloor>a\<rfloor> \<noteq> \<lfloor>b\<rfloor> ==> \<not> (a \<sim> b)"
    1.58 +  by (simp add: quot_equality)
    1.59 +
    1.60  
    1.61  subsection {* Picking representing elements *}
    1.62