Definitions of Reflexive Structures.
Overview
 This document defines encodings of functions into well-founded sets.
 Introduction PolyMorphic Functions Polymorphic function are defined using ``patterns''.
Definable functions are are those definable in set theory from the ``PolyMorphic'' functions.
Introduction
Goals
 1. Goals
 3
The Theory refl-defs
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"];

PolyMorphic Functions
 Polymorphic function are defined using ``patterns''.
Instantiate
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-holconstinstantiate : (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.
Membership
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
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)
Definable Functions
 Definable functions are are those definable in set theory from the ``PolyMorphic'' functions.
Elaborate

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-holconstelaborate : (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 (Pairg (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.
Membership
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