diff -r 97a397ba5743 -r fe2a37cfecd3 Quot/QuotList.thy
--- a/Quot/QuotList.thy	Tue Dec 08 20:55:55 2009 +0100
+++ b/Quot/QuotList.thy	Tue Dec 08 22:02:14 2009 +0100
@@ -92,12 +92,21 @@
   shows "list_rel R [] []"
 by simp
 
-lemma map_prs:
+lemma map_prs_aux:
   assumes a: "Quotient R1 abs1 rep1"
   and     b: "Quotient R2 abs2 rep2"
   shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l"
 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
 
+
+lemma map_prs[quot_preserve]:
+  assumes a: "Quotient R1 abs1 rep1"
+  and     b: "Quotient R2 abs2 rep2"
+  shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
+by (simp only: expand_fun_eq fun_map.simps map_prs_aux[OF a b])
+   (simp)
+
+
 lemma map_rsp[quot_respect]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
@@ -110,18 +119,33 @@
 apply simp_all
 done
 
-lemma foldr_prs:
+lemma foldr_prs_aux:
   assumes a: "Quotient R1 abs1 rep1"
   and     b: "Quotient R2 abs2 rep2"
   shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
 
-lemma foldl_prs:
+lemma foldr_prs[quot_respect]:
+  assumes a: "Quotient R1 abs1 rep1"
+  and     b: "Quotient R2 abs2 rep2"
+  shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"
+by (simp only: expand_fun_eq fun_map.simps foldr_prs_aux[OF a b])
+   (simp)
+
+lemma foldl_prs_aux:
   assumes a: "Quotient R1 abs1 rep1"
   and     b: "Quotient R2 abs2 rep2"
   shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l"
 by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
 
+
+lemma foldl_prs[quot_preserve]:
+  assumes a: "Quotient R1 abs1 rep1"
+  and     b: "Quotient R2 abs2 rep2"
+  shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
+by (simp only: expand_fun_eq fun_map.simps foldl_prs_aux[OF a b])
+   (simp)
+
 lemma list_rel_empty: "list_rel R [] b \<Longrightarrow> length b = 0"
 by (induct b) (simp_all)