src/HOL/Quotient.thy
changeset 40818 b117df72e56b
parent 40814 fa64f6278568
child 41452 c291e0826902
     1.1 --- a/src/HOL/Quotient.thy	Mon Nov 29 22:41:17 2010 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Mon Nov 29 22:47:55 2010 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4  text {* Composition of Relations *}
     1.5  
     1.6  abbreviation
     1.7 -  rel_conj (infixr "OOO" 75)
     1.8 +  rel_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" (infixr "OOO" 75)
     1.9  where
    1.10    "r1 OOO r2 \<equiv> r1 OO r2 OO r1"
    1.11  
    1.12 @@ -75,7 +75,14 @@
    1.13  definition
    1.14    "Quotient R Abs Rep \<longleftrightarrow>
    1.15       (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. R (Rep a) (Rep a)) \<and>
    1.16 -     (\<forall>r s. R r s = (R r r \<and> R s s \<and> (Abs r = Abs s)))"
    1.17 +     (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s)"
    1.18 +
    1.19 +lemma QuotientI:
    1.20 +  assumes "\<And>a. Abs (Rep a) = a"
    1.21 +    and "\<And>a. R (Rep a) (Rep a)"
    1.22 +    and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s"
    1.23 +  shows "Quotient R Abs Rep"
    1.24 +  using assms unfolding Quotient_def by blast
    1.25  
    1.26  lemma Quotient_abs_rep:
    1.27    assumes a: "Quotient R Abs Rep"
    1.28 @@ -93,14 +100,14 @@
    1.29  
    1.30  lemma Quotient_rel:
    1.31    assumes a: "Quotient R Abs Rep"
    1.32 -  shows " R r s = (R r r \<and> R s s \<and> (Abs r = Abs s))"
    1.33 +  shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
    1.34    using a
    1.35    unfolding Quotient_def
    1.36    by blast
    1.37  
    1.38  lemma Quotient_rel_rep:
    1.39    assumes a: "Quotient R Abs Rep"
    1.40 -  shows "R (Rep a) (Rep b) = (a = b)"
    1.41 +  shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
    1.42    using a
    1.43    unfolding Quotient_def
    1.44    by metis