Theory: rich_list

Parents

• operator
• list

Types

Constants

• GENLIST  :(num -> 'a) -> num -> 'a list
• IS_SUBLIST  :'a list -> 'a list -> bool
• LAST  :'a list -> 'a
• BUTFIRSTN  :num -> 'a list -> 'a list
• SUFFIX  :('a -> bool) -> 'a list -> 'a list
• AND_EL  :bool list -> bool
• ALL_EL  :('a -> bool) -> 'a list -> bool
• PREFIX  :('a -> bool) -> 'a list -> 'a list
• REVERSE  :'a list -> 'a list
• SNOC  :'a -> 'a list -> 'a list
• SCANL  :('b -> 'a -> 'b) -> 'b -> 'a list -> 'b list
• SCANR  :('a -> 'b -> 'b) -> 'b -> 'a list -> 'b list
• SOME_EL  :('a -> bool) -> 'a list -> bool
• IS_SUFFIX  :'a list -> 'a list -> bool
• IS_PREFIX  :'a list -> 'a list -> bool
• OR_EL  :bool list -> bool
• LASTN  :num -> 'a list -> 'a list
• BUTLAST  :'a list -> 'a list
• FIRSTN  :num -> 'a list -> 'a list
• ELL  :num -> 'a list -> 'a
• BUTLASTN  :num -> 'a list -> 'a list
• UNZIP_FST  :('a # 'b) list -> 'a list
• SEG  :num -> num -> 'a list -> 'a list
• UNZIP_SND  :('a # 'b) list -> 'b list
• REPLICATE  :num -> 'a -> 'a list
• IS_EL  :'a -> 'a list -> bool
• SPLITP  :('a -> bool) -> 'a list -> 'a list # 'a list

Definitions

ALL_EL

|- (!P. ALL_EL P [] = T) /\ !P x l. ALL_EL P (x::l) = P x /\ ALL_EL P l

AND_EL_DEF

|- AND_EL = ALL_EL I

BUTFIRSTN

|- (!l. BUTFIRSTN 0 l = l) /\ !n x l. BUTFIRSTN (SUC n) (x::l) = BUTFIRSTN n l

BUTLAST_DEF

|- !l. BUTLAST l = SEG (PRE (LENGTH l)) 0 l

BUTLASTN

|- (!l. BUTLASTN 0 l = l) /\
   !n x l. BUTLASTN (SUC n) (SNOC x l) = BUTLASTN n l

ELL

|- (!l. ELL 0 l = LAST l) /\ !n l. ELL (SUC n) l = ELL n (BUTLAST l)

FIRSTN

|- (!l. FIRSTN 0 l = []) /\ !n x l. FIRSTN (SUC n) (x::l) = x::FIRSTN n l

GENLIST

|- (!f. GENLIST f 0 = []) /\
   !f n. GENLIST f (SUC n) = SNOC (f n) (GENLIST f n)

IS_EL_DEF

|- !x l. IS_EL x l = SOME_EL ($= x) l

IS_PREFIX

|- (!l. IS_PREFIX l [] = T) /\ (!x l. IS_PREFIX [] (x::l) = F) /\
   !x1 l1 x2 l2. IS_PREFIX (x1::l1) (x2::l2) = (x1 = x2) /\ IS_PREFIX l1 l2

IS_SUBLIST

|- (!l. IS_SUBLIST l [] = T) /\ (!x l. IS_SUBLIST [] (x::l) = F) /\
   !x1 l1 x2 l2.
     IS_SUBLIST (x1::l1) (x2::l2) =
     (x1 = x2) /\ IS_PREFIX l1 l2 \/ IS_SUBLIST l1 (x2::l2)

IS_SUFFIX

|- (!l. IS_SUFFIX l [] = T) /\ (!x l. IS_SUFFIX [] (SNOC x l) = F) /\
   !x1 l1 x2 l2.
     IS_SUFFIX (SNOC x1 l1) (SNOC x2 l2) = (x1 = x2) /\ IS_SUFFIX l1 l2

LAST_DEF

|- !l. LAST l = HD (SEG 1 (PRE (LENGTH l)) l)

LASTN

|- (!l. LASTN 0 l = []) /\
   !n x l. LASTN (SUC n) (SNOC x l) = SNOC x (LASTN n l)

OR_EL_DEF

|- OR_EL = SOME_EL I

PREFIX_DEF

|- !P l. PREFIX P l = FST (SPLITP ($~ o P) l)

REPLICATE

|- (!x. REPLICATE 0 x = []) /\ !n x. REPLICATE (SUC n) x = x::REPLICATE n x

REVERSE

|- (REVERSE [] = []) /\ !x l. REVERSE (x::l) = SNOC x (REVERSE l)

SCANL

|- (!f e. SCANL f e [] = [e]) /\
   !f e x l. SCANL f e (x::l) = e::SCANL f (f e x) l

SCANR

|- (!f e. SCANR f e [] = [e]) /\
   !f e x l. SCANR f e (x::l) = f x (HD (SCANR f e l))::SCANR f e l

SEG

|- (!k l. SEG 0 k l = []) /\ (!m x l. SEG (SUC m) 0 (x::l) = x::SEG m 0 l) /\
   !m k x l. SEG (SUC m) (SUC k) (x::l) = SEG (SUC m) k l

SNOC

|- (!x. SNOC x [] = [x]) /\ !x x' l. SNOC x (x'::l) = x'::SNOC x l

SOME_EL

|- (!P. SOME_EL P [] = F) /\ !P x l. SOME_EL P (x::l) = P x \/ SOME_EL P l

SPLITP

|- (!P. SPLITP P [] = ([],[])) /\
   !P x l.
     SPLITP P (x::l) =
     (if P x then ([],x::l) else (x::FST (SPLITP P l),SND (SPLITP P l)))

SUFFIX_DEF

|- !P l. SUFFIX P l = FOLDL (\l' x. (if P x then SNOC x l' else [])) [] l

UNZIP_FST_DEF

|- !l. UNZIP_FST l = FST (UNZIP l)

UNZIP_SND_DEF

|- !l. UNZIP_SND l = SND (UNZIP l)

Theorems

ALL_EL_APPEND

|- !P l1 l2. ALL_EL P (APPEND l1 l2) = ALL_EL P l1 /\ ALL_EL P l2

ALL_EL_BUTFIRSTN

|- !P l. ALL_EL P l ==> !m. m <= LENGTH l ==> ALL_EL P (BUTFIRSTN m l)

ALL_EL_BUTLASTN

|- !P l. ALL_EL P l ==> !m. m <= LENGTH l ==> ALL_EL P (BUTLASTN m l)

ALL_EL_CONJ

|- !P Q l. ALL_EL (\x. P x /\ Q x) l = ALL_EL P l /\ ALL_EL Q l

ALL_EL_FIRSTN

|- !P l. ALL_EL P l ==> !m. m <= LENGTH l ==> ALL_EL P (FIRSTN m l)

ALL_EL_FOLDL

|- !P l. ALL_EL P l = FOLDL (\l' x. l' /\ P x) T l

ALL_EL_FOLDL_MAP

|- !P l. ALL_EL P l = FOLDL $/\ T (MAP P l)

ALL_EL_FOLDR

|- !P l. ALL_EL P l = FOLDR (\x l'. P x /\ l') T l

ALL_EL_FOLDR_MAP

|- !P l. ALL_EL P l = FOLDR $/\ T (MAP P l)

ALL_EL_LASTN

|- !P l. ALL_EL P l ==> !m. m <= LENGTH l ==> ALL_EL P (LASTN m l)

ALL_EL_MAP

|- !P f l. ALL_EL P (MAP f l) = ALL_EL (P o f) l

ALL_EL_REPLICATE

|- !x n. ALL_EL ($= x) (REPLICATE n x)

ALL_EL_REVERSE

|- !P l. ALL_EL P (REVERSE l) = ALL_EL P l

ALL_EL_SEG

|- !P l. ALL_EL P l ==> !m k. m + k <= LENGTH l ==> ALL_EL P (SEG m k l)

ALL_EL_SNOC

|- !P x l. ALL_EL P (SNOC x l) = ALL_EL P l /\ P x

AND_EL_FOLDL

|- !l. AND_EL l = FOLDL $/\ T l

AND_EL_FOLDR

|- !l. AND_EL l = FOLDR $/\ T l

APPEND

|- (!l. APPEND [] l = l) /\ !l1 l2 x. APPEND (x::l1) l2 = x::APPEND l1 l2

APPEND_ASSOC

|- !l1 l2 l3. APPEND l1 (APPEND l2 l3) = APPEND (APPEND l1 l2) l3

APPEND_BUTLAST_LAST

|- !l. ~(l = []) ==> (APPEND (BUTLAST l) [LAST l] = l)

APPEND_BUTLASTN_BUTFIRSTN

|- !m n l. (m + n = LENGTH l) ==> (APPEND (BUTLASTN m l) (BUTFIRSTN n l) = l)

APPEND_BUTLASTN_LASTN

|- !n l. n <= LENGTH l ==> (APPEND (BUTLASTN n l) (LASTN n l) = l)

APPEND_FIRSTN_BUTFIRSTN

|- !n l. n <= LENGTH l ==> (APPEND (FIRSTN n l) (BUTFIRSTN n l) = l)

APPEND_FIRSTN_LASTN

|- !m n l. (m + n = LENGTH l) ==> (APPEND (FIRSTN n l) (LASTN m l) = l)

APPEND_FOLDL

|- !l1 l2. APPEND l1 l2 = FOLDL (\l' x. SNOC x l') l1 l2

APPEND_FOLDR

|- !l1 l2. APPEND l1 l2 = FOLDR CONS l2 l1

APPEND_LENGTH_EQ

|- !l1 l1'.
     (LENGTH l1 = LENGTH l1') ==>
     !l2 l2'.
       (LENGTH l2 = LENGTH l2') ==>
       ((APPEND l1 l2 = APPEND l1' l2') = (l1 = l1') /\ (l2 = l2'))

APPEND_NIL

|- (!l. APPEND l [] = l) /\ !l. APPEND [] l = l

APPEND_SNOC

|- !l1 x l2. APPEND l1 (SNOC x l2) = SNOC x (APPEND l1 l2)

ASSOC_APPEND

|- ASSOC APPEND

ASSOC_FOLDL_FLAT

|- !f.
     ASSOC f ==>
     !e.
       RIGHT_ID f e ==> !l. FOLDL f e (FLAT l) = FOLDL f e (MAP (FOLDL f e) l)

ASSOC_FOLDR_FLAT

|- !f.
     ASSOC f ==>
     !e.
       LEFT_ID f e ==> !l. FOLDR f e (FLAT l) = FOLDR f e (MAP (FOLDR f e) l)

BUTFIRSTN_APPEND1

|- !n l1.
     n <= LENGTH l1 ==>
     !l2. BUTFIRSTN n (APPEND l1 l2) = APPEND (BUTFIRSTN n l1) l2

BUTFIRSTN_APPEND2

|- !l1 n.
     LENGTH l1 <= n ==>
     !l2. BUTFIRSTN n (APPEND l1 l2) = BUTFIRSTN (n - LENGTH l1) l2

BUTFIRSTN_BUTFIRSTN

|- !n m l.
     n + m <= LENGTH l ==> (BUTFIRSTN n (BUTFIRSTN m l) = BUTFIRSTN (n + m) l)

BUTFIRSTN_LASTN

|- !n l. n <= LENGTH l ==> (BUTFIRSTN n l = LASTN (LENGTH l - n) l)

BUTFIRSTN_LENGTH_APPEND

|- !l1 l2. BUTFIRSTN (LENGTH l1) (APPEND l1 l2) = l2

BUTFIRSTN_LENGTH_NIL

|- !l. BUTFIRSTN (LENGTH l) l = []

BUTFIRSTN_REVERSE

|- !n l. n <= LENGTH l ==> (BUTFIRSTN n (REVERSE l) = REVERSE (BUTLASTN n l))

BUTFIRSTN_SEG

|- !n l. n <= LENGTH l ==> (BUTFIRSTN n l = SEG (LENGTH l - n) n l)

BUTFIRSTN_SNOC

|- !n l. n <= LENGTH l ==> !x. BUTFIRSTN n (SNOC x l) = SNOC x (BUTFIRSTN n l)

BUTLAST

|- !x l. BUTLAST (SNOC x l) = l

BUTLAST_CONS

|- (!x. BUTLAST [x] = []) /\ !x y z. BUTLAST (x::y::z) = x::BUTLAST (y::z)

BUTLASTN_1

|- !l. ~(l = []) ==> (BUTLASTN 1 l = BUTLAST l)

BUTLASTN_APPEND1

|- !l2 n.
     LENGTH l2 <= n ==>
     !l1. BUTLASTN n (APPEND l1 l2) = BUTLASTN (n - LENGTH l2) l1

BUTLASTN_APPEND2

|- !n l1 l2.
     n <= LENGTH l2 ==>
     (BUTLASTN n (APPEND l1 l2) = APPEND l1 (BUTLASTN n l2))

BUTLASTN_BUTLAST

|- !n l. n < LENGTH l ==> (BUTLASTN n (BUTLAST l) = BUTLAST (BUTLASTN n l))

BUTLASTN_BUTLASTN

|- !m n l.
     n + m <= LENGTH l ==> (BUTLASTN n (BUTLASTN m l) = BUTLASTN (n + m) l)

BUTLASTN_CONS

|- !n l. n <= LENGTH l ==> !x. BUTLASTN n (x::l) = x::BUTLASTN n l

BUTLASTN_FIRSTN

|- !n l. n <= LENGTH l ==> (BUTLASTN n l = FIRSTN (LENGTH l - n) l)

BUTLASTN_LASTN

|- !m n l.
     m <= n /\ n <= LENGTH l ==>
     (BUTLASTN m (LASTN n l) = LASTN (n - m) (BUTLASTN m l))

BUTLASTN_LASTN_NIL

|- !n l. n <= LENGTH l ==> (BUTLASTN n (LASTN n l) = [])

BUTLASTN_LENGTH_APPEND

|- !l2 l1. BUTLASTN (LENGTH l2) (APPEND l1 l2) = l1

BUTLASTN_LENGTH_CONS

|- !l x. BUTLASTN (LENGTH l) (x::l) = [x]

BUTLASTN_LENGTH_NIL

|- !l. BUTLASTN (LENGTH l) l = []

BUTLASTN_MAP

|- !n l. n <= LENGTH l ==> !f. BUTLASTN n (MAP f l) = MAP f (BUTLASTN n l)

BUTLASTN_REVERSE

|- !n l. n <= LENGTH l ==> (BUTLASTN n (REVERSE l) = REVERSE (BUTFIRSTN n l))

BUTLASTN_SEG

|- !n l. n <= LENGTH l ==> (BUTLASTN n l = SEG (LENGTH l - n) 0 l)

BUTLASTN_SUC_BUTLAST

|- !n l. n < LENGTH l ==> (BUTLASTN (SUC n) l = BUTLASTN n (BUTLAST l))

COMM_ASSOC_FOLDL_REVERSE

|- !f. COMM f ==> ASSOC f ==> !e l. FOLDL f e (REVERSE l) = FOLDL f e l

COMM_ASSOC_FOLDR_REVERSE

|- !f. COMM f ==> ASSOC f ==> !e l. FOLDR f e (REVERSE l) = FOLDR f e l

COMM_MONOID_FOLDL

|- !f. COMM f ==> !e'. MONOID f e' ==> !e l. FOLDL f e l = f e (FOLDL f e' l)

COMM_MONOID_FOLDR

|- !f. COMM f ==> !e'. MONOID f e' ==> !e l. FOLDR f e l = f e (FOLDR f e' l)

CONS

|- !l. ~NULL l ==> (HD l::TL l = l)

CONS_11

|- !x l x' l'. (x::l = x'::l') = (x = x') /\ (l = l')

CONS_APPEND

|- !x l. x::l = APPEND [x] l

EL

|- (!l. EL 0 l = HD l) /\ !n l. EL (SUC n) l = EL n (TL l)

EL_APPEND1

|- !n l1 l2. n < LENGTH l1 ==> (EL n (APPEND l1 l2) = EL n l1)

EL_APPEND2

|- !l1 n. LENGTH l1 <= n ==> !l2. EL n (APPEND l1 l2) = EL (n - LENGTH l1) l2

EL_CONS

|- !n. 0 < n ==> !x l. EL n (x::l) = EL (PRE n) l

EL_ELL

|- !n l. n < LENGTH l ==> (EL n l = ELL (PRE (LENGTH l - n)) l)

EL_IS_EL

|- !n l. n < LENGTH l ==> IS_EL (EL n l) l

EL_LENGTH_APPEND

|- !l2 l1. ~NULL l2 ==> (EL (LENGTH l1) (APPEND l1 l2) = HD l2)

EL_LENGTH_SNOC

|- !l x. EL (LENGTH l) (SNOC x l) = x

EL_MAP

|- !n l. n < LENGTH l ==> !f. EL n (MAP f l) = f (EL n l)

EL_PRE_LENGTH

|- !l. ~(l = []) ==> (EL (PRE (LENGTH l)) l = LAST l)

EL_REVERSE

|- !n l. n < LENGTH l ==> (EL n (REVERSE l) = EL (PRE (LENGTH l - n)) l)

EL_REVERSE_ELL

|- !n l. n < LENGTH l ==> (EL n (REVERSE l) = ELL n l)

EL_SEG

|- !n l. n < LENGTH l ==> (EL n l = HD (SEG 1 n l))

EL_SNOC

|- !n l. n < LENGTH l ==> !x. EL n (SNOC x l) = EL n l

ELL_0_SNOC

|- !l x. ELL 0 (SNOC x l) = x

ELL_APPEND1

|- !l2 n.
     LENGTH l2 <= n ==> !l1. ELL n (APPEND l1 l2) = ELL (n - LENGTH l2) l1

ELL_APPEND2

|- !n l2. n < LENGTH l2 ==> !l1. ELL n (APPEND l1 l2) = ELL n l2

ELL_CONS

|- !n l. n < LENGTH l ==> !x. ELL n (x::l) = ELL n l

ELL_EL

|- !n l. n < LENGTH l ==> (ELL n l = EL (PRE (LENGTH l - n)) l)

ELL_IS_EL

|- !n l. n < LENGTH l ==> IS_EL (EL n l) l

ELL_LAST

|- !l. ~NULL l ==> (ELL 0 l = LAST l)

ELL_LENGTH_APPEND

|- !l1 l2. ~NULL l1 ==> (ELL (LENGTH l2) (APPEND l1 l2) = LAST l1)

ELL_LENGTH_CONS

|- !l x. ELL (LENGTH l) (x::l) = x

ELL_LENGTH_SNOC

|- !l x. ELL (LENGTH l) (SNOC x l) = (if NULL l then x else HD l)

ELL_MAP

|- !n l f. n < LENGTH l ==> (ELL n (MAP f l) = f (ELL n l))

ELL_PRE_LENGTH

|- !l. ~(l = []) ==> (ELL (PRE (LENGTH l)) l = HD l)

ELL_REVERSE

|- !n l. n < LENGTH l ==> (ELL n (REVERSE l) = ELL (PRE (LENGTH l - n)) l)

ELL_REVERSE_EL

|- !n l. n < LENGTH l ==> (ELL n (REVERSE l) = EL n l)

ELL_SEG

|- !n l. n < LENGTH l ==> (ELL n l = HD (SEG 1 (PRE (LENGTH l - n)) l))

ELL_SNOC

|- !n. 0 < n ==> !x l. ELL n (SNOC x l) = ELL (PRE n) l

ELL_SUC_SNOC

|- !n x l. ELL (SUC n) (SNOC x l) = ELL n l

EQ_LIST

|- !x1 x2. (x1 = x2) ==> !l1 l2. (l1 = l2) ==> (x1::l1 = x2::l2)

FCOMM_FOLDL_APPEND

|- !f g.
     FCOMM f g ==>
     !e.
       RIGHT_ID g e ==>
       !l1 l2. FOLDL f e (APPEND l1 l2) = g (FOLDL f e l1) (FOLDL f e l2)

FCOMM_FOLDL_FLAT

|- !f g.
     FCOMM f g ==>
     !e.
       RIGHT_ID g e ==> !l. FOLDL f e (FLAT l) = FOLDL g e (MAP (FOLDL f e) l)

FCOMM_FOLDR_APPEND

|- !g f.
     FCOMM g f ==>
     !e.
       LEFT_ID g e ==>
       !l1 l2. FOLDR f e (APPEND l1 l2) = g (FOLDR f e l1) (FOLDR f e l2)

FCOMM_FOLDR_FLAT

|- !g f.
     FCOMM g f ==>
     !e.
       LEFT_ID g e ==> !l. FOLDR f e (FLAT l) = FOLDR g e (MAP (FOLDR f e) l)

FILTER

|- (!P. FILTER P [] = []) /\
   !P h t. FILTER P (h::t) = (if P h then h::FILTER P t else FILTER P t)

FILTER_APPEND

|- !f l1 l2. FILTER f (APPEND l1 l2) = APPEND (FILTER f l1) (FILTER f l2)

FILTER_COMM

|- !f1 f2 l. FILTER f1 (FILTER f2 l) = FILTER f2 (FILTER f1 l)

FILTER_FILTER

|- !P Q l. FILTER P (FILTER Q l) = FILTER (\x. P x /\ Q x) l

FILTER_FLAT

|- !P l. FILTER P (FLAT l) = FLAT (MAP (FILTER P) l)

FILTER_FOLDL

|- !P l. FILTER P l = FOLDL (\l' x. (if P x then SNOC x l' else l')) [] l

FILTER_FOLDR

|- !P l. FILTER P l = FOLDR (\x l'. (if P x then x::l' else l')) [] l

FILTER_IDEM

|- !f l. FILTER f (FILTER f l) = FILTER f l

FILTER_MAP

|- !f1 f2 l. FILTER f1 (MAP f2 l) = MAP f2 (FILTER (f1 o f2) l)

FILTER_REVERSE

|- !P l. FILTER P (REVERSE l) = REVERSE (FILTER P l)

FILTER_SNOC

|- !P x l.
     FILTER P (SNOC x l) = (if P x then SNOC x (FILTER P l) else FILTER P l)

FIRSTN_APPEND1

|- !n l1. n <= LENGTH l1 ==> !l2. FIRSTN n (APPEND l1 l2) = FIRSTN n l1

FIRSTN_APPEND2

|- !l1 n.
     LENGTH l1 <= n ==>
     !l2. FIRSTN n (APPEND l1 l2) = APPEND l1 (FIRSTN (n - LENGTH l1) l2)

FIRSTN_BUTLASTN

|- !n l. n <= LENGTH l ==> (FIRSTN n l = BUTLASTN (LENGTH l - n) l)

FIRSTN_FIRSTN

|- !m l. m <= LENGTH l ==> !n. n <= m ==> (FIRSTN n (FIRSTN m l) = FIRSTN n l)

FIRSTN_LENGTH_APPEND

|- !l1 l2. FIRSTN (LENGTH l1) (APPEND l1 l2) = l1

FIRSTN_LENGTH_ID

|- !l. FIRSTN (LENGTH l) l = l

FIRSTN_REVERSE

|- !n l. n <= LENGTH l ==> (FIRSTN n (REVERSE l) = REVERSE (LASTN n l))

FIRSTN_SEG

|- !n l. n <= LENGTH l ==> (FIRSTN n l = SEG n 0 l)

FIRSTN_SNOC

|- !n l. n <= LENGTH l ==> !x. FIRSTN n (SNOC x l) = FIRSTN n l

FLAT

|- (FLAT [] = []) /\ !x l. FLAT (x::l) = APPEND x (FLAT l)

FLAT_APPEND

|- !l1 l2. FLAT (APPEND l1 l2) = APPEND (FLAT l1) (FLAT l2)

FLAT_FLAT

|- !l. FLAT (FLAT l) = FLAT (MAP FLAT l)

FLAT_FOLDL

|- !l. FLAT l = FOLDL APPEND [] l

FLAT_FOLDR

|- !l. FLAT l = FOLDR APPEND [] l

FLAT_REVERSE

|- !l. FLAT (REVERSE l) = REVERSE (FLAT (MAP REVERSE l))

FLAT_SNOC

|- !x l. FLAT (SNOC x l) = APPEND (FLAT l) x

FOLDL

|- (!f e. FOLDL f e [] = e) /\ !f e x l. FOLDL f e (x::l) = FOLDL f (f e x) l

FOLDL_APPEND

|- !f e l1 l2. FOLDL f e (APPEND l1 l2) = FOLDL f (FOLDL f e l1) l2

FOLDL_FILTER

|- !f e P l.
     FOLDL f e (FILTER P l) = FOLDL (\x y. (if P y then f x y else x)) e l

FOLDL_FOLDR_REVERSE

|- !f e l. FOLDL f e l = FOLDR (\x y. f y x) e (REVERSE l)

FOLDL_MAP

|- !f e g l. FOLDL f e (MAP g l) = FOLDL (\x y. f x (g y)) e l

FOLDL_REVERSE

|- !f e l. FOLDL f e (REVERSE l) = FOLDR (\x y. f y x) e l

FOLDL_SINGLE

|- !f e x. FOLDL f e [x] = f e x

FOLDL_SNOC

|- !f e x l. FOLDL f e (SNOC x l) = f (FOLDL f e l) x

FOLDL_SNOC_NIL

|- !l. FOLDL (\xs x. SNOC x xs) [] l = l

FOLDR

|- (!f e. FOLDR f e [] = e) /\ !f e x l. FOLDR f e (x::l) = f x (FOLDR f e l)

FOLDR_APPEND

|- !f e l1 l2. FOLDR f e (APPEND l1 l2) = FOLDR f (FOLDR f e l2) l1

FOLDR_CONS_NIL

|- !l. FOLDR CONS [] l = l

FOLDR_FILTER

|- !f e P l.
     FOLDR f e (FILTER P l) = FOLDR (\x y. (if P x then f x y else y)) e l

FOLDR_FILTER_REVERSE

|- !f.
     (!a b c. f a (f b c) = f b (f a c)) ==>
     !e P l. FOLDR f e (FILTER P (REVERSE l)) = FOLDR f e (FILTER P l)

FOLDR_FOLDL

|- !f e. MONOID f e ==> !l. FOLDR f e l = FOLDL f e l

FOLDR_FOLDL_REVERSE

|- !f e l. FOLDR f e l = FOLDL (\x y. f y x) e (REVERSE l)

FOLDR_MAP

|- !f e g l. FOLDR f e (MAP g l) = FOLDR (\x y. f (g x) y) e l

FOLDR_MAP_REVERSE

|- !f.
     (!a b c. f a (f b c) = f b (f a c)) ==>
     !e g l. FOLDR f e (MAP g (REVERSE l)) = FOLDR f e (MAP g l)

FOLDR_REVERSE

|- !f e l. FOLDR f e (REVERSE l) = FOLDL (\x y. f y x) e l

FOLDR_SINGLE

|- !f e x. FOLDR f e [x] = f x e

FOLDR_SNOC

|- !f e x l. FOLDR f e (SNOC x l) = FOLDR f (f x e) l

HD

|- !x l. HD (x::l) = x

IS_EL

|- (!x. IS_EL x [] = F) /\ !y x l. IS_EL y (x::l) = (y = x) \/ IS_EL y l

IS_EL_APPEND

|- !l1 l2 x. IS_EL x (APPEND l1 l2) = IS_EL x l1 \/ IS_EL x l2

IS_EL_BUTFIRSTN

|- !m l. m <= LENGTH l ==> !x. IS_EL x (BUTFIRSTN m l) ==> IS_EL x l

IS_EL_BUTLASTN

|- !m l. m <= LENGTH l ==> !x. IS_EL x (BUTLASTN m l) ==> IS_EL x l

IS_EL_FILTER

|- !P x. P x ==> !l. IS_EL x (FILTER P l) = IS_EL x l

IS_EL_FIRSTN

|- !m l. m <= LENGTH l ==> !x. IS_EL x (FIRSTN m l) ==> IS_EL x l

IS_EL_FOLDL

|- !y l. IS_EL y l = FOLDL (\l' x. l' \/ (y = x)) F l

IS_EL_FOLDL_MAP

|- !x l. IS_EL x l = FOLDL $\/ F (MAP ($= x) l)

IS_EL_FOLDR

|- !y l. IS_EL y l = FOLDR (\x l'. (y = x) \/ l') F l

IS_EL_FOLDR_MAP

|- !x l. IS_EL x l = FOLDR $\/ F (MAP ($= x) l)

IS_EL_LASTN

|- !m l. m <= LENGTH l ==> !x. IS_EL x (LASTN m l) ==> IS_EL x l

IS_EL_REPLICATE

|- !n. 0 < n ==> !x. IS_EL x (REPLICATE n x)

IS_EL_REVERSE

|- !x l. IS_EL x (REVERSE l) = IS_EL x l

IS_EL_SEG

|- !n m l. n + m <= LENGTH l ==> !x. IS_EL x (SEG n m l) ==> IS_EL x l

IS_EL_SNOC

|- !y x l. IS_EL y (SNOC x l) = (y = x) \/ IS_EL y l

IS_EL_SOME_EL

|- !x l. IS_EL x l = SOME_EL ($= x) l

IS_PREFIX_APPEND

|- !l1 l2. IS_PREFIX l1 l2 = ?l. l1 = APPEND l2 l

IS_PREFIX_IS_SUBLIST

|- !l1 l2. IS_PREFIX l1 l2 ==> IS_SUBLIST l1 l2

IS_PREFIX_PREFIX

|- !P l. IS_PREFIX l (PREFIX P l)

IS_PREFIX_REVERSE

|- !l1 l2. IS_PREFIX (REVERSE l1) (REVERSE l2) = IS_SUFFIX l1 l2

IS_SUBLIST_APPEND

|- !l1 l2. IS_SUBLIST l1 l2 = ?l l'. l1 = APPEND l (APPEND l2 l')

IS_SUBLIST_REVERSE

|- !l1 l2. IS_SUBLIST (REVERSE l1) (REVERSE l2) = IS_SUBLIST l1 l2

IS_SUFFIX_APPEND

|- !l1 l2. IS_SUFFIX l1 l2 = ?l. l1 = APPEND l l2

IS_SUFFIX_IS_SUBLIST

|- !l1 l2. IS_SUFFIX l1 l2 ==> IS_SUBLIST l1 l2

IS_SUFFIX_REVERSE

|- !l2 l1. IS_SUFFIX (REVERSE l1) (REVERSE l2) = IS_PREFIX l1 l2

LAST

|- !x l. LAST (SNOC x l) = x

LAST_CONS

|- (!x. LAST [x] = x) /\ !x y z. LAST (x::y::z) = LAST (y::z)

LAST_LASTN_LAST

|- !n l. n <= LENGTH l ==> 0 < n ==> (LAST (LASTN n l) = LAST l)

LASTN_1

|- !l. ~(l = []) ==> (LASTN 1 l = [LAST l])

LASTN_APPEND1

|- !l2 n.
     LENGTH l2 <= n ==>
     !l1. LASTN n (APPEND l1 l2) = APPEND (LASTN (n - LENGTH l2) l1) l2

LASTN_APPEND2

|- !n l2. n <= LENGTH l2 ==> !l1. LASTN n (APPEND l1 l2) = LASTN n l2

LASTN_BUTFIRSTN

|- !n l. n <= LENGTH l ==> (LASTN n l = BUTFIRSTN (LENGTH l - n) l)

LASTN_BUTLASTN

|- !n m l.
     n + m <= LENGTH l ==>
     (LASTN n (BUTLASTN m l) = BUTLASTN m (LASTN (n + m) l))

LASTN_CONS

|- !n l. n <= LENGTH l ==> !x. LASTN n (x::l) = LASTN n l

LASTN_LASTN

|- !l n m. m <= LENGTH l ==> n <= m ==> (LASTN n (LASTN m l) = LASTN n l)

LASTN_LENGTH_APPEND

|- !l2 l1. LASTN (LENGTH l2) (APPEND l1 l2) = l2

LASTN_LENGTH_ID

|- !l. LASTN (LENGTH l) l = l

LASTN_MAP

|- !n l. n <= LENGTH l ==> !f. LASTN n (MAP f l) = MAP f (LASTN n l)

LASTN_REVERSE

|- !n l. n <= LENGTH l ==> (LASTN n (REVERSE l) = REVERSE (FIRSTN n l))

LASTN_SEG

|- !n l. n <= LENGTH l ==> (LASTN n l = SEG n (LENGTH l - n) l)

LENGTH

|- (LENGTH [] = 0) /\ !x l. LENGTH (x::l) = SUC (LENGTH l)

LENGTH_APPEND

|- !l1 l2. LENGTH (APPEND l1 l2) = LENGTH l1 + LENGTH l2

LENGTH_BUTFIRSTN

|- !n l. n <= LENGTH l ==> (LENGTH (BUTFIRSTN n l) = LENGTH l - n)

LENGTH_BUTLAST

|- !l. ~(l = []) ==> (LENGTH (BUTLAST l) = PRE (LENGTH l))

LENGTH_BUTLASTN

|- !n l. n <= LENGTH l ==> (LENGTH (BUTLASTN n l) = LENGTH l - n)

LENGTH_CONS

|- !l n. (LENGTH l = SUC n) = ?x l'. (LENGTH l' = n) /\ (l = x::l')

LENGTH_EQ

|- !x y. (x = y) ==> (LENGTH x = LENGTH y)

LENGTH_EQ_NIL

|- !P. (!l. (LENGTH l = 0) ==> P l) = P []

LENGTH_FIRSTN

|- !n l. n <= LENGTH l ==> (LENGTH (FIRSTN n l) = n)

LENGTH_FLAT

|- !l. LENGTH (FLAT l) = SUM (MAP LENGTH l)

LENGTH_FOLDL

|- !l. LENGTH l = FOLDL (\l' x. SUC l') 0 l

LENGTH_FOLDR

|- !l. LENGTH l = FOLDR (\x l'. SUC l') 0 l

LENGTH_GENLIST

|- !f n. LENGTH (GENLIST f n) = n

LENGTH_LASTN

|- !n l. n <= LENGTH l ==> (LENGTH (LASTN n l) = n)

LENGTH_MAP

|- !l f. LENGTH (MAP f l) = LENGTH l

LENGTH_MAP2

|- !l1 l2.
     (LENGTH l1 = LENGTH l2) ==>
     !f.
       (LENGTH (MAP2 f l1 l2) = LENGTH l1) /\
       (LENGTH (MAP2 f l1 l2) = LENGTH l2)

LENGTH_NIL

|- !l. (LENGTH l = 0) = (l = [])

LENGTH_NOT_NULL

|- !l. 0 < LENGTH l = ~NULL l

LENGTH_REPLICATE

|- !n x. LENGTH (REPLICATE n x) = n

LENGTH_REVERSE

|- !l. LENGTH (REVERSE l) = LENGTH l

LENGTH_SCANL

|- !f e l. LENGTH (SCANL f e l) = SUC (LENGTH l)

LENGTH_SCANR

|- !f e l. LENGTH (SCANR f e l) = SUC (LENGTH l)

LENGTH_SEG

|- !n k l. n + k <= LENGTH l ==> (LENGTH (SEG n k l) = n)

LENGTH_SNOC

|- !x l. LENGTH (SNOC x l) = SUC (LENGTH l)

LENGTH_UNZIP_FST

|- !l. LENGTH (UNZIP_FST l) = LENGTH l

LENGTH_UNZIP_SND

|- !l. LENGTH (UNZIP_SND l) = LENGTH l

LENGTH_ZIP

|- !l1 l2.
     (LENGTH l1 = LENGTH l2) ==>
     (LENGTH (ZIP (l1,l2)) = LENGTH l1) /\ (LENGTH (ZIP (l1,l2)) = LENGTH l2)

list_CASES

|- !l. (l = []) \/ ?t h. l = h::t

list_INDUCT

|- !P. P [] /\ (!l. P l ==> !x. P (x::l)) ==> !l. P l

LIST_NOT_EQ

|- !l1 l2. ~(l1 = l2) ==> !x1 x2. ~(x1::l1 = x2::l2)

MAP

|- (!f. MAP f [] = []) /\ !f x l. MAP f (x::l) = f x::MAP f l

MAP2

|- (!f. MAP2 f [] [] = []) /\
   !f x1 l1 x2 l2. MAP2 f (x1::l1) (x2::l2) = f x1 x2::MAP2 f l1 l2

MAP2_ZIP

|- !l1 l2.
     (LENGTH l1 = LENGTH l2) ==>
     !f. MAP2 f l1 l2 = MAP (UNCURRY f) (ZIP (l1,l2))

MAP_APPEND

|- !f l1 l2. MAP f (APPEND l1 l2) = APPEND (MAP f l1) (MAP f l2)

MAP_FILTER

|- !f P l. (!x. P (f x) = P x) ==> (MAP f (FILTER P l) = FILTER P (MAP f l))

MAP_FLAT

|- !f l. MAP f (FLAT l) = FLAT (MAP (MAP f) l)

MAP_FOLDL

|- !f l. MAP f l = FOLDL (\l' x. SNOC (f x) l') [] l

MAP_FOLDR

|- !f l. MAP f l = FOLDR (\x l'. f x::l') [] l

MAP_MAP_o

|- !f g l. MAP f (MAP g l) = MAP (f o g) l

MAP_o

|- !f g. MAP (f o g) = MAP f o MAP g

MAP_REVERSE

|- !f l. MAP f (REVERSE l) = REVERSE (MAP f l)

MAP_SNOC

|- !f x l. MAP f (SNOC x l) = SNOC (f x) (MAP f l)

MONOID_APPEND_NIL

|- MONOID APPEND []

NOT_ALL_EL_SOME_EL

|- !P l. ~ALL_EL P l = SOME_EL ($~ o P) l

NOT_CONS_NIL

|- !x l. ~(x::l = [])

NOT_EQ_LIST

|- !x1 x2. ~(x1 = x2) ==> !l1 l2. ~(x1::l1 = x2::l2)

NOT_NIL_CONS

|- !x l. ~([] = x::l)

NOT_NIL_SNOC

|- !x l. ~([] = SNOC x l)

NOT_SNOC_NIL

|- !x l. ~(SNOC x l = [])

NOT_SOME_EL_ALL_EL

|- !P l. ~SOME_EL P l = ALL_EL ($~ o P) l

NULL

|- NULL [] /\ !x l. ~NULL (x::l)

NULL_DEF

|- (NULL [] = T) /\ !x l. NULL (x::l) = F

NULL_EQ_NIL

|- !l. NULL l = (l = [])

NULL_FOLDL

|- !l. NULL l = FOLDL (\x l'. F) T l

NULL_FOLDR

|- !l. NULL l = FOLDR (\x l'. F) T l

OR_EL_FOLDL

|- !l. OR_EL l = FOLDL $\/ F l

OR_EL_FOLDR

|- !l. OR_EL l = FOLDR $\/ F l

PREFIX

|- (!P. PREFIX P [] = []) /\
   !P x l. PREFIX P (x::l) = (if P x then x::PREFIX P l else [])

PREFIX_FOLDR

|- !P l. PREFIX P l = FOLDR (\x l'. (if P x then x::l' else [])) [] l

REVERSE_APPEND

|- !l1 l2. REVERSE (APPEND l1 l2) = APPEND (REVERSE l2) (REVERSE l1)

REVERSE_EQ_NIL

|- !l. (REVERSE l = []) = (l = [])

REVERSE_FLAT

|- !l. REVERSE (FLAT l) = FLAT (REVERSE (MAP REVERSE l))

REVERSE_FOLDL

|- !l. REVERSE l = FOLDL (\l' x. x::l') [] l

REVERSE_FOLDR

|- !l. REVERSE l = FOLDR SNOC [] l

REVERSE_REVERSE

|- !l. REVERSE (REVERSE l) = l

REVERSE_SNOC

|- !x l. REVERSE (SNOC x l) = x::REVERSE l

SEG_0_SNOC

|- !m l x. m <= LENGTH l ==> (SEG m 0 (SNOC x l) = SEG m 0 l)

SEG_APPEND

|- !m l1 n l2.
     m < LENGTH l1 /\ LENGTH l1 <= n + m /\ n + m <= LENGTH l1 + LENGTH l2 ==>
     (SEG n m (APPEND l1 l2) =
      APPEND (SEG (LENGTH l1 - m) m l1) (SEG (n + m - LENGTH l1) 0 l2))

SEG_APPEND1

|- !n m l1. n + m <= LENGTH l1 ==> !l2. SEG n m (APPEND l1 l2) = SEG n m l1

SEG_APPEND2

|- !l1 m n l2.
     LENGTH l1 <= m /\ n <= LENGTH l2 ==>
     (SEG n m (APPEND l1 l2) = SEG n (m - LENGTH l1) l2)

SEG_FIRSTN_BUTFISTN

|- !n m l. n + m <= LENGTH l ==> (SEG n m l = FIRSTN n (BUTFIRSTN m l))

SEG_LASTN_BUTLASTN

|- !n m l.
     n + m <= LENGTH l ==>
     (SEG n m l = LASTN n (BUTLASTN (LENGTH l - (n + m)) l))

SEG_LENGTH_ID

|- !l. SEG (LENGTH l) 0 l = l

SEG_LENGTH_SNOC

|- !l x. SEG 1 (LENGTH l) (SNOC x l) = [x]

SEG_REVERSE

|- !n m l.
     n + m <= LENGTH l ==>
     (SEG n m (REVERSE l) = REVERSE (SEG n (LENGTH l - (n + m)) l))

SEG_SEG

|- !n1 m1 n2 m2 l.
     n1 + m1 <= LENGTH l /\ n2 + m2 <= n1 ==>
     (SEG n2 m2 (SEG n1 m1 l) = SEG n2 (m1 + m2) l)

SEG_SNOC

|- !n m l. n + m <= LENGTH l ==> !x. SEG n m (SNOC x l) = SEG n m l

SEG_SUC_CONS

|- !m n l x. SEG m (SUC n) (x::l) = SEG m n l

SNOC_11

|- !x l x' l'. (SNOC x l = SNOC x' l') = (x = x') /\ (l = l')

SNOC_APPEND

|- !x l. SNOC x l = APPEND l [x]

SNOC_Axiom

|- !e f. ?fn. (fn [] = e) /\ !x l. fn (SNOC x l) = f x l (fn l)

SNOC_CASES

|- !l. (l = []) \/ ?x l'. l = SNOC x l'

SNOC_EQ_LENGTH_EQ

|- !x1 l1 x2 l2. (SNOC x1 l1 = SNOC x2 l2) ==> (LENGTH l1 = LENGTH l2)

SNOC_FOLDR

|- !x l. SNOC x l = FOLDR CONS [x] l

SNOC_INDUCT

|- !P. P [] /\ (!l. P l ==> !x. P (SNOC x l)) ==> !l. P l

SNOC_REVERSE_CONS

|- !x l. SNOC x l = REVERSE (x::REVERSE l)

SOME_EL_APPEND

|- !P l1 l2. SOME_EL P (APPEND l1 l2) = SOME_EL P l1 \/ SOME_EL P l2

SOME_EL_BUTFIRSTN

|- !m l. m <= LENGTH l ==> !P. SOME_EL P (BUTFIRSTN m l) ==> SOME_EL P l

SOME_EL_BUTLASTN

|- !m l. m <= LENGTH l ==> !P. SOME_EL P (BUTLASTN m l) ==> SOME_EL P l

SOME_EL_DISJ

|- !P Q l. SOME_EL (\x. P x \/ Q x) l = SOME_EL P l \/ SOME_EL Q l

SOME_EL_FIRSTN

|- !m l. m <= LENGTH l ==> !P. SOME_EL P (FIRSTN m l) ==> SOME_EL P l

SOME_EL_FOLDL

|- !P l. SOME_EL P l = FOLDL (\l' x. l' \/ P x) F l

SOME_EL_FOLDL_MAP

|- !P l. SOME_EL P l = FOLDL $\/ F (MAP P l)

SOME_EL_FOLDR

|- !P l. SOME_EL P l = FOLDR (\x l'. P x \/ l') F l

SOME_EL_FOLDR_MAP

|- !P l. SOME_EL P l = FOLDR $\/ F (MAP P l)

SOME_EL_LASTN

|- !m l. m <= LENGTH l ==> !P. SOME_EL P (LASTN m l) ==> SOME_EL P l

SOME_EL_MAP

|- !P f l. SOME_EL P (MAP f l) = SOME_EL (P o f) l

SOME_EL_REVERSE

|- !P l. SOME_EL P (REVERSE l) = SOME_EL P l

SOME_EL_SEG

|- !m k l. m + k <= LENGTH l ==> !P. SOME_EL P (SEG m k l) ==> SOME_EL P l

SOME_EL_SNOC

|- !P x l. SOME_EL P (SNOC x l) = P x \/ SOME_EL P l

SUM

|- (SUM [] = 0) /\ !x l. SUM (x::l) = x + SUM l

SUM_APPEND

|- !l1 l2. SUM (APPEND l1 l2) = SUM l1 + SUM l2

SUM_FLAT

|- !l. SUM (FLAT l) = SUM (MAP SUM l)

SUM_FOLDL

|- !l. SUM l = FOLDL $+ 0 l

SUM_FOLDR

|- !l. SUM l = FOLDR $+ 0 l

SUM_REVERSE

|- !l. SUM (REVERSE l) = SUM l

SUM_SNOC

|- !x l. SUM (SNOC x l) = SUM l + x

TL

|- !x l. TL (x::l) = l

TL_SNOC

|- !x l. TL (SNOC x l) = (if NULL l then [] else SNOC x (TL l))

UNZIP

|- (UNZIP [] = ([],[])) /\
   !x l. UNZIP (x::l) = (FST x::FST (UNZIP l),SND x::SND (UNZIP l))

UNZIP_SNOC

|- !x l.
     UNZIP (SNOC x l) =
     (SNOC (FST x) (FST (UNZIP l)),SNOC (SND x) (SND (UNZIP l)))

UNZIP_ZIP

|- !l1 l2. (LENGTH l1 = LENGTH l2) ==> (UNZIP (ZIP (l1,l2)) = (l1,l2))

ZIP

|- (ZIP ([],[]) = []) /\
   !x1 l1 x2 l2. ZIP (x1::l1,x2::l2) = (x1,x2)::ZIP (l1,l2)

ZIP_SNOC

|- !l1 l2.
     (LENGTH l1 = LENGTH l2) ==>
     !x1 x2. ZIP (SNOC x1 l1,SNOC x2 l2) = SNOC (x1,x2) (ZIP (l1,l2))

ZIP_UNZIP

|- !l. ZIP (UNZIP l) = l