listLib.list_thm

The conversion LIST_CONV uses a database of theorems relating to system list constants. These theorems fall into two categories: definitions of list operators in terms of FOLDR and FOLDL; and auxiliary theorems about the base element and step functions in those definitions. list_thm_database provides a means of inspecting the database.

A call to list_thm_database() returns a pair of lists. The first element of the pair contains the known fold definitions. The second contains the known auxiliary theorems.

The following is an example of a fold definition in the database:

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

Here $+ is the step function and 0 is the base element of the definition. Definitions are initially held for the following system operators: APPEND, FLAT, LENGTH, NULL, REVERSE, MAP, FILTER, ALL_EL, SUM, SOME_EL, IS_EL, AND_EL, OR_EL, PREFIX, SUFFIX, SNOC and FLAT combined with REVERSE.

The following is an example of an auxiliary theorem:

   |- MONOID $+ 0

Auxiliary theorems stored include monoid, commutativity, associativity, binary function commutativity, left identity and right identity theorems.