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.
 Extensionality The principle of extensionality is more easily applied if it is expressed as an equation which can be used for rewriting. Union and Intersection In the introduction we do some preliminaries and introduce the new type of sets. Pairs After proving a theorem about when (un-ordered) pairs are equal we introduce ordered pairs, which are required for representing functions as graphs.
 Relations and Functions A relation is a set of ordered pairs, a function is a many-one relation. Domain Range and Field Empty Set Theorems Functional Abstraction, Abstraction and Extensionality 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"; *)