theory QuotList

imports QuotScript List

begin

lemma LIST_map_id:

  shows "map (\<lambda>x. x) = (\<lambda>x. x)"

  by simp

fun

where

apply(rule eq_reflection)

unfolding expand_fun_eq

apply(rule allI)+

apply(induct_tac x xa rule: list_induct2')

apply(simp_all)

done

  assumes a: "\<And>x y. R x y = (R x = R y)"

by (induct x) (auto simp add: a)

lemma LIST_equivp:

  assumes a: "equivp R"

unfolding equivp_def

apply(rule allI)+

apply(induct_tac x y rule: list_induct2')

apply(simp)

apply(simp add: expand_fun_eq)

apply(simp add: expand_fun_eq)

apply(simp add: expand_fun_eq)

apply(rule iffI)

apply(rule allI)

apply(case_tac x)

apply(simp)

apply(simp)

using a

apply(unfold equivp_def)

apply(auto)[1]

done

  assumes q: "Quotient R Abs Rep"

apply(induct r s rule: list_induct2')

apply(simp_all)

using Quotient_REL[OF q]

apply(metis)

done

  assumes q: "Quotient R Abs 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_reflp[OF q])

apply(rule allI)+

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"

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"

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"

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)--),

*)