--- a/QuotList.thy	Fri Dec 04 15:41:09 2009 +0100
+++ b/QuotList.thy	Fri Dec 04 15:50:57 2009 +0100
@@ -7,15 +7,15 @@
   by simp
 
 fun
-  LIST_REL
+  list_rel
 where
-  "LIST_REL R [] [] = True"
-| "LIST_REL R (x#xs) [] = False"
-| "LIST_REL R [] (x#xs) = False"
-| "LIST_REL R (x#xs) (y#ys) = (R x y \<and> LIST_REL R xs ys)"
+  "list_rel R [] [] = True"
+| "list_rel R (x#xs) [] = False"
+| "list_rel R [] (x#xs) = False"
+| "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)"
 
-lemma LIST_REL_EQ:
-  shows "LIST_REL (op =) \<equiv> (op =)"
+lemma list_rel_EQ:
+  shows "list_rel (op =) \<equiv> (op =)"
 apply(rule eq_reflection)
 unfolding expand_fun_eq
 apply(rule allI)+
@@ -23,22 +23,22 @@
 apply(simp_all)
 done
 
-lemma LIST_REL_REFL:
+lemma list_rel_REFL:
   assumes a: "\<And>x y. R x y = (R x = R y)"
-  shows "LIST_REL R x x"
+  shows "list_rel R x x"
 by (induct x) (auto simp add: a)
 
 lemma LIST_equivp:
   assumes a: "equivp R"
-  shows "equivp (LIST_REL R)"
+  shows "equivp (list_rel R)"
 unfolding equivp_def
 apply(rule allI)+
 apply(induct_tac x y rule: list_induct2')
 apply(simp)
 apply(simp add: expand_fun_eq)
-apply(metis LIST_REL.simps(1) LIST_REL.simps(2))
+apply(metis list_rel.simps(1) list_rel.simps(2))
 apply(simp add: expand_fun_eq)
-apply(metis LIST_REL.simps(1) LIST_REL.simps(2))
+apply(metis list_rel.simps(1) list_rel.simps(2))
 apply(simp add: expand_fun_eq)
 apply(rule iffI)
 apply(rule allI)
@@ -48,21 +48,21 @@
 using a
 apply(unfold equivp_def)
 apply(auto)[1]
-apply(metis LIST_REL.simps(4))
+apply(metis list_rel.simps(4))
 done
 
-lemma LIST_REL_REL: 
+lemma list_rel_REL: 
   assumes q: "Quotient R Abs Rep"
-  shows "LIST_REL R r s = (LIST_REL R r r \<and> LIST_REL R s s \<and> (map Abs r = map Abs s))"
+  shows "list_rel R r s = (list_rel R r r \<and> list_rel R s s \<and> (map Abs r = map Abs s))"
 apply(induct r s rule: list_induct2')
 apply(simp_all)
 using Quotient_REL[OF q]
 apply(metis)
 done
 
-lemma LIST_Quotient:
+lemma list_quotient:
   assumes q: "Quotient R Abs Rep"
-  shows "Quotient (LIST_REL R) (map Abs) (map Rep)"
+  shows "Quotient (list_rel R) (map Abs) (map Rep)"
 unfolding Quotient_def
 apply(rule conjI)
 apply(rule allI)
@@ -76,7 +76,7 @@
 apply(simp)
 apply(simp add: Quotient_REP_reflp[OF q])
 apply(rule allI)+
-apply(rule LIST_REL_REL[OF q])
+apply(rule list_rel_REL[OF q])
 done
 
 lemma CONS_PRS:
@@ -86,8 +86,8 @@
 
 lemma CONS_RSP:
   assumes q: "Quotient R Abs Rep"
-  and     a: "R h1 h2" "LIST_REL R t1 t2"
-  shows "LIST_REL R (h1#t1) (h2#t2)"
+  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:
@@ -97,7 +97,7 @@
 
 lemma NIL_RSP:
   assumes q: "Quotient R Abs Rep"
-  shows "LIST_REL R [] []"
+  shows "list_rel R [] []"
 by simp
 
 lemma MAP_PRS:
@@ -110,9 +110,9 @@
 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)"
+  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)