--- a/Nominal/Abs.thy	Tue Mar 16 20:07:13 2010 +0100
+++ b/Nominal/Abs.thy	Wed Mar 17 08:39:46 2010 +0100
@@ -718,6 +718,22 @@
   apply (simp add: swap_fresh_fresh)
   done
 
+(* TODO: The following lemmas can be moved somewhere... *)
+lemma split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===>
+  prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split"
+  by auto
+
+lemma split_prs2[quot_preserve]:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  and q2: "Quotient R2 Abs2 Rep2"
+  shows "((Abs1 ---> Abs2 ---> prod_fun Abs1 Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> prod_fun Rep1 Rep2 ---> id) split = split"
+  by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+
+lemma alpha_gen2:
+  "(bs, x1, x2) \<approx>gen (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) =
+  (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2)"
+by (simp add: alpha_gen)
+
 
 end