--- a/QuotScript.thy	Wed Oct 14 18:13:16 2009 +0200
+++ b/QuotScript.thy	Thu Oct 15 10:25:23 2009 +0200
@@ -403,6 +403,9 @@
 using a1 a2 unfolding o_def expand_fun_eq
 by (auto)
 
+
+(* TODO: Put the following lemmas in proper places *)
+
 lemma equiv_res_forall:
   fixes P :: "'a \<Rightarrow> bool"
   assumes a: "EQUIV E"
@@ -415,5 +418,53 @@
   shows "Bex (Respects E) P = (Ex P)"
   using a by (metis EQUIV_def IN_RESPECTS a)
 
+lemma FORALL_REGULAR:
+  assumes a: "!x :: 'a. (P x --> Q x)"
+  and     b: "All P"
+  shows "All Q"
+  using a b by (metis)
+
+lemma EXISTS_REGULAR:
+  assumes a: "!x :: 'a. (P x --> Q x)"
+  and     b: "Ex P"
+  shows "Ex Q"
+  using a b by (metis)
+
+lemma RES_FORALL_REGULAR:
+  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:
+  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: "!x. (R x \<and> (Q x --> P x))"
+  shows "Ball R Q ==> All P"
+  using a
+  apply (metis COMBC_def Collect_def Collect_mem_eq a)
+  done
+
+lemma RIGHT_RES_FORALL_REGULAR:
+  assumes a: "!x :: 'a. (R x --> P x --> Q x)"
+  shows "All P ==> Ball R Q"
+  using a
+  apply (metis COMBC_def Collect_def Collect_mem_eq a)
+  done
+
+lemma LEFT_RES_EXISTS_REGULAR:
+  assumes a: "!x :: 'a. (R x --> Q x --> P x)"
+  shows "Bex R Q ==> Ex P"
+  using a by (metis COMBC_def Collect_def Collect_mem_eq)
+
+lemma RIGHT_RES_EXISTS_REGULAR:
+  assumes a: "!x :: 'a. (R x \<and> (P x --> Q x))"
+  shows "Ex P \<Longrightarrow> Bex R Q"
+  using a by (metis COMBC_def Collect_def Collect_mem_eq)
+
 end