A new "gst-fun" theory is created as a child of "gst-ax". The theory will contain the definitions of ordered pairs, relations and functions and related material for general use.

We now introduce ordered pairs, which are required for representing functions as graphs.

A relation is defined as a set of ordered pairs. Cartesian product and relation space are defined.

The domain, range and field of a relation are defined.

Definition of partial and total functions and the corresponding function spaces.

Functional abstraction is defined as a new variable binding construct yeilding a functional set.

In this section we define function application and show that functions are extensional.

Finalisation of a proof context.

Most of the specification work which I am likely to do with galactic set theory will make use of functions. My first application of the functions will be in the theory of pure functors, which is frivolous and unlikely to be widely applied, and so I am creating this theory first so that more generally applicable results which are required for the theory of pure functors will be available separately. I have no clear idea of what this theory will contain, it will initially contain basic materials about functions, but will be augmented by anything else that turns out to be necessary elsewhere and which can appropriately be placed here.

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-ax"; force_new_theory "gst-fun"; force_new_pc "gst-fun"; merge_pcs ["xl_cs__conv"] "gst-fun"; set_merge_pcs ["basic_hol", "gst-ax", "gst-fun"];

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

This is more abstract than the usual definition since it conceals the way in which ordered pairs are encoded. We can't hide everything about the representation, because we will need to know at least that galaxies are closed under formation of ordered pairs, usually a much tighter constraint is known but I will say nothing stronger until I know why it is needed. Behind the scenes the usual definition is used to prove that this looser definition is a conservative extension.

xl-holconst $g : GS GS GS

s t u v:GS (s g t = u g v s = u t = v) Pair s t g Gx (s g t)

xl-sml add_pc_thms "gst-fun" [get_spec $g]; set_merge_pcs ["basic_hol", "gst-ax", "gst-fun"];

The following functions may be used for extracting the components of ordered pairs.

xl-holconst fst snd : GS GS

s t fst(s g t) = s snd(s g t) = t

The following theorem is required to introduce the conservative specification of cartesian product. The witness for the proof is shown, involving a double application of replacement. This is necessary because the loose specification of ordered pair does not provide sufficient information for a more conventional definition using separation.

xl-sml declare_infix(240,"g"); set_goal([], $g s t e e g s g t l rl g s r g t e = l g r ); a (_tac s t g ( Imagep (se (Imagep (te se g te) t)) s) );

After completing this proof cartesian product can be specified by conservative extension as follows:

xl-holconst $g : GS GS GS

s t e e g s g t l rl g s r g t e = l g r

xl-sml set_goal ([],s t p p g s g t fst(p) g snd(p) = p); a (prove_tac[g_spec]); a (asm_rewrite_tac[]); val fgs_thm = save_pop_thm "fgs_thm";

xl-sml set_goal([],p s t p g (s g t) fst p g s snd p g t); a (prove_tac[get_spec$g] THEN_TRY asm_rewrite_tac[]); val vgg_thm = save_pop_thm "vgg_thm"; add_pc_thms "gst-fun" [vgg_thm]; set_merge_pcs ["basic_hol", "gst-ax", "gst-fun"];

xl-sml set_goal([],l r s t (l g r) g (s g t) l g s r g t); a (prove_tac[get_spec$g]); a (_tac l THEN _tac r THEN asm_prove_tac[]); val ggg_thm = save_pop_thm "ggg_thm"; add_pc_thms "gst-fun" [ggg_thm]; set_merge_pcs ["basic_hol", "gst-ax", "gst-fun"];

This is the set of all relations over some domain and codomain, i.e. the power set of the cartesian product.

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

xl-holconst $g : GS GS GS

s t s g t = g(s g t)

We prove here that relations are subsets of cartesian products.

xl-sml set_goal ([], s t r r g s g t r g (s g t)); a (prove_tac[get_spec$g, gst_relext_clauses]); val ggg_thm = save_pop_thm "ggg_thm";

We prove here that the empty set is a member of every relation space.

xl-sml set_goal ([], s t g g s g t); a (prove_tac[get_spec$g, gst_relext_clauses]); val ggg_thm = save_pop_thm "ggg_thm"; add_pc_thms "gst-fun" [ggg_thm]; set_merge_pcs ["basic_hol", "gst-ax", "gst-fun"];

Couched in terms of membership of relation spaces.

xl-sml set_goal ([], p r s t p g r r g s g t fst(p) g snd(p) = p); a (prove_tac[ get_spec $g, g_thm]); a (REPEAT (asm_fc_tac[fgs_thm])); val fgs_thm1 = save_pop_thm "fgs_thm1";

xl-sml set_goal ([],p r s t p g r r g s g t fst(p) g s snd(p) g t); a (prove_tac[ get_spec $g, g_thm]); a (asm_fc_tac[]); a (fc_tac[vgg_thm]); a (asm_fc_tac[]); a (fc_tac[vgg_thm]); val gg_thm = save_pop_thm "gg_thm";

xl-holconst rel : GS BOOL

x rel x y y g x s t y = s g t

xl-sml val rel_g_thm = prove_thm ( "rel_g_thm", rel g, prove_tac[get_specrel]);

xl-sml declare_infix (250,"og");

xl-holconst $og : GS GS GS

f g f og g = Imagep (p (fst(fst p) g snd(snd p))) (Sep (g g f) p q r s p = (q g r) g (r g s))

xl-gft og_thm = f g x x g f og g q r s q g r g g r g s g f x = q g s og_thm2 = f g x y x g y g f og g ( z x g z g g z g y g f) og_associative_thm = f g h (f og g) og h = f og g og h og_rel_thm = r s rel r rel s rel (r og s)

The domain is the set of elements which are related to something under the relationship.

xl-holconst dom : GS GS

x dom x = Sep (Gx x) (w v w g v g x)

xl-gft dom_g_thm = dom g = g dom_thm = r y y g dom r ( x y g x g r)

xl-holconst ran : GS GS

x ran x = Sep (Gx x) (w v v g w g x)

xl-gft ran_g_thm ran g = g ran_thm = r y y g ran r x x g y g r

xl-gft rel_sub_cp_thm = x rel x ( s t x g s g t)

xl-holconst field : GS GS

s e e g (field s) e g (dom s) e g (ran s)

xl-gft field_g_thm = field g = g

xl-holconst fun : GS BOOL

x fun x rel x s t u s g u g x s g t g x u = t

xl-gft fun_g_thm = fun g og_fun_thm = f g fun f fun g fun (f og g) ran_og_thm = f g ran (f og g) g ran f dom_og_thm = f g dom (f og g) g dom g dom_og_thm2 = f g ran g g dom f dom (f og g) = dom g

This is the set of all partial functions (i.e. many one mapings) over some domain and codomain.

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

xl-holconst $g : GS GS GS

s t s g t = Sep (s g t) fun

First the theorem that the empty set is a partial function over any domain and codomain.

xl-sml set_goal([], s t g g s g t); a (prove_tac[ get_spec $g, fun_g_thm]); val ggg_thm = save_pop_thm "ggg_thm";

And then that every partial function space is non-empty.

xl-sml set_goal([], s t f f g s g t); a (REPEAT strip_tac THEN _tac g THEN rewrite_tac [ggg_thm]); val g_thm = save_pop_thm "g_thm";

This is the set of all total functions over some domain and codomain.

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

xl-holconst $g : GS GS GS

s t s g t = Sep (s g t) r dom r = s

First, for the special case of function spaces with empty domain we prove the theorem that the empty set is a member:

xl-sml set_goal([],s t g g g g t); a (prove_tac[get_spec $g, fun_g_thm, ggg_thm]); val gggg_thm = save_pop_thm "gggg_thm";

Then that whenever the codomain is non-empty the function space is non-empty.

xl-gft g_thm = s t ( x x g t) ( f f g s g t)