Lists in Isabelle [isa-0021]

The Isabelle/HOL theory of Lists defines lists as follows:

datatype 'a list = Nil | Cons "'a" "'a list"

This is an example of a polymorphic data type, where the type variable 'a stands for a type. For example, the type nat list is the type of lists of nat, and oot list is the type of a list of oots.

The notation x#xs is syntax sugar for Cons x xs and [] is syntax sugar for Nil. Lists can also be written in square brackets, so:

[1,2,3]

is equivalent to:

1 # 2 # 3 # []

which is equivalent to:

Cons 1 (Cons 2 (Cons 3 Nil))

Some provided functions are useful, including replicate :: nat ⇒ 'a ⇒ 'a list, which produces a list of n copies of the given value, and append :: 'a list ⇒ 'a list ⇒ 'a list which joins two lists together into one. The append function also has special notation, so a @ b is equivalent to append a b