--- a/QuotScript.thy	Fri Dec 04 16:40:23 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 16:53:11 2009 +0100
@@ -28,12 +28,12 @@
   by (simp add: equivp_reflp_symp_transp reflp_def)
 
 definition
-  "PART_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
+  "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
 
-lemma equivp_IMP_PART_equivp:
+lemma equivp_IMP_part_equivp:
   assumes a: "equivp E"
-  shows "PART_equivp E"
-using a unfolding equivp_def PART_equivp_def
+  shows "part_equivp E"
+using a unfolding equivp_def part_equivp_def
 by auto
 
 definition
@@ -47,9 +47,9 @@
 using a unfolding Quotient_def
 by simp
 
-lemma Quotient_REP_reflp:
+lemma Quotient_rep_reflp:
   assumes a: "Quotient E Abs Rep"
-  shows "E (Rep a) (Rep a)" 
+  shows "E (Rep a) (Rep a)"
 using a unfolding Quotient_def
 by blast
 
@@ -59,21 +59,10 @@
 using a unfolding Quotient_def
 by blast
 
-lemma Quotient_REL_ABS:
-  assumes a: "Quotient E Abs Rep"
-  shows "E r s \<Longrightarrow> Abs r = Abs s"
-using a unfolding Quotient_def
-by blast
-
-lemma Quotient_REL_ABS_EQ:
-  assumes a: "Quotient E Abs Rep"
-  shows "E r r \<Longrightarrow> E s s \<Longrightarrow> E r s = (Abs r = Abs s)"
-using a unfolding Quotient_def
-by blast
-
-lemma Quotient_REL_REP:
+lemma Quotient_rel_rep:
   assumes a: "Quotient R Abs Rep"
-  shows "R (Rep a) (Rep b) = (a = b)"
+  shows "R (Rep a) (Rep b) \<equiv> (a = b)"
+apply (rule eq_reflection)
 using a unfolding Quotient_def
 by metis
 
@@ -251,7 +240,7 @@
 apply(metis fun_rel_IMP)
 using r1 unfolding Respects_def expand_fun_eq
 apply(simp (no_asm_use))
-apply(metis Quotient_rel[OF q2] Quotient_REL_REP[OF q1])
+apply(metis Quotient_rel[OF q2] Quotient_rel_rep[OF q1])
 done
 
 (* ask Peter: fun_rel_IMP used twice *) 
@@ -265,12 +254,6 @@
 using q1 q2 r1 r2 a
 by (simp add: fun_rel_EQUALS)
 
-(* We don't use it, it is exactly the same as Quotient_REL_REP but wrong way *)
-lemma EQUALS_PRS:
-  assumes q: "Quotient R Abs Rep"
-  shows "(x = y) = R (Rep x) (Rep y)"
-by (rule Quotient_REL_REP[OF q, symmetric])
-
 lemma equals_rsp:
   assumes q: "Quotient R Abs Rep"
   and     a: "R xa xb" "R ya yb"
@@ -328,14 +311,14 @@
   assumes q: "Quotient R Abs Rep"
   and     a: "R x1 x2"
   shows "R x1 (Rep (Abs x2))"
-using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_REP_reflp[OF q])
+using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])
 
 (* Not used *)
 lemma REP_ABS_RSP_LEFT:
   assumes q: "Quotient R Abs Rep"
   and     a: "R x1 x2"
   shows "R x1 (Rep (Abs x2))"
-using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_REP_reflp[OF q])
+using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])
 
 (* ----------------------------------------------------- *)
 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE,           *)
@@ -567,5 +550,21 @@
   using a unfolding Quotient_def
   by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply)
 
+
+(* UNUSED *)
+lemma Quotient_rel_abs:
+  assumes a: "Quotient E Abs Rep"
+  shows "E r s \<Longrightarrow> Abs r = Abs s"
+using a unfolding Quotient_def
+by blast
+
+lemma Quotient_rel_abs_eq:
+  assumes a: "Quotient E Abs Rep"
+  shows "E r r \<Longrightarrow> E s s \<Longrightarrow> E r s = (Abs r = Abs s)"
+using a unfolding Quotient_def
+by blast
+
+
+
 end