--- a/QuotScript.thy	Mon Nov 30 10:16:10 2009 +0100
+++ b/QuotScript.thy	Mon Nov 30 11:53:20 2009 +0100
@@ -223,6 +223,7 @@
 using FUN_QUOTIENT[OF q1 q2] unfolding Respects_def QUOTIENT_def expand_fun_eq
 by blast
 
+(* TODO: it is the same as APPLY_RSP *)
 (* q1 and q2 not used; see next lemma *)
 lemma FUN_REL_MP:
   assumes q1: "QUOTIENT R1 Abs1 Rep1"
@@ -430,6 +431,17 @@
 
 
 
+
+
+lemma COND_PRS:
+  assumes a: "QUOTIENT R absf repf"
+  shows "(if a then b else c) = absf (if a then repf b else repf c)"
+  using a unfolding QUOTIENT_def by auto
+
+
+
+
+
 (* Set of lemmas for regularisation of ball and bex *)
 lemma ball_reg_eqv:
   fixes P :: "'a \<Rightarrow> bool"
@@ -525,49 +537,29 @@
   "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
 by auto
 
-
-
-(* TODO: Add similar *)
-lemma RES_FORALL_RSP:
-  shows "\<And>f g. (R ===> (op =)) f g ==>
-        (Ball (Respects R) f = Ball (Respects R) g)"
-  apply (simp add: FUN_REL.simps Ball_def IN_RESPECTS)
-  done
+(* 2 lemmas needed for proving repabs_inj *)
+lemma ball_rsp:
+  assumes a: "(R ===> (op =)) f g"
+  shows "Ball (Respects R) f = Ball (Respects R) g"
+  using a by (simp add: Ball_def IN_RESPECTS)
 
-lemma RES_EXISTS_RSP:
-  shows "\<And>f g. (R ===> (op =)) f g ==>
-        (Bex (Respects R) f = Bex (Respects R) g)"
-  apply (simp add: FUN_REL.simps Bex_def IN_RESPECTS)
-  done
+lemma bex_rsp:
+  assumes a: "(R ===> (op =)) f g"
+  shows "(Bex (Respects R) f = Bex (Respects R) g)"
+  using a by (simp add: Bex_def IN_RESPECTS)
 
-
-lemma FORALL_PRS:
+(* 2 lemmas needed for cleaning of quantifiers *)
+lemma all_prs:
   assumes a: "QUOTIENT R absf repf"
-  shows "All f = Ball (Respects R) ((absf ---> id) f)"
-  using a
-  unfolding QUOTIENT_def
+  shows "Ball (Respects R) ((absf ---> id) f) = All f"
+  using a unfolding QUOTIENT_def
   by (metis IN_RESPECTS fun_map.simps id_apply)
 
-lemma EXISTS_PRS:
-  assumes a: "QUOTIENT R absf repf"
-  shows "Ex f = Bex (Respects R) ((absf ---> id) f)"
-  using a
-  unfolding QUOTIENT_def
-  by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply mem_def)
-
-lemma COND_PRS:
+lemma ex_prs:
   assumes a: "QUOTIENT R absf repf"
-  shows "(if a then b else c) = absf (if a then repf b else repf c)"
-  using a unfolding QUOTIENT_def by auto
-
-(* These are the fixed versions, general ones need to be proved. *)
-lemma ho_all_prs:
-  shows "((op = ===> op =) ===> op =) All All"
-  by auto
-
-lemma ho_ex_prs:
-  shows "((op = ===> op =) ===> op =) Ex Ex"
-  by auto
+  shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
+  using a unfolding QUOTIENT_def
+  by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply)
 
 end