# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264496083 -3600
# Node ID 0879d144aaa3961fda32ba2db8def0282e341223
# Parent  68c1f378a70a6d13e042f08ba42ac769cf6a9c34
Generalized split_prs and split_rsp

diff -r 68c1f378a70a -r 0879d144aaa3 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Jan 26 09:28:32 2010 +0100
+++ b/Quot/Examples/FSet.thy	Tue Jan 26 09:54:43 2010 +0100
@@ -377,22 +377,6 @@
 apply(assumption)
 done
 
-lemma [quot_respect]:
-  "((op \<approx> ===> op \<approx> ===> op =) ===> prod_rel op \<approx> op \<approx> ===> op =) split split"
-apply(simp)
-done
-
-thm quot_preserve
-term split
-
-
-lemma [quot_preserve]:
-  shows "(((abs_fset ---> abs_fset ---> id) ---> prod_fun rep_fset rep_fset ---> id) split) = split"
-apply(simp add: expand_fun_eq)
-apply(simp add: Quotient_abs_rep[OF Quotient_fset])
-done
-
-
 lemma test: "All (\<lambda>(x::'a list, y). x = y)"
 sorry
 
diff -r 68c1f378a70a -r 0879d144aaa3 Quot/QuotProd.thy
--- 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)