The theory of functions in GST
Overview
This document introduces definitions and derives results relating to the representation of functions in galactic set theory.
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.
Introduction
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.
Motivation
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 Theory gst-fun
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"];

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

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
fttab∀s t u v:GS•
fttab(s ↦g t = u ↦g v
fttab⇔ s = u ∧ t = v)
fttab∧ Pairg 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"];

Projections
The following functions may be used for extracting the components of ordered pairs.
xl-holconst
fst snd : GS → GS
∀s t•
fttabfst(s ↦g t) = s
fttab∧ snd(s ↦g t) = t
Relations
A relation is defined as a set of ordered pairs. Cartesian product and relation space are defined.
Cartesian Product
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 ⇔
fttab∃l r•l ∈g s ∧ r ∈g t
fttab∧ e = l ↦g r
⌝);
a (∃_tac ⌜
λs t• ⋃g (
fttabImagep
fttab(λse• (Imagep (λte• se ↦g te) t))
fttabs)
⌝);

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 ⇔
fttab∃l r•l ∈g s ∧ r ∈g t
fttab∧ e = l ↦g r
Pair-Projection inverse theorem

xl-sml
set_goal ([],⌜∀s t p• p ∈g s ×g t
fttab⇒ fst(p) ↦g snd(p) = p⌝);
a (prove_tac[×g_spec]);
a (asm_rewrite_tac[]);
val f↦gs_thm = save_pop_thm "f↦gs_thm";

Var in Product theorem

xl-sml
set_goal([],⌜∀p s t•
fttabp ∈g (s ×g t)
fttab⇒ fst p ∈g s ∧ snd p ∈g t⌝);
a (prove_tac[get_spec⌜$×g⌝]
ftbr THEN_TRY asm_rewrite_tac[]);
val v∈g×g_thm =
fttabsave_pop_thm "v∈g×g_thm";
add_pc_thms "gst-fun" [v∈g×g_thm];
set_merge_pcs ["basic_hol", "gst-ax", "gst-fun"];

Pair in Product theorem

xl-sml
set_goal([],⌜∀l r s t•
fttab(l ↦g r) ∈g (s ×g t)
fttab⇔ l ∈g s ∧ r ∈g t⌝);
a (prove_tac[get_spec⌜$×g⌝]);
a (∃_tac ⌜l⌝
fttabTHEN ∃_tac ⌜r⌝
fttabTHEN asm_prove_tac[]);
val ↦gg×g_thm = save_pop_thm "↦gg×g_thm";
add_pc_thms "gst-fun" [↦gg×g_thm];
set_merge_pcs ["basic_hol", "gst-ax", "gst-fun"];

Relation Space
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)
Relation Subset Product Theorem
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⌝,
fttabgst_relext_clauses]);
val ↔gg×g_thm = save_pop_thm "↔gg×g_thm";

Relation Space Non-Empty
We prove here that the empty set is a member of every relation space.
xl-sml
set_goal ([], ⌜∀s t• ∅gg s ↔g t⌝);
a (prove_tac[get_spec⌜$↔g⌝,
fttabgst_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"];

Another Pair-Projection Inverse Theorem
Couched in terms of membership of relation spaces.
xl-sml
set_goal ([], ⌜∀p r s t•
fttabp ∈g r ∧
fttabr ∈g s ↔g t ⇒
fttabfst(p) ↦g snd(p) = p⌝);
a (prove_tac[
fttabget_spec ⌜$↔g⌝,
fttabg_thm]);
a (REPEAT
fttab(asm_fc_tac[f↦gs_thm]));
val f↦gs_thm1 =
fttabsave_pop_thm "f↦gs_thm1";

Member of Relation Theorem

xl-sml
set_goal ([],⌜∀p r s t•
fttabp ∈g r ∧
fttabr ∈g s ↔g t ⇒
fttabfst(p) ∈g s ∧
fttabsnd(p) ∈g t⌝);
a (prove_tac[
fttabget_spec ⌜$↔g⌝,
fttabg_thm]);
a (asm_fc_tac[]);
a (fc_tac[v∈g×g_thm]);
a (asm_fc_tac[]);
a (fc_tac[v∈g×g_thm]);
val ∈gg_thm =
fttabsave_pop_thm "∈gg_thm";

Relations

xl-holconst
rel : GS → BOOL
∀x• rel x ⇔
fttab∀y• y ∈g x ⇒ ∃s t• y = s ↦g t
Empty Set a Relation

xl-sml
val rel_∅g_thm = prove_thm (
fttab"rel_∅g_thm",
fttab⌜rel ∅g⌝,
fttabprove_tac[get_spec⌜rel⌝]);

Relational Composition

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


xl-holconst
$og : GS → GS → GS
∀f g• f og g =
fttabImagep
fttab(λp• (fst(fst p) ↦g snd(snd p)))
fttab(Sep (g ×g f) λp• ∃q r s• p = (q ↦g r) ↦g (r ↦g s))

xl-gft
og_thm =
ftbr ⊢ ∀f g x• x ∈g f og g ⇔
fttab∃q r s• q ↦g r ∈g g ∧ r ↦g s ∈g f
fttabfttab∧ x = q ↦g s
og_thm2 =
ftbr ⊢ ∀ f g x y• x ↦g y ∈g f og g
fttab⇔ (∃ z• x ↦g z ∈g g ∧ z ↦g y ∈g f)

og_associative_thm =
ftbr ⊢ ∀f g h• (f og g) og h = f og g og h

og_rel_thm =
ftbr ⊢ ∀ r s• rel r ∧ rel s ⇒ rel (r og s)

Domain, Range and Field
The domain, range and field of a relation are defined.
domain
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 =
fttab⊢ dom ∅g = ∅g
dom_thm =
fttab⊢ ∀ r y• y ∈g dom r ⇔ (∃ x• y ↦g x ∈g r)

range

xl-holconst
ran : GS → GS
∀x• ran x = Sep (Gx x) (λw• ∃v• v ↦g w ∈g x)

xl-gft
ran_∅g_thm
fttab⊢ ran ∅g = ∅g
ran_thm =
fttab⊢ ∀r y• y ∈g ran r ⇔ ∃ x• x ↦g y ∈g r

Relation Subset of Cartesian Product

xl-gft
rel_sub_cp_thm =
fttab⊢ ∀ x• rel x ⇔ (∃ s t• x ⊆g s ×g t)

field

xl-holconst
field : GS → GS
∀s e• e ∈g (field s)
⇔ e ∈g (dom s) ∨ e ∈g (ran s)
The field of the empty set

xl-gft
field_∅g_thm = ⊢ field ∅g = ∅g

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

xl-holconst
fun : GS → BOOL
∀x• fun x ⇔ rel x ∧
fttab∀s t u• s ↦g u ∈g x
fttabfttab∧ s ↦g t ∈g x
fttabfttab⇒ u = t
lemmas

xl-gft
fun_∅g_thm =
fttab⊢ fun ∅g
og_fun_thm =
fttab⊢ ∀ f g• fun f ∧ fun g ⇒ fun (f og g)
ran_og_thm =
fttab⊢ ∀ f g• ran (f og g) ⊆g ran f
dom_og_thm =
fttab⊢ ∀ f g• dom (f og g) ⊆g dom g
dom_og_thm2 =
fttab⊢ ∀ f g• ran g ⊆g dom f ⇒ dom (f og g) = dom g

Partial Function Space
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
Partial Function Space Non-Empty
First the theorem that the empty set is a partial function over any domain and codomain.
xl-sml
set_goal([],
fttab⌜∀s t• ∅gg s g t⌝);
a (prove_tac[
fttabget_spec ⌜$g⌝,
fttabfun_∅g_thm]);
val ∅ggg_thm =
fttabsave_pop_thm "∅ggg_thm";

And then that every partial function space is non-empty.
xl-sml
set_goal([],
fttab⌜∀s t• ∃ f• f ∈g s g t⌝);
a (REPEAT strip_tac
fttabTHEN ∃_tac ⌜∅g
fttabTHEN
fttabrewrite_tac [∅ggg_thm]);
val ∃g_thm =
fttabsave_pop_thm "∃g_thm";

Function Space
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)
fttabλr• dom r = s
Function Space Non-Empty
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• ∅gggg t⌝);
a (prove_tac[get_spec ⌜$→g⌝,
fttabfun_∅g_thm,
fttabggg_thm]);
val ∅gggg_thm =
fttabsave_pop_thm "∅gggg_thm";

Then that whenever the codomain is non-empty the function space is non-empty.
xl-gft
∃→g_thm =
ftbr ⊢ ∀ s t• (∃ x• x ∈g t) ⇒ (∃ f• f ∈g s →g t)

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

Because of the closeness to lambda abstraction "λg" is used as the name of a new binder for set theoretic functional abstraction. declare_binder "λg"; To define a functional set we need a HOL function over sets together with a set which is to be the domain of the function. Specification of the range is not needed. The binding therefore yields a function which maps sets to sets (maps the domain to the function).

The following definition is a placeholder, a more abstract definition might eventually be substituted. The function is defined as that subset of the cartesian product of the set s and its image under the function f which coincides with the graph of f over s.


xl-holconst
g: (GS → GS) →
fttabGS → GS
∀f s• $λg f s =
fttabSep (s ×g (Imagep f s))
fttab(λp• snd p = f (fst p))
Application and Extensionality
In this section we define function application and show that functions are extensional.
Application
Application by juxtaposition cannot be overloaded and is used for application of HOL functions. Application of functional sets is therefore defined as an infix operator whose name is the empty name subscripted by "g".
xl-sml
declare_infix (250,"g");

The particular form shown here is innovative in the value specified for applications of functions to values outside their domain. The merit of the particular value chosen is that it makes true an extensionality theorem which quantifies over all sets as arguments to the function, which might not otherwise be the case. Whether this form is useful I don't know. Generally a result with fewer conditionals is harder to prove but easier to use, but in this case I'm not so sure of the benefit.

It may be noted that it may also be used to apply a non-functional relation, if what you want it some arbitrary value (selected by the choice function) to which some object relates.
xl-holconst
$g : GS → GS → GS
∀f x• f g x =
fttabif ∃y• x ↦g y ∈g f
fttabthen εy• x ↦g y ∈g f
fttabelse f

xl-gft
app_thm1 =
fttab⊢ ∀f x• (∃1y• x ↦g y ∈g f)
fttab ⇒ x ↦g (f g x) ∈g f

app_thm2 =
fttab⊢ ∀f x y• fun f ∧ (x ↦g y ∈g f)
fttab ⇒ f g x = y

app_thm3 =
fttab⊢ ∀f x• fun f ∧ x ∈g dom f
fttab ⇒ x ↦g f g x ∈g f

og_g_thm =
fttab⊢ ∀f g x• fun f ∧ fun g ∧ x ∈g dom g ∧ ran g ⊆g dom f
fttab ⇒ (f og g) g x = f g g g x

The "Type" of an Application (1)
The following theorem states that the result of applying a partial function to a value in its domain is a value in its codomain.∧
xl-sml
set_goal([],
fttab⌜∀f s t u• f ∈g s g t ∧
fttabu ∈g dom f ⇒
fttabf g u ∈g t⌝);
a (prove_tac[
fttabget_spec ⌜$g⌝,
fttabget_spec ⌜dom⌝]);
a (all_fc_tac [app_thm2] THEN asm_rewrite_tac[]);
a (all_fc_tac [f↦gs_thm1]);
a (all_fc_tac [∈gg_thm]);
a (POP_ASM_T ante_tac THEN asm_rewrite_tac []);
val gg_thm = save_pop_thm "gg_thm";

The "Type" of an Application (2)
The following theorem states that the result of applying a total function to a value in its domain is a value in its codomain.
xl-sml
set_goal([],
fttab⌜∀f s t u• f ∈g s →g t ∧
fttabu ∈g s ⇒
fttabf g u ∈g t⌝);
a (prove_tac[
fttabget_spec ⌜$→g⌝]);
a (bc_thm_tac gg_thm);
a (∃_tac ⌜s⌝
fttabTHEN asm_rewrite_tac[]);
val gg_thm1 = save_pop_thm "gg_thm1";

Partial functions are total
Every partial function is total over its domain. (there is an ambiguity in the use of the term "domain" for a partial function. It might mean the left hand operand of some partial function space construction within which the partial function concerned may be found, or it might mean the set of values over which the function is defined. Here we are saying that if f is a partial function over A, then its domain is some subset of A and f is a total function over that subset of A.)
xl-sml
set_goal([],⌜∀f s t u• f ∈g s g t ⇒ f ∈g dom f →g t⌝);
a (rewrite_tac[
fttabget_spec ⌜$→g⌝,
fttabget_spec ⌜$↔g⌝,
fttabget_spec ⌜dom⌝,
fttabget_spec ⌜$g⌝]);
a (once_rewrite_tac[gst_relext_clauses]);
a (REPEAT strip_tac);
a (rewrite_tac[get_spec ⌜$×g⌝]);
a (asm_fc_tac[]);
a (all_fc_tac[
fttabf↦gs_thm,
fttabv∈g×g_thm]);
a (∃_tac ⌜fst e⌝
fttabTHEN ∃_tac ⌜snd e⌝
fttabTHEN asm_rewrite_tac[]
fttabTHEN strip_tac);
(* *** Goal "1" *** *)
a (LEMMA_T ⌜Pairg (fst e) (snd e) ∈g Gx (fst e ↦g snd e)⌝ ante_tac
fttabTHEN1 rewrite_tac [get_spec ⌜$↦g⌝]);
a (pure_rewrite_tac[asm_rule ⌜fst e ↦g snd e = e⌝]
fttabTHEN strip_tac);
a (LEMMA_T ⌜Gx e ⊆g Gx f⌝ ante_tac THEN1 fc_tac [Gx_mono_thm2]);
a (rewrite_tac [gst_relext_clauses] THEN strip_tac THEN asm_fc_tac[]);
a (LEMMA_T ⌜fst e ∈g Pairg (fst e) (snd e)⌝ asm_tac THEN1 rewrite_tac[]);
a (all_fc_tac [Gx_trans_thm3]);
(* *** Goal "2" *** *)
a (∃_tac ⌜snd e⌝fttabTHEN asm_rewrite_tac[]);
val ∈gg⇒∈gg_thm = save_pop_thm "∈gg⇒∈gg_thm";

The Identity Function
specification

xl-holconst
id : GS → GS
∀s• id s = Sep
fttab(s ×g s)
fttabλx• fst x = snd x
lemmas

xl-gft
id_thm1 =
fttab⊢ ∀s x• x ∈g id sfttab
fttab ⇔ ∃y• y ∈g s ∧ x = y ↦g y

id_ap_thm =
fttab⊢ ∀s x• x ∈g sfttab
fttab ⇒ (id s) g x = x

id∈gg_thm1 =
fttab⊢ ∀s t u• s ⊆g t ∩g u
fttab ⇒ id s ∈g t g u

id∈gg_thm2 =
fttab⊢ ∀s t u• s ⊆g t
fttab ⇒ id s ∈g t g t

id_clauses =
fttab⊢ ∀s• rel(id s) ∧ fun (id s)
fttab ∧ dom(id s) = s ∧ ran(id s) = s

Proof Contexts
Finalisation of a proof context.
Proof Context

xl-sml
add_pc_thms "gst-fun" ([
fttabfield_∅g_thm,
fttabfun_∅g_thm,
fttabggg_thm]);
set_merge_pcs ["basic_hol", "gst-ax", "gst-fun"];
commit_pc "gst-fun";


up quick index © RBJ

privacy policy

Created:

$Id: gst-functions.xml,v 1.3 2012/08/11 21:01:52 rbj Exp $

V