--- a/Nominal/Abs.thy	Thu May 06 10:43:41 2010 +0200
+++ b/Nominal/Abs.thy	Thu May 06 13:25:37 2010 +0200
@@ -825,6 +825,20 @@
   apply (simp)
   done
 
+fun
+  prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"
+where
+  "prod_fv fvx fvy (x, y) = (fvx x \<union> fvy y)"
+
+lemma [quot_respect]:
+  "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
+  by auto
+
+lemma [quot_preserve]:
+  assumes q1: "Quotient R1 abs1 rep1"
+  and     q2: "Quotient R2 abs2 rep2"
+  shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv"
+  by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 
 end