Theory "quotient_list"

Parents rich_list quotient

Signature

Constant	Type
LIST_REL_tupled	:('a -> 'a -> bool) # 'a list # 'a list -> bool
LIST_REL	:('a -> 'a -> bool) -> 'a list -> 'a list -> bool

Definitions

LIST_REL_tupled_primitive_def

|- LIST_REL_tupled =
   WFREC (@R'. WF R' /\ !b a bs as R. R' (R,as,bs) (R,a::as,b::bs))
     (\LIST_REL_tupled a'.
        case a' of
           (R,[],[]) -> I T
        || (R,[],b::bs) -> I F
        || (R,a::as,[]) -> I F
        || (R,a::as,b'::bs') -> I (R a b' /\ LIST_REL_tupled (R,as,bs')))

LIST_REL_curried_def

|- !x x1 x2. LIST_REL x x1 x2 = LIST_REL_tupled (x,x1,x2)

Theorems

LIST_MAP_I

|- MAP I = I

LIST_REL_ind

|- !P.
     (!R. P R [] []) /\ (!R a as. P R (a::as) []) /\
     (!R b bs. P R [] (b::bs)) /\
     (!R a as b bs. P R as bs ==> P R (a::as) (b::bs)) ==>
     !v v1 v2. P v v1 v2

LIST_REL_def

|- (LIST_REL R [] [] = T) /\ (LIST_REL R (a::as) [] = F) /\
   (LIST_REL R [] (b::bs) = F) /\
   (LIST_REL R (a::as) (b::bs) = R a b /\ LIST_REL R as bs)

LIST_REL_EQ

|- LIST_REL $= = $=

LIST_REL_REFL

|- !R. (!x y. R x y = (R x = R y)) ==> !x. LIST_REL R x x

LIST_EQUIV

|- !R. EQUIV R ==> EQUIV (LIST_REL R)

LIST_REL_REL

|- !R abs rep.
     QUOTIENT R abs rep ==>
     !r s.
       LIST_REL R r s =
       LIST_REL R r r /\ LIST_REL R s s /\ (MAP abs r = MAP abs s)

LIST_QUOTIENT

|- !R abs rep.
     QUOTIENT R abs rep ==> QUOTIENT (LIST_REL R) (MAP abs) (MAP rep)

CONS_PRS

|- !R abs rep. QUOTIENT R abs rep ==> !t h. h::t = MAP abs (rep h::MAP rep t)

CONS_RSP

|- !R abs rep.
     QUOTIENT R abs rep ==>
     !t1 t2 h1 h2.
       R h1 h2 /\ LIST_REL R t1 t2 ==> LIST_REL R (h1::t1) (h2::t2)

NIL_PRS

|- !R abs rep. QUOTIENT R abs rep ==> ([] = MAP abs [])

NIL_RSP

|- !R abs rep. QUOTIENT R abs rep ==> LIST_REL R [] []

MAP_PRS

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ==>
       !l f. MAP f l = MAP abs2 (MAP ((abs1 --> rep2) f) (MAP rep1 l))

MAP_RSP

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ==>
       !l1 l2 f1 f2.
         (R1 ===> R2) f1 f2 /\ LIST_REL R1 l1 l2 ==>
         LIST_REL R2 (MAP f1 l1) (MAP f2 l2)

LENGTH_PRS

|- !R abs rep. QUOTIENT R abs rep ==> !l. LENGTH l = LENGTH (MAP rep l)

LENGTH_RSP

|- !R abs rep.
     QUOTIENT R abs rep ==>
     !l1 l2. LIST_REL R l1 l2 ==> (LENGTH l1 = LENGTH l2)

APPEND_PRS

|- !R abs rep.
     QUOTIENT R abs rep ==> !l m. l ++ m = MAP abs (MAP rep l ++ MAP rep m)

APPEND_RSP

|- !R abs rep.
     QUOTIENT R abs rep ==>
     !l1 l2 m1 m2.
       LIST_REL R l1 l2 /\ LIST_REL R m1 m2 ==>
       LIST_REL R (l1 ++ m1) (l2 ++ m2)

FLAT_PRS

|- !R abs rep.
     QUOTIENT R abs rep ==> !l. FLAT l = MAP abs (FLAT (MAP (MAP rep) l))

FLAT_RSP

|- !R abs rep.
     QUOTIENT R abs rep ==>
     !l1 l2. LIST_REL (LIST_REL R) l1 l2 ==> LIST_REL R (FLAT l1) (FLAT l2)

REVERSE_PRS

|- !R abs rep.
     QUOTIENT R abs rep ==> !l. REVERSE l = MAP abs (REVERSE (MAP rep l))

REVERSE_RSP

|- !R abs rep.
     QUOTIENT R abs rep ==>
     !l1 l2. LIST_REL R l1 l2 ==> LIST_REL R (REVERSE l1) (REVERSE l2)

FILTER_PRS

|- !R abs rep.
     QUOTIENT R abs rep ==>
     !P l. FILTER P l = MAP abs (FILTER ((abs --> I) P) (MAP rep l))

FILTER_RSP

|- !R abs 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)

NULL_PRS

|- !R abs rep. QUOTIENT R abs rep ==> !l. NULL l = NULL (MAP rep l)

NULL_RSP

|- !R abs rep.
     QUOTIENT R abs rep ==> !l1 l2. LIST_REL R l1 l2 ==> (NULL l1 = NULL l2)

SOME_EL_PRS

|- !R abs rep.
     QUOTIENT R abs rep ==>
     !l P. EXISTS P l = EXISTS ((abs --> I) P) (MAP rep l)

SOME_EL_RSP

|- !R abs rep.
     QUOTIENT R abs rep ==>
     !l1 l2 P1 P2.
       (R ===> $=) P1 P2 /\ LIST_REL R l1 l2 ==> (EXISTS P1 l1 = EXISTS P2 l2)

ALL_EL_PRS

|- !R abs rep.
     QUOTIENT R abs rep ==>
     !l P. EVERY P l = EVERY ((abs --> I) P) (MAP rep l)

ALL_EL_RSP

|- !R abs rep.
     QUOTIENT R abs rep ==>
     !l1 l2 P1 P2.
       (R ===> $=) P1 P2 /\ LIST_REL R l1 l2 ==> (EVERY P1 l1 = EVERY P2 l2)

FOLDL_PRS

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ==>
       !l f e.
         FOLDL f e l =
         abs1 (FOLDL ((abs1 --> abs2 --> rep1) f) (rep1 e) (MAP rep2 l))

FOLDL_RSP

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 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)

FOLDR_PRS

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ==>
       !l f e.
         FOLDR f e l =
         abs2 (FOLDR ((abs1 --> abs2 --> rep2) f) (rep2 e) (MAP rep1 l))

FOLDR_RSP

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 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)