--- a/QuotScript.thy	Sat Nov 28 03:17:22 2009 +0100
+++ b/QuotScript.thy	Sat Nov 28 04:02:54 2009 +0100
@@ -429,67 +429,96 @@
 by (auto)
 
 
-(* TODO: Put the following lemmas in proper places *)
 
-lemma equiv_res_forall:
+(* Set of lemmas for regularisation of ball and bex *)
+lemma ball_reg_eqv:
+  fixes P :: "'a \<Rightarrow> bool"
+  assumes a: "EQUIV R"
+  shows "Ball (Respects R) P = (All P)"
+  by (metis EQUIV_def IN_RESPECTS a)
+
+lemma bex_reg_eqv:
   fixes P :: "'a \<Rightarrow> bool"
-  assumes a: "EQUIV E"
-  shows "Ball (Respects E) P = (All P)"
-  using a by (metis EQUIV_def IN_RESPECTS a)
+  assumes a: "EQUIV R"
+  shows "Bex (Respects R) P = (Ex P)"
+  by (metis EQUIV_def IN_RESPECTS a)
+
+lemma ball_reg_right:
+  assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
+  shows "All P \<longrightarrow> Ball R Q"
+  by (metis COMBC_def Collect_def Collect_mem_eq a)
+
+lemma bex_reg_left:
+  assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
+  shows "Bex R Q \<longrightarrow> Ex P"
+  by (metis COMBC_def Collect_def Collect_mem_eq a)
+
+lemma ball_reg_left:
+  assumes a: "EQUIV R"
+  shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
+  by (metis EQUIV_REFL IN_RESPECTS a)
 
-lemma equiv_res_exists:
-  fixes P :: "'a \<Rightarrow> bool"
-  assumes a: "EQUIV E"
-  shows "Bex (Respects E) P = (Ex P)"
-  using a by (metis EQUIV_def IN_RESPECTS a)
+lemma bex_reg_right:
+  assumes a: "EQUIV R"
+  shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
+  by (metis EQUIV_REFL IN_RESPECTS a)
 
-lemma FORALL_REGULAR:
+lemma ball_reg_eqv_range:
+  fixes P::"'a \<Rightarrow> bool"
+  and x::"'a"
+  assumes a: "EQUIV R2"
+  shows   "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
+  apply(rule iffI)
+  apply(rule allI)
+  apply(drule_tac x="\<lambda>y. f x" in bspec)
+  apply(simp add: Respects_def IN_RESPECTS)
+  apply(rule impI)
+  using a EQUIV_REFL_SYM_TRANS[of "R2"]
+  apply(simp add: REFL_def)
+  apply(simp)
+  apply(simp)
+  done
+
+lemma bex_reg_eqv_range:
+  fixes P::"'a \<Rightarrow> bool"
+  and x::"'a"
+  assumes a: "EQUIV R2"
+  shows   "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
+  apply(auto)
+  apply(rule_tac x="\<lambda>y. f x" in bexI)
+  apply(simp)
+  apply(simp add: Respects_def IN_RESPECTS)
+  apply(rule impI)
+  using a EQUIV_REFL_SYM_TRANS[of "R2"]
+  apply(simp add: REFL_def)
+  done
+
+lemma all_reg:
   assumes a: "!x :: 'a. (P x --> Q x)"
   and     b: "All P"
   shows "All Q"
   using a b by (metis)
 
-lemma EXISTS_REGULAR:
+lemma ex_reg:
   assumes a: "!x :: 'a. (P x --> Q x)"
   and     b: "Ex P"
   shows "Ex Q"
   using a b by (metis)
 
-lemma RES_FORALL_REGULAR:
+lemma ball_reg:
   assumes a: "!x :: 'a. (R x --> P x --> Q x)"
   and     b: "Ball R P"
   shows "Ball R Q"
   using a b by (metis COMBC_def Collect_def Collect_mem_eq)
 
-lemma RES_EXISTS_REGULAR:
+lemma bex_reg:
   assumes a: "!x :: 'a. (R x --> P x --> Q x)"
   and     b: "Bex R P"
   shows "Bex R Q"
   using a b by (metis COMBC_def Collect_def Collect_mem_eq)
 
-lemma LEFT_RES_FORALL_REGULAR:
-  assumes a: "\<And>x. (R x \<and> (Q x \<longrightarrow> P x))"
-  shows "Ball R Q \<longrightarrow> All P"
-  using a
-  apply (metis COMBC_def Collect_def Collect_mem_eq a)
-  done
 
-lemma RIGHT_RES_FORALL_REGULAR:
-  assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
-  shows "All P \<longrightarrow> Ball R Q"
-  using a
-  apply (metis COMBC_def Collect_def Collect_mem_eq a)
-  done
 
-lemma LEFT_RES_EXISTS_REGULAR:
-  assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
-  shows "Bex R Q \<longrightarrow> Ex P"
-  using a by (metis COMBC_def Collect_def Collect_mem_eq)
-
-lemma RIGHT_RES_EXISTS_REGULAR:
-  assumes a: "\<And>x. (R x \<and> (P x \<longrightarrow> Q x))"
-  shows "Ex P \<longrightarrow> Bex R Q"
-  using a by (metis COMBC_def Collect_def Collect_mem_eq)
 
 (* TODO: Add similar *)
 lemma RES_FORALL_RSP: