# HG changeset patch # User wenzelm # Date 974397806 -3600 # Node ID c21bee84cefecd16517bd06e25bd0116c26ab182 # Parent dbc181a3270260842ca8f4663cb534a99951d203 added not_equiv_sym, not_equiv_trans1/2; tuned; diff -r dbc181a32702 -r c21bee84cefe src/HOL/Library/Quotient.thy --- a/src/HOL/Library/Quotient.thy Thu Nov 16 19:01:39 2000 +0100 +++ b/src/HOL/Library/Quotient.thy Thu Nov 16 19:03:26 2000 +0100 @@ -31,6 +31,31 @@ equiv_trans [trans]: "x \ y ==> y \ z ==> x \ z" equiv_sym [elim?]: "x \ y ==> y \ x" +lemma not_equiv_sym [elim?]: "\ (x \ y) ==> \ (y \ (x::'a::equiv))" +proof - + assume "\ (x \ y)" thus "\ (y \ x)" + by (rule contrapos_nn) (rule equiv_sym) +qed + +lemma not_equiv_trans1 [trans]: "\ (x \ y) ==> y \ z ==> \ (x \ (z::'a::equiv))" +proof - + assume "\ (x \ y)" and yz: "y \ z" + show "\ (x \ z)" + proof + assume "x \ z" + also from yz have "z \ y" .. + finally have "x \ y" . + thus False by contradiction + qed +qed + +lemma not_equiv_trans2 [trans]: "x \ y ==> \ (y \ z) ==> \ (x \ (z::'a::equiv))" +proof - + assume "\ (y \ z)" hence "\ (z \ y)" .. + also assume "x \ y" hence "y \ x" .. + finally have "\ (z \ x)" . thus "(\ x \ z)" .. +qed + text {* \medskip The quotient type @{text "'a quot"} consists of all \emph{equivalence classes} over elements of the base type @{typ 'a}. @@ -73,7 +98,7 @@ relation. *} -theorem equivalence_class_iff [iff?]: "(\a\ = \b\) = (a \ b)" +theorem quot_equality: "(\a\ = \b\) = (a \ b)" proof assume eq: "\a\ = \b\" show "a \ b" @@ -106,6 +131,18 @@ qed qed +lemma quot_equalI [intro?]: "a \ b ==> \a\ = \b\" + by (simp only: quot_equality) + +lemma quot_equalD [dest?]: "\a\ = \b\ ==> a \ b" + by (simp only: quot_equality) + +lemma quot_not_equalI [intro?]: "\ (a \ b) ==> \a\ \ \b\" + by (simp add: quot_equality) + +lemma quot_not_equalD [dest?]: "\a\ \ \b\ ==> \ (a \ b)" + by (simp add: quot_equality) + subsection {* Picking representing elements *}