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