diff -r c9231c2903bc -r af118149ffd4 UnusedQuotMain.thy
--- a/UnusedQuotMain.thy	Thu Dec 10 08:55:30 2009 +0100
+++ b/UnusedQuotMain.thy	Thu Dec 10 10:21:51 2009 +0100
@@ -628,3 +628,60 @@
   |> cprop_of |> Thm.dest_equals |> snd
 
 *}
+
+(* Unused part of the locale *)
+
+lemma R_trans:
+  assumes ab: "R a b"
+  and     bc: "R b c"
+  shows "R a c"
+proof -
+  have tr: "transp R" using equivp equivp_reflp_symp_transp[of R] by simp
+  moreover have ab: "R a b" by fact
+  moreover have bc: "R b c" by fact
+  ultimately show "R a c" unfolding transp_def by blast
+qed
+
+lemma R_sym:
+  assumes ab: "R a b"
+  shows "R b a"
+proof -
+  have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp
+  then show "R b a" using ab unfolding symp_def by blast
+qed
+
+lemma R_trans2:
+  assumes ac: "R a c"
+  and     bd: "R b d"
+  shows "R a b = R c d"
+using ac bd
+by (blast intro: R_trans R_sym)
+
+lemma REPS_same:
+  shows "R (REP a) (REP b) \<equiv> (a = b)"
+proof -
+  have "R (REP a) (REP b) = (a = b)"
+  proof
+    assume as: "R (REP a) (REP b)"
+    from rep_prop
+    obtain x y
+      where eqs: "Rep a = R x" "Rep b = R y" by blast
+    from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
+    then have "R x (Eps (R y))" using lem9 by simp
+    then have "R (Eps (R y)) x" using R_sym by blast
+    then have "R y x" using lem9 by simp
+    then have "R x y" using R_sym by blast
+    then have "ABS x = ABS y" using thm11 by simp
+    then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
+    then show "a = b" using rep_inverse by simp
+  next
+    assume ab: "a = b"
+    have "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp
+    then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto
+  qed
+  then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
+qed
+
+
+
+