The HOL more lists Library

Paul Curzon

University of Cambridge, Computer Laboratory

New Museums Site, Pembroke Street Cambridge, CB2 3QG, England.

June 1993

Authors

This library is the combination of the list theories of the following people:

Mike Benjamin (British Aerospace Sowerby Research Centre, Bristol, U.K.), R. J. Boulton (University of Cambridge, Computer Laboratory, U.K.), Albert J. Camilleri (Hewlett-Packard Laboratories, Bristol, U.K.), Rachel Cardell-Oliver (University of Cambridge, Computer Laboratory, U.K.), Paul Curzon (University of Cambridge, Computer Laboratory, U.K.), Andy Gordon (University of Cambridge, Computer Laboratory, U.K.), Brian Graham (University of Cambridge, Computer Laboratory, U.K.), John Harrison (University of Cambridge, Computer Laboratory, U.K.), Paul Loewenstein (Mitsubishi Electronics America Inc., USA), Wim Ploegaerts (Imec vzw. Leuven, Belgium), Wai Wong (University of Cambridge, Computer Laboratory, U.K.).

Wim Ploegaerts compiled the theorems which came from other libraries in the HOL system and made many useful suggestions about the organization of the library.

Contents

1 The more lists Library 3 1.1 The Theory more lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2 The Theory general lists . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.3 The Theory snoc . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.4 The Theory tail . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.5 The Theory append . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.6 The Theory el . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.7 The Theory ell . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.8 The Theory map . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1.9 The Theory member . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.10 The Theory unappend . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.11 The Theory subseq . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 1.12 The Theory last subseq . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 1.13 The Theory shift . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 1.14 The Theory zip . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 1.15 The Theory num lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 1.16 Using the Library . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

1.16.1 An Example of a Session . . . . . . . . . . . . . . . . . . . . . . . . 18 1.16.2 The load more lists Function . . . . . . . . . . . . . . . . . . . . 19

2 ML Functions in the more lists Library 21

3 Pre-proved Theorems 33 3.1 General List Theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 3.2 Theorems about the Tail End of a List . . . . . . . . . . . . . . . . . . . . 34 3.3 Theorems about TAIL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 3.4 Theorems about APPEND and Related Operators . . . . . . . . . . . . . . . 38 3.5 Theorems about Higher Order Functions . . . . . . . . . . . . . . . . . . . 42 3.6 Theorems about EL and EL1 . . . . . . . . . . . . . . . . . . . . . . . . . . 43 3.7 Theorems about ELL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 3.8 Theorems about Accessing Subsequences of Lists from the Front . . . . . . 46 3.9 Theorems about Accessing Subsequences of Lists from the Tail End …. 49 3.10 Theorems about List Membership . . . . . . . . . . . . . . . . . . . . . . . 53 3.11 Theorems about UNAPPEND . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 3.12 Theorems about Shifting and Rotating Lists . . . . . . . . . . . . . . . . . 59 3.13 Theorems about Pairing Lists . . . . . . . . . . . . . . . . . . . . . . . . . 60 3.14 Theorems about num Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . 61

Index 63

Chapter 1

The more lists Library

This document describes the facilities provided by the more_lists library. The library contains an ad hoc collection of definitions and theorems about lists which extends the standard theory list. Included are many general purpose theorems about the list operators defined in the theory list. In addition, definitions of new operators are given with associated theorems. Several tactics and conversions related to lists are also provided. The library is split into several theories, the ancestry of which is shown below.

                 more lists            zip shift            num lists unappend el ell map tail    subseq last subseq member append snoc general lists list

A complete list of the theorems which are available in the library is given in Chapter 3. Due to the large number of theorems, users of the library may find the theorem retrieval library of help. The above hierarchy should be kept in mind when searching for theorems. All definitions and theorems from the ancestor theories are automatically loaded, if possible, when their names are first mentioned during a HOL session.

1.1 The Theory more lists

The theory more_lists is the descendant theory of all the theories in the library. It contains no theorems or definitions itself.

1.2 The Theory general lists

The theory general_lists contains an ad hoc collection of theorems about the basic list operators defined in the standard theory list. In particular, it contains theorems about the operators CONS, TL, NULL and LENGTH. It does not contain theorems about the standard operators APPEND or EL which may be found in the theories append and el, respectively, nor about MAP and EVERY which may be found in the theory map. A selection of the theorems available are given below.

   NULL_EQ_EMPTY  |- !l. NULL l = (l = [])
   LENGTH_EQ      |- !x y. (x = y) ==> (LENGTH x = LENGTH y)
   TL_NULL        |- !l. (LENGTH l = 1) ==> NULL(TL l)
   LENGTH_NULL    |- !l. (LENGTH l = 0) = NULL l
   CONS_ONE_ONE   |- !h t h' t'. (CONS h t = CONS h' t') ==>
                                           (h = h') /\ (t = t')

The tactic LIST_LENGTH_INDUCT_TAC performs induction on the length of a list. If the tactic is applied to the goal

   ?- !(x :* list) (y:** list). (LENGTH x = LENGTH y) ==> P x y

it will yield the following subgoals:

   ?- P[][]
   P(TL x)(TL y) ?- P(CONS(HD x)(TL x))(CONS(HD y)(TL y))

See the documentation of the function in Chapter 2 for more details.

1.3 The Theory snoc

The theory snoc introduces operators for accessing the tail end of a list. For problems which naturally use both ends of a list, proofs can be simplified considerably using this theory. The operators SNOC, LAST and BUTLAST are equivalent to CONS, HD and TL respectively, except working from the tail end of the list rather than the start. REVERSE is also defined, providing a link between accessing the start and the tail end of a list. The ability to make recursive definitions and perform induction using SNOC is provided.

SNOC adds an element to the tail end of a list.

SNOC h[a_{1}; a_{2}; …; a_{n}] = [a_{1}; a_{2}; …; a_{n}; h]

It is defined by primitive recursion.

   SNOC_DEF       |- (!d. SNOC d[] = [d]) /\
                     (!d h t. SNOC d(CONS h t) = CONS h(SNOC d t))

The theorems pre-proved about SNOC include:

   SNOC_NOT_NULL  |- !d l. ~NULL(SNOC d l)
   HD_SNOC        |- !h t. HD(SNOC h t) = (NULL t => h | HD t)
   TL_SNOC        |- !h t. TL(SNOC h t) = (NULL t => [] | SNOC h(TL t))
   SNOC_Axiom     |- !x f. ?! fn. (fn[] = x) /\
                                  (!h t. fn(SNOC h t) = f(fn t)h t)
   SNOC_INDUCT    |- !P. P[] /\ (!t. P t ==> (!h. P(SNOC h t))) ==> (!l. P l)

The theorem SNOC_INDUCT allows induction to be performed from the tail end of the list. It is in the correct form for use with the built-in induction tactic INDUCT_THEN. See the HOL manual for details of this function. An associated tactic SNOC_INDUCT_TAC is provided. If this tactic is applied to the goal

   ?- !(l:* list). P l

it will yield the subgoals:

   ?- P[]
   P l ?- !h. P(SNOC h l)

See the documentation of the function in Chapter 2 for more details.

The theorem SNOC_Axiom is in the form produced by the type definition package of the HOL system. The tools provided with the package can therefore be used. In particular the function new_recursive_definition can be used to make recursive definitions using SNOC. For example, an alternative definition for the length of the list could be made as follows:

1

 #let S_LENGTH =
    new_recursive_definition false SNOC_Axiom `S_LENGTH`
      "(S_LENGTH NIL = 0) /\
       (!h:*. !t. S_LENGTH (SNOC h t) = SUC (S_LENGTH t))";;
 S_LENGTH = |- (S_LENGTH[] = 0) /\ (!h t. S_LENGTH(SNOC h t) = SUC(S_LENGTH t))

LAST returns the last element of a list and BUTLAST returns the remainder of the list with the last element removed. Both are undefined for null lists.

LAST [a_{1}; …; a_{n}; h] = h

     BUTLAST [a_{1}; . . . ; a_{n}; h] = [a_{1}; . . . ; a_{n}]

They are defined in HOL by

   LAST_DEF            |- !l. LAST l = (@h. ?t. SNOC h t = l)
   BUTLAST_DEF         |- !l. BUTLAST l = (@t. SNOC(LAST l)t = l)

A sample of the theorems pre-proved about LAST and BUTLAST is given below.

   LAST                |- !h t. LAST(SNOC h t) = h
   BUTLAST             |- !h t. BUTLAST(SNOC h t) = t
   LAST_CONS           |- !h t. LAST(CONS h t) = (NULL t => h | LAST t)
   BUTLAST_CONS        |- !h t. BUTLAST(CONS h t) =
                                   (NULL t => [] | CONS h(BUTLAST t))
   LAST_EL             |- !a. LAST[a] = a

REVERSE reverses the elements in a list.

     REVERSE [a_{1}; . . . ; a_{n}] = [a_{n}; . . . ; a_{1}]

It is defined by

   REVERSE_DEF         |- (REVERSE[] = []) /\
                          (!h l. REVERSE(CONS h l) = SNOC h(REVERSE l))

1.4. The Theory tail 7

Pre-proved theorems about REVERSE include

REVERSE_CLAUSES    |- (REVERSE[] = []) /\
                      (!h l. REVERSE(CONS h l) = SNOC h(REVERSE l)) /\
                      (!d l. REVERSE(SNOC d l) = CONS d(REVERSE l)) /\
                      (!l. REVERSE(REVERSE l) = l)
REVERSE_SINGLE     |- !h. REVERSE[h] = [h]
REVERSE_NULL       |- !l. NULL(REVERSE l) = NULL l
LENGTH_REVERSE     |- !l. LENGTH(REVERSE l) = LENGTH l

A conversion SUBST_REVERSE_CONV is also provided. When applied to a term of the form !x.P x it returns the theorem:

 |- (!x. P x) = (!y. P(REVERSE y))

1.4 The Theory tail

It is sometimes useful to be able to say that the tail of an empty list is an empty list. However TL is undefined in this situation. The theory tail provides an alternative definition TAIL for taking the tail of a list which has this property.

 TAIL[] = []

TAIL[h; a_{1}; …; a_{n}] = [a_{1}; …; a_{n}] It is defined using primitive recursion

TAIL  |- (TAIL[] = []) /\ (!h t. TAIL(CONS h t) = t)

Several theorems are pre-proved.

CON               |- !l. ~NULL l ==> (CONS(HD l)(TAIL l) = l)
TAIL_APPEND       |- !x y. TAIL(APPEND x y) =
                           ((x = []) => TAIL y | APPEND(TAIL x)y)
list_CASES2       |- !l. (l = []) \/ (l = CONS(HD l)(TAIL l))
list_NULL_CASES2  |- !l. NULL l \/ (l = CONS(HD l)(TAIL l))
LENGTH_TAIL       |- !l. ~NULL l ==> (LENGTH(TAIL l) = (LENGTH l) - 1)
TL_TAIL           |- !l. ~NULL l ==> (TL l = TAIL l)
NOT_NULL_TAIL     |- !l. ~NULL(TAIL l) ==> ~NULL l

8 Chapter 1. The more lists Library

1.5 The Theory append

The theory append contains theorems and definitions for constructing lists from smaller elements. It contains further theorems about APPEND (which is defined in the theory list). In addition it contains definitions and associated theorems for ITERATED and REPLICATE. ITERATED appends a given number of copies of a list together, whereas REPLICATE forms a list of a given number of copies of a single element.

ITERATED n[a_{1}; …; a_{n}] = [a_{1}; …; a_{n}; a_{1}; …; a_{n}; …]

  REPLICATE n a = [a; . . . ; a]

They are defined in HOL by primitive recursion.

REPLICATE    |- (!in. REPLICATE 0 in = []) /\
                (!n in. REPLICATE(SUC n)in = CONS in(REPLICATE n in))
ITERATED     |- (!s. ITERATED 0 s = []) /\
                (!n s. ITERATED(SUC n)s = APPEND s(ITERATED n s))

There are a large collection of pre-proved theorems in this theory, a few of which are given below.

APPEND_CLAUSES  |- (!l. APPEND[]l = l) /\
                   (!l1. APPEND l1[] = l1) /\
                   (!l1 l2 h. APPEND(CONS h l1)l2 = CONS h(APPEND l1 l2)) /\
                   (!d l1 l2. APPEND l1(SNOC d l2) = SNOC d(APPEND l1 l2))
APPEND_IS_NULL    |- !l1 l2. NULL(APPEND l1 l2) = NULL l1 /\ NULL l2
CONS_APPEND_CONS  |- !a l. CONS a l = APPEND[a]l
SNOC_APPEND_CONS  |- !l h. SNOC h l = APPEND l[h]
HD_APPEND_NULL    |- !l1. ~NULL l1 ==> (!l2. HD(APPEND l1 l2) = HD l1)
REVERSE           |- (REVERSE[] = []) /\
                     (!h t. REVERSE(CONS h t) = APPEND(REVERSE t)[h])
ITERATED_EMPTY    |- !n. ITERATED n[] = []
LENGTH_REPLICATE  |- !x n. LENGTH(REPLICATE n x) = n
A similar tactic to SNOC_INDUCT_TAC, LIST_APPEND_INDUCT_TAC is provided which uses

APPEND to access the tail of the list rather than SNOC. If this tactic is applied to the goal

?- !(l:* list). P l

1.6. The Theory el 9

it will yield the following subgoals:

   ?- P[]
   P l ?- !h. P(APPEND l [h])

See the documentation of the function in Chapter 2 for more details.

1.6 The Theory el

The theory el is concerned with selecting elements from a list. It contains several new theorems about the function EL, defined in the theory list. A similar function EL1 is also defined here. It chooses an element from a list indexing from 1. It is undefined for an index of 0. This contrasts with EL which indexes from 0.

EL1 k[a_{1}; …; a_{n}] = a_{k}

It is defined as follows:

   EL1          |- !n l. EL1(SUC n)l = EL n l

Following are some of the theorems pre-proved in this theory.

   EL_HD        |- !l. ~NULL l ==> (EL 0 l = HD l)
   EL_APPEND_1  |- !l1 l2 k. k < (LENGTH l1) ==> (EL k(APPEND l1 l2) = EL k l1)
   EL_APPEND_2  |- !l1 l2 k.  (LENGTH l1) <= k ==>
                                   (EL k(APPEND l1 l2) = EL(k - (LENGTH l1))l2)
   EL1_SUC_CONS |- !n h l. 0 < n ==> (EL1(SUC n)(CONS h l) = EL1 n l)
   EL1_HD       |- !l. ~NULL l ==> (EL1 1 l = HD l)

1.7 The Theory ell

The theory ell is concerned with selecting elements from a list, indexing from the end. The function ELL is defined here. It chooses an element from a list indexing from 0 starting at the end of the list.

ELL k[a_{n}; …; a_{0}] = a_{k}

It is defined as follows:

10 Chapter 1. The more lists Library

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

Following are some of the theorems pre-proved in this theory.

ELL_CONS     |- !l x k. k < (LENGTH l) ==> (ELL k(CONS x l) = ELL k l)
ELL_LAST     |- !l. ~NULL l ==> (ELL 0 l = LAST l)
EL_ELL
      |- !l k. k < (LENGTH l) ==> (EL k l = ELL(PRE((LENGTH l) - k))l)
ELL_APPEND_1
     |- !l1 l2 k. k < (LENGTH l2) ==> (ELL k(APPEND l1 l2) = ELL k l2)

1.8 The Theory map

The theory map is concerned with higher-order functions and predicates which act on the elements of a list. Examples which occur in the theory list are MAP and EVERY. Further theorems about these operators are pre-proved in this theory. Additionally, the operator ITLIST is provided.

ITLIST f[a_{1}; a_{2}; …; a_{n}] x = f a_{1} (f a_{2} ( … f a_{n} x) …)

Its definition is

ITLIST    |- (!f x. ITLIST f[]x = x) /\
             (!f hd tl x. ITLIST f(CONS hd tl)x = f hd(ITLIST f tl x))

Theorems about MAP, EVERY, and ITLIST which are pre-proved include

MAP_MAP_o      |- !f g l. MAP f(MAP g l) = MAP(f o g)l
EVERY_MAP      |- !f P l. EVERY P(MAP f l) = EVERY(P o f)l
HD_MAP         |- !f l. ~NULL l ==> (HD(MAP f l) = f(HD l))
TL_MAP         |- !f l. ~NULL l ==> (TL(MAP f l) = MAP f(TL l))
ITLIST_MAP     |- !l. ITLIST p(MAP f l) = ITLIST(\x y. p(f x)y)l

1.9 The Theory member

The theory member contains definitions of predicates which test for membership of elements and sublists within a list. The predicate MEMBER tests for a given element being a member of a list. LLESS_LEFT tests if a list is an initial sublist not equal to a given list. LLEQ_LEFT tests if a list is an initial proper sublist of a given list. LLESS_RIGHT tests if a list is a final sublist not equal to a given list. LLEQ_RIGHT tests if a list is a final proper sublist of a given list.

MEMBER a_{i} [a_{1}; …; a_{n}]= T (i < n)
MEMBER b [a_{1}; …; a_{n}] = F (otherwise)
LLESS_LEFT[a_{1}; …; a_{n}] [a_{1}; …; a_{n}; b_{1}; …; b_{m}]= T
LLESS_LEFT[a_{1}; …; a_{n}] [b_{1}; …; b_{m}]  = F (otherwise)
LLEQ_LEFT[a_{1}; …; a_{n}] [a_{1}; …; a_{n}; b_{1}; …; b_{m}]= T

LLEQ_LEFT[a_{1}; . . . ; a_{n}] [a_{1}; . . . ; a_{n}]  = T

LLEQ_LEFT[a_{1}; …; a_{n}] [b_{1}; …; b_{m}]  = F (otherwise)
LLESS_RIGHT[a_{1}; …; a_{n}] [b_{1}; …; b_{m}; a_{1}; …; a_{n}]= T
LLESS_RIGHT[a_{1}; …; a_{n}] [b_{1}; …; b_{m}]  = F (otherwise)
LLEQ_RIGHT[a_{1}; …; a_{n}] [b_{1}; …; b_{m}; a_{1}; …; a_{n}]= T

LLEQ_RIGHT[a_{1}; . . . ; a_{n}] [a_{1}; . . . ; a_{n}]  = T

LLEQ_RIGHT[a_{1}; …; a_{n}] [b_{1}; …; b_{m}]  = F (otherwise)

They have the following definitions

MEMBER     |- (!x. MEMBER x[] = F) /\
             (!x h t. MEMBER x(CONS h t) = (h = x) \/ MEMBER x t)
LLESS_LEFT |- (!l. [] LLESS_LEFT l = ~NULL l) /\
             (!a rest l. (CONS a rest) LLESS_LEFT l =
                           ~NULL l /\ (a = HD l) /\ rest LLESS_LEFT (TL l))
LLEQ_LEFT  |- !l1 l2. l1 LLEQ_LEFT l2 = l1 LLESS_LEFT l2 \/ (l1 = l2)
LLESS_RIGHT |- (!l. []  LLESS_RIGHT l = ~NULL l) /\
              (!a rest l. (SNOC a rest) LLESS_RIGHT l =
                           ~(NULL l) /\ (a = LAST l) /\
                           rest LLESS_RIGHT (BUTLAST l))
LLEQ_RIGHT  |- !l1 l2. l1 LLEQ_RIGHT l2 = l1 LLESS_RIGHT l2 \/ (l1 = l2)

The theorems pre-proved in this theory include:

12 Chapter 1. The more lists Library

MEMBER_SNOC              |- !t x h. MEMBER x(SNOC h t) =
                                              (h = x) \/ MEMBER x t
NOT_LLESS_LEFT_NIL       |- !l. ~l LLESS_LEFT []
CONS_LLESS_LEFT_TL       |- !l1 l2. (CONS h l1) LLESS_LEFT l2 ==>
                                              l1 LLESS_LEFT (TL l2)
CONS_LLEQ_LEFT_TL        |- !l1 l2. (CONS h l1) LLEQ_LEFT l2 ==>
                                              l1 LLEQ_LEFT (TL l2)
SNOC_LLESS_RIGHT_BUTLAST |-  !l1 l2. (SNOC h l1) LLESS_RIGHT l2 ==>
                                              l1 LLESS_RIGHT (BUTLAST l2)
NIL_LLEQ_RIGHT           |- !l. [] LLEQ_RIGHT l

1.10 The Theory unappend

The theory unappend deals with the operators UNAPPEND_LEFT and UNAPPEND_RIGHT. The operator UNAPPEND_LEFT removes a given initial sublist from the front of a list. It returns the empty list if the first list is not an initial sublist of the second. UNAPPEND_RIGHT is similar, removing a given final sublist from the tail end of a list.

UNAPPEND_LEFT [a_{1}; …; a_{n}][a_{1}; …; a_{n}; b_{1}; …; b_{m}] = [b_{1}; …; b_{m}]

 UNAPPEND_RIGHT [b_{1}; . . . ; b_{m}][a_{1}; . . . ; a_{n}; b_{1}; . . . ; b_{m}] = [a_{1}; . . . ; a_{n}]

They are defined by HOL specifications.

UNAPPEND_LEFT   |- !l1 l2. UNAPPEND_LEFT l1 (APPEND l1 l2) = l2
UNAPPEND_RIGHT  |- !l1 l2. UNAPPEND_RIGHT l2 (APPEND l1 l2) = l1

A sample of the theorems contained in this theory is given below.

NULL_UNAPPEND_LEFT       |- !l. NULL(UNAPPEND_LEFT l l)
UNAPPEND_RIGHT_NIL       |- !l. UNAPPEND_RIGHT[]l = l
APPEND_UNAPPEND_LEFT_ID  |- !l. l = APPEND l(UNAPPEND_LEFT l l)
LLESS_LEFT_APPEND_UNAPPEND_LEFT
     |- !l1 l2. l1 LLESS_LEFT l2 ==> (l2 = APPEND l1(UNAPPEND_LEFT l1 l2))
LLEQ_RIGHT_APPEND_UNAPPEND_RIGHT
     |- !l1 l2. l1 LLEQ_RIGHT l2 ==> (l2 = APPEND (UNAPPEND_RIGHT l1 l2) l1)

1.11 The Theory subseq

The theory subseq deals with extracting subsequences from a list, indexing from the front of the list.

FIRSTN, given an argument k, returns a list of the first k elements of a list. It is undefined if k is larger than the length of the list.

FIRSTN k[a_{1}; …; a_{k}; …; a_{n}] = [a_{1}; …; a_{k}]

SUBSEQ, is similar to FIRSTN except that it returns the empty list if k is larger than the length of the list.

SUBSEQ k[a_{1}; …; a_{k}; …; a_{n}]= [a_{1}; …; a_{k}]
SUBSEQ k[a_{1}; …; a_{n}]  = []  (k > n)

NTL, given an argument k, returns the remainder of a list after the first k elements have been removed. It is undefined if k is larger than the length of the list.

NTL k[a_{1}; …; a_{k}; …; a_{n}] = [a_{k+1}; …; a_{n}]

NTAIL, is similar to NTL except that it returns the empty list if k is larger than the length of the list.

NTAIL k[a_{1}; …; a_{k}; …; a_{n}]= [a_{k+1}; …; a_{n}]
NTAIL k[a_{1}; …; a_{n}]  = []  (k > n)

The HOL definitions of these operators are

   FIRSTN    |- (!X. FIRSTN 0 X = []) /\
                (!n X. FIRSTN(SUC n)X = CONS(HD X)(FIRSTN n(TL X)))
   SUBSEQ    |- (!x. SUBSEQ 0 x = []) /\
                (!n x. SUBSEQ(SUC n)x =
                          (NULL x => [] | CONS(HD x)(SUBSEQ n(TAIL x))))
   NTL       |- (!X. NTL 0 X = X) /\ (!n X. NTL(SUC n)X = NTL n(TL X))
   NTAIL     |- (!l. NTAIL 0 l = l) /\ (!n l. NTAIL(SUC n)l = TAIL(NTAIL n l))

This theory contains a large number of theorems, a sample of which is given below.

   NTL_TL_SYM            |- !n X. NTL n(TL X) = TL(NTL n X)
   FIRSTN_NULL           |- !n X. NULL(FIRSTN n X) ==> (n = 0)
   SUBSEQ_SUBSEQ         |- !n x. SUBSEQ n(SUBSEQ n x) = SUBSEQ n x
   EL_HD_NTAIL           |- !x l. ~NULL(NTAIL x l) ==> (EL x l = HD(NTAIL x l))

1.12 The Theory last subseq

The theory last_subseq deals with extracting subsequences from a list. Unlike the operators in the theory subseq, the operators in this theory access the list indexing from the tail end.

LASTN, given an argument k, returns a list of the last k elements of a list. It is undefined if k is larger than the length of the list.

LASTN k[a_{n}; …; a_{k}; …; a_{1}] = [a_{k}; …; a_{1}]

NBUTLAST, given an argument k, returns the remainder of a list after the last k elements have been removed. It is undefined if k is larger than the length of the list.

NBUTLAST k[a_{n}; …; a_{k}; …; a_{1}] = [a_{n}; …; a_{k+1}]

The HOL definitions of these operators are

   LASTN     |- (!X. LASTN 0 X = []) /\
                (!n X. LASTN(SUC n)X = APPEND(LASTN n(BUTLAST X))[LAST X])
   NBUTLAST  |- (!X. NBUTLAST 0 X = X) /\
                (!n X. NBUTLAST(SUC n)X = NBUTLAST n(BUTLAST X))

This theory contains a large number of theorems, a sample of which is given below.

   LASTN_LENGTH_ID       |- !X. LASTN(LENGTH X)X = X
   LASTN_NULL            |- !n X. NULL(LASTN n X) ==> (n = 0)
   NBUTLAST_BUTLAST_SYM  |- !n X. NBUTLAST n(BUTLAST X) = BUTLAST(NBUTLAST n X)
   NBUTLAST_LENGTH_NULL  |- !X. NULL(NBUTLAST(LENGTH X)X)
   APPEND_NBUTLAST_LASTN |- !n X. n <= (LENGTH X) ==>
                                          (APPEND(NBUTLAST n X)(LASTN n X) = X)

1.13 The Theory shift

The theory shift contains definitions concerned with shifting lists in various ways.

PAD_RIGHT pads a list on the right (tail end) with a given number of copies of a given element.

PAD_RIGHT x n [a_{1}; …; a_{n}] = [a_{1}; …; a_{n}; x; …; x]

1.13. The Theory shift 15

PAD_LEFT pads a list on the left (front end) with a given number of copies of a given element.

PAD_LEFT x n [a_{1}; …; a_{n}] = [x; …; x; a_{1}; …; a_{n}] ROTATE1_RIGHT rotates a list right by one position, the last element of the list becoming

the head.

  ROTATE1_RIGHT[a_{1}; . . . ; a_{n−1}; a_{n}] = [a_{n}; a_{1}; . . . ; a_{n−1}]

ROTATE1_LEFT rotates a list left by one position, the head of the list becoming the last element.

  ROTATE1_LEFT[a_{1}; a_{2}; . . . ; a_{n}] = [a_{2}; . . . ; a_{n}; a_{1}]

ROTATE_RIGHT rotates a list right by a given number of positions.

ROTATE_RIGHT k [a_{1}; …; a_{n−1}; a_{n}] = [a_{n−k−1}; …; a_{n}; a_{1}; …; a_{n−k}] ROTATE_LEFT rotates a list left by a given number of positions.

ROTATE_LEFT k [a_{1}; a_{2}; …; a_{n}] = [a_{k+1}; …; a_{n}; a_{1}; …; a_{k}] The HOL definitions are

 PAD_LEFT      |- (!x l. PAD_LEFT x 0 l = l) /\
                  (!x n l. PAD_LEFT x(SUC n)l = CONS x(PAD_LEFT x n l))
 PAD_RIGHT     |- (!x l. PAD_RIGHT x 0 l = l) /\
                  (!x n l. PAD_RIGHT x(SUC n)l = SNOC x(PAD_RIGHT x n l))
 ROTATE1_LEFT  |- !l. ROTATE1_LEFT l = SNOC(HD l)(TL l)
 ROTATE1_RIGHT |- !l. ROTATE1_RIGHT l = CONS(LAST l)(BUTLAST l)
 ROTATE_LEFT   |- (!l. ROTATE_LEFT 0 l = l) /\
                  (!n l. ROTATE_LEFT(SUC n)l = ROTATE1_LEFT(ROTATE_LEFT n l))
 ROTATE_RIGHT  |- (!l. ROTATE_RIGHT 0 l = l) /\
                  (!n l. ROTATE_RIGHT(SUC n)l =
                                   ROTATE1_RIGHT(ROTATE_RIGHT n l))

An ad hoc collection of elementary theorems are pre-proved in the theory shift, some of which are given below.

16 Chapter 1. The more lists Library

LENGTH_PAD_LEFT    |- !l n x. LENGTH(PAD_LEFT x n l) = (LENGTH l) + n
LENGTH_PAD_RIGHT   |- !l n x. LENGTH(PAD_RIGHT x n l) = (LENGTH l) + n
ROTATE1_LEFT_CONS  |- !x l. ROTATE1_LEFT(CONS x l) = SNOC x l
ROTATE1_RIGHT_NIL  |- !l. ~NULL l ==> ~NULL(ROTATE1_RIGHT l)
ROTATE_LEFT_EL     |- !n x. ROTATE_LEFT n[x] = [x]
ROTATE_RIGHT_ROTATE_LEFT   |- !n l. ~NULL l ==>
                                       (ROTATE_RIGHT n(ROTATE_LEFT n l) = l)

1.14 The Theory zip

The theory zip contains primitive recursive definitions for forming a list of pairs from two lists and vice versa. Given two lists, ZIP pairs corresponding elements to give a list of pairs. If one list is longer than the other the extra elements are discarded.

\begin{matrix}ZIP [a_{1}; …; a_{n}][b_{1}; …; b_{m}] = [(a_{1},b_{1}); …; (a_{n},b_{n})] & (n ≤ m) \\ ZIP [a_{1}; …; a_{n}][b_{1}; …; b_{m}] = [(a_{1},b_{1}); …; (a_{m},b_{m})] & (n > m) \end{matrix}

Given a list of pairs UNZIP_FST extracts a list of the first elements and UNZIP_SND extracts a list of the second elements.

  UNZIP_FST[(a_{1},b_{1}); . . . ;(a_{n},b_{n})] = [a_{1}; . . . ; a_{n}]
  UNZIP_SND[(a_{1},b_{1}); . . . ;(a_{n},b_{n})] = [b_{1}; . . . ; b_{n}]

The HOL definitions are

ZIP_DEF       |- (!l. ZIP l[] = []) /\
                 (!l h t. ZIP l(CONS h t) =
                              (NULL l => [] | CONS(HD l,h)(ZIP(TL l)t)))
UNZIP_FST     |- (UNZIP_FST[] = []) /\
                 (!h t. UNZIP_FST(CONS h t) = CONS(FST h)(UNZIP_FST t))
UNZIP_SND     |- (UNZIP_SND[] = []) /\
                 (!h t. UNZIP_SND(CONS h t) = CONS(SND h)(UNZIP_SND t))

A collection of elementary theorems are pre-proved in the theory zip.

1.15. The Theory num lists 17

ZIP_CLAUSES       |- (!l. ZIP[]l = []) /\
                     (!l. ZIP l[] = []) /\
                     (!h1 t1 h2 t2. ZIP(CONS h1 t1)(CONS h2 t2) =
                                      CONS(h1,h2)(ZIP t1 t2))
ZIP_UNZIP_FST_SND |- !l. ZIP(UNZIP_FST l)(UNZIP_SND l) = l
UNZIP_FST_ZIP     |- !l1 l2. (LENGTH l1) <= (LENGTH l2) =
                                       (UNZIP_FST(ZIP l1 l2) = l1)
UNZIP_SND_ZIP     |- !l1 l2. (LENGTH l2) <= (LENGTH l1) =
                                       (UNZIP_SND(ZIP l1 l2) = l2)
FST_SND_UNZIP_ZIP |- !l1 l2. (LENGTH l1 = LENGTH l2) =
                                       (UNZIP_FST(ZIP l1 l2) = l1) /\
                                       (UNZIP_SND(ZIP l1 l2) = l2)

1.15 The Theory num lists

The theory num_lists deals with lists of numbers (of type :num list).

FROM0 returns a list of numbers from 0 up to a given number.

  FROM0 n = [0; 1; . . . ; n]

UPTO is an infix operator which returns a list of the numbers between two given numbers. It returns an empty list if the second argument is smaller than the first.

m UPTO n = [m; m + 1; …; n](m < n)

 m UPTO m = [m]

m UPTO n = []  (m > n)

RANGE is similar to UPTO except that the second argument gives the length of the list.

RANGE m n = [m; m + 1; …; m + n − 1]

 RANGE m 0 = []

The definitions in HOL are

FROM0    |- (FROM0 0 = [0]) /\ (!n. FROM0(SUC n) = CONS 0(MAP SUC(FROM0 n)))
UPTO     |- !n1 n2. n1 UPTO n2 = MAP($+ n1)(n1 <= n2 => FROM0(n2 - n1) | [])
RANGE    |- (!m. RANGE m 0 = []) /\
            (!m n. RANGE m(SUC n) = CONS m(RANGE(SUC m)n))

Below is a selection of theorems proved about them in the theory.

   RANGE_TOP             |- !n m. RANGE m(SUC n) = APPEND(RANGE m n)[m + n]
   RANGE_SHIFT           |- !n m. RANGE(SUC m)n = MAP SUC(RANGE m n)
   FROM0_APPEND          |- !n. FROM0(SUC n) = APPEND(FROM0 n)[SUC n]
   UPTO_EQ_CONS_SUC_UPTO |- !m n. m <= n ==>
                                   (m UPTO n = CONS m((SUC m) UPTO n))
   INTERVAL              |- (!m. m UPTO 0 = (m > 0 => [] | [0])) /\
                            (!m n. m UPTO (SUC n) =
                                   (m > (SUC n) => [] | SNOC(SUC n)(m UPTO n)))

1.16 Using the Library

The more_lists library is loaded into a user’s HOL session using the function load_library (see the HOL manual for a general description of library loading). The library has as parents the libraries auxiliary and more_arithmetic. The first action in the load sequence initiated by load_library is therefore to automatically load these libraries. Next the internal HOL search paths are updated. A pathname to the more_lists library is added to the search path, so that theorems may be autoloaded from the constituent theories of the library. The HOL help search path is also updated with a pathname to on-line help files for the ML functions in the library.

After updating search paths, the load sequence for more_lists depends on the current state of the HOL session. If the system is in draft mode, the library theory more_lists is added as a new parent to the current theory. If the system is not in draft mode, but the current theory is an ancestor of the more_lists theory in the library (e.g. the user is in a fresh HOL session) then the more_lists theory is made into the current theory. In both cases, the ML functions in the library are loaded into HOL and the theorems in the library theories are set up to be autoloaded on demand. The more_lists library is at this point fully loaded into the user’s HOL session.

1.16.1 An Example of a Session

The following session shows how the more_lists library may be loaded using load_library. Suppose, beginning in a fresh HOL session, the user wishes to create a theory foo whose parents include the theories in the more_lists library. This may be done as follows:

1

 #new_theory `foo`;;
 () : void
 #load_library `more lists`;;

⋮

 Library `more lists` loaded.
 () : void

Loading the library while drafting the theory foo makes the theory more_lists into a parent of foo. The same effect could have been achieved (in a fresh session) by first loading the library and then creating foo:

1

 #load_library `more lists`;;

⋮

 Library `more lists` loaded.
 () : void
 #new_theory `foo`;;
 () : void

Here, the theory more_lists is first made the current theory of the new session. It then automatically becomes a parent of foo when this theory is created by new_theory.

Now, suppose that foo has been created as shown above, and the user does some work in this theory, quits HOL and in a later session wishes to load the theory foo. This must be done by first loading the more_lists library and then loading the theory foo.

1

 #load_library `more lists`;;

⋮

 Library `more lists` loaded.
 () : void
 #load_theory `foo`;;
 Theory foo loaded
 () : void

This sequence of actions ensures that the system can find the parent theory more_lists when it comes to load foo, since loading the library updates the search path.

1.16.2 The load more lists Function

The more_lists library may in many cases simply be loaded into the system as illustrated by the examples given above. There are, however, certain situations in which the more_lists library cannot be fully loaded at the time when load_library is used. This occurs when the system is not in draft mode and the current theory is not an ancestor of the theory more_lists. In this case, loading the library can and will update the search paths, as usual. But the more_lists theory in the library can neither be made into a parent of the current theory nor can it be made the current theory. This means that autoloading from the library cannot at this stage be activated. Nor can the ML code in the library be loaded into HOL, since it requires access to some of the theorems in the library.

In the situation described above—when the system is not in draft mode and the current theory is not an ancestor of the theory more_lists—the library load sequence defines an ML function called load_more_lists in the current HOL session. If at a future point in the session the more_lists theory (now accessible via the search path) becomes an ancestor of the current theory, this function can then be used to complete loading of the library. Evaluating

    load_more_lists();;

in such a context loads the ML functions of the more_lists library into HOL and activates autoloading from its theory files. The function load_more_lists fails if the theory more_lists is not a parent of the current theory.

Note that the function load_more_lists becomes available when loading the more_lists library only if the more_lists theory at that point can neither be made into a new parent (i.e. the system is not in draft mode) nor be made the current theory.

ML Functions in the more lists Library

This chapter provides documentation on all the ML functions that are made available in HOL when the more_lists library is loaded. This documentation is also available online via the help facility.

 BUTLAST_CONV

BUTLAST_CONV : conv

Synopsis

Computes by inference the result of stripping the last element of a list.

Description

For any object language list of the form "[x0;...x(n-1)]" , the result of evaluating

   BUTLAST_CONV "BUTLAST [x0;...;x(n-1)]"

is the theorem

   |- BUTLAST [x0;...;x(n-1)] = [x0;...; x(n-2)]

Failure

BUTLAST_CONV tm fails if tm is not a non-null list.

 ELL_CONV

ELL_CONV : conv

Synopsis

Computes by inference the result of taking an element of a list.

Description

For any object language list of the form "[x1;...;xk;...xn]" , the result of evaluating

   ELL_CONV "ELL k [x1;...;xk;...;xn]"

is the theorem

   |- ELL k [x1;...;xk;...;xn] = xk

where k must not be greater then the length of the list. Note that ELL index the list elements from 1.

Failure

ELL_CONV tm fails if tm is not of the form described above, or k is greater than the length of the list.

See also

EL_CONV

 EL_CONV

EL_CONV : conv

Synopsis

Computes by inference the result of taking an element from a list.

Description

For any object language list of the form "[x0;...xk;...;xn]" , the result of evaluating

   EL_CONV "EL k [x0;...xk;...;xn]"

is the theorem

   |- EL k [x0;...;xk;...;xn] = xk

Failure

EL_CONV tm fails if tm is not of the form described above, or k is not less than the length of the list.

See also

ELL_CONV

 EQ_LENGTH_INDUCT_TAC

EQ_LENGTH_INDUCT_TAC : tactic

Synopsis

Performs tactical proof by structural induction on two equal length lists.

Description

EQ_LENGTH_INDUCT_TAC reduces a goal !x y . (LENGTH x = LENGTH y) ==> t[x,y], where

x and y range over lists, to two subgoals corresponding to the base and step cases in a proof by induction on the length of x and y. The induction hypothesis appears among the assumptions of the subgoal for the step case. The specification of EQ_LENGTH_INDUCT_TAC is:

         A ?- !x y . (LENGTH x = LENGTH y) ==> t[x,y]
   ====================================================  EQ_LENGTH_INDUCT_TAC
                            A ?- t[NIL/x][NIL/y]
    A u {LENGTH x = LENGTH y, t[x'/x, y'/y]} ?-
         !h h'. t[(CONS h x)/x, (CONS h' y)/y]

Failure

EQ_LENGTH_INDUCT_TAC g fails unless the conclusion of the goal g has the form

   !x y . (LENGTH x = LENGTH y) ==> t[x,y]

where the variables x and y have types (xty)list and (yty)list for some types xty and yty. It also fails if either of the variables x or y appear free in the assumptions.

Uses

use this tactic when structural induction is performed on two lists and they have identical length.

See also

LIST_APPEND_INDUCT_TAC, LIST_INDUCT_TAC, SNOC_INDUCT_TAC,
LENGTH_LIST_INDUCT_TAC, EQ_LENGTH_SNOC_INDUCT_TAC.

 EQ_LENGTH_SNOC_INDUCT_TAC

EQ_LENGTH_SNOC_INDUCT_TAC : tactic

Synopsis

Performs tactical proof by structural induction on two equal length lists from the tail end.

Description

EQ_LENGTH_SNOC_INDUCT_TAC reduces a goal !x y . (LENGTH x = LENGTH y) ==> t[x,y],

where x and y range over lists, to two subgoals corresponding to the base and step cases in a proof by induction on the length of x and y. The induction hypothesis appears among the assumptions of the subgoal for the step case. The specification of

EQ_LENGTH_SNOC_INDUCT_TAC is:
     A ?- !x y . (LENGTH x = LENGTH y) ==> t[x,y]
   ================================================  EQ_LENGTH_SNOC_INDUCT_TAC
                            A ?- t[NIL/x][NIL/y]
    A u {LENGTH x = LENGTH y, t[x'/x, y'/y]} ?-
         !h h'. t[(SNOC h x)/x, (SNOC h' y)/y]

Failure

EQ_LENGTH_SNOC_INDUCT_TAC g fails unless the conclusion of the goal g has the form

   !x y . (LENGTH x = LENGTH y) ==> t[x,y]

where the variables x and y have types (xty)list and (yty)list for some types xty and yty. It also fails if either of the variables x or y appear free in the assumptions.

Uses

use this tactic when structural induction is performed on two lists and they have identical length.

See also

LIST_APPEND_INDUCT_TAC, LIST_INDUCT_TAC, SNOC_INDUCT_TAC,
LENGTH_LIST_INDUCT_TAC, EQ_LENGTH_INDUCT_TAC

 LASTN_CONV

LASTN_CONV : conv

Synopsis

Computes by inference the result of taking the last n elements of a list.

Description

For any object language list of the form "[x0;...x(n-k);...;x(n-1)]" , the result of evaluating

   LASTN_CONV "LASTN k [x0;...x(n-k);...;x(n-1)]"

is the theorem

   |- LASTN k [x0;...;x(n-k);...;x(n-1)] = [x(n-k);...;x(n-1)]

Failure

LASTN_CONV tm fails if tm is not of the form described above, or k is greater than the length of the list.

 LAST_CONV

LAST_CONV : conv

Synopsis

Computes by inference the result of taking the last element of a list.

Description

For any object language list of the form "[x0;...x(n-1)]" , the result of evaluating

   LAST_CONV "LAST [x0;...;x(n-1)]"

is the theorem

   |- LAST [x0;...;x(n-1)] = x(n-1)

Failure

LAST_CONV tm fails if tm is not a non-null list.

 LENGTH_LIST_INDUCT_TAC

LENGTH_LIST_INDUCT_TAC : tactic

Synopsis

Performs tactical proof by structural induction on the length of lists.

Description

LENGTH_LIST_INDUCT_TAC reduces a goal !x y . (LENGTH x = LENGTH y) ==> P, where x

and y range over lists, to two subgoals corresponding to the base and step cases in a proof by induction on the length of x and y. The induction hypothesis appears among the assumptions of the subgoal for the step case. The specification of LENGTH_LIST_INDUCT_TAC is:

         A ?- !x y . (LENGTH x = LENGTH y) ==> P
   ====================================================  LENGTH_LIST_INDUCT_TAC
                            A ?- P[NIL/x][NIL/y]
    A u {P[TL x/x][TL y/y]} ?-
         P[(CONS(HD x)(TL x))/x][(CONS(HD y)(TL y))/y]

When LENGTH_LIST_INDUCT_TAC is applied to a goal of the form

   !x y . (LENGTH x = LENGTH y) ==> P

where x does not appear free in P, the subgoals generated are just A ?- P[NIL/x] and

A u {P[TL x/x]} ?- P[CONS(HD x)(TL x)/x]. Similar subgoals are generated if y does

not appear free in P. If neither x nor y appear free the goal is unchanged.

Failure

LENGTH_LIST_INDUCT_TAC g fails unless the conclusion of the goal g has the form

   !x y . (LENGTH x = LENGTH y) ==> P

where the variables x and y have types (xty)list and (yty)list for some types xty and yty. It also fails if either of the variables x or y appear free in the assumptions.

See also

LIST_APPEND_INDUCT_TAC, LIST_INDUCT_TAC, SNOC_INDUCT_TAC.

 LIST_APPEND_INDUCT_TAC

LIST_APPEND_INDUCT_TAC : tactic

Synopsis

Performs tactical proof by structural induction on lists from the tail end using APPEND.

\underline{MAP2 CONV 27}

Description

LIST_APPEND_INDUCT_TAC reduces a goal !l.P, where l ranges over lists, to two subgoals corresponding to the base and step cases in a proof by structural induction on l from the tail end using APPEND. The induction hypothesis appears among the assumptions of the subgoal for the step case. The specification of LIST_APPEND_INDUCT_TAC is:

                       A ?- !l. P
   ==================================================  LIST_APPEND_INDUCT_TAC
                  A ?- P[NIL/l]
    A u {P[l'/l]} ?- !h. P[APPEND l' (CONS h NIL)/l]

where l' is a primed variant of l that does not appear free in the assumptions A (usually, l' is just l). When LIST_APPEND_INDUCT_TAC is applied to a goal of the form !l.P, where l does not appear free in P, the subgoals are just A ?- P and A u {P} ?- !h.P.

Failure

LIST_APPEND_INDUCT_TAC g fails unless the conclusion of the goal g has the form !l.t, where the variable l has type (ty)list for some type ty.

See also

LENGTH_LIST_INDUCT_TAC, LIST_INDUCT_TAC, SNOC_INDUCT_TAC.

 MAP2_CONV

MAP2_CONV : conv -> conv

Synopsis

Compute the result of mapping a binary function down two lists.

Description

The function MAP2_CONV is a parameterized conversion for computing the result of mapping a binary function f:ty1->ty2->ty3 down two lists "[l11;...;l1n]" whose elements are of type ty1 and "[l21;...;l2n]" whose elements are of type ty2. The lengths of the two lists must be identical. The first argument to MAP2_CONV is expected to be a conversion that computes the result of applying the function f to a pair of corresponding elements of these lists. When applied to a term "f l1i l2i", this conversion should return a theorem of the form |- (f l1i l2i) = ri, where ri is the result of applying the function f to the elements l1i and l2i.

Given an appropriate conv, the conversion MAP2_CONV conv takes a term of the form

"[MAP2 f [l11;...;dl2tn] [l21;...;l2n]" to the theorem
   |- MAP2 f [l11;...;l1n] [l21;...;l2n] = [r1;...;rn]
where conv "f l1i l2i" returns |- (f l1i l2i) = ri for i from 1 to n.

Example

The following is a very simple example in which the corresponding elements from the two lists are summed to form the resulting list:

   #MAP2_CONV ADD_CONV "MAP2 $+ [1;2;3] [1;2;3]";;
   |- MAP2 $+ [1;2;3] [1;2;3] = [2;4;6]

Failure

MAP2_CONV conv fails if applied to a term not of the form described above. An application

of MAP2_CONV conv to a term "MAP2 f [l11;...;l1n] [l21;...;l2n]" fails unless for all
i where 1<=i<=n evaluating conv "f l1i l2i" returns |- (f l1i l2i) = ri for some ri.

See also

MAP_CONV

 NBUTLAST_CONV

NBUTLAST_CONV : conv

Synopsis

Computes by inference the result of taking the initial segment of a list.

Description

For any object language list of the form "[x0;...x(n-k);...;x(n-1)]" , the result of evaluating

   NBUTLAST_CONV "NBUTLAST k [x0;...x(n-k);...;x(n-1)]"

is the theorem

   |- NBUTLAST k [x0;...;x(n-k);...;x(n-1)] = [x0;...;x(n-k-1)]

Failure

NBUTLAST_CONV tm fails if tm is not of the form described above, or k is greater than the length of the list.

 SNOC_CONV

SNOC_CONV : conv

Synopsis

Computes by inference the result of adding an element to the end of a list.

Description

For any object language list of the form "[x0;...;x(n-1)]" , the result of evaluating

   SNOC_CONV "SNOC x [x0;...;x(n-1)]"

is the theorem

   |- SNOC x [x0;...;x(n-1)] = [x0;...;x(n-1);x]

Failure

SNOC_CONV tm fails if tm is not of the form described above.

 SNOC_INDUCT_TAC

SNOC_INDUCT_TAC : tactic

Synopsis

Performs tactical proof by structural induction on lists from the tail end using SNOC.

Description

SNOC_INDUCT_TAC reduces a goal !l.P, where l ranges over lists, to two subgoals corresponding to the base and step cases in a proof by structural induction on l from the tail end using SNOC. The induction hypothesis appears among the assumptions of the subgoal for the step case. The specification of SNOC_INDUCT_TAC is:

                         A ?- !l. P
   =====================================================  SNOC_INDUCT_TAC
    A ?- P[NIL/l]   A u {P[l'/l]} ?- !h. P[SNOC h l'/l]

where l' is a primed variant of l that does not appear free in the assumptions A (usually, l' is just l). When SNOC_INDUCT_TAC is applied to a goal of the form !l.P, where l does not appear free in P, the subgoals are just A ?- P and A u {P} ?- !h.P.

Failure

SNOC_INDUCT_TAC g fails unless the conclusion of the goal g has the form !l.t, where the variable l has type (ty)list for some type ty.

See also

LENGTH_LIST_INDUCT_TAC, LIST_APPEND_INDUCT_TAC, LIST_INDUCT_TAC.

 SPLIT_CONV

SPLIT_CONV : conv

Synopsis

Computes by inference the result of splitting a list into two.

Description

For any object language list of the form "[x0;...xk;...;xn]" , the result of evaluating

   SPLIT_CONV "SPLIT k [x0;...xk;...;xn]"

is the theorem

   |- SPLIT k [x0;...;xk;...;xn] = [x0;...;x(k-1)],[xk;...;xn]

Failure

SPLIT_CONV tm fails if tm is not of the form described above, or k is not less than the length of the list.

 SUBST_REVERSE_CONV

SUBST_REVERSE_CONV : conv

Synopsis

Applies a predicate to the reverse of a list rather than the list.

Description

When applied to a term of the form "!x. P x", where x has type :(ty)list for some type ty, the conversion SUBST_REVERSE_CONV returns the theorem:

   |- (!x. P x) = (!y. P(REVERSE y))

Failure

Fails if applied to a term not of the form "!x. P x", where x has type :(ty)list for some type ty.

32 Chapter 2. ML Functions in the more lists Library

Pre-proved Theorems

The following pages give all the definitions and theorems about lists in the more_lists library. The theorems are grouped into sections according to subject matter. Some theorems could be classified under more than one subject, but each theorem is listed in only one section. The reader may therefore have to consult more than one section when searching for any particular theorem.

When the library is loaded, all the theorems in the library are set up to autoload when their names are mentioned in ML. The name of the theory in which each theorem is stored is given in parentheses after the name of the theorem.

3.1 General List Theorems

CONS_ONE_ONE (general lists)
  |- !h t h' t'. (CONS h t = CONS h' t') ==> (h = h') /\ (t = t')
LENGTH1_CONS_HD (general lists)
  |- !l. (LENGTH l = 1) = ([HD l] = l)
LENGTH_EQ (general lists)
  |- !x y. (x = y) ==> (LENGTH x = LENGTH y)
LENGTH_EQ_SUC_IMP_NOT_NIL (general lists)
  |- !l k. (LENGTH l = SUC k) ==> ~(l = [])
LENGTH_EQ_SUC_IMP_NOT_NULL (general lists)
  |- !l k. (LENGTH l = SUC k) ==> ~NULL l
LENGTH_GR_0_NOT_NIL (general lists)
  |- !l. 0 < (LENGTH l) ==> ~(l = [])
LENGTH_LESS_EQ (general lists)
  |- !l1 l2.
      (LENGTH l1) <= (LENGTH l2) ==>
      (!a. (LENGTH l1) < (LENGTH(CONS a l2)))

34 Chapter 3. Pre-proved Theorems

LENGTH_LESS_EQ_EQ (general lists)
  |- !l1 l2 a.
      (LENGTH l1) <= (LENGTH l2) = (LENGTH l1) < (LENGTH(CONS a l2))
LENGTH_LESS_IMP_NOT_EQ (general lists)
  |- !l1 l2. (LENGTH l1) < (LENGTH l2) ==> ~(l1 = l2)
LENGTH_NOT_NULL (general lists)
  |- !l. 0 < (LENGTH l) = ~NULL l
LENGTH_NULL (general lists)
  |- !l. (LENGTH l = 0) = NULL l
LENGTH_TL_SUB (general lists)
  |- !l. ~NULL l ==> (LENGTH(TL l) = (LENGTH l) - 1)
list_NULL_CASES (general lists)
  |- !l. NULL l \/ (?t h. l = CONS h t)
L_EQ_NIL (general lists)
  |- !l. (l = []) = NULL l
NIL_EQ_L (general lists)
  |- !l. ([] = l) = NULL l
NOT_LENGTH_EQ (general lists)
  |- !l2 l1. ~(LENGTH l1 = LENGTH l2) ==> ~(l1 = l2)
NULL_EQ_EMPTY (general lists)
  |- !l. NULL l = (l = [])
TL_NIL (general lists)
  |- !l. (LENGTH l = 1) ==> (TL l = [])
TL_NULL (general lists)
  |- !l. (LENGTH l = 1) ==> NULL(TL l)

3.2 Theorems about the Tail End of a List

BUTLAST (snoc)
  |- !h t. BUTLAST(SNOC h t) = t
BUTLAST_CONS (snoc)
  |- !h t. BUTLAST(CONS h t) = (NULL t => [] | CONS h(BUTLAST t))

3.2. Theorems about the Tail End of a List 35

BUTLAST_CONS_NOT_NULL (snoc)
  |- !h l. ~NULL l ==> (BUTLAST(CONS h l) = CONS h(BUTLAST l))
BUTLAST_DEF (snoc)
  |- !l. BUTLAST l = (@t. SNOC(LAST l)t = l)
BUTLAST_EL (snoc)
  |- !a. BUTLAST[a] = []
BUTLAST_NIL (snoc)
  |- !l. (LENGTH l = 1) ==> (BUTLAST l = [])
BUTLAST_NULL (snoc)
  |- !l. (LENGTH l = 1) ==> NULL(BUTLAST l)
BUTLAST_REVERSE_EQ_REVERSE_TL (snoc)
  |- !l. ~NULL l ==> (BUTLAST(REVERSE l) = REVERSE(TL l))
BUTLAST_TL (snoc)
  |- !l. 1 < (LENGTH l) ==> (BUTLAST(TL l) = TL(BUTLAST l))
HD_BUTLAST (snoc)
  |- !l. 1 < (LENGTH l) ==> (HD(BUTLAST l) = HD l)
HD_SNOC (snoc)
  |- !h t. HD(SNOC h t) = (NULL t => h | HD t)
ISO_REVERSE (snoc)
  |- ISO REVERSE
LAST (snoc)
  |- !h t. LAST(SNOC h t) = h
LAST_BUTLAST_exist (snoc)
  |- !l. ~NULL l ==> (?h t. SNOC h t = l)
LAST_CONS (snoc)
  |- !h t. LAST(CONS h t) = (NULL t => h | LAST t)
LAST_CONS_NOT_NULL (snoc)
  |- !h l. ~NULL l ==> (LAST(CONS h l) = LAST l)
LAST_DEF (snoc)
  |- !l. LAST l = (@h. ?t. SNOC h t = l)
LAST_EL (snoc)
  |- !a. LAST[a] = a

LAST_REVERSE_EQ_HD (snoc)
  |- !l. ~NULL l ==> (LAST(REVERSE l) = HD l)
LAST_TL (snoc)
  |- !l. 1 < (LENGTH l) ==> (LAST(TL l) = LAST l)
LENGTH_BUTLAST (snoc)
  |- !l. ~NULL l ==> (LENGTH(BUTLAST l) = PRE(LENGTH l))
LENGTH_SNOC (snoc)
  |- !l n.
      (LENGTH l = SUC n) = (?h l'. (LENGTH l' = n) /\ (l = SNOC h l'))
LENGTH_TL (snoc)
  |- !l. ~NULL l ==> (LENGTH(TL l) = PRE(LENGTH l))
NOT_NIL_SNOC (snoc)
  |- !h t. ~([] = SNOC h t)
NOT_SNOC_NIL (snoc)
  |- !h t. ~(SNOC h t = [])
REVERSE_CLAUSES (snoc)
  |- (REVERSE[] = []) /\
     (!h l. REVERSE(CONS h l) = SNOC h(REVERSE l)) /\
     (!d l. REVERSE(SNOC d l) = CONS d(REVERSE l)) /\
     (!l. REVERSE(REVERSE l) = l)
REVERSE_DEF (snoc)
  |- (REVERSE[] = []) /\ (!h l. REVERSE(CONS h l) = SNOC h(REVERSE l))
REVERSE_EQ_NIL (snoc)
  |- !l. (REVERSE l = []) = (l = [])
REVERSE_EXISTS (snoc)
  |- !s. ?t. t = REVERSE s
REVERSE_NULL (snoc)
  |- !l. NULL(REVERSE l) = NULL l
REVERSE_REVERSE (snoc)
  |- !l. REVERSE(REVERSE l) = l
REVERSE_SINGLE (snoc)
  |- !h. REVERSE[h] = [h]

3.3. Theorems about TAIL 37

SAME_LENGTH_SNOC (snoc)
  |- !l a b.
      (LENGTH l = LENGTH(SNOC a b)) =
      (?a' b'. (LENGTH b' = LENGTH b) /\ (l = SNOC a' b'))
SNOC (snoc)
  |- !l. ~NULL l ==> (SNOC(LAST l)(BUTLAST l) = l)
SNOC_11 (snoc)
  |- !h t h' t'. (SNOC h t = SNOC h' t') = (h = h') /\ (t = t')
SNOC_Axiom (snoc)
  |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(SNOC h t) = f(fn t)h t)
SNOC_CASES (snoc)
  |- !l. (l = []) \/ (?t h. l = SNOC h t)
SNOC_DEF (snoc)
  |- (!d. SNOC d[] = [d]) /\ (!d h t. SNOC d(CONS h t) = CONS h(SNOC d t))
SNOC_EQ_LENGTH_EQ (snoc)
  |- !l1 y1 l2 y2. (SNOC y1 l1 = SNOC y2 l2) ==> (LENGTH l1 = LENGTH l2)
SNOC_INDUCT (snoc)
  |- !P. P[] /\ (!t. P t ==> (!h. P(SNOC h t))) ==> (!l. P l)
SNOC_NOT_NULL (snoc)
  |- !d l. ~NULL(SNOC d l)
SNOC_NULL_CASES (snoc)
  |- !l. NULL l \/ (?t h. l = SNOC h t)
SNOC_ONE_ONE (snoc)
  |- !h t h' t'. (SNOC h t = SNOC h' t') ==> (h = h') /\ (t = t')
SNOC_REVERSE_CONS (snoc)
  |- !d l. SNOC d l = REVERSE(CONS d(REVERSE l))
TL_SNOC (snoc)
  |- !h t. TL(SNOC h t) = (NULL t => [] | SNOC h(TL t))

3.3 Theorems about TAIL

CON (tail)
  |- !l. ~NULL l ==> (CONS(HD l)(TAIL l) = l)

LENGTH_TAIL (tail)
  |- !l. ~NULL l ==> (LENGTH(TAIL l) = (LENGTH l) - 1)
list_CASES2 (tail)
  |- !l. (l = []) \/ (l = CONS(HD l)(TAIL l))
list_NULL_CASES2 (tail)
  |- !l. NULL l \/ (l = CONS(HD l)(TAIL l))
NOT_NULL_TAIL (tail)
  |- !l. ~NULL(TAIL l) ==> ~NULL l
TAIL (tail)
  |- (TAIL[] = []) /\ (!h t. TAIL(CONS h t) = t)
TAIL_APPEND (tail)
  |- !x y. TAIL(APPEND x y) = ((x = []) => TAIL y | APPEND(TAIL x)y)
TL_TAIL (tail)
  |- !l. ~NULL l ==> (TL l = TAIL l)

3.4 Theorems about APPEND and Related Operators

APPEND_11 (append)
  |- !x y z. (APPEND x y = APPEND x z) = (y = z)
APPEND_BUTLAST_LAST (append)
  |- !l. ~NULL l ==> (APPEND(BUTLAST l)[LAST l] = l)
APPEND_CLAUSES (append)
  |- (!l. APPEND[]l = l) /\
     (!l1. APPEND l1[] = l1) /\
     (!l1 l2 h. APPEND(CONS h l1)l2 = CONS h(APPEND l1 l2)) /\
     (!d l1 l2. APPEND l1(SNOC d l2) = SNOC d(APPEND l1 l2))
APPEND_CONS (append)
  |- !l1 l2 h. APPEND(CONS h l1)l2 = APPEND[h](APPEND l1 l2)
APPEND_CONS_EQ_APPEND (append)
  |- !l1 l2 h. APPEND l1(CONS h l2) = APPEND(APPEND l1[h])l2
APPEND_CONS_EQ_APPEND_SNOC (append)
  |- !l1 l2 h. APPEND l1(CONS h l2) = APPEND(SNOC h l1)l2

3.4. Theorems about APPEND and Related Operators 39

APPEND_EL_11 (append)
  |- !l1 y1 l2 y2.
      (APPEND l1[y1] = APPEND l2[y2]) = (l1 = l2) /\ ([y1] = [y2])
APPEND_EL_REVERSE_CONS (append)
  |- !t h. APPEND t[h] = REVERSE(CONS h(REVERSE t))
APPEND_ID (append)
  |- !l l'. (l = APPEND l l') = (l' = [])
APPEND_ID_NULL (append)
  |- !l l'. (l = APPEND l l') = NULL l'
APPEND_IS_NIL (append)
  |- !l1 l2. (APPEND l1 l2 = []) = (l1 = []) /\ (l2 = [])
APPEND_IS_NULL (append)
  |- !l1 l2. NULL(APPEND l1 l2) = NULL l1 /\ NULL l2
APPEND_JOIN (append)
  |- !l1 l2.
      ~NULL l1 /\ ~NULL l2 ==>
      (APPEND l1 l2 = APPEND(BUTLAST l1)(APPEND[LAST l1;HD l2](TL l2)))
APPEND_LENGTH_EQ (append)
  |- !l1 l1'.
      (LENGTH l1 = LENGTH l1') ==>
      (!l2 l2'.
        (LENGTH l2 = LENGTH l2') ==>
        ((APPEND l1 l2 = APPEND l1' l2') = (l1 = l1') /\ (l2 = l2')))
APPEND_NIL (append)
  |- (!l. APPEND l[] = l) /\ (!l. APPEND[]l = l)
BUTLAST1 (append)
  |- !l y. BUTLAST(APPEND l[y]) = l
BUTLAST_APPEND (append)
  |- !l2.
      ~NULL l2 ==> (!l1. BUTLAST(APPEND l1 l2) = APPEND l1(BUTLAST l2))
CONS_APPEND_CONS (append)
  |- !a l. CONS a l = APPEND[a]l

CONS_MEMBER_LIST (append)
  |- !s s' t a.
      (APPEND s t = CONS a s') ==>
      (s = []) \/ (?r. (s = CONS a r) /\ (s' = APPEND r t))
CONS_MEMBER_LIST_NULL (append)
  |- !s s' t a.
      (APPEND s t = CONS a s') ==>
      NULL s \/ (?r. (s = CONS a r) /\ (s' = APPEND r t))
HD_APPEND (append)
  |- !l1. ~(l1 = []) ==> (!l2. HD(APPEND l1 l2) = HD l1)
HD_APPEND_NULL (append)
  |- !l1. ~NULL l1 ==> (!l2. HD(APPEND l1 l2) = HD l1)
HEAD_APPEND (append)
  |- !x y. HD(APPEND x y) = ((x = []) => HD y | HD x)
HEAD_APPEND_NULL (append)
  |- !x y. HD(APPEND x y) = (NULL x => HD y | HD x)
IMP_APPEND_NOT_NIL (append)
  |- !l1 l2. ~(l1 = []) \/ ~(l2 = []) ==> ~(APPEND l1 l2 = [])
IMP_APPEND_NOT_NULL (append)
  |- !l1 l2. ~NULL l1 \/ ~NULL l2 ==> ~NULL(APPEND l1 l2)
ITERATED (append)
  |- (!s. ITERATED 0 s = []) /\
     (!n s. ITERATED(SUC n)s = APPEND s(ITERATED n s))
ITERATED_EMPTY (append)
  |- !n. ITERATED n[] = []
LAST1 (append)
  |- !l y. LAST(APPEND l[y]) = y
LAST_APPEND (append)
  |- !l2. ~NULL l2 ==> (!l1. LAST(APPEND l1 l2) = LAST l2)
LENGTH_APPEND_EL (append)
  |- !l1 y1 l2 y2.
      (APPEND l1[y1] = APPEND l2[y2]) ==> (LENGTH l1 = LENGTH l2)

3.4. Theorems about APPEND and Related Operators 41

LENGTH_CLAUSES (append)
  |- (LENGTH[] = 0) /\
     (!h t. LENGTH(CONS h t) = SUC(LENGTH t)) /\
     (!d l. LENGTH(SNOC d l) = SUC(LENGTH l)) /\
     (!l1 l2. LENGTH(APPEND l1 l2) = (LENGTH l1) + (LENGTH l2)) /\
     (!l. LENGTH(REVERSE l) = LENGTH l)
LENGTH_REPLICATE (append)
  |- !x n. LENGTH(REPLICATE n x) = n
list_APPEND_Axiom (append)
  |- !x f. ?! fa. (fa[] = x) /\ (!h t. fa(APPEND t[h]) = f(fa t)h t)
list_APPEND_CASES (append)
  |- !l. (l = []) \/ (?t h. l = APPEND t[h])
list_APPEND_INDUCT (append)
  |- !P. P[] /\ (!t. P t ==> (!h. P(APPEND t[h]))) ==> (!l. P l)
list_APPEND_NULL_CASES (append)
  |- !l. NULL l \/ (?t h. l = APPEND t[h])
NIL_NOT_APPEND_CONS2 (append)
  |- !l1 l2. (l2 = CONS h t) ==> ~([] = APPEND l1 l2)
NOT_NIL_APPEND_EL (append)
  |- !l h. ~([] = APPEND l[h])
NULL_ITERATED (append)
  |- !n. NULL(ITERATED n[])
NULL_NOT_APPEND_CONS (append)
  |- !l1 l2. (l2 = CONS h t) ==> ~([] = APPEND l1 l2)
ONE_MEMBER_LIST (append)
  |- !s t a. (APPEND s t = [a]) ==> (s = []) \/ (s = [a])
ONE_MEMBER_LIST_NULL (append)
  |- !s t a. (APPEND s t = [a]) ==> NULL s \/ (s = [a])
REPLICATE (append)
  |- (!in. REPLICATE 0 in = []) /\
     (!n in. REPLICATE(SUC n)in = CONS in(REPLICATE n in))
REVERSE (append)
  |- (REVERSE[] = []) /\ (!h t. REVERSE(CONS h t) = APPEND(REVERSE t)[h])

REVERSE_APPEND (append)
  |- !l1 l2. REVERSE(APPEND l2 l1) = APPEND(REVERSE l1)(REVERSE l2)
REVERSE_APPEND_EL_CONS (append)
  |- !h t. REVERSE(APPEND t[h]) = CONS h(REVERSE t)
SNOC_APPEND_CONS (append)
  |- !l h. SNOC h l = APPEND l[h]
SUBSEQUENCE_EXISTS (append)
  |- !s. ?a b. s = APPEND a b
TL_APPEND (append)
  |- !l1. ~(l1 = []) ==> (!l2. TL(APPEND l1 l2) = APPEND(TL l1)l2)
TL_APPEND_NULL (append)
  |- !l1. ~NULL l1 ==> (!l2. TL(APPEND l1 l2) = APPEND(TL l1)l2)

3.5 Theorems about Higher Order Functions

EVERY_APPEND (map)
  |- !l1 l2 P. EVERY P(APPEND l1 l2) = EVERY P l1 /\ EVERY P l2
EVERY_MAP (map)
  |- !f P l. EVERY P(MAP f l) = EVERY(P o f)l
EVERY_SNOC (snoc)
  |- !P h l. EVERY P(SNOC h l) = EVERY P l /\ P
HD_MAP (map)
  |- !f l. ~NULL l ==> (HD(MAP f l) = f(HD l))
ITLIST (map)
  |- (!f x. ITLIST f[]x = x) /\
     (!f hd tl x. ITLIST f(CONS hd tl)x = f hd(ITLIST f tl x))
ITLIST_MAP_EQ (map)
  |- !f g l. ITLIST $/\(MAP(\x. f x = g x)l)T = (MAP f l = MAP g l)
MAP2_SNOC (map)
  |- !f h1 h2 l1 l2.
      (LENGTH l1 = LENGTH l2) ==>
      (MAP2 f(SNOC h1 l1)(SNOC h2 l2) = SNOC(f h1 h2)(MAP2 f l1 l2))

3.6. Theorems about EL and EL1 43

MAP_MAP_o (map)
  |- !f g l. MAP f(MAP g l) = MAP(f o g)l
MAP_SNOC (map)
  |- !f h t. MAP f(SNOC h t) = SNOC(f h)(MAP f t)
NULL_MAP (map)
  |- !f l. NULL(MAP f l) = NULL l
TAIL_MAP (map)
  |- !f l. TAIL(MAP f l) = MAP f(TAIL l)
TL_MAP (map)
  |- !f l. ~NULL l ==> (TL(MAP f l) = MAP f(TL l))

3.6 Theorems about EL and EL1

EL1 (el)
  |- !n l. EL1(SUC n)l = EL n l
EL1_HD (el)
  |- !l. ~NULL l ==> (EL1 1 l = HD l)
EL1_SUC_CONS (el)
  |- !n h l. 0 < n ==> (EL1(SUC n)(CONS h l) = EL1 n l)
EL_0_REVERSE (el)
  |- !l. ~NULL l ==> (EL 0(REVERSE l) = EL(PRE(LENGTH l))l)
EL_APPEND_1 (el)
  |- !l1 l2 k. k < (LENGTH l1) ==> (EL k(APPEND l1 l2) = EL k l1)
EL_APPEND_2 (el)
  |- !l1 l2 k.
      (LENGTH l1) <= k ==> (EL k(APPEND l1 l2) = EL(k - (LENGTH l1))l2)
EL_APPEND_EL (el)
  |- !l y k. k < (LENGTH l) ==> (EL k(APPEND l[y]) = EL k l)
EL_BUTLAST (el)
  |- !l x. ~NULL l ==> (SUC x) < (LENGTH l) ==> (EL x(BUTLAST l) = EL x l)
EL_CONS (el)
  |- !k l y. 0 < k ==> (EL k(CONS y l) = EL(PRE k)l)

EL_CONS_SUB1 (el)
  |- !n h l. ~(n = 0) ==> (EL n(CONS h l) = EL(n - 1)l)
EL_HD (el)
  |- !l. ~NULL l ==> (EL 0 l = HD l)
EL_LENGTH_APPEND (el)
  |- !l1 l2. ~NULL l2 ==> (EL(LENGTH l1)(APPEND l1 l2) = HD l2)
EL_MAP (el)
  |- !f l n. n < (LENGTH l) ==> (EL n(MAP f l) = f(EL n l))
EL_MAP2 (el)
  |- !f l l' n.
      (LENGTH l = LENGTH l') ==>
      n < (LENGTH l) \/ n < (LENGTH l') ==>
      (EL n(MAP2 f l l') = f(EL n l)(EL n l'))
EL_REPLICATE (el)
  |- !x n m. m < n ==> (EL m(REPLICATE n x) = x)
EL_REVERSE (el)
  |- !l k.
      k < (PRE(LENGTH l)) ==> (EL k(REVERSE l) = EL((PRE(LENGTH l)) - k)l)
EL_SNOC (el)
  |- !l y k. k < (LENGTH l) ==> (EL k(SNOC y l) = EL k l)
EXISTS_EL (el)
  |- !n a. ?l. EL n l = a
LAST_EL_LENGTH (el)
  |- !l. ~NULL l ==> (LAST l = EL(PRE(LENGTH l))l)
MAP2_EL (el)
  |- !f l l' n.
      (LENGTH l = LENGTH l') ==>
      n < (LENGTH l) \/ n < (LENGTH l') ==>
      (MAP2 f[EL n l][EL n l'] = [f(EL n l)(EL n l')])
MAP_EL (el)
  |- !f l n. n < (LENGTH l) ==> (MAP f[EL n l] = [f(EL n l)])
MAP_EL1_SUC_CONS (el)
  |- !l l' h'.
      EVERY(\n. 0 < n)l ==>
      (MAP(\n. EL1(SUC n)(CONS h' l'))l = MAP(\n. EL1 n l')l)

3.7. Theorems about ELL 45

3.7 Theorems about ELL

ELL (ell)
  |- (!l. ELL 0 l = LAST l) /\ (!n l. ELL(SUC n)l = ELL n(BUTLAST l))
ELL_APPEND_1 (ell)
  |- !l1 l2 k. k < (LENGTH l2) ==> (ELL k(APPEND l1 l2) = ELL k l2)
ELL_APPEND_2 (ell)
  |- !l1 l2 k.
      (LENGTH l2) <= k ==> (ELL k(APPEND l1 l2) = ELL(k - (LENGTH l2))l1)
ELL_CONS (ell)
  |- !l x k. k < (LENGTH l) ==> (ELL k(CONS x l) = ELL k l)
ELL_EL (ell)
  |- !l k. k < (LENGTH l) ==> (ELL k l = EL(PRE((LENGTH l) - k))l)
ELL_LAST (ell)
  |- !l. ~NULL l ==> (ELL 0 l = LAST l)
ELL_LENGTH_APPEND (ell)
  |- !l1 l2. ~NULL l1 ==> (ELL(LENGTH l2)(APPEND l1 l2) = LAST l1)
ELL_MAP (ell)
  |- !f l n. n < (LENGTH l) ==> (ELL n(MAP f l) = f(ELL n l))
ELL_MAP2 (ell)
  |- !f l l' n.
      (LENGTH l = LENGTH l') ==>
      n < (LENGTH l) \/ n < (LENGTH l') ==>
      (ELL n(MAP2 f l l') = f(ELL n l)(ELL n l'))
ELL_SNOC (ell)
  |- !l x k. 0 < k ==> (ELL k(SNOC x l) = ELL(PRE k)l)
ELL_SNOC0 (ell)
  |- !l x. ELL 0(SNOC x l) = x
ELL_SUC_SNOC (ell)
  |- !k x l. ELL(SUC k)(SNOC x l) = ELL k l
EL_ELL (ell)
  |- !l k. k < (LENGTH l) ==> (EL k l = ELL(PRE((LENGTH l) - k))l)

HD_ELL_LENGTH_CONS (ell)
  |- !l x. ELL(LENGTH l)(CONS x l) = x
HD_ELL_LENGTH_SNOC (ell)
  |- !l x. ELL(LENGTH l)(SNOC x l) = (NULL l => x | HD l)
HD_ELL_PRE_LENGTH (ell)
  |- !l. ~NULL l ==> (ELL(PRE(LENGTH l))l = HD l)
MAP2_ELL (ell)
  |- !f l l' n.
      (LENGTH l = LENGTH l') ==>
      n < (LENGTH l) \/ n < (LENGTH l') ==>
      (MAP2 f[ELL n l][ELL n l'] = [f(ELL n l)(ELL n l')])
MAP_ELL (ell)
  |- !f l n. n < (LENGTH l) ==> (MAP f[ELL n l] = [f(ELL n l)])

3.8 Theorems about Accessing Subsequences of Lists from the Front

APPEND_FIRSTN_NTL (subseq)
  |- !X n. n <= (LENGTH X) ==> (APPEND(FIRSTN n X)(NTL n X) = X)
APPEND_SUBSEQ (subseq)
  |- !r x y. (?n. r = APPEND x(SUBSEQ n y)) ==> (?a. r = APPEND x a)
APPEND_SUBSEQ2 (subseq)
  |- !r s x y.
      (APPEND r s = APPEND x y) /\ (LENGTH x) <= (LENGTH r) ==>
      (?a. r = APPEND x a)
EL_HD_NTAIL (subseq)
  |- !x l. ~NULL(NTAIL x l) ==> (EL x l = HD(NTAIL x l))
EL_NTAIL_1 (subseq)
  |- !x l.
      ~NULL(NTAIL x l) ==> (APPEND[EL x l](NTAIL(x + 1)l) = NTAIL x l)
FIRSTN (subseq)
  |- (!X. FIRSTN 0 X = []) /\
     (!n X. FIRSTN(SUC n)X = CONS(HD X)(FIRSTN n(TL X)))

3.8. Theorems about Accessing Subsequences of Lists from the Front 47

FIRSTN_APPEND1 (subseq)
  |- !x X n. n <= (LENGTH X) ==> (FIRSTN n(APPEND X[x]) = FIRSTN n X)
FIRSTN_FIRSTN (subseq)
  |- !X n m.
      m <= (LENGTH X) ==> n <= m ==> (FIRSTN n(FIRSTN m X) = FIRSTN n X)
FIRSTN_LENGTH_ID (subseq)
  |- !X. FIRSTN(LENGTH X)X = X
FIRSTN_NIL (subseq)
  |- !n X. (FIRSTN n X = []) ==> (n = 0)
FIRSTN_NULL (subseq)
  |- !n X. NULL(FIRSTN n X) ==> (n = 0)
LENGTH_FIRSTN (subseq)
  |- !n X. n <= (LENGTH X) ==> (LENGTH(FIRSTN n X) = n)
LENGTH_NTAIL (subseq)
  |- !x l. LENGTH(NTAIL x l) = (LENGTH l) - x
LENGTH_NTAIL_LESS (subseq)
  |- !l1 l2 x.
      ~NULL l2 /\ (l1 = NTAIL x l2) /\ 0 < x ==> (LENGTH l1) < (LENGTH l2)
NOT_NULL_NTAIL (subseq)
  |- !x l. ~NULL(NTAIL x l) ==> ~NULL l
NOT_NULL_NTAIL_TL (subseq)
  |- !x l. ~NULL(TAIL(NTAIL x l)) ==> ~NULL(NTAIL x(TL l))
NTAIL (subseq)
  |- (!l. NTAIL 0 l = l) /\ (!n l. NTAIL(SUC n)l = TAIL(NTAIL n l))
NTAIL_NIL (subseq)
  |- !n. NTAIL n[] = []
NTAIL_NTAIL (subseq)
  |- !x y l. NTAIL x(NTAIL y l) = NTAIL(x + y)l
NTAIL_TAIL (subseq)
  |- !x l. NTAIL x(TAIL l) = NTAIL(SUC x)l
NTL (subseq)
  |- (!X. NTL 0 X = X) /\ (!n X. NTL(SUC n)X = NTL n(TL X))

NTL_APPEND (subseq)
  |- !X Y n. n <= (LENGTH X) ==> (NTL n(APPEND X Y) = APPEND(NTL n X)Y)
NTL_LENGTH (subseq)
  |- !n X. n <= (LENGTH X) ==> (LENGTH(NTL n X) = (LENGTH X) - n)
NTL_LENGTH_APPEND (subseq)
  |- !l1 l2. NTL(LENGTH l1)(APPEND l1 l2) = l2
NTL_LENGTH_NIL (subseq)
  |- !X. NTL(LENGTH X)X = []
NTL_LENGTH_NULL (subseq)
  |- !X. NULL(NTL(LENGTH X)X)
NTL_NTL (subseq)
  |- !X n m. (n + m) <= (LENGTH X) ==> (NTL n(NTL m X) = NTL(n + m)X)
NTL_SIMP_REC (subseq)
  |- !n X. NTL n X = SIMP_REC X TL n
NTL_TL_SYM (subseq)
  |- !n X. NTL n(TL X) = TL(NTL n X)
NULL_NTAIL (subseq)
  |- !n. NULL(NTAIL n[])
NULL_SUBSEQ (subseq)
  |- !n. NULL(SUBSEQ n[])
SUBSEQ (subseq)
  |- (!x. SUBSEQ 0 x = []) /\
     (!n x.
       SUBSEQ(SUC n)x = (NULL x => [] | CONS(HD x)(SUBSEQ n(TAIL x))))
SUBSEQ2 (subseq)
  |- !n x y. CONS x(SUBSEQ n y) = SUBSEQ(SUC n)(CONS x y)
SUBSEQUENCES (subseq)
  |- !r s x y.
      (APPEND r s = APPEND x y) ==>
      (?a. r = APPEND x a) \/ (?a. x = APPEND r a)
SUBSEQ_APPEND (subseq)
  |- !x y n. SUBSEQ((LENGTH x) + n)(APPEND x y) = APPEND x(SUBSEQ n y)

3.9. Theorems about Accessing Subsequences of Lists from the Tail End 49

SUBSEQ_APPEND2 (subseq)
  |- !x y. SUBSEQ(LENGTH x)(APPEND x y) = x
SUBSEQ_EMPTY_LIST (subseq)
  |- !n. SUBSEQ n[] = []
SUBSEQ_EQ (subseq)
  |- !x y n. (x = y) ==> (SUBSEQ n x = SUBSEQ n y)
SUBSEQ_EXISTS (subseq)
  |- !s n. ?a. s = APPEND(SUBSEQ n s)a
SUBSEQ_MAP (subseq)
  |- !n s f. SUBSEQ n(MAP f s) = MAP f(SUBSEQ n s)
SUBSEQ_SUBSEQ (subseq)
  |- !n x. SUBSEQ n(SUBSEQ n x) = SUBSEQ n x
TAIL_NTAIL (subseq)
  |- !x l. TAIL(NTAIL x l) = NTAIL x(TAIL l)

3.9 Theorems about Accessing Subsequences of Lists from the Tail End

APPEND_FIRSTN_LASTN (last subseq)
  |- !X m n. (LENGTH X = m + n) ==> (APPEND(FIRSTN n X)(LASTN m X) = X)
APPEND_LASTN_LASTN (last subseq)
  |- !l m1 m2.
      (m1 + m2) <= (LENGTH l) ==>
      (APPEND(LASTN m2(NBUTLAST m1 l))(LASTN m1 l) = LASTN(m1 + m2)l)
APPEND_NBUTLAST_LASTN (last subseq)
  |- !n X. n <= (LENGTH X) ==> (APPEND(NBUTLAST n X)(LASTN n X) = X)
APPEND_NBUTLAST_NTL (last subseq)
  |- !X m n. (LENGTH X = m + n) ==> (APPEND(NBUTLAST n X)(NTL m X) = X)
BUTLAST_TO_NBUTLAST (last subseq)
  |- !l. ~NULL l ==> (BUTLAST l = NBUTLAST 1 l)
ELL_LASTN (last subseq)
  |- !l m j. m <= (LENGTH l) ==> j < m ==> (ELL j(LASTN m l) = ELL j l)

ELL_NBUTLAST (last subseq)
  |- !l k j. (j + k) <= (LENGTH l) ==> (ELL j(NBUTLAST k l) = ELL(j + k)l)
EL_NBUTLAST (last subseq)
  |- !l x k.
      k < (LENGTH l) /\ x < ((LENGTH l) - k) ==>
      (EL x(NBUTLAST k l) = EL x l)
EVERY_LASTN (last subseq)
  |- !P l. EVERY P l ==> (!m. m <= (LENGTH l) ==> EVERY P(LASTN m l))
LASTN (last subseq)
  |- (!X. LASTN 0 X = []) /\
     (!n X. LASTN(SUC n)X = APPEND(LASTN n(BUTLAST X))[LAST X])
LASTN_APPEND (last subseq)
  |- !l1 l2 n. n <= (LENGTH l2) ==> (LASTN n(APPEND l1 l2) = LASTN n l2)
LASTN_APPEND2 (last subseq)
  |- !l1 l2 n.
      (LENGTH l2) <= n ==>
      (LASTN n(APPEND l1 l2) = APPEND(LASTN(n - (LENGTH l2))l1)l2)
LASTN_CONS (last subseq)
  |- !x X n. n <= (LENGTH X) ==> (LASTN n(CONS x X) = LASTN n X)
LASTN_LASTN (last subseq)
  |- !X n m.
      m <= (LENGTH X) ==> n <= m ==> (LASTN n(LASTN m X) = LASTN n X)
LASTN_LENGTH_APPEND (last subseq)
  |- !l1 l2. LASTN(LENGTH l2)(APPEND l1 l2) = l2
LASTN_LENGTH_ID (last subseq)
  |- !X. LASTN(LENGTH X)X = X
LASTN_MAP (last subseq)
  |- !f l n. n <= (LENGTH l) ==> (LASTN n(MAP f l) = MAP f(LASTN n l))
LASTN_MAP2 (last subseq)
  |- !f l1 l2 n.
      (LENGTH l1 = LENGTH l2) ==>
      n <= (LENGTH l1) ==>
      (LASTN n(MAP2 f l1 l2) = MAP2 f(LASTN n l1)(LASTN n l2))

3.9. Theorems about Accessing Subsequences of Lists from the Tail End 51

LASTN_NBUTLAST (last subseq)
  |- !l i k.
      (i + k) < (LENGTH l) ==>
      (LASTN k(NBUTLAST i l) = NBUTLAST i(LASTN(i + k)l))
LASTN_NBUTLAST_APPEND (last subseq)
  |- !l1 l2 m k.
      (m + k) <= ((LENGTH l1) + (LENGTH l2)) /\
      k < (LENGTH l2) /\
      (LENGTH l2) <= (m + k) ==>
      (LASTN m(NBUTLAST k(APPEND l1 l2)) =
       APPEND
       (LASTN((m + k) - (LENGTH l2))l1)
       (LASTN((LENGTH l2) - k)(NBUTLAST k l2)))
LASTN_NBUTLAST_TL_SPLIT (last subseq)
  |- !l m k.
      0 < m /\ (k + m) < (LENGTH l) ==>
      (LASTN m(NBUTLAST k l) =
       APPEND(LASTN(m - 1)(NBUTLAST(k + 1)l))(LASTN 1(NBUTLAST k l)))
LASTN_NIL (last subseq)
  |- !n X. (LASTN n X = []) ==> (n = 0)
LASTN_NULL (last subseq)
  |- !n X. NULL(LASTN n X) ==> (n = 0)
LASTN_SUC_SNOC (last subseq)
  |- !l x i. LASTN(SUC i)(SNOC x l) = SNOC x(LASTN i l)
LAST_LASTN (last subseq)
  |- !l m. m <= (LENGTH l) ==> 0 < m ==> (LAST(LASTN m l) = LAST l)
LAST_NBUTLAST_EL (last subseq)
  |- !k l.
      k < (LENGTH l) ==> (LAST(NBUTLAST k l) = EL(PRE((LENGTH l) - k))l)
LAST_NBUTLAST_ELL (last subseq)
  |- !k l. k < (LENGTH l) ==> (LAST(NBUTLAST k l) = ELL k l)
LAST_TO_LASTN (last subseq)
  |- !l. ~NULL l ==> ([LAST l] = LASTN 1 l)
LENGTH_LASTN (last subseq)
  |- !n X. n <= (LENGTH X) ==> (LENGTH(LASTN n X) = n)

NBUTLAST (last subseq)
  |- (!X. NBUTLAST 0 X = X) /\
     (!n X. NBUTLAST(SUC n)X = NBUTLAST n(BUTLAST X))
NBUTLAST_APPEND (last subseq)
  |- !l1 l2 n.
      n <= (LENGTH l2) ==>
      (NBUTLAST n(APPEND l1 l2) = APPEND l1(NBUTLAST n l2))
NBUTLAST_APPEND1 (last subseq)
  |- !l1 l2 k.
      (LENGTH l2) <= k ==>
      (NBUTLAST k(APPEND l1 l2) = NBUTLAST(k - (LENGTH l2))l1)
NBUTLAST_BUTLAST_SYM (last subseq)
  |- !n X. NBUTLAST n(BUTLAST X) = BUTLAST(NBUTLAST n X)
NBUTLAST_CONS (last subseq)
  |- !h l2 n.
      n <= (LENGTH l2) ==> (NBUTLAST n(CONS h l2) = CONS h(NBUTLAST n l2))
NBUTLAST_LASTN (last subseq)
  |- !l i k.
      i <= k /\ k <= (LENGTH l) ==>
      (NBUTLAST i(LASTN k l) = LASTN(k - i)(NBUTLAST i l))
NBUTLAST_LASTN_NIL (last subseq)
  |- !l i. i <= (LENGTH l) ==> (NBUTLAST i(LASTN i l) = [])
NBUTLAST_LENGTH (last subseq)
  |- !n X. n <= (LENGTH X) ==> (LENGTH(NBUTLAST n X) = (LENGTH X) - n)
NBUTLAST_LENGTH_APPEND (last subseq)
  |- !l2 l1. NBUTLAST(LENGTH l2)(APPEND l1 l2) = APPEND l1[]
NBUTLAST_LENGTH_CONS (last subseq)
  |- !l h. NBUTLAST(LENGTH l)(CONS h l) = [h]
NBUTLAST_LENGTH_NIL (last subseq)
  |- !X. NBUTLAST(LENGTH X)X = []
NBUTLAST_LENGTH_NULL (last subseq)
  |- !X. NULL(NBUTLAST(LENGTH X)X)
NBUTLAST_MAP (last subseq)
  |- !f l n.
      n <= (LENGTH l) ==> (NBUTLAST n(MAP f l) = MAP f(NBUTLAST n l))

3.10. Theorems about List Membership 53

NBUTLAST_MAP2 (last subseq)
  |- !f l1 l2 n.
      (LENGTH l1 = LENGTH l2) ==>
      n <= (LENGTH l1) ==>
      (NBUTLAST n(MAP2 f l1 l2) = MAP2 f(NBUTLAST n l1)(NBUTLAST n l2))
NBUTLAST_NBUTLAST (last subseq)
  |- !X n m.
      (n + m) <= (LENGTH X) ==>
      (NBUTLAST n(NBUTLAST m X) = NBUTLAST(n + m)X)
NBUTLAST_SIMP_REC (last subseq)
  |- !n X. NBUTLAST n X = SIMP_REC X BUTLAST n
NBUTLAST_SUC_SNOC (last subseq)
  |- !l x i. NBUTLAST(SUC i)(SNOC x l) = NBUTLAST i l
NOT_NULL_NBUTLAST (last subseq)
  |- !k l. k < (LENGTH l) ==> ~NULL(NBUTLAST k l)

3.10 Theorems about List Membership

CONS_LLEQ_LEFT_TL (member)
  |- !l1 l2. (CONS h l1) LLEQ_LEFT l2 ==> l1 LLEQ_LEFT (TL l2)
CONS_LLESS_LEFT_APPEND_HD (member)
  |- !l l1 l2.
      ~NULL l1 /\ (CONS h l) LLESS_LEFT (APPEND l1 l2) ==> (h = HD l1)
CONS_LLESS_LEFT_HD (member)
  |- !h l1 l2. (CONS h l1) LLESS_LEFT l2 ==> (h = HD l2)
CONS_LLESS_LEFT_TL (member)
  |- !l1 l2. (CONS h l1) LLESS_LEFT l2 ==> l1 LLESS_LEFT (TL l2)
LLEQ_LEFT (member)
  |- !l1 l2. l1 LLEQ_LEFT l2 = l1 LLESS_LEFT l2 \/ (l1 = l2)
LLEQ_RIGHT (member)
  |- !l1 l2. l1 LLEQ_RIGHT l2 = l1 LLESS_RIGHT l2 \/ (l1 = l2)

LLESS_LEFT (member)
  |- (!l. [] LLESS_LEFT l = ~NULL l) /\
     (!a rest l.
       (CONS a rest) LLESS_LEFT l =
       ~NULL l /\ (a = HD l) /\ rest LLESS_LEFT (TL l))
LLESS_LEFT_APPEND (member)
  |- !l l1 l2. l LLESS_LEFT l1 ==> l LLESS_LEFT (APPEND l1 l2)
LLESS_LEFT_APPEND_LLEQ_LEFT (member)
  |- !l l1 l2.
      ~l LLESS_LEFT l1 /\ l LLESS_LEFT (APPEND l1 l2) ==> l1 LLEQ_LEFT l
LLESS_LEFT_CONS (member)
  |- !l1 l2 h.
      (TL l1) LLESS_LEFT l2 /\ (h = HD l1) /\ ~NULL l1 ==>
      l1 LLESS_LEFT (CONS h l2)
LLESS_LEFT_CONS_HD (member)
  |- !l h t. l LLESS_LEFT (CONS h t) /\ ~NULL l ==> (h = HD l)
LLESS_LEFT_CONS_TL_LLESS_LEFT (member)
  |- !l h t. l LLESS_LEFT (CONS h t) /\ ~NULL l ==> (TL l) LLESS_LEFT t
LLESS_LEFT_EXISTS_APPEND (member)
  |- !l1 l2. l1 LLESS_LEFT l2 ==> (?l. l2 = APPEND l1 l)
LLESS_LEFT_LENGTH1_NULL (member)
  |- !l1 l2. l2 LLESS_LEFT l1 /\ (LENGTH l1 = 1) ==> NULL l2
LLESS_LEFT_NULL (member)
  |- !l1 l2. l1 LLESS_LEFT l2 ==> ~NULL l2
LLESS_LEFT_SINGLE_NULL (member)
  |- !l h. l LLESS_LEFT [h] = NULL l
LLESS_RIGHT (member)
  |- (!l. [] LLESS_RIGHT l = ~NULL l) /\
     (!a rest l.
       (SNOC a rest) LLESS_RIGHT l =
       ~NULL l /\ (a = LAST l) /\ rest LLESS_RIGHT (BUTLAST l))
LLESS_RIGHT_APPEND (member)
  |- !l l1 l2. l LLESS_RIGHT l2 ==> l LLESS_RIGHT (APPEND l1 l2)

3.10. Theorems about List Membership 55

LLESS_RIGHT_APPEND_LLEQ_RIGHT (member)
  |- !l l1 l2.
      ~l LLESS_RIGHT l2 /\ l LLESS_RIGHT (APPEND l1 l2) ==>
      l2 LLEQ_RIGHT l
LLESS_RIGHT_EXISTS_APPEND (member)
  |- !l1 l2. l1 LLESS_RIGHT l2 ==> (?l. l2 = APPEND l l1)
LLESS_RIGHT_LENGTH1_NULL (member)
  |- !l1 l2. l2 LLESS_RIGHT l1 /\ (LENGTH l1 = 1) ==> NULL l2
LLESS_RIGHT_NULL (member)
  |- !l1 l2. l1 LLESS_RIGHT l2 ==> ~NULL l2
LLESS_RIGHT_SINGLE_NULL (member)
  |- !l h. l LLESS_RIGHT [h] = NULL l
LLESS_RIGHT_SNOC (member)
  |- !l1 l2 h.
      (BUTLAST l1) LLESS_RIGHT l2 /\ (h = LAST l1) /\ ~NULL l1 ==>
      l1 LLESS_RIGHT (SNOC h l2)
LLESS_RIGHT_SNOC_BUTLAST_LLESS_RIGHT (member)
  |- !l h t.
      l LLESS_RIGHT (SNOC h t) /\ ~NULL l ==> (BUTLAST l) LLESS_RIGHT t
LLESS_RIGHT_SNOC_LAST (member)
  |- !l h t. l LLESS_RIGHT (SNOC h t) /\ ~NULL l ==> (h = LAST l)
MEMBER (member)
  |- (!x. MEMBER x[] = F) /\
     (!x h t. MEMBER x(CONS h t) = (h = x) \/ MEMBER x t)
MEMBER_SNOC (member)
  |- !t x h. MEMBER x(SNOC h t) = (h = x) \/ MEMBER x t
NIL_LLEQ_LEFT (member)
  |- !l. [] LLEQ_LEFT l
NIL_LLEQ_RIGHT (member)
  |- !l. [] LLEQ_RIGHT l
NOT_LLESS_LEFT_CONS_NOT_NULL (member)
  |- !l h t. ~l LLESS_LEFT (CONS h t) ==> ~NULL l

NOT_LLESS_LEFT_CONS_NOT_TL_LLESS_LEFT (member)
  |- !l h t.
      ~l LLESS_LEFT (CONS h t) /\ ~NULL l /\ (h = HD l) ==>
      ~(TL l) LLESS_LEFT t
NOT_LLESS_LEFT_NIL (member)
  |- !l. ~l LLESS_LEFT []
NOT_LLESS_LEFT_NOT_NULL (member)
  |- !l1 l2. ~l1 LLESS_LEFT l2 /\ ~NULL l2 ==> ~NULL l1
NOT_LLESS_LEFT_TL (member)
  |- !l1 l2 h.
      ~(CONS h l1) LLESS_LEFT l2 /\ (h = HD l2) /\ ~NULL l2 ==>
      ~l1 LLESS_LEFT (TL l2)
NOT_LLESS_RIGHT_BUTLAST (member)
  |- !l1 l2 h.
      ~(SNOC h l1) LLESS_RIGHT l2 /\ (h = LAST l2) /\ ~NULL l2 ==>
      ~l1 LLESS_RIGHT (BUTLAST l2)
NOT_LLESS_RIGHT_NIL (member)
  |- !l. ~l LLESS_RIGHT []
NOT_LLESS_RIGHT_NOT_NULL (member)
  |- !l1 l2. ~l1 LLESS_RIGHT l2 /\ ~NULL l2 ==> ~NULL l1
NOT_LLESS_RIGHT_SNOC_NOT_BUTLAST_LLESS_RIGHT (member)
  |- !l h t.
      ~l LLESS_RIGHT (SNOC h t) /\ ~NULL l /\ (h = LAST l) ==>
      ~(BUTLAST l) LLESS_RIGHT t
NOT_LLESS_RIGHT_SNOC_NOT_NULL (member)
  |- !l h t. ~l LLESS_RIGHT (SNOC h t) ==> ~NULL l
NOT_NIL_LLESS_LEFT (member)
  |- !l. ~[] LLESS_LEFT l ==> NULL l
NOT_NIL_LLESS_RIGHT (member)
  |- !l. ~[] LLESS_RIGHT l ==> NULL l
SNOC_LLEQ_RIGHT_BUTLAST (member)
  |- !l1 l2. (SNOC h l1) LLEQ_RIGHT l2 ==> l1 LLEQ_RIGHT (BUTLAST l2)
SNOC_LLESS_RIGHT_APPEND_LAST (member)
  |- !l l1 l2.
      ~NULL l2 /\ (SNOC h l) LLESS_RIGHT (APPEND l1 l2) ==> (h = LAST l2)

3.11. Theorems about UNAPPEND 57

SNOC_LLESS_RIGHT_BUTLAST (member)
  |- !l1 l2. (SNOC h l1) LLESS_RIGHT l2 ==> l1 LLESS_RIGHT (BUTLAST l2)
SNOC_LLESS_RIGHT_LAST (member)
  |- !h l1 l2. (SNOC h l1) LLESS_RIGHT l2 ==> (h = LAST l2)

3.11 Theorems about UNAPPEND

APPEND_UNAPPEND_LEFT_ID (unappend)
  |- !l. l = APPEND l(UNAPPEND_LEFT l l)
APPEND_UNAPPEND_RIGHT_ID (unappend)
  |- !l. l = APPEND l(UNAPPEND_RIGHT l l)
EXISTS_UNAPPEND_LEFT (unappend)
  |- ?f. !l1 l2. f l1(APPEND l1 l2) = l2
EXISTS_UNAPPEND_RIGHT (unappend)
  |- ?f. !l1 l2. f l2(APPEND l1 l2) = l1
LLEQ_LEFT_APPEND_UNAPPEND_LEFT (unappend)
  |- !l1 l2. l1 LLEQ_LEFT l2 ==> (l2 = APPEND l1(UNAPPEND_LEFT l1 l2))
LLEQ_LEFT_UNAPPEND_LEFT_CONS (unappend)
  |- !h l1 l2.
      l1 LLEQ_LEFT l2 ==>
      (UNAPPEND_LEFT(CONS h l1)(CONS h l2) = UNAPPEND_LEFT l1 l2)
LLEQ_RIGHT_APPEND_UNAPPEND_RIGHT (unappend)
  |- !l1 l2. l1 LLEQ_RIGHT l2 ==> (l2 = APPEND(UNAPPEND_RIGHT l1 l2)l1)
LLEQ_RIGHT_UNAPPEND_RIGHT_SNOC (unappend)
  |- !h l1 l2.
      l1 LLEQ_RIGHT l2 ==>
      (UNAPPEND_RIGHT(SNOC h l1)(SNOC h l2) = UNAPPEND_RIGHT l1 l2)
LLESS_LEFT_APPEND_UNAPPEND_LEFT (unappend)
  |- !l1 l2. l1 LLESS_LEFT l2 ==> (l2 = APPEND l1(UNAPPEND_LEFT l1 l2))
LLESS_LEFT_APPEND_UNAPPEND_LEFT_LLESS_LEFT (unappend)
  |- !l1 l2 l.
      ~l LLESS_LEFT l1 /\ l LLESS_LEFT (APPEND l1 l2) ==>
      (UNAPPEND_LEFT l1 l) LLESS_LEFT l2

LLESS_RIGHT_APPEND_UNAPPEND_RIGHT (unappend)
  |- !l1 l2. l1 LLESS_RIGHT l2 ==> (l2 = APPEND(UNAPPEND_RIGHT l1 l2)l1)
LLESS_RIGHT_APPEND_UNAPPEND_RIGHT_LLESS_RIGHT (unappend)
  |- !l1 l2 l.
      ~l LLESS_RIGHT l2 /\ l LLESS_RIGHT (APPEND l1 l2) ==>
      (UNAPPEND_RIGHT l2 l) LLESS_RIGHT l1
NULL_UNAPPEND_LEFT (unappend)
  |- !l. NULL(UNAPPEND_LEFT l l)
NULL_UNAPPEND_RIGHT (unappend)
  |- !l. NULL(UNAPPEND_RIGHT l l)
UNAPPEND_LEFT (unappend)
  |- !l1 l2. UNAPPEND_LEFT l1(APPEND l1 l2) = l2
UNAPPEND_LEFT_CONS (unappend)
  |- !h l1 l2.
      l1 LLESS_LEFT l2 ==>
      (UNAPPEND_LEFT(CONS h l1)(CONS h l2) = UNAPPEND_LEFT l1 l2)
UNAPPEND_LEFT_EQ_NIL (unappend)
  |- !l. UNAPPEND_LEFT l l = []
UNAPPEND_LEFT_NIL (unappend)
  |- !l. UNAPPEND_LEFT[]l = l
UNAPPEND_LEFT_UNAPPEND_RIGHT (unappend)
  |- !l1 l2.
      l2 LLESS_RIGHT l1 ==> (UNAPPEND_LEFT(UNAPPEND_RIGHT l2 l1)l1 = l2)
UNAPPEND_RIGHT (unappend)
  |- !l1 l2. UNAPPEND_RIGHT l2(APPEND l1 l2) = l1
UNAPPEND_RIGHT_EQ_NIL (unappend)
  |- !l. UNAPPEND_RIGHT l l = []
UNAPPEND_RIGHT_NIL (unappend)
  |- !l. UNAPPEND_RIGHT[]l = l
UNAPPEND_RIGHT_SNOC (unappend)
  |- !h l1 l2.
      l1 LLESS_RIGHT l2 ==>
      (UNAPPEND_RIGHT(SNOC h l1)(SNOC h l2) = UNAPPEND_RIGHT l1 l2)
UNAPPEND_RIGHT_UNAPPEND_LEFT (unappend)
  |- !l1 l2.
      l2 LLESS_LEFT l1 ==> (UNAPPEND_RIGHT(UNAPPEND_LEFT l2 l1)l1 = l2)

3.12. Theorems about Shifting and Rotating Lists 59

3.12 Theorems about Shifting and Rotating Lists

LENGTH_PAD_LEFT (shift)
  |- !l n x. LENGTH(PAD_LEFT x n l) = (LENGTH l) + n
LENGTH_PAD_RIGHT (shift)
  |- !l n x. LENGTH(PAD_RIGHT x n l) = (LENGTH l) + n
LENGTH_ROTATE1_LEFT (shift)
  |- !l. ~NULL l ==> (LENGTH(ROTATE1_LEFT l) = LENGTH l)
LENGTH_ROTATE1_RIGHT (shift)
  |- !l. ~NULL l ==> (LENGTH(ROTATE1_RIGHT l) = LENGTH l)
PAD_LEFT (shift)
  |- (!x l. PAD_LEFT x 0 l = l) /\
     (!x n l. PAD_LEFT x(SUC n)l = CONS x(PAD_LEFT x n l))
PAD_RIGHT (shift)
  |- (!x l. PAD_RIGHT x 0 l = l) /\
     (!x n l. PAD_RIGHT x(SUC n)l = SNOC x(PAD_RIGHT x n l))
ROTATE1_LEFT (shift)
  |- !l. ROTATE1_LEFT l = SNOC(HD l)(TL l)
ROTATE1_LEFT_CONS (shift)
  |- !x l. ROTATE1_LEFT(CONS x l) = SNOC x l
ROTATE1_LEFT_NIL (shift)
  |- !l. ~NULL l ==> ~NULL(ROTATE1_LEFT l)
ROTATE1_LEFT_ROTATE1_RIGHT (shift)
  |- !l. ~NULL l ==> (ROTATE1_LEFT(ROTATE1_RIGHT l) = l)
ROTATE1_RIGHT (shift)
  |- !l. ROTATE1_RIGHT l = CONS(LAST l)(BUTLAST l)
ROTATE1_RIGHT_NIL (shift)
  |- !l. ~NULL l ==> ~NULL(ROTATE1_RIGHT l)
ROTATE1_RIGHT_ROTATE1_LEFT (shift)
  |- !l. ~NULL l ==> (ROTATE1_RIGHT(ROTATE1_LEFT l) = l)
ROTATE1_RIGHT_SNOC (shift)
  |- !x l. ROTATE1_RIGHT(SNOC x l) = CONS x l

ROTATE_LEFT (shift)
  |- (!l. ROTATE_LEFT 0 l = l) /\
     (!n l. ROTATE_LEFT(SUC n)l = ROTATE1_LEFT(ROTATE_LEFT n l))
ROTATE_LEFT_EL (shift)
  |- !n x. ROTATE_LEFT n[x] = [x]
ROTATE_LEFT_ROTATE1_LEFT (shift)
  |- !l n.
      ~NULL l ==> (ROTATE_LEFT(SUC n)l = ROTATE_LEFT n(ROTATE1_LEFT l))
ROTATE_LEFT_ROTATE_RIGHT (shift)
  |- !n l. ~NULL l ==> (ROTATE_LEFT n(ROTATE_RIGHT n l) = l)
ROTATE_LEFT_SUC_CONS (shift)
  |- !l x n. ROTATE_LEFT(SUC n)(CONS x l) = ROTATE_LEFT n(SNOC x l)
ROTATE_RIGHT (shift)
  |- (!l. ROTATE_RIGHT 0 l = l) /\
     (!n l. ROTATE_RIGHT(SUC n)l = ROTATE1_RIGHT(ROTATE_RIGHT n l))
ROTATE_RIGHT_EL (shift)
  |- !n x. ROTATE_RIGHT n[x] = [x]
ROTATE_RIGHT_ROTATE1_RIGHT (shift)
  |- !l n.
      ~NULL l ==> (ROTATE_RIGHT(SUC n)l = ROTATE_RIGHT n(ROTATE1_RIGHT l))
ROTATE_RIGHT_ROTATE_LEFT (shift)
  |- !n l. ~NULL l ==> (ROTATE_RIGHT n(ROTATE_LEFT n l) = l)
ROTATE_RIGHT_SUC_SNOC (shift)
  |- !l x n. ROTATE_RIGHT(SUC n)(SNOC x l) = ROTATE_RIGHT n(CONS x l)

3.13 Theorems about Pairing Lists

FST_SND_UNZIP_ZIP (zip)
  |- !l1 l2.
      (LENGTH l1 = LENGTH l2) =
      (UNZIP_FST(ZIP l1 l2) = l1) /\ (UNZIP_SND(ZIP l1 l2) = l2)
UNZIP_FST (zip)
  |- (UNZIP_FST[] = []) /\
     (!h t. UNZIP_FST(CONS h t) = CONS(FST h)(UNZIP_FST t))

3.14. Theorems about num Lists 61

UNZIP_FST_ZIP (zip)
  |- !l1 l2. (LENGTH l1) <= (LENGTH l2) = (UNZIP_FST(ZIP l1 l2) = l1)
UNZIP_SND (zip)
  |- (UNZIP_SND[] = []) /\
     (!h t. UNZIP_SND(CONS h t) = CONS(SND h)(UNZIP_SND t))
UNZIP_SND_ZIP (zip)
  |- !l1 l2. (LENGTH l2) <= (LENGTH l1) = (UNZIP_SND(ZIP l1 l2) = l2)
ZIP (zip)
  |- (ZIP[][] = []) /\
     (!h1 t1. ZIP(CONS h1 t1)[] = []) /\
     (!h2 t2. ZIP[](CONS h2 t2) = []) /\
     (!h1 t1 h2 t2. ZIP(CONS h1 t1)(CONS h2 t2) = CONS(h1,h2)(ZIP t1 t2))
ZIP_CLAUSES (zip)
  |- (!l. ZIP[]l = []) /\
     (!l. ZIP l[] = []) /\
     (!h1 t1 h2 t2. ZIP(CONS h1 t1)(CONS h2 t2) = CONS(h1,h2)(ZIP t1 t2))
ZIP_DEF (zip)
  |- (!l. ZIP l[] = []) /\
     (!l h t. ZIP l(CONS h t) = (NULL l => [] | CONS(HD l,h)(ZIP(TL l)t)))
ZIP_UNZIP_FST_SND (zip)
  |- !l. ZIP(UNZIP_FST l)(UNZIP_SND l) = l

3.14 Theorems about num Lists

EL1_TL (num lists)
  |- !l. ~NULL l ==> (MAP(\n. EL1 n l)(2 UPTO (LENGTH l)) = TL l)
EL_FROM0 (num lists)
  |- !n m. m <= n ==> (EL m(FROM0 n) = m)
EL_MAP_FROM0 (num lists)
  |- !f m n. m <= n ==> (EL m(MAP f(FROM0 n)) = f(EL m(FROM0 n)))
EVERY_FROM0 (num lists)
  |- !n. EVERY(\m. m <= n)(FROM0 n)
EVERY_UPTO (num lists)
  |- !m n. EVERY(\p. m <= p /\ p <= n)(m UPTO n)

FROM0 (num lists)
  |- (FROM0 0 = [0]) /\ (!n. FROM0(SUC n) = CONS 0(MAP SUC(FROM0 n)))
FROM0_APPEND (num lists)
  |- !n. FROM0(SUC n) = APPEND(FROM0 n)[SUC n]
FROM0_PRE (num lists)
  |- !n. 0 < n ==> (FROM0 n = CONS 0(MAP SUC(FROM0(PRE n))))
FROM0_SUB (num lists)
  |- !m n. m < n ==> (FROM0(n - m) = CONS 0(MAP SUC(FROM0(n - (SUC m)))))
INTERVAL (num lists)
  |- (!m. m UPTO 0 = (m > 0 => [] | [0])) /\
     (!m n. m UPTO (SUC n) = (m > (SUC n) => [] | SNOC(SUC n)(m UPTO n)))
LENGTH_FROM0 (num lists)
  |- !n. LENGTH(FROM0 n) = SUC n
NOT_NULL_FROM0 (num lists)
  |- !n. ~NULL(FROM0 n)
RANGE (num lists)
  |- (!m. RANGE m 0 = []) /\
     (!m n. RANGE m(SUC n) = CONS m(RANGE(SUC m)n))
RANGE_SHIFT (num lists)
  |- !n m. RANGE(SUC m)n = MAP SUC(RANGE m n)
RANGE_TOP (num lists)
  |- !n m. RANGE m(SUC n) = APPEND(RANGE m n)[m + n]
SUC_UPTO_SUC (num lists)
  |- !m n. (SUC m) UPTO (SUC n) = MAP SUC(m UPTO n)
UPTO (num lists)
  |- !n1 n2. n1 UPTO n2 = MAP($+ n1)(n1 <= n2 => FROM0(n2 - n1) | [])
UPTO_EQ_CONS_SUC_UPTO (num lists)
  |- !m n. m <= n ==> (m UPTO n = CONS m((SUC m) UPTO n))
UPTO_SUC_EQ_APPEND_UPTO (num lists)
  |- !m n. m <= (SUC n) ==> (m UPTO (SUC n) = APPEND(m UPTO n)[SUC n])

Index

APPEND, 8

append, theory, 8

APPEND_11, 38
APPEND_BUTLAST_LAST, 38
APPEND_CLAUSES, 8, 38
APPEND_CONS, 38
APPEND_CONS_EQ_APPEND, 38
APPEND_CONS_EQ_APPEND_SNOC, 38
APPEND_EL_11, 39
APPEND_EL_REVERSE_CONS, 39
APPEND_FIRSTN_LASTN, 49
APPEND_FIRSTN_NTL, 46
APPEND_ID, 39
APPEND_ID_NULL, 39
APPEND_IS_NIL, 39
APPEND_IS_NULL, 8, 39
APPEND_JOIN, 39
APPEND_LASTN_LASTN, 49
APPEND_LENGTH_EQ, 39
APPEND_NBUTLAST_LASTN, 14, 49
APPEND_NBUTLAST_NTL, 49
APPEND_NIL, 39
APPEND_SUBSEQ, 46
APPEND_SUBSEQ2, 46
APPEND_UNAPPEND_LEFT_ID, 12, 57
APPEND_UNAPPEND_RIGHT_ID, 57
BUTLAST, 5, 6, 34
BUTLAST1, 39
BUTLAST_APPEND, 39
BUTLAST_CONS, 6, 34
BUTLAST_CONS_NOT_NULL, 35
BUTLAST_CONV, 21

                                       BUTLAST_DEF, 6, 35
                                       BUTLAST_EL, 35
                                       BUTLAST_NIL, 35
                                       BUTLAST_NULL, 35
                                       BUTLAST_REVERSE_EQ_-
                                             REVERSE_TL, 35
                                       BUTLAST_TL, 35
                                       BUTLAST_TO_NBUTLAST, 49

CON, 7, 37

                                       CONS, 4, 5
                                       CONS_APPEND_CONS, 8, 39
                                       CONS_LLEQ_LEFT_TL, 12, 53
                                       CONS_LLESS_LEFT_APPEND_HD, 53
                                       CONS_LLESS_LEFT_HD, 53
                                       CONS_LLESS_LEFT_TL, 12, 53
                                       CONS_MEMBER_LIST, 40
                                       CONS_MEMBER_LIST_NULL, 40
                                       CONS_ONE_ONE, 4, 33
                                       EL, 9

el, theory, 9 EL1, 9, 43

                                       EL1_HD, 9, 43
                                       EL1_SUC_CONS, 9, 43
                                       EL1_TL, 61
                                       EL_0_REVERSE, 43
                                       EL_APPEND_1, 9, 43
                                       EL_APPEND_2, 9, 43
                                       EL_APPEND_EL, 43
                                       EL_BUTLAST, 43
                                       EL_CONS, 43
                                       EL_CONS_SUB1, 44

\underline{64 Index}

EL_CONV, 22
EL_ELL, 10, 45
EL_FROM0, 61
EL_HD, 9, 44
EL_HD_NTAIL, 13, 46
EL_LENGTH_APPEND, 44
EL_MAP, 44
EL_MAP2, 44
EL_MAP_FROM0, 61
EL_NBUTLAST, 50
EL_NTAIL_1, 46
EL_REPLICATE, 44
EL_REVERSE, 44
EL_SNOC, 44

ELL, 9, 10, 45 ell, theory, 9

ELL_APPEND_1, 10, 45
ELL_APPEND_2, 45
ELL_CONS, 10, 45
ELL_CONV, 21
ELL_EL, 45
ELL_LAST, 10, 45
ELL_LASTN, 49
ELL_LENGTH_APPEND, 45
ELL_MAP, 45
ELL_MAP2, 45
ELL_NBUTLAST, 50
ELL_SNOC, 45
ELL_SNOC0, 45
ELL_SUC_SNOC, 45
EQ_LENGTH_INDUCT_TAC, 23
EQ_LENGTH_SNOC_INDUCT_TAC, 24
EVERY, 10
EVERY_APPEND, 42
EVERY_FROM0, 61
EVERY_LASTN, 50
EVERY_MAP, 10, 42
EVERY_SNOC, 42
EVERY_UPTO, 61
EXISTS_EL, 44

                                       EXISTS_UNAPPEND_LEFT, 57
                                       EXISTS_UNAPPEND_RIGHT, 57
                                       FIRSTN, 13, 46
                                       FIRSTN_APPEND1, 47
                                       FIRSTN_FIRSTN, 47
                                       FIRSTN_LENGTH_ID, 47
                                       FIRSTN_NIL, 47
                                       FIRSTN_NULL, 13, 47

FROM0, 17, 62

                                       FROM0_APPEND, 18, 62
                                       FROM0_PRE, 62
                                       FROM0_SUB, 62
                                       FST_SND_UNZIP_ZIP, 17, 60
                                       general_lists, theory, 4
                                       HD, 5
                                       HD_APPEND, 40
                                       HD_APPEND_NULL, 8, 40
                                       HD_BUTLAST, 35
                                       HD_ELL_LENGTH_CONS, 46
                                       HD_ELL_LENGTH_SNOC, 46
                                       HD_ELL_PRE_LENGTH, 46
                                       HD_MAP, 10, 42
                                       HD_SNOC, 5, 35
                                       HEAD_APPEND, 40
                                       HEAD_APPEND_NULL, 40
                                       IMP_APPEND_NOT_NIL, 40
                                       IMP_APPEND_NOT_NULL, 40
                                       INTERVAL, 18, 62
                                       ISO_REVERSE, 35
                                       ITERATED, 8, 40
                                       ITERATED_EMPTY, 8, 40
                                       ITLIST, 10, 42
                                       ITLIST_MAP, 10
                                       ITLIST_MAP_EQ, 42
                                       L_EQ_NIL, 34

LAST, 5, 6, 35

                                       LAST1, 40

\underline{Index 65}

LAST_APPEND, 40
LAST_BUTLAST_exist, 35
LAST_CONS, 6, 35
LAST_CONS_NOT_NULL, 35
LAST_CONV, 25
LAST_DEF, 6, 35
LAST_EL, 6, 35
LAST_EL_LENGTH, 44
LAST_LASTN, 51
LAST_NBUTLAST_EL, 51
LAST_NBUTLAST_ELL, 51
LAST_REVERSE_EQ_HD, 36
last_subseq, theory, 14
LAST_TL, 36
LAST_TO_LASTN, 51

LASTN, 14, 50

LASTN_APPEND, 50
LASTN_APPEND2, 50
LASTN_CONS, 50
LASTN_CONV, 24
LASTN_LASTN, 50
LASTN_LENGTH_APPEND, 50
LASTN_LENGTH_ID, 14, 50
LASTN_MAP, 50
LASTN_MAP2, 50
LASTN_NBUTLAST, 51
LASTN_NBUTLAST_APPEND, 51
LASTN_NBUTLAST_TL_SPLIT, 51
LASTN_NIL, 51
LASTN_NULL, 51
LASTN_NULLN, 14
LASTN_SUC_SNOC, 51
LENGTH, 4
LENGTH1_CONS_HD, 33
LENGTH_APPEND_EL, 40
LENGTH_BUTLAST, 36
LENGTH_CLAUSES, 41
LENGTH_EQ, 4, 33
LENGTH_EQ_SUC_IMP_NOT_-
      NIL, 33

                                       LENGTH_EQ_SUC_IMP_NOT_-
                                             NULL, 33
                                       LENGTH_FIRSTN, 47
                                       LENGTH_FROM0, 62
                                       LENGTH_GR_0_NOT_NIL, 33
                                       LENGTH_LASTN, 51
                                       LENGTH_LESS_EQ, 33
                                       LENGTH_LESS_EQ_EQ, 34
                                       LENGTH_LESS_IMP_NOT_-

EQ, 34

                                       LENGTH_LIST_INDUCT_TAC, 25
                                       LENGTH_NOT_NULL, 34
                                       LENGTH_NTAIL, 47
                                       LENGTH_NTAIL_LESS, 47
                                       LENGTH_NULL, 4, 34
                                       LENGTH_PAD_LEFT, 16, 59
                                       LENGTH_PAD_RIGHT, 16, 59
                                       LENGTH_REPLICATE, 8, 41
                                       LENGTH_REVERSE, 7
                                       LENGTH_ROTATE1_LEFT, 59
                                       LENGTH_ROTATE1_RIGHT, 59
                                       LENGTH_SNOC, 36
                                       LENGTH_TAIL, 7, 38
                                       LENGTH_TL, 36
                                       LENGTH_TL_SUB, 34
                                       list_APPEND_Axiom, 41
                                       list_APPEND_CASES, 41
                                       list_APPEND_INDUCT, 41
                                       LIST_APPEND_INDUCT_TAC, 8, 26
                                       list_APPEND_NULL_CASES, 41
                                       list_CASES2, 7, 38
                                       LIST_LENGTH_INDUCT_TAC, 4
                                       list_NULL_CASES, 34
                                       list_NULL_CASES2, 7, 38
                                       LLEQ_LEFT, 11, 53
                                       LLEQ_LEFT_APPEND_UNAPPEND_LEFT, 57
                                       LLEQ_LEFT_UNAPPEND_LEFT_-
                                             CONS, 57
                                       LLEQ_RIGHT, 11, 53
                                       LLEQ_RIGHT_APPEND_UNAPPEND_-

RIGHT, 12, 57

LLEQ_RIGHT_UNAPPEND_RIGHT_-
SNOC, 57
LLESS_LEFT, 11, 54
LLESS_LEFT_APPEND, 54
LLESS_LEFT_APPEND_LLEQ_-
LEFT, 54
LLESS_LEFT_APPEND_UNAPPEND_-

LEFT, 12, 57

LLESS_LEFT_APPEND_UNAPPEND_-
LEFT_LLESS_LEFT, 57
LLESS_LEFT_CONS, 54
LLESS_LEFT_CONS_HD, 54
LLESS_LEFT_CONS_TL_LLESS_-
LEFT, 54
LLESS_LEFT_EXISTS_APPEND, 54
LLESS_LEFT_LENGTH1_NULL, 54
LLESS_LEFT_NULL, 54
LLESS_LEFT_SINGLE_NULL, 54
LLESS_RIGHT, 11, 54
LLESS_RIGHT_APPEND, 54
LLESS_RIGHT_APPEND_LLEQ_-
RIGHT, 55
LLESS_RIGHT_APPEND_UNAPPEND_-
RIGHT, 58
LLESS_RIGHT_APPEND_UNAPPEND_-
RIGHT_LLESS_RIGHT, 58
LLESS_RIGHT_EXISTS_APPEND, 55
LLESS_RIGHT_LENGTH1_NULL, 55
LLESS_RIGHT_NULL, 55
LLESS_RIGHT_SINGLE_NULL, 55
LLESS_RIGHT_SNOC, 55
LLESS_RIGHT_SNOC_BUTLAST_-
LLESS_RIGHT, 55
LLESS_RIGHT_SNOC_LAST, 55
load_more_lists, 19–20
MAP, 10

map, theory, 10

MAP2_CONV, 27

MAP2_EL, 44
MAP2_ELL, 46
MAP2_SNOC, 42
MAP_EL, 44
MAP_EL1_SUC_CONS, 44
MAP_ELL, 46
MAP_MAP_o, 10, 43
MAP_SNOC, 43
MEMBER, 11, 55

member, theory, 11

MEMBER_SNOC, 12, 55
more_lists, theory, 4
NBUTLAST, 14, 52
NBUTLAST_APPEND, 52
NBUTLAST_APPEND1, 52
NBUTLAST_BUTLAST_SYM, 14, 52
NBUTLAST_CONS, 52
NBUTLAST_CONV, 28
NBUTLAST_LASTN, 52
NBUTLAST_LASTN_NIL, 52
NBUTLAST_LENGTH, 52
NBUTLAST_LENGTH_APPEND, 52
NBUTLAST_LENGTH_CONS, 52
NBUTLAST_LENGTH_NIL, 52
NBUTLAST_LENGTH_NULL, 14, 52
NBUTLAST_MAP, 52
NBUTLAST_MAP2, 53
NBUTLAST_NBUTLAST, 53
NBUTLAST_SIMP_REC, 53
NBUTLAST_SUC_SNOC, 53
NIL_EQ_L, 34
NIL_LLEQ_LEFT, 55
NIL_LLEQ_RIGHT, 12, 55
NIL_NOT_APPEND_CONS2, 41
NOT_LENGTH_EQ, 34
NOT_LLESS_LEFT_CONS_NOT_-
      NULL, 55
NOT_LLESS_LEFT_CONS_NOT_-
      TL_LLESS_LEFT, 56

NOT_LLESS_LEFT_NIL, 12, 56
NOT_LLESS_LEFT_NOT_NULL, 56
NOT_LLESS_LEFT_TL, 56
NOT_LLESS_RIGHT_BUTLAST, 56
NOT_LLESS_RIGHT_NIL, 56
NOT_LLESS_RIGHT_NOT_NULL, 56
NOT_LLESS_RIGHT_SNOC_NOT_-
      BUTLAST_LLESS_RIGHT, 56
NOT_LLESS_RIGHT_SNOC_NOT_-
      NULL, 56
NOT_NIL_APPEND_EL, 41
NOT_NIL_LLESS_LEFT, 56
NOT_NIL_LLESS_RIGHT, 56
NOT_NIL_SNOC, 36
NOT_NULL_FROM0, 62
NOT_NULL_NBUTLAST, 53
NOT_NULL_NTAIL, 47
NOT_NULL_NTAIL_TL, 47
NOT_NULL_TAIL, 7, 38
NOT_SNOC_NIL, 36

NTAIL, 13, 47

NTAIL_NIL, 47
NTAIL_NTAIL, 47
NTAIL_TAIL, 47

NTL, 13, 47

NTL_APPEND, 48
NTL_LENGTH, 48
NTL_LENGTH_APPEND, 48
NTL_LENGTH_NIL, 48
NTL_LENGTH_NULL, 48
NTL_NTL, 48
NTL_SIMP_REC, 48
NTL_TL_SYM, 13, 48
NULL, 4
NULL_EQ_EMPTY, 4, 34
NULL_ITERATED, 41
NULL_MAP, 43
NULL_NOT_APPEND_CONS, 41
NULL_NTAIL, 48
NULL_SUBSEQ, 48

                                       NULL_UNAPPEND_LEFT, 12, 58
                                       NULL_UNAPPEND_RIGHT, 58

num_lists, theory, 17

                                       ONE_MEMBER_LIST, 41
                                       ONE_MEMBER_LIST_NULL, 41
                                       PAD_LEFT, 15, 59
                                       PAD_RIGHT, 14, 15, 59

RANGE, 17, 62

                                       RANGE_SHIFT, 18, 62
                                       RANGE_TOP, 18, 62
                                       REPLICATE, 8, 41
                                       REVERSE, 5, 8, 41
                                       REVERSE_APPEND, 42
                                       REVERSE_APPEND_EL_CONS, 42
                                       REVERSE_CLAUSES, 7, 36
                                       REVERSE_DEF, 6, 36
                                       REVERSE_EQ_NIL, 36
                                       REVERSE_EXISTS, 36
                                       REVERSE_NULL, 7, 36
                                       REVERSE_REVERSE, 36
                                       REVERSE_SINGLE, 7, 36
                                       ROTATE1_LEFT, 15, 59
                                       ROTATE1_LEFT_CONS, 16, 59
                                       ROTATE1_LEFT_NIL, 59
                                       ROTATE1_LEFT_ROTATE1_RIGHT, 59
                                       ROTATE1_RIGHT, 15, 59
                                       ROTATE1_RIGHT_NIL, 16, 59
                                       ROTATE1_RIGHT_ROTATE1_LEFT, 59
                                       ROTATE1_RIGHT_SNOC, 59
                                       ROTATE_LEFT, 15, 60
                                       ROTATE_LEFT_EL, 16, 60
                                       ROTATE_LEFT_ROTATE1_LEFT, 60
                                       ROTATE_LEFT_ROTATE_RIGHT, 60
                                       ROTATE_LEFT_SUC_CONS, 60
                                       ROTATE_RIGHT, 15, 60
                                       ROTATE_RIGHT_EL, 60
                                       ROTATE_RIGHT_ROTATE1_RIGHT, 60
                                       ROTATE_RIGHT_ROTATE_LEFT, 16, 60

ROTATE_RIGHT_SUC_SNOC, 60
SAME_LENGTH_SNOC, 37

shift, theory, 14 SNOC, 5, 37 snoc, theory, 5

SNOC_11, 37
SNOC_APPEND_CONS, 8, 42
SNOC_Axiom, 5, 37
SNOC_CASES, 37
SNOC_CONV, 29
SNOC_DEF, 5, 37
SNOC_EQ_LENGTH_EQ, 37
SNOC_INDUCT, 5, 37
SNOC_INDUCT_TAC, 29
SNOC_INDUCT_TAC, 8
SNOC_LLEQ_RIGHT_BUTLAST, 56
SNOC_LLESS_RIGHT_APPEND_LAST, 56
SNOC_LLESS_RIGHT_BUTLAST, 12, 57
SNOC_LLESS_RIGHT_LAST, 57
SNOC_NOT_NULL, 5, 37
SNOC_NULL_CASES, 37
SNOC_ONE_ONE, 37
SNOC_REVERSE_CONS, 37
SNOC_INDUCT_TAC, 5
SPLIT_CONV, 30
SUBSEQ, 13, 48

subseq, theory, 13

SUBSEQ2, 48
SUBSEQ_APPEND, 48
SUBSEQ_APPEND2, 49
SUBSEQ_EMPTY_LIST, 49
SUBSEQ_EQ, 49
SUBSEQ_EXISTS, 49
SUBSEQ_MAP, 49
SUBSEQ_SUBSEQ, 13, 49
SUBSEQUENCE_EXISTS, 42
SUBSEQUENCES, 48
SUBST_REVERSE_CONV, 7, 30
SUC_UPTO_SUC, 62

TAIL, 7, 38 tail, theory, 7

                                       TAIL_APPEND, 7, 38
                                       TAIL_MAP, 43
                                       TAIL_NTAIL, 49

TL, 4, 5, 7

                                       TL_APPEND, 42
                                       TL_APPEND_NULL, 42
                                       TL_MAP, 10, 43
                                       TL_NIL, 34
                                       TL_NULL, 4, 34
                                       TL_SNOC, 5, 37
                                       TL_TAIL, 7, 38

unappend, theory, 12

                                       UNAPPEND_LEFT, 12, 58
                                       UNAPPEND_LEFT_CONS, 58
                                       UNAPPEND_LEFT_EQ_NIL, 58
                                       UNAPPEND_LEFT_NIL, 58
                                       UNAPPEND_LEFT_UNAPPEND_RIGHT, 58
                                       UNAPPEND_RIGHT, 12, 58
                                       UNAPPEND_RIGHT_EQ_NIL, 58
                                       UNAPPEND_RIGHT_NIL, 12, 58
                                       UNAPPEND_RIGHT_SNOC, 58
                                       UNAPPEND_RIGHT_UNAPPEND_-
                                             LEFT, 58
                                       UNZIP_FST, 16, 60
                                       UNZIP_FST_ZIP, 17, 61
                                       UNZIP_SND, 16, 61
                                       UNZIP_SND_ZIP, 17, 61

UPTO, 17, 62

                                       UPTO_EQ_CONS_SUC_UPTO, 18, 62
                                       UPTO_SUC_EQ_APPEND_UPTO, 62

ZIP, 16, 17, 61 zip, theory, 16

                                       ZIP_CLAUSES, 17, 61
                                       ZIP_DEF, 16, 61
                                       ZIP_UNZIP_FST_SND, 17, 61