# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260373474 -3600
# Node ID 3c15b9809831466ea314b7daaa88ff146ec03403
# Parent  adcceaf31f923438c18ea60655c5d05cae967463# Parent  cc0fac4fd46c592a498e1e2fffd3404ff1369fe3
merge

diff -r cc0fac4fd46c -r 3c15b9809831 Quot/QuotList.thy
--- a/Quot/QuotList.thy	Wed Dec 09 16:09:25 2009 +0100
+++ b/Quot/QuotList.thy	Wed Dec 09 16:44:34 2009 +0100
@@ -174,12 +174,19 @@
 apply (simp_all)
 done
 
-(* TODO: foldr_rsp should be similar *)
-
+lemma foldr_rsp[quot_respect]:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  and     q2: "Quotient R2 Abs2 Rep2"
+  shows "((R1 ===> R2 ===> R2) ===> list_rel R1 ===> R2 ===> R2) foldr foldr"
+apply auto
+apply(subgoal_tac "R2 xb yb \<longrightarrow> list_rel R1 xa ya \<longrightarrow> R2 (foldr x xa xb) (foldr y ya yb)")
+apply simp
+apply (rule_tac xs="xa" and ys="ya" in list_induct2)
+apply (rule list_rel_len)
+apply (simp_all)
+done
 
-
-
-(* TODO: Rest are unused *)
+(* Rest are unused *)
 
 lemma list_rel_eq:
   shows "list_rel (op =) \<equiv> (op =)"