--- a/Quot/QuotList.thy	Mon Dec 07 14:14:07 2009 +0100
+++ b/Quot/QuotList.thy	Mon Dec 07 14:35:45 2009 +0100
@@ -1,5 +1,5 @@
 theory QuotList
-imports QuotScript List
+imports QuotMain List
 begin
 
 fun
@@ -10,7 +10,9 @@
 | "list_rel R [] (x#xs) = False"
 | "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)"
 
-lemma list_equivp:
+declare [[map list = (map, list_rel)]]
+
+lemma list_equivp[quotient_equiv]:
   assumes a: "equivp R"
   shows "equivp (list_rel R)"
   unfolding equivp_def
@@ -38,7 +40,7 @@
   apply(metis)
   done
 
-lemma list_quotient:
+lemma list_quotient[quotient_thm]:
   assumes q: "Quotient R Abs Rep"
   shows "Quotient (list_rel R) (map Abs) (map Rep)"
   unfolding Quotient_def
@@ -57,13 +59,20 @@
   apply(rule list_rel_rel[OF q])
   done
 
+lemma map_id: "map id \<equiv> id"
+  apply (rule eq_reflection)
+  apply (rule ext)
+  apply (rule_tac list="x" in list.induct)
+  apply (simp_all)
+  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])
 
-lemma cons_rsp:
+lemma cons_rsp[quotient_rsp]:
   assumes q: "Quotient R Abs Rep"
   shows "(R ===> list_rel R ===> list_rel R) op # op #"
 by (auto)
@@ -73,7 +82,7 @@
   shows "map Abs [] \<equiv> []"
 by (simp)
 
-lemma nil_rsp:
+lemma nil_rsp[quotient_rsp]:
   assumes q: "Quotient R Abs Rep"
   shows "list_rel R [] []"
 by simp
@@ -132,7 +141,7 @@
          induct     doesn't accept 'rule'.
    that's why the proof uses manual generalisation and needs assumptions
    both in conclusion for induction and in assumptions. *)
-lemma foldl_rsp:
+lemma foldl_rsp[quotient_rsp]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl"
@@ -153,10 +162,6 @@
 
 (* TODO: Rest are unused *)
 
-lemma list_map_id:
-  shows "map (\<lambda>x. x) = (\<lambda>x. x)"
-  by simp
-
 lemma list_rel_eq:
   shows "list_rel (op =) \<equiv> (op =)"
 apply(rule eq_reflection)