--- a/Quot/QuotProd.thy	Tue Dec 08 22:02:14 2009 +0100
+++ b/Quot/QuotProd.thy	Tue Dec 08 22:24:24 2009 +0100
@@ -1,5 +1,5 @@
 theory QuotProd
-imports QuotScript
+imports QuotMain
 begin
 
 fun
@@ -35,12 +35,25 @@
   shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
 by auto
 
-lemma pair_prs:
+lemma pair_prs_aux:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(prod_fun Abs1 Abs2) (Rep1 l, Rep2 r) \<equiv> (l, r)"
   by (simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 
+term Pair
+
+lemma pair_prs[quot_preserve]:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  assumes q2: "Quotient R2 Abs2 Rep2"
+  shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair"
+apply(simp only: expand_fun_eq fun_map.simps pair_prs_aux[OF q1 q2])
+apply(simp)
+done
+
+
+
+
 (* TODO: Is the quotient assumption q1 necessary? *)
 (* TODO: Aren't there hard to use later? *)
 lemma fst_rsp:
@@ -77,4 +90,13 @@
   shows "Abs2 (snd ((prod_fun Rep1 Rep2) p)) = snd p"
 by (case_tac p) (auto simp add: Quotient_abs_rep[OF q2])
 
+
+section {* general setup for products *}
+
+declare [[map * = (prod_fun, prod_rel)]]
+
+lemmas [quot_thm] = prod_quotient
+lemmas [quot_respect] = pair_rsp
+lemmas [quot_equiv] = prod_equivp
+
 end