The theory of lists in GST
Overview
 This document introduces definitions and derives results relating to the theory of lists in galactic set theory.
 Introduction A new "gst-lists" theory is created as a child of "gst-fun". Probably This is really a placeholder, it is probably that lists will end up a special case of a more general theory of inductively defined types. Lists Though we could do n-ary tuples for n>2, lists are better.
 Proof Context In this section I will create a decent proof context for lists, maybe. Listing of Theory gst-lists
Introduction
 A new "gst-lists" theory is created as a child of "gst-fun". Probably This is really a placeholder, it is probably that lists will end up a special case of a more general theory of inductively defined types.
 Motivation Can't remember why I started this, but its hard to imagine getting far without it.
The Theory gst-lists
The new theory is first created, together with a proof context which we will build up as we develop the theory.
 xl-sml open_theory "gst-fun"; force_new_theory "gst-lists"; force_new_pc "gst-lists"; merge_pcs ["xl_cs__conv"] "gst-lists"; set_merge_pcs ["basic_hol", "gst-ax", "gst-fun", "gst-lists"];

Lists
 Though we could do n-ary tuples for n>2, lists are better.
Introduction
Working in an untyped set theory in higher order logic, some of the things already available as typed constructions have to be reworked in this untyped universe of sets. In higher order logic arbitrary tuples are available as typed constructions by iterating the typed ordered pair constructor, and lists are separately available. Both are desirable because the tuples are of fixed length determined by their type, but can have components of distinct types, while lists are of arbitrary length but must be of uniform type. In the set theory things work our differently. Lists are themselves more easily constructed (and this can be done using the ordered pair constructor) and are not restrained by a type system (within the set theory). Ordered tuples are less useful in this context and are probably superfluous if lists are available.
Cons and nil
We can use the ordered pair constructor and the empty set for the list constructor and the empty list, but, just in case we want to differentiate between pairs and lists in the proof automation I will give them new names.
 xl-holconstnil : 'a GS nil =

 xl-holconst cons : 'a GS 'a GS 'a GS h t cons h t = h t
The List Constructor
We can borrow a bit of the special syntax for lists in HOL by providing a list (set) constructor which takes a HOL list (of sets) as its argument.
 xl-holconst list : 'a GS LIST 'a GS h t list [] = nil list (Cons h t) = cons h (list t)
Destructors
Having adopted new names for existing constructors we now do the same for the destructors.
 xl-holconsthead tail: 'a GS 'a GS head = fst tail = snd
To which we add a numeric selector.
 xl-holconst nth : 'a GS 'a GS n l nth 0 l = head l nth (n+1) l = nth n (tail l)
Proof Context
 In this section I will create a decent proof context for lists, maybe.
Proof Context

 xl-sml commit_pc "gst-lists";