Theory "list"

Parents ind_type

Signature

Type	Arity
list	1
Constant	Type
mk_list	:'a recspace -> 'a list
list_size	:('a -> num) -> 'a list -> num
list_case	:'b -> ('a -> 'a list -> 'b) -> 'a list -> 'b
listRel	:('a -> 'b -> bool) -> 'a list -> 'b list -> bool
list1	:'a -> 'a list -> 'a list
list0	:'a list
dest_list	:'a list -> 'a recspace
ZIP	:'a list # 'b list -> ('a # 'b) list
UNZIP	:('a # 'b) list -> 'a list # 'b list
TL	:'a list -> 'a list
SUM	:num list -> num
REVERSE	:'a list -> 'a list
REV	:'a list -> 'a list -> 'a list
NULL	:'a list -> bool
NIL	:'a list
MEM	:'a -> 'a list -> bool
MAP2	:('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
MAP	:('a -> 'b) -> 'a list -> 'b list
LIST_TO_SET	:'a list -> 'a -> bool
LENGTH	:'a list -> num
LEN	:'a list -> num -> num
LAST	:'a list -> 'a
HD	:'a list -> 'a
FRONT	:'a list -> 'a list
FOLDR	:('a -> 'b -> 'b) -> 'b -> 'a list -> 'b
FOLDL	:('b -> 'a -> 'b) -> 'b -> 'a list -> 'b
FLAT	:'a list list -> 'a list
FILTER	:('a -> bool) -> 'a list -> 'a list
EXISTS	:('a -> bool) -> 'a list -> bool
EVERY	:('a -> bool) -> 'a list -> bool
EL	:num -> 'a list -> 'a
CONS	:'a -> 'a list -> 'a list
APPEND	:'a list -> 'a list -> 'a list
ALL_DISTINCT	:'a list -> bool

Definitions

MAP2

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

EL

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

EXISTS_DEF

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

EVERY_DEF

|- (!P. EVERY P [] = T) /\ !P h t. EVERY P (h::t) = P h /\ EVERY P 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)

FILTER

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

MEM

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

MAP

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

LENGTH

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

FLAT

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

APPEND

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

SUM

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

TL

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

HD

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

NULL_DEF

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

list_TY_DEF

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

list_repfns

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

list0_def

|- list0 = mk_list (ind_type$CONSTR 0 (@v. T) (\n. ind_type$BOTTOM))

list1_def

|- list1 =
   (\a0 a1.
      mk_list
        ((\a0 a1. ind_type$CONSTR (SUC 0) a0 (FCONS a1 (\n. ind_type$BOTTOM)))
           a0 (dest_list a1)))

NIL

|- [] = list0

CONS_def

|- CONS = list1

list_case_def

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

list_size_def

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

ZIP

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

UNZIP

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

REVERSE_DEF

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

LAST_DEF

|- !h t. LAST (h::t) = (if t = [] then h else LAST t)

FRONT_DEF

|- !h t. FRONT (h::t) = (if t = [] then [] else h::FRONT t)

ALL_DISTINCT

|- (ALL_DISTINCT [] = T) /\
   !h t. ALL_DISTINCT (h::t) = ~MEM h t /\ ALL_DISTINCT t

LIST_TO_SET

|- LIST_TO_SET = combin$C MEM

listRel

|- listRel =
   (\R a0 a1.
      !listRel'.
        (!a0 a1.
           (a0 = []) /\ (a1 = []) \/
           (?h1 h2 t1 t2.
              (a0 = h1::t1) /\ (a1 = h2::t2) /\ R h1 h2 /\ listRel' t1 t2) ==>
           listRel' a0 a1) ==>
        listRel' a0 a1)

LEN_DEF

|- (!n. LEN [] n = n) /\ !h t n. LEN (h::t) n = LEN t (n + 1)

REV_DEF

|- (!acc. REV [] acc = acc) /\ !h t acc. REV (h::t) acc = REV t (h::acc)

Theorems

list_CASES

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

FORALL_LIST

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

list_induction

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

list_Axiom

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

list_INDUCT

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

NULL

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

list_Axiom_old

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

datatype_list

|- DATATYPE (list [] CONS)

list_11

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

list_distinct

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

list_case_cong

|- !M M' v f.
     (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_nchotomy

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

list_case_compute

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

CONS_11

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

NOT_NIL_CONS

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

NOT_CONS_NIL

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

LIST_NOT_EQ

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

NOT_EQ_LIST

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

EQ_LIST

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

CONS

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

APPEND_NIL

|- !l. l ++ [] = l

APPEND_ASSOC

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

LENGTH_APPEND

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

MAP_APPEND

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

LENGTH_MAP

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

MAP_EQ_NIL

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

EVERY_EL

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

EVERY_CONJ

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

EVERY_MEM

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

EVERY_MAP

|- !P f l. EVERY P (MAP f l) = EVERY (\x. P (f x)) l

EVERY_SIMP

|- !c l. EVERY (\x. c) l = (l = []) \/ c

MONO_EVERY

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

EXISTS_MEM

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

EXISTS_MAP

|- !P f l. EXISTS P (MAP f l) = EXISTS (\x. P (f x)) l

EXISTS_SIMP

|- !c l. EXISTS (\x. c) l = ~(l = []) /\ c

MONO_EXISTS

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

EVERY_NOT_EXISTS

|- !P l. EVERY P l = ~EXISTS (\x. ~P x) l

EXISTS_NOT_EVERY

|- !P l. EXISTS P l = ~EVERY (\x. ~P x) l

MEM_APPEND

|- !e l1 l2. MEM e (l1 ++ l2) = MEM e l1 \/ MEM e l2

MEM_FILTER

|- !P L x. MEM x (FILTER P L) = P x /\ MEM x L

EVERY_APPEND

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

EXISTS_APPEND

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

NOT_EVERY

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

NOT_EXISTS

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

MEM_MAP

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

LENGTH_NIL

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

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 []

CONS_ACYCLIC

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

APPEND_eq_NIL

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

APPEND_11

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

EL_compute

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

EL_simp

|- (EL (NUMERAL (BIT1 n)) l = EL (PRE (NUMERAL (BIT1 n))) (TL l)) /\
   (EL (NUMERAL (BIT2 n)) l = EL (NUMERAL (BIT1 n)) (TL l))

WF_LIST_PRED

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

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)

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

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

MAP_CONG

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

EXISTS_CONG

|- !l1 l2 P P'.
     (l1 = l2) /\ (!x. MEM x l2 ==> (P x = P' x)) ==>
     (EXISTS P l1 = EXISTS 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_MONOTONIC

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

UNZIP_THM

|- (UNZIP [] = ([],[])) /\
   (UNZIP ((x,y)::t) = (let (L1,L2) = UNZIP t in (x::L1,y::L2)))

LENGTH_ZIP

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

LENGTH_UNZIP

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

ZIP_UNZIP

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

UNZIP_ZIP

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

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

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

EL_ZIP

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

MAP2_ZIP

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

MEM_EL

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

REVERSE_APPEND

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

REVERSE_REVERSE

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

MEM_REVERSE

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

LAST_CONS

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

FRONT_CONS

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

APPEND_FRONT_LAST

|- !l. ~(l = []) ==> (FRONT l ++ [LAST l] = l)

FILTER_APPEND_DISTRIB

|- !P L M. FILTER P (L ++ M) = FILTER P L ++ FILTER P M

ALL_DISTINCT_FILTER

|- !l. ALL_DISTINCT l = !x. MEM x l ==> (FILTER ($= x) l = [x])

IN_LIST_TO_SET

|- x IN LIST_TO_SET l = MEM x l

listRel_rules

|- !R.
     listRel R [] [] /\
     !h1 h2 t1 t2. R h1 h2 /\ listRel R t1 t2 ==> listRel R (h1::t1) (h2::t2)

listRel_ind

|- !R listRel'.
     listRel' [] [] /\
     (!h1 h2 t1 t2.
        R h1 h2 /\ listRel' t1 t2 ==> listRel' (h1::t1) (h2::t2)) ==>
     !a0 a1. listRel R a0 a1 ==> listRel' a0 a1

listRel_cases

|- !R a0 a1.
     listRel R a0 a1 =
     (a0 = []) /\ (a1 = []) \/
     ?h1 h2 t1 t2.
       (a0 = h1::t1) /\ (a1 = h2::t2) /\ R h1 h2 /\ listRel R t1 t2

listRel_NIL

|- (listRel R [] y = (y = [])) /\ (listRel R x [] = (x = []))

listRel_CONS

|- (listRel R (h::t) y = ?h' t'. (y = h'::t') /\ R h h' /\ listRel R t t') /\
   (listRel R x (h'::t') = ?h t. (x = h::t) /\ R h h' /\ listRel R t t')

listRel_LENGTH

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

listRel_strong_ind

|- !R listRel'.
     listRel' [] [] /\
     (!h1 h2 t1 t2.
        R h1 h2 /\ listRel R t1 t2 /\ listRel' t1 t2 ==>
        listRel' (h1::t1) (h2::t2)) ==>
     !a0 a1. listRel R a0 a1 ==> listRel' a0 a1

MONO_listRel

|- (!x y. R x y ==> R' x y) ==> listRel R x y ==> listRel R' x y

LEN_LENGTH_LEM

|- !L n. LEN L n = LENGTH L + n

REV_REVERSE_LEM

|- !L1 L2. REV L1 L2 = REVERSE L1 ++ L2

LENGTH_LEN

|- !L. LENGTH L = LEN L 0

REVERSE_REV

|- !L. REVERSE L = REV L []