--- a/QuotList.thy	Fri Dec 04 16:12:40 2009 +0100
+++ b/QuotList.thy	Fri Dec 04 16:40:23 2009 +0100
@@ -46,7 +46,7 @@
   apply(rule allI)
   apply(induct_tac a)
   apply(simp)
-  apply(simp add: Quotient_ABS_REP[OF q])
+  apply(simp add: Quotient_abs_rep[OF q])
   apply(rule conjI)
   apply(rule allI)
   apply(induct_tac a)
@@ -58,53 +58,62 @@
   done
 
 
-
-
-
+lemma cons_prs:
+  assumes q: "Quotient R Abs Rep"
+  shows "(map Abs) ((Rep h) # (map Rep t)) = h # t"
+by (induct t) (simp_all add: Quotient_abs_rep[OF q])
 
-(* Rest is not used *)
-
-
-lemma CONS_PRS:
+lemma cons_rsp:
   assumes q: "Quotient R Abs Rep"
-  shows "(h#t) = (map Abs) ((Rep h)#(map Rep t))"
-by (induct t) (simp_all add: Quotient_ABS_REP[OF q])
+  shows "(R ===> list_rel R ===> list_rel R) op # op #"
+by (auto)
 
-lemma CONS_RSP:
+lemma nil_prs:
   assumes q: "Quotient R Abs Rep"
-  and     a: "R h1 h2" "list_rel R t1 t2"
-  shows "list_rel R (h1#t1) (h2#t2)"
-using a by (auto)
-
-lemma NIL_PRS:
-  assumes q: "Quotient R Abs Rep"
-  shows "[] = (map Abs [])"
+  shows "map Abs [] \<equiv> []"
 by (simp)
 
-lemma NIL_RSP:
+lemma nil_rsp:
   assumes q: "Quotient R Abs Rep"
   shows "list_rel R [] []"
 by simp
 
-lemma MAP_PRS:
-  assumes q1: "Quotient R1 Abs1 Rep1"
-  and     q2: "Quotient R2 Abs2 Rep2"
-  shows "map f l = (map Abs2) (map ((Abs1 ---> Rep2) f) (map Rep1 l))"
-by (induct l)
-   (simp_all add: Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2])
+lemma map_prs:
+  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_RSP:
+(* We need an ho version *)
+lemma map_rsp:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   and     a: "(R1 ===> R2) f1 f2"
   and     b: "list_rel R1 l1 l2"
   shows "list_rel R2 (map f1 l1) (map f2 l2)"
 using b a
-by (induct l1 l2 rule: list_induct2')
-   (simp_all)
+by (induct l1 l2 rule: list_induct2') (simp_all)
+
+lemma foldr_prs:
+  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:
+  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])
 
 
 
+
+
+
+
+(* TODO: Rest are unused *)
+
 lemma LIST_map_id:
   shows "map (\<lambda>x. x) = (\<lambda>x. x)"
   by simp