631 

   632 (* Unused part of the locale *)

   633 

   634 lemma R_trans:

   635   assumes ab: "R a b"

   636   and     bc: "R b c"

   637   shows "R a c"

   638 proof -

   639   have tr: "transp R" using equivp equivp_reflp_symp_transp[of R] by simp

   640   moreover have ab: "R a b" by fact

   641   moreover have bc: "R b c" by fact

   642   ultimately show "R a c" unfolding transp_def by blast

   643 qed

   644 

   645 lemma R_sym:

   646   assumes ab: "R a b"

   647   shows "R b a"

   648 proof -

   649   have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp

   650   then show "R b a" using ab unfolding symp_def by blast

   651 qed

   652 

   653 lemma R_trans2:

   654   assumes ac: "R a c"

   655   and     bd: "R b d"

   656   shows "R a b = R c d"

   657 using ac bd

   658 by (blast intro: R_trans R_sym)

   659 

   660 lemma REPS_same:

   661   shows "R (REP a) (REP b) \<equiv> (a = b)"

   662 proof -

   663   have "R (REP a) (REP b) = (a = b)"

   664   proof

   665     assume as: "R (REP a) (REP b)"

   666     from rep_prop

   667     obtain x y

   668       where eqs: "Rep a = R x" "Rep b = R y" by blast

   669     from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp

   670     then have "R x (Eps (R y))" using lem9 by simp

   671     then have "R (Eps (R y)) x" using R_sym by blast

   672     then have "R y x" using lem9 by simp

   673     then have "R x y" using R_sym by blast

   674     then have "ABS x = ABS y" using thm11 by simp

   675     then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp

   676     then show "a = b" using rep_inverse by simp

   677   next

   678     assume ab: "a = b"

   679     have "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp

   680     then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto

   681   qed

   682   then show "R (REP a) (REP b) \<equiv> (a = b)" by simp

   683 qed

   684 

   685 

   686 

   687