--- a/Quot/QuotProd.thy Tue Jan 26 09:28:32 2010 +0100
+++ b/Quot/QuotProd.thy Tue Jan 26 09:54:43 2010 +0100
@@ -74,6 +74,16 @@
apply (simp add: Quotient_abs_rep[OF q2])
done
+lemma split_rsp[quot_respect]:
+ "((R1 ===> R2 ===> op =) ===> (prod_rel R1 R2) ===> op =) split split"
+ by auto
+
+lemma split_prs[quot_preserve]:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ and q2: "Quotient R2 Abs2 Rep2"
+ shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split"
+ by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+
lemma prod_fun_id[id_simps]:
shows "prod_fun id id = id"
by (simp add: prod_fun_def)