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