--- a/QuotMain.thy	Mon Dec 07 04:41:42 2009 +0100
+++ b/QuotMain.thy	Mon Dec 07 08:45:04 2009 +0100
@@ -1,5 +1,5 @@
 theory QuotMain
-imports QuotScript QuotList Prove
+imports QuotScript QuotList QuotProd Prove
 uses ("quotient_info.ML")
      ("quotient.ML")
      ("quotient_def.ML")
@@ -146,15 +146,17 @@
 declare [[map * = (prod_fun, prod_rel)]]
 declare [[map "fun" = (fun_map, fun_rel)]]
 
+(* identity quotient is not here as it has to be applied first *)
 lemmas [quotient_thm] =
-  fun_quotient list_quotient
+  fun_quotient list_quotient prod_quotient
 
 lemmas [quotient_rsp] =
-  quot_rel_rsp nil_rsp cons_rsp foldl_rsp
+  quot_rel_rsp nil_rsp cons_rsp foldl_rsp pair_rsp
 
-(* OPTION, PRODUCTS *)
+(* fun_map is not here since equivp is not true *)
+(* TODO: option, ... *)
 lemmas [quotient_equiv] =
-  identity_equivp list_equivp
+  identity_equivp list_equivp prod_equivp
 
 
 ML {* maps_lookup @{theory} "List.list" *}
@@ -708,9 +710,10 @@
   let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in
   thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)]
   end
-  handle _ => error "solve_quotient_assums"
+  handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"
 *}
 
+(* Not used *)
 (* It proves the Quotient assumptions by calling quotient_tac *)
 ML {*
 fun solve_quotient_assum i ctxt thm =
@@ -917,11 +920,17 @@
           (resolve_tac trans2 THEN' RANGE [
             quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
 
+(* TODO: These patterns should should be somehow combined and generalized... *)
 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
     (Const (@{const_name fun_rel}, _) $ _ $ _) $
     (Const (@{const_name fun_rel}, _) $ _ $ _)
     => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt
 
+| (Const (@{const_name fun_rel}, _) $ _ $ _) $
+    (Const (@{const_name prod_rel}, _) $ _ $ _) $
+    (Const (@{const_name prod_rel}, _) $ _ $ _)
+    => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt
+
    (* respectfulness of constants; in particular of a simple relation *)
 | _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
     => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt