Polymorphic function are defined using ``patterns''.

First we introduce for these definitions the new theory "refl-defs", a child of gst.

xl-sml open_theory "gst"; force_new_theory "refl-defs"; force_new_pc "refl-defs"; set_merge_pcs ["gst","refl-defs"];

The following defines how a pattern is instantiated. A pattern is instantiated using a function which assigns a value to all possible ``wildcards''. A wildcard is any set which more or less than one member.

xl-holconst instantiate : (GS GS) GS GS

f s instantiate f (Unit s) = Imagep (instantiate f) s ((t s = Unit t) instantiate f s = f s)

A unit set is a set of patterns, each of which is to be instantiated. Any other set is a wildcard which must be replaced by the value assigned to it.

Using pattern instantiation we define a new membership relation, _gp, which may be thought of as ``polymorphic'' membership.

xl-sml declare_infix (230,"gp");

xl-holconst $gp : GS GS BOOL

s t s gp t f s = instantiate f t

Function application is by juxtaposition (i.e. nothing), which however we have to subscript. So its an infix subscript p.

xl-sml declare_infix (240,"p");

xl-holconst $p : GS GS GS

f x f p x = y (x g y gp f)

This is the analogue for definable functions of the function ``instantiate''. The idea is to encode as sets the definable functions roughly as described in Chapter V of Kunen's Set Theory, except that you get to use any set as a starting point (so instead of a countable number of functions you get a collection the same size as WF).

To understand ``elaborate'' you must think of a set as an encoding of a formula in a set theory with a very large term language (every set in GS is a term). The formula has free variables, and elaborate, given an assignment of values to free variables will give a truth value for the encoded formula.

xl-holconst elaborate : (GS GS) GS BOOL

f s t v elaborate f (g g (s g t)) instantiate f s = instantiate f t elaborate f ((Unit g) g (s g t)) instantiate f s g instantiate f t elaborate f (Pair (Unit g) g g (v g (s g t))) x let f' y = if y = v then x else f y in (elaborate f' s elaborate f' t)

The first two clauses in the above definition concern atomic formulae (membership and equality), the terms of which are evaluated using "instantiate". The final clause addresses non-atomic formulae via a generalised scheffer stroke.

Using elaborate we define another new membership relation, _gp, which may be thought of as ``polymorphic'' membership.

xl-sml declare_infix (230,"gd");

xl-holconst $gd : GS GS BOOL

s t s gd t elaborate (v s) t