# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260302155 -3600
# Node ID 97a397ba57437df184ae3a63f19464eff5551745
# Parent  cd4226736c3716a00c3bb1017081c870bf72a59d
started to reformulate preserve lemmas

diff -r cd4226736c37 -r 97a397ba5743 Quot/QuotList.thy
--- a/Quot/QuotList.thy	Tue Dec 08 20:34:00 2009 +0100
+++ b/Quot/QuotList.thy	Tue Dec 08 20:55:55 2009 +0100
@@ -66,18 +66,23 @@
   apply (simp_all)
   done
 
-
-lemma cons_prs:
+lemma cons_prs_aux:
   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_prs[quot_preserve]:
+  assumes q: "Quotient R Abs Rep"
+  shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
+by (simp only: expand_fun_eq fun_map.simps cons_prs_aux[OF q])
+   (simp)
+
 lemma cons_rsp[quot_respect]:
   assumes q: "Quotient R Abs Rep"
   shows "(R ===> list_rel R ===> list_rel R) op # op #"
 by (auto)
 
-lemma nil_prs:
+lemma nil_prs[quot_preserve]:
   assumes q: "Quotient R Abs Rep"
   shows "map Abs [] \<equiv> []"
 by (simp)