--- a/Quot/QuotBase.thy	Wed Feb 10 11:09:30 2010 +0100
+++ b/Quot/QuotBase.thy	Wed Feb 10 11:27:49 2010 +0100
@@ -47,7 +47,7 @@
 
 lemma eq_imp_rel:  
   shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" 
-by (simp add: equivp_reflp)
+  by (simp add: equivp_reflp)
 
 lemma identity_equivp:
   shows "equivp (op =)"
@@ -252,15 +252,15 @@
   assumes q: "Quotient R Abs Rep"
   and     a: "R x1 x2"
   shows "R x1 (Rep (Abs x2))"
-using a 
-by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])
+  using a 
+  by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])
 
 lemma rep_abs_rsp_left:
   assumes q: "Quotient R Abs Rep"
   and     a: "R x1 x2"
   shows "R (Rep (Abs x1)) x2"
-using a 
-by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])
+  using a 
+  by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])
 
 (* In the following theorem R1 can be instantiated with anything,
    but we know some of the types of the Rep and Abs functions;
@@ -436,14 +436,14 @@
   assumes a: "(R ===> (op =)) f g"
   shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)"
   using a 
-by (simp add: Ex1_def in_respects) auto
+  by (simp add: Ex1_def in_respects) auto
 
-(* 3 lemmas needed for cleaning of quantifiers *)
+(* 2 lemmas needed for cleaning of quantifiers *)
 lemma all_prs:
   assumes a: "Quotient R absf repf"
   shows "Ball (Respects R) ((absf ---> id) f) = All f"
   using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply
-by metis
+  by metis
 
 lemma ex_prs:
   assumes a: "Quotient R absf repf"
@@ -458,45 +458,55 @@
 where
   "Bex1_rel R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
 
-(* TODO/FIXME: simplify the repetitions in this proof *)
-lemma bexeq_rsp:
+lemma bex1_rel_aux:
+  "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y"
+  unfolding Bex1_rel_def
+  apply (erule conjE)+
+  apply (erule bexE)
+  apply rule
+  apply (rule_tac x="xa" in bexI)
+  apply metis
+  apply metis
+  apply rule+
+  apply (erule_tac x="xaa" in ballE)
+  prefer 2
+  apply (metis)
+  apply (erule_tac x="ya" in ballE)
+  prefer 2
+  apply (metis)
+  apply (metis in_respects)
+  done
+
+lemma bex1_rel_aux2:
+  "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R y\<rbrakk> \<Longrightarrow> Bex1_rel R x"
+  unfolding Bex1_rel_def
+  apply (erule conjE)+
+  apply (erule bexE)
+  apply rule
+  apply (rule_tac x="xa" in bexI)
+  apply metis
+  apply metis
+  apply rule+
+  apply (erule_tac x="xaa" in ballE)
+  prefer 2
+  apply (metis)
+  apply (erule_tac x="ya" in ballE)
+  prefer 2
+  apply (metis)
+  apply (metis in_respects)
+  done
+
+lemma bex1_rel_rsp:
   assumes a: "Quotient R absf repf"
   shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
-apply simp
-unfolding Bex1_rel_def
-apply rule
-apply rule
-apply rule
-apply rule
-apply (erule conjE)+
-apply (erule bexE)
-apply rule
-apply (rule_tac x="xa" in bexI)
-apply metis
-apply metis
-apply rule+
-apply (erule_tac x="xb" in ballE)
-prefer 2
-apply (metis)
-apply (erule_tac x="ya" in ballE)
-prefer 2
-apply (metis)
-apply (metis in_respects)
-apply (erule conjE)+
-apply (erule bexE)
-apply rule
-apply (rule_tac x="xa" in bexI)
-apply metis
-apply metis
-apply rule+
-apply (erule_tac x="xb" in ballE)
-prefer 2
-apply (metis)
-apply (erule_tac x="ya" in ballE)
-prefer 2
-apply (metis)
-apply (metis in_respects)
-done
+  apply simp
+  apply clarify
+  apply rule
+  apply (simp_all add: bex1_rel_aux bex1_rel_aux2)
+  apply (erule bex1_rel_aux2)
+  apply assumption
+  done
+
 
 lemma ex1_prs:
   assumes a: "Quotient R absf repf"
@@ -512,7 +522,6 @@
  apply (erule conjE)
  apply (subgoal_tac "\<forall>y. R y y \<longrightarrow> f (absf y) \<longrightarrow> R x y")
   apply (rule_tac x="absf x" in exI)
-  apply (thin_tac "\<forall>x\<in>Respects R. \<forall>y\<in>Respects R. f (absf x) \<and> f (absf y) \<longrightarrow> R x y")
   apply (simp)
   apply rule+
   using a unfolding Quotient_def
@@ -582,14 +591,14 @@
 lemma if_prs:
   assumes q: "Quotient R Abs Rep"
   shows "Abs (If a (Rep b) (Rep c)) = If a b c"
-using Quotient_abs_rep[OF q] by auto
+  using Quotient_abs_rep[OF q] by auto
 
 (* q not used *)
 lemma if_rsp:
   assumes q: "Quotient R Abs Rep"
   and     a: "a1 = a2" "R b1 b2" "R c1 c2"
   shows "R (If a1 b1 c1) (If a2 b2 c2)"
-using a by auto
+  using a by auto
 
 lemma let_prs:
   assumes q1: "Quotient R1 Abs1 Rep1"
@@ -605,15 +614,13 @@
   using apply_rsp[OF q1 a1] a2 by auto
 
 
-(******************************************)
-(* REST OF THE FILE IS UNUSED (until now) *)
-(******************************************)
+(*** REST OF THE FILE IS UNUSED (until now) ***)
 
 text {*
 lemma in_fun:
   shows "x \<in> ((f ---> g) s) = g (f x \<in> s)"
   by (simp add: mem_def)
- 
+
 lemma respects_thm:
   shows "Respects (R1 ===> R2) f = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (f y))"
   unfolding Respects_def
@@ -657,7 +664,7 @@
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   and     r1: "Respects (R1 ===> R2) f"
-  and     r2: "Respects (R1 ===> R2) g" 
+  and     r2: "Respects (R1 ===> R2) g"
   shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
   apply(rule_tac iffI)
   apply(rule)+
@@ -689,11 +696,6 @@
   shows "(R1 ===> R2) f1 f2 \<Longrightarrow> (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))"
   using r1 r2 by auto
 
-(* ask peter what are literal_case *)
-(* literal_case_PRS *)
-(* literal_case_RSP *)
-(* Cez: !f x. literal_case f x = f x *)
-
 (* We use id_simps which includes id_apply; so these 2 theorems can be removed *)
 lemma id_prs:
   assumes q: "Quotient R Abs Rep"