diff -r 000000000000 -r ebe0ea8fe247 QuotList.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/QuotList.thy	Tue Aug 11 12:29:15 2009 +0200
@@ -0,0 +1,255 @@
+theory QuotList
+imports QuotScript
+begin
+
+
+lemma LIST_map_I:
+  shows "map (\<lambda>x. x) = (\<lambda>x. x)"
+  by simp
+
+fun
+  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)"
+
+lemma LIST_REL_EQ:
+  shows "LIST_REL (op =) = (op =)"
+unfolding expand_fun_eq
+apply(rule allI)+
+apply(induct_tac x xa rule: list_induct2')
+apply(simp_all)
+done
+
+lemma LIST_REL_REFL:
+  assumes a: "\<And>x y. R x y = (R x = R y)"
+  shows "LIST_REL R x x"
+by (induct x) (auto simp add: a)
+
+lemma LIST_EQUIV:
+  assumes a: "EQUIV R"
+  shows "EQUIV (LIST_REL R)"
+unfolding EQUIV_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(simp add: expand_fun_eq)
+apply(metis LIST_REL.simps(1) LIST_REL.simps(2))
+apply(simp add: expand_fun_eq)
+apply(rule iffI)
+apply(rule allI)
+apply(case_tac x)
+apply(simp)
+apply(simp)
+using a
+apply(unfold EQUIV_def)
+apply(auto)[1]
+apply(metis LIST_REL.simps(4))
+done
+
+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))"
+apply(induct r s rule: list_induct2')
+apply(simp_all)
+using QUOTIENT_REL[OF q]
+apply(metis)
+done
+
+lemma LIST_QUOTIENT:
+  assumes q: "QUOTIENT R Abs Rep"
+  shows "QUOTIENT (LIST_REL R) (map Abs) (map Rep)"
+unfolding QUOTIENT_def
+apply(rule conjI)
+apply(rule allI)
+apply(induct_tac a)
+apply(simp)
+apply(simp add: QUOTIENT_ABS_REP[OF q])
+apply(rule conjI)
+apply(rule allI)
+apply(induct_tac a)
+apply(simp)
+apply(simp)
+apply(simp add: QUOTIENT_REP_REFL[OF q])
+apply(rule allI)+
+apply(rule LIST_REL_REL[OF q])
+done
+
+lemma CONS_PRS:
+  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])
+
+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)"
+using a by (auto)
+
+lemma NIL_PRS:
+  assumes q: "QUOTIENT R Abs Rep"
+  shows "[] = (map Abs [])"
+by (simp)
+
+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_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)
+
+
+end
+
+(*
+val LENGTH_PRS = store_thm
+   ("LENGTH_PRS",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l. LENGTH l = LENGTH (MAP rep l)--),
+
+val LENGTH_RSP = store_thm
+   ("LENGTH_RSP",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l1 l2.
+          (LIST_REL R) l1 l2 ==>
+          (LENGTH l1 = LENGTH l2)--),
+val APPEND_PRS = store_thm
+   ("APPEND_PRS",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l m. APPEND l m = MAP abs (APPEND (MAP rep l) (MAP rep m))--),
+
+val APPEND_RSP = store_thm
+   ("APPEND_RSP",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l1 l2 m1 m2.
+          (LIST_REL R) l1 l2 /\ (LIST_REL R) m1 m2 ==>
+          (LIST_REL R) (APPEND l1 m1) (APPEND l2 m2)--),
+val FLAT_PRS = store_thm
+   ("FLAT_PRS",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l. FLAT l = MAP abs (FLAT (MAP (MAP rep) l))--),
+
+val FLAT_RSP = store_thm
+   ("FLAT_RSP",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l1 l2.
+          LIST_REL (LIST_REL R) l1 l2 ==>
+          (LIST_REL R) (FLAT l1) (FLAT l2)--),
+
+val REVERSE_PRS = store_thm
+   ("REVERSE_PRS",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l. REVERSE l = MAP abs (REVERSE (MAP rep l))--),
+
+val REVERSE_RSP = store_thm
+   ("REVERSE_RSP",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l1 l2.
+          LIST_REL R l1 l2 ==>
+          (LIST_REL R) (REVERSE l1) (REVERSE l2)--),
+
+val FILTER_PRS = store_thm
+   ("FILTER_PRS",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !P l. FILTER P l = (MAP abs) (FILTER ((abs --> I) P) (MAP rep l))
+       --),
+
+val FILTER_RSP = store_thm
+   ("FILTER_RSP",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !P1 P2 l1 l2.
+          (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==>
+          (LIST_REL R) (FILTER P1 l1) (FILTER P2 l2)--),
+
+val NULL_PRS = store_thm
+   ("NULL_PRS",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l. NULL l = NULL (MAP rep l)--),
+
+val NULL_RSP = store_thm
+   ("NULL_RSP",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l1 l2.
+          LIST_REL R l1 l2 ==>
+          (NULL l1 = NULL l2)--),
+
+val SOME_EL_PRS = store_thm
+   ("SOME_EL_PRS",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l P. SOME_EL P l = SOME_EL ((abs --> I) P) (MAP rep l)--),
+
+val SOME_EL_RSP = store_thm
+   ("SOME_EL_RSP",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l1 l2 P1 P2.
+          (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==>
+          (SOME_EL P1 l1 = SOME_EL P2 l2)--),
+
+val ALL_EL_PRS = store_thm
+   ("ALL_EL_PRS",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l P. ALL_EL P l = ALL_EL ((abs --> I) P) (MAP rep l)--),
+
+val ALL_EL_RSP = store_thm
+   ("ALL_EL_RSP",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l1 l2 P1 P2.
+          (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==>
+          (ALL_EL P1 l1 = ALL_EL P2 l2)--),
+
+val FOLDL_PRS = store_thm
+   ("FOLDL_PRS",
+    (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
+        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
+         !l f e. FOLDL f e l =
+                 abs1 (FOLDL ((abs1 --> abs2 --> rep1) f)
+                      (rep1 e)
+                      (MAP rep2 l))--),
+
+val FOLDL_RSP = store_thm
+   ("FOLDL_RSP",
+    (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
+        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
+         !l1 l2 f1 f2 e1 e2.
+          (R1 ===> R2 ===> R1) f1 f2 /\
+             R1 e1 e2 /\ (LIST_REL R2) l1 l2 ==>
+          R1 (FOLDL f1 e1 l1) (FOLDL f2 e2 l2)--),
+
+val FOLDR_PRS = store_thm
+   ("FOLDR_PRS",
+    (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
+        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
+         !l f e. FOLDR f e l =
+                 abs2 (FOLDR ((abs1 --> abs2 --> rep2) f)
+                      (rep2 e)
+                      (MAP rep1 l))--),
+
+val FOLDR_RSP = store_thm
+   ("FOLDR_RSP",
+    (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
+        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
+         !l1 l2 f1 f2 e1 e2.
+          (R1 ===> R2 ===> R2) f1 f2 /\
+             R2 e1 e2 /\ (LIST_REL R1) l1 l2 ==>
+          R2 (FOLDR f1 e1 l1) (FOLDR f2 e2 l2)--),
+*)
+