# HG changeset patch
# User Ning@localhost
# Date 1253420316 -3600
# Node ID 5023bf36d81af10be25d144499a9cda1b75eb9a4
# Parent  d15121412caa5f390c8af0a2a8eb6f5a74bb9aa9
beautification of some proofs

diff -r d15121412caa -r 5023bf36d81a QuotMain.thy
--- a/QuotMain.thy	Fri Sep 18 17:30:33 2009 +0200
+++ b/QuotMain.thy	Sun Sep 20 05:18:36 2009 +0100
@@ -48,7 +48,7 @@
 by (simp add: equiv[simplified EQUIV_def])
 
 lemma lem7:
-  "(R x = R y) = (Abs (R x) = Abs (R y))"
+  shows "(R x = R y) = (Abs (R x) = Abs (R y))"
 apply(rule iffI)
 apply(simp)
 apply(drule rep_inject[THEN iffD2])
@@ -80,23 +80,27 @@
 done
 
 lemma R_trans:
-  assumes ab: "R a b" and bc: "R b c" shows "R a c"
+  assumes ab: "R a b" 
+  and     bc: "R b c" 
+  shows "R a c"
 proof -
   have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
   moreover have ab: "R a b" by fact
   moreover have bc: "R b c" by fact
-  ultimately show ?thesis unfolding TRANS_def by blast
+  ultimately show "R a c" unfolding TRANS_def by blast
 qed
 
 lemma R_sym:
-  assumes ab: "R a b" shows "R b a"
+  assumes ab: "R a b" 
+  shows "R b a"
 proof -
   have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
-  then show ?thesis using ab unfolding SYM_def by blast
+  then show "R b a" using ab unfolding SYM_def by blast
 qed
 
 lemma R_trans2: 
-  assumes ac: "R a c" and bd: "R b d"
+  assumes ac: "R a c" 
+  and     bd: "R b d"
   shows "R a b = R c d"
 proof
   assume ab: "R a b"
@@ -118,7 +122,7 @@
   assume as: "R (REP a) (REP b)"
   from rep_prop
   obtain x where eq: "Rep a = R x" by auto
-  also 
+  (*also ... not useful in the proof  *) 
   from rep_prop
   obtain y where eq2: "Rep b = R y" by auto
   then have "R (Eps (R x)) (Eps (R y))" using as eq unfolding REP_def by simp