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.
|
|
|
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"];
|
|
|
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• 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-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
xl-sml
commit_pc "gst-lists";
|
|
|