Theory: list

Parents

Types

list(Arity = 1)

Constants

FLAT :'a list list -> 'a list
LENGTH :'a list -> num
MAP2 :('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
EL :num -> 'a list -> 'a
HD :'a list -> 'a
TL :'a list -> 'a list
FOLDL :('b -> 'a -> 'b) -> 'b -> 'a list -> 'b
FOLDR :('a -> 'b -> 'b) -> 'b -> 'a list -> 'b
UNZIP :('a # 'b) list -> 'a list # 'b list
list_size :('a -> num) -> 'a list -> num
EVERY :('a -> bool) -> 'a list -> bool
NULL :'a list -> bool
ii_internal_dest_list :'a list -> 'a recspace
ii_internallist0 :'a list
ii_internallist1 :'a -> 'a list -> 'a list
FILTER :('a -> bool) -> 'a list -> 'a list
ii_internal_mk_list :'a recspace -> 'a list
list_case :'b -> ('a -> 'a list -> 'b) -> 'a list -> 'b
MAP :('a -> 'b) -> 'a list -> 'b list
MEM :'a -> 'a list -> bool
NIL :'a list
EXISTS :('a -> bool) -> 'a list -> bool
APPEND :'a list -> 'a list -> 'a list
SUM :num list -> num
ZIP :'a list # 'b list -> ('a # 'b) list
CONS :'a -> 'a list -> 'a list

Definitions

APPEND

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

CONS_def

|- CONS = ii_internallist1

EL

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

EVERY_DEF

|- (!P. EVERY P [] = T) /\ !P h t. EVERY P (h::t) = P h /\ EVERY P t

EXISTS_DEF

|- (!P. EXISTS P [] = F) /\ !P h t. EXISTS P (h::t) = P h \/ EXISTS P t

FILTER

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

FLAT

|- (FLAT [] = []) /\ !h t. FLAT (h::t) = APPEND h (FLAT t)

FOLDL

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

FOLDR

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

HD

|- !h t. HD (h::t) = h

ii_internallist0_def

|- ii_internallist0 = ii_internal_mk_list (CONSTR 0 (@v. T) (\n. BOTTOM))

ii_internallist1_def

|- ii_internallist1 =
   (\a0 a1.
      ii_internal_mk_list
        ((\a0 a1. CONSTR (SUC 0) a0 (FCONS a1 (\n. BOTTOM))) a0
           (ii_internal_dest_list a1)))

LENGTH

|- (LENGTH [] = 0) /\ !h t. LENGTH (h::t) = SUC (LENGTH t)

list_case_def

|- (!v f. list_case v f [] = v) /\
   !v f a0 a1. list_case v f (a0::a1) = f a0 a1

list_repfns

|- (!a. ii_internal_mk_list (ii_internal_dest_list a) = a) /\
   !r.
     (\a0'.
        !'list'.
          (!a0'.
             (a0' = CONSTR 0 (@v. T) (\n. BOTTOM)) \/
             (?a0 a1.
                (a0' =
                 (\a0 a1. CONSTR (SUC 0) a0 (FCONS a1 (\n. BOTTOM))) a0 a1) /\
                'list' a1) ==>
             'list' a0') ==>
          'list' a0') r =
     (ii_internal_dest_list (ii_internal_mk_list r) = r)

list_size_def

|- (!f. list_size f [] = 0) /\
   !f a0 a1. list_size f (a0::a1) = 1 + (f a0 + list_size f a1)

list_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a0'.
          !'list'.
            (!a0'.
               (a0' = CONSTR 0 (@v. T) (\n. BOTTOM)) \/
               (?a0 a1.
                  (a0' =
                   (\a0 a1. CONSTR (SUC 0) a0 (FCONS a1 (\n. BOTTOM))) a0
                     a1) /\ 'list' a1) ==>
               'list' a0') ==>
            'list' a0') rep

MAP

|- (!f. MAP f [] = []) /\ !f h t. MAP f (h::t) = f h::MAP f t

MAP2

|- (!f. MAP2 f [] [] = []) /\
   !f h1 t1 h2 t2. MAP2 f (h1::t1) (h2::t2) = f h1 h2::MAP2 f t1 t2

MEM

|- (!x. MEM x [] = F) /\ !x h t. MEM x (h::t) = (x = h) \/ MEM x t

NIL

|- [] = ii_internallist0

NULL_DEF

|- (NULL [] = T) /\ !h t. NULL (h::t) = F

SUM

|- (SUM [] = 0) /\ !h t. SUM (h::t) = h + SUM t

TL

|- !h t. TL (h::t) = t

UNZIP

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

ZIP

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

Theorems

APPEND_11

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

APPEND_ASSOC

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

APPEND_eq_NIL

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

APPEND_NIL

|- !l. APPEND l [] = l

CONS

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

CONS_11

|- !a0 a1 a0' a1'. (a0::a1 = a0'::a1') = (a0 = a0') /\ (a1 = a1')

CONS_ACYCLIC

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

EL_compute

|- !n. EL n l = (if n = 0 then HD l else EL (PRE n) (TL l))

EL_ZIP

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

EQ_LIST

|- !h1 h2. (h1 = h2) ==> !l1 l2. (l1 = l2) ==> (h1::l1 = h2::l2)

EVERY_APPEND

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

EVERY_CONG

|- !l1 l2 P P'.
     (l1 = l2) /\ (!x. MEM x l2 ==> (P x = P' x)) ==>
     (EVERY P l1 = EVERY P' l2)

EVERY_CONJ

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

EVERY_EL

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

EVERY_MEM

|- !P l. EVERY P l = !e. MEM e l ==> P e

EVERY_MONOTONIC

|- !P Q. (!x. P x ==> Q x) ==> !l. EVERY P l ==> EVERY Q l

EXISTS_APPEND

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

EXISTS_CONG

|- !l1 l2 P P'.
     (l1 = l2) /\ (!x. MEM x l2 ==> (P x = P' x)) ==>
     (EXISTS P l1 = EXISTS P' l2)

EXISTS_MEM

|- !P l. EXISTS P l = ?e. MEM e l /\ P e

FOLDL_CONG

|- !l l' b b' f f'.
     (l = l') /\ (b = b') /\ (!x a. MEM x l' ==> (f a x = f' a x)) ==>
     (FOLDL f b l = FOLDL f' b' l')

FOLDR_CONG

|- !l l' b b' f f'.
     (l = l') /\ (b = b') /\ (!x a. MEM x l' ==> (f x a = f' x a)) ==>
     (FOLDR f b l = FOLDR f' b' l')

LENGTH_APPEND

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

LENGTH_CONS

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

LENGTH_EQ_CONS

|- !P n.
     (!l. (LENGTH l = SUC n) ==> P l) =
     !l. (LENGTH l = n) ==> (\l. !x. P (x::l)) l

LENGTH_EQ_NIL

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

LENGTH_MAP

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

LENGTH_NIL

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

LENGTH_UNZIP

|- !pl.
     (LENGTH (FST (UNZIP pl)) = LENGTH pl) /\
     (LENGTH (SND (UNZIP pl)) = LENGTH pl)

LENGTH_ZIP

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

list_11

|- !a0 a1 a0' a1'. (a0::a1 = a0'::a1') = (a0 = a0') /\ (a1 = a1')

list_Axiom

|- !f0 f1. ?fn. (fn [] = f0) /\ !a0 a1. fn (a0::a1) = f1 a0 a1 (fn a1)

list_Axiom_old

|- !x f. ?!fn1. (fn1 [] = x) /\ !h t. fn1 (h::t) = f (fn1 t) h t

list_case_compute

|- !l. list_case b f l = (if NULL l then b else f (HD l) (TL l))

list_case_cong

|- !f' f v' v M' M.
     (M = M') /\ ((M' = []) ==> (v = v')) /\
     (!a0 a1. (M' = a0::a1) ==> (f a0 a1 = f' a0 a1)) ==>
     (list_case v f M = list_case v' f' M')

list_CASES

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

list_distinct

|- !a1 a0. ~([] = a0::a1)

list_INDUCT

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

list_induction

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

list_nchotomy

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

LIST_NOT_EQ

|- !l1 l2. ~(l1 = l2) ==> !h1 h2. ~(h1::l1 = h2::l2)

list_size_cong

|- !M N f f'.
     (M = N) /\ (!x. MEM x N ==> (f x = f' x)) ==>
     (list_size f M = list_size f' N)

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_CONG

|- !l1 l2 f f'.
     (l1 = l2) /\ (!x. MEM x l2 ==> (f x = f' x)) ==> (MAP f l1 = MAP f' l2)

MAP_EQ_NIL

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

MEM_EL

|- !l x. MEM x l = ?n. n < LENGTH l /\ (x = EL n l)

MEM_MAP

|- !l f x. MEM x (MAP f l) = ?y. (x = f y) /\ MEM y l

MEM_ZIP

|- !l1 l2 p.
     (LENGTH l1 = LENGTH l2) ==>
     (MEM p (ZIP (l1,l2)) = ?n. n < LENGTH l1 /\ (p = (EL n l1,EL n l2)))

NOT_CONS_NIL

|- !a1 a0. ~(a0::a1 = [])

NOT_EQ_LIST

|- !h1 h2. ~(h1 = h2) ==> !l1 l2. ~(h1::l1 = h2::l2)

NOT_EVERY

|- !P l. ~EVERY P l = EXISTS ($~ o P) l

NOT_EXISTS

|- !P l. ~EXISTS P l = EVERY ($~ o P) l

NOT_NIL_CONS

|- !a1 a0. ~([] = a0::a1)

NULL

|- NULL [] /\ !h t. ~NULL (h::t)

UNZIP_ZIP

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

WF_LIST_PRED

|- WF (\L1 L2. ?h. L2 = h::L1)

ZIP_MAP

|- !l1 l2 f1 f2.
     (LENGTH l1 = LENGTH l2) ==>
     (ZIP (MAP f1 l1,l2) = MAP (\p. (f1 (FST p),SND p)) (ZIP (l1,l2))) /\
     (ZIP (l1,MAP f2 l2) = MAP (\p. (FST p,f2 (SND p))) (ZIP (l1,l2)))

ZIP_UNZIP

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