# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260373392 -3600
# Node ID adcceaf31f923438c18ea60655c5d05cae967463
# Parent  546ba31fbb830151a8b6df68ee36b2a8c82055b4
foldr_rsp.

diff -r 546ba31fbb83 -r adcceaf31f92 Quot/QuotList.thy
--- a/Quot/QuotList.thy	Wed Dec 09 15:59:02 2009 +0100
+++ b/Quot/QuotList.thy	Wed Dec 09 16:43:12 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 =)"