# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273148525 -7200
# Node ID b434506fb0d41c436bc9858824420625e0d759f8
# Parent  978e6469b504a078b5cd993edbde910d6d97f755
respectfullness and preservation of prod_rel

diff -r 978e6469b504 -r b434506fb0d4 src/HOL/Library/Quotient_Product.thy
--- a/src/HOL/Library/Quotient_Product.thy	Thu May 06 10:55:09 2010 +0200
+++ b/src/HOL/Library/Quotient_Product.thy	Thu May 06 14:22:05 2010 +0200
@@ -93,6 +93,25 @@
   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 [quot_respect]:
+  shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===>
+  prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel"
+  by auto
+
+lemma [quot_preserve]:
+  assumes q1: "Quotient R1 abs1 rep1"
+  and     q2: "Quotient R2 abs2 rep2"
+  shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) --->
+  prod_fun rep1 rep2 ---> prod_fun rep1 rep2 ---> id) prod_rel = prod_rel"
+  by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+
+lemma [quot_preserve]:
+  shows"(prod_rel ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2)
+  (l1, l2) (r1, r2)) = (R1 (rep1 l1) (rep1 r1) \<and> R2 (rep2 l2) (rep2 r2))"
+  by simp
+
+declare Pair_eq[quot_preserve]
+
 lemma prod_fun_id[id_simps]:
   shows "prod_fun id id = id"
   by (simp add: prod_fun_def)