The theory of lists in GST
Overview
This document introduces definitions and derives results relating to the theory of lists in galactic set theory.
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.
Though we could do n-ary tuples for n>2, lists are better.
In this section I will create a decent proof context for lists, maybe.
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-holconst
nil : GS
nil = ∅g

xl-holconst
cons : GS → GS → GS
∀h t• cons h t = h ↦g 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 : GS LIST → GS
∀h t•
fttablist [] = nil
fttab∧ 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-holconst
head tail: GS → GS
head = fst
∧ tail = snd
To which we add a numeric selector.
xl-holconst
nth : ℕ → GS → 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";


up quick index © RBJ

privacy policy

Created:

$Id: gst-thlists.xml,v 1.1 2002/12/24 16:02:49 rbj Exp $

V