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
```