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 =) \<equiv> (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)--),

*)