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