ZFC in HOL - functions
Overview
This document proves some elementary consequences of the ZFC axioms in HOL, and then introduces further definitions relating to the representation of functions in set theory.
The principle of extensionality is more easily applied if it is expressed as an equation which can be used for rewriting.
In the introduction we do some preliminaries and introduce the new type of sets.
After proving a theorem about when (un-ordered) pairs are equal we introduce ordered pairs, which are required for representing functions as graphs.
A relation is a set of ordered pairs, a function is a many-one relation.
In this section we define function application and functional abstraction, and show that functions are extensional.
Extensionality
The principle of extensionality is more easily applied if it is expressed as an equation which can be used for rewriting.
Extensionality

The axiom of extensionality tells us that whenever two sets have all the same members then they are equal. The properties of equality tell us that the converse is also true. From these two we infer that a two sets are equal iff they have the same members, and this is a boolean equality which can conveniently be used as a rewriting rule.

The application of this rule will prove to be more delicate than that of extensionality in the typed set theory available in HOL (in effect as a congenial syntax for talking about properties). This is because in a typed set theory repeated application of the principle eventually translates all set equations into talk about elements, but in a pure untyped set theory, only sets exist and rewriting with the principle of extensionality may never terminate.


xl-sml
open_theory("zfc");
set_goal([],
s t:SETz s=t
(u:SETz u z s u z t));
a (
REPEAT _tac
THEN _tac
THEN_TRY asm_rewrite_tac[]);
a (fc_tac[ext_axiom]);
val set_ext_thm = save_pop_thm "set_ext_thm";

Union and Intersection
In the introduction we do some preliminaries and introduce the new type of sets.
Union
The union of a set of sets has already been introduced axiomatically. It is convenient also to have an infix binary union operator, which is defined below. First we chose an appropriate symbol and declare it as an infix operator.
xl-sml
declare_infix (240,"z");

Binary union is then defined as the union of a pair.
xl-holconst
$z : SETzSETzSETz
s t s z t = z (Pair s t)
Extensional Characterisation
The following theorem assists in reasoning about unions by permitting statements about members of unions to be eliminated in favour of statements about members of the operands of the union. (the union axiom is already in this form, we just want an analogous theorem for binary union)
xl-sml
set_goal([],
s t u:SETz u z (s z t)
(u z s u z t));
a (prove_tac
[get_spec $z,
z_axiom,
pair_axiom]);
val z_ext_thm =
save_pop_thm "z_ext_thm";

Intersection
The intersection of a set of sets is contained in each of the sets, and hence in their union. It can therefore be defined using separation as follows:
xl-holconst
$z : SETzSETz
s z s =
Sepz
(e t t z s e z t)
(z s)
Bearing in mind that the intersection is not defined for empty sets.
Extensional Characterisation
We now prove an extensional characterisation of intersection (which, however must be qualified).
xl-sml
prove_thm ("z_ext_thm2",
t (x x z t) s
(s z (z t)
u u z t s z u),
prove_tac[
get_spec $z,
separation_axiom,
z_axiom]);

Binary Intersection
Binary intersection could be defined using the previous definition, but because the definition behaves awkardly in relation to the empty set of sets it is easier to define binary intersection independently.
xl-sml
declare_infix (240,"z");


xl-holconst
$z : SETzSETzSETz
s t s z t = Sepz
(e e z t)
s
The proof of the extensional characterisation is then
Extensional Characterisation

xl-sml
set_goal([],
s t u u z (s z t)
u z s u z t);
a (rewrite_tac[
get_spec$z,
separation_axiom]);
val z_ext_thm =
save_pop_thm "z_ext_thm";

Pairs
After proving a theorem about when (un-ordered) pairs are equal we introduce ordered pairs, which are required for representing functions as graphs.
Equality of Pairs
The following theorem permits the elimination of statements about equality of pairs in favour of statements about the equality of the elements in the pairs.
xl-sml
set_goal ([],s t u v
Pair s t = Pair u v
(s = u t = v s = v t = u));
a (prove_tac[
_elim Pair s t set_ext_thm,
pair_axiom]);
(* *** Goal "1" *** *)
a (spec_nth_asm_tac 2 u
THEN_TRY all_var_elim_asm_tac
THEN_TRY asm_rewrite_tac[]);
(* *** Goal "2" *** *)
a (spec_nth_asm_tac 2 v
THEN_TRY all_var_elim_asm_tac
THEN_TRY asm_rewrite_tac[]);
val pair_eq_thm = save_pop_thm "pair_eq_thm";

Ordered Pairs

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


xl-holconst
$z : SETzSETzSETz

s t s z t = Pair (Pair s t) (Pair s s)

xl-sml
declare_infix (240,"z");
val z_spec = get_spec $z;

set_goal ([],s t u v
s z t = u z v
s = u t = v);
a (prove_tac[z_spec, pair_eq_thm]);
val z_eq_thm = save_pop_thm "z_eq_thm";

Relations and Functions
A relation is a set of ordered pairs, a function is a many-one relation.
Relations

xl-holconst
relz : SETzBOOL
x
relz x
y y z x
s t y = s z t
Empty Set a Relation

xl-sml
val relz_z_thm =
prove_thm ("relz_z_thm",
relz z,
prove_tac[
get_specrelz,
z_thm]);

Functions

xl-holconst
funz : SETzBOOL

x funz x relz x
s t u s z u z x
t z u z x
s = t
Empty Set a Function

xl-sml
val funz_z_thm =
prove_thm ("funz_z_thm",
funz z,
prove_tac[
get_specfunz,
z_thm,
relz_z_thm]);

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
domz : SETzSETz
x domz x = Sepz
(y z y z z z x)
(z (z x))
The domain of the empty set

xl-sml
set_goal([],domz z = z);
a (prove_tac[
get_specdomz,
z_thm,
separation_axiom,
set_ext_thm]);
val domz_z_thm = save_pop_thm "domz_z_thm";

range

xl-holconst
ranz : SETzSETz
x ranz x = Sepz
(z y y z z z x)
(z (z x))
The range of the empty set

xl-sml
set_goal([],ranz z = z);
a (prove_tac[
get_specranz,
z_thm,
separation_axiom,
set_ext_thm]);
val ranz_z_thm = save_pop_thm "ranz_z_thm";

field

xl-holconst
fieldz : SETzSETz
x fieldz x = (domz x) z (ranz x)
The field of the empty set

xl-sml
set_goal([],fieldz z = z);
a (prove_tac[
get_specfieldz,
domz_z_thm,
ranz_z_thm,
z_ext_thm,
set_ext_thm]);
val fieldz_z_thm = save_pop_thm "fieldz_z_thm";

Functional Abstraction, Abstraction and Extensionality
In this section we define function application and functional abstraction, and show that functions are extensional.
Application

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


xl-holconst
$z : SETzSETzSETz
f x f z x =
if y x z y z f
then y x z y z f
else f

xl-sml
(*
set_goal([],
f x (1y x z y z f)
x z (f z x) z f
);
a step_strip_tac;
a (asm_fc_tac [all__rule(_elim y x z y z f _axiom)]);
val app_thm = save_top_thm "app_thm";
*)


up quick index © RBJ

$Id: holzfc2.xml,v 1.1.1.1 2000/12/04 17:24:43 rbjones Exp $