The theory of ordinals in GST
Overview
This document introduces definitions and derives results relating to ordinal numbers in galactic set theory.
A new "ord" theory is created as a child of "gst-ax". The theory will contain the definitions of ordinals and related material for general use, roughly following "Set Theory" by Frank Drake, chapter 2 section 2. The subsections in this document correspondend to the subsections in the book.
An ordinal is defined as a transitive and connected set. The usual ordering over the ordinals is defined and also the successor function.
We prove that the empty set is an ordinal, and that the members of an ordinal and the successor of an ordinal are ordinals.
We prove that the ordinals are linearly ordered by $<o.
Successor and limit ordinals are defined. Natural numbers are defined.
Induction theorems over ordinals and natural numbers.
The set of natural numbers.
We define the rank of a set.
In this section we define a proof context for ordinals.
Introduction
A new "ord" theory is created as a child of "gst-ax". The theory will contain the definitions of ordinals and related material for general use, roughly following "Set Theory" by Frank Drake, chapter 2 section 2. The subsections in this document correspondend to the subsections in the book.
Motivation
This is really motivated purely by interest and self-education. Since its so fundamental I think it likely to turn out handy. Some of the material required is not specific to set theory and is quite widely applicable (in which case I actually develop it elsewhere and then just use it here. Well-foundedness and induction over well-founded relations is the obvious case relevant to this part of Drake. The recursion theorem is the important more general result which appears in the next section in Drake. "more general" means "can be developed as a polymorphic theory in HOL and applied outside the context of set theory". In fact these things have to be developed in the more general context to be used in the ways they are required in the development of set theory, since, for example, one wants to do definitions by recursion over the set membership relation where neither the function defined nor the relevant well-founded relation are actually sets.
Divergence

I have not followed Drake slavishly. More or less, I follow him where it works out OK and looks reasonable and doesn't trigger any of my prejudices.

Sometimes the context in which I am doing the work makes some divergence desirable or necessary. For example, I am doing the work in the context of a slightly eccentric set theory ("Galactic Set Theory") which mainly makes no difference, but has a non-standard formulation of the axiom of foundation. Mainly this is covered by deriving the standard formulation and its consequences and using them where this is used by Drake (in proving the trichotomy theorem). However, the machinery for dealing with well-foundedness makes a difference to how induction principles are best formulated and derived.

Sometimes I look at what he has done and I think, "no way am I going to do that". Not necessarily big things, for example, I couldn't use his definition of successor ordinal which he pretty much admits himself is what we nerds call a kludge.

The Theory ord
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 "ord";
new_parent "wf_recp";
force_new_pc "ord";
merge_pcs ["xl_cs_∃_conv"] "ord";
set_merge_pcs ["basic_hol", "gst-ax", "ord"];

Definitions 2.1 and 2.3
An ordinal is defined as a transitive and connected set. The usual ordering over the ordinals is defined and also the successor function.
The Definition
The concept of transitive set has already been defined in theory gst-ax. The concepts connected and ordinal are now defined.
xl-holconst
connected : GS → BOOL
∀s :GS• connected s ⇔
fttab∀t u :GS• t ∈g s ∧ u ∈g s ⇒ t ∈g u ∨ t = u ∨ u ∈g t

xl-holconst
ordinal : GS → BOOL
∀s :GS• ordinal s ⇔ transitive s ∧ connected s
We now introduce infix ordering relations over ordinals.
xl-sml
declare_infix(240,"<o");
declare_infix(240,"≤o");


xl-holconst
$<o : GS → GS → BOOL
∀x y:GS• x <o y ⇔ ordinal x ∧ ordinal y ∧ x ∈g y

xl-holconst
$≤o : GS → GS → BOOL
∀x y:GS• x ≤o y ⇔ ordinal x ∧ ordinal y ∧ x ∈g y ∨ x = y
The following definition gives the successor function over the ordinals (this appears later in Drake).
xl-holconst
suco : GS → GS
∀x:GS• suco x = x ∪g (Unit x)
Theorem 2.2
We prove that the empty set is an ordinal, and that the members of an ordinal and the successor of an ordinal are ordinals.
The Empty Set is an Ordinal
First we prove that the empty set is an ordinal, which requires only rewriting with the relevant definitions.
xl-sml
set_goal([],⌜fttabordinal ∅gfttab⌝);
a (rewrite_tac[get_spec ⌜ordinal⌝, get_spec ⌜transitive⌝, get_spec ⌜connected⌝]);
val ordinal_∅g = save_pop_thm "ordinal_∅g";

The Successor of an Ordinal is an Ordinal
Next we prove that the successor of an ordinal is an ordinal. This is done in two parts, transitivity and connectedness.
xl-sml
set_goal([], ⌜fttab∀ x:GS• transitive x ⇒ transitive (suco x)fttab⌝);

(proof omitted)
xl-sml
set_goal([],⌜∀ x:GS•
fttabconnected x ⇒ connected (suco x)
⌝);

(proof omitted)
These together enable us to prove:
xl-sml
set_goal([],⌜fttab∀ x:GS• ordinal x ⇒ ordinal (suco x)fttab⌝);

The proof expands using the definition of ordinal, strips the goal and reasons forward from the resulting assumptions using the two lemmas proved above.
xl-sml
a (rewrite_tac[get_spec ⌜ordinal⌝]
fttabTHEN REPEAT strip_tac
fttabTHEN fc_tac [trans_suc_trans, conn_suc_conn]);
val ord_suc_ord_thm = save_pop_thm "ord_suc_ord_thm";

The members of an Ordinal are Ordinals
We now aim to prove that the members of an ordinal are ordinals. We do this by proving first that they are connected and then that they are transitive. First however, we show that any subset of a connected set is connected.
xl-sml
set_goal([],⌜
fttab∀ x:GS• connected x ⇒ ∀ y:GS• y ⊆g x ⇒ connected y
⌝);

The proof consists of expanding appropriate definitions, stripping the goal and then reasoning forward from the assumptions.
xl-sml
a (rewrite_tac (map get_spec [⌜connected⌝, ⌜$⊆g⌝])
fttabTHEN REPEAT_N 7 strip_tac);


xl-gft
(* *** Goal "" *** *)

(* 4 *) ⌜∀ t u• t ∈g x ∧ u ∈g x ⇒ t ∈g u ∨ t = u ∨ u ∈g t⌝
(* 3 *) ⌜∀ e• e ∈g y ⇒ e ∈g x⌝
(* 2 *) ⌜t ∈g y⌝
(* 1 *) ⌜u ∈g y⌝

(* ?⊢ *) ⌜t ∈g u ∨ t = u ∨ u ∈g t⌝


xl-sml
a (all_asm_fc_tac[]);
a (REPEAT_N 2 (asm_fc_tac[]) THEN REPEAT strip_tac);
val conn_sub_conn = save_pop_thm "conn_sub_conn";

Now we show that any member of an ordinal is an ordinal.
xl-sml
set_goal([],⌜
fttab∀ x:GS• ordinal x ⇒ ∀ y:GS• y ∈g x ⇒ connected y
⌝);

Expanding the definition of ordinal and making use of transitivity enables us to infer that members of an ordinals are subsets and permits application of the previous result to obtain connectedness.
xl-sml
a (rewrite_tac (map get_spec [⌜ordinal⌝, ⌜transitive⌝])
fttabTHEN REPEAT strip_tac);
a (all_asm_fc_tac []);
a (all_asm_fc_tac [conn_sub_conn]);
val conn_mem_ord = save_pop_thm "conn_mem_ord";

To prove that the members of an ordinal are transitive, well-foundedness is needed. First we prove the particular consequences of well-foundedness which are required (these results really belong somewhere else).
xl-sml
set_goal([], ⌜
fttab∀ x:GS• ¬ x ∈g x
⌝);

The proof uses well-founded transfinite induction over the membership relation.
xl-sml
a (asm_tac (gs_wf_ind_thm));
a (spec_nth_asm_tac 1 ⌜λx• ¬ x ∈g x⌝);


xl-gft
(* *** Goal "1" *** *)

(* 3 *) ⌜∀ s• (∀ x• (∀ y• y ∈g x ⇒ s y) ⇒ s x) ⇒ (∀ x• s x)⌝
(* 2 *) ⌜∀ y• y ∈g x ⇒ (λ x• ¬ x ∈g x) y⌝
(* 1 *) ⌜¬ (λ x• ¬ x ∈g x) x⌝

(* ?⊢ *) ⌜∀ x• ¬ x ∈g x⌝


xl-sml
a (swap_nth_asm_concl_tac 1
fttabTHEN rewrite_tac[]
fttabTHEN swap_nth_asm_concl_tac 1
fttabTHEN ALL_ASM_FC_T (MAP_EVERY ante_tac) []
fttabTHEN asm_rewrite_tac[]);


xl-gft
(* *** Goal "2" *** *)

(* 2 *) ⌜∀ s• (∀ x• (∀ y• y ∈g x ⇒ s y) ⇒ s x) ⇒ (∀ x• s x)⌝
(* 1 *) ⌜∀ x• (λ x• ¬ x ∈g x) x⌝

(* ?⊢ *) ⌜∀ x• ¬ x ∈g x⌝


xl-sml
a (strip_tac
fttabTHEN swap_nth_asm_concl_tac 1
fttabTHEN rewrite_tac[]
fttabTHEN REPEAT strip_tac
fttabTHEN ∃_tac ⌜x⌝
fttabTHEN asm_rewrite_tac[]);
val wf_l1 = save_pop_thm "wf_l1";


xl-sml
set_goal([], ⌜∀ x y:GS• ¬ (x ∈g y ∧ y ∈g x)⌝);


xl-sml
set_goal([], ⌜∀ x y z:GS• ¬ (x ∈g y ∧ y ∈g z ∧ z ∈g x)⌝);

Now we are ready to prove that the members of an ordinal are transitive.
xl-sml
set_goal([], ⌜∀ x:GS• ordinal x ⇒ ∀ y:GS• y ∈g x ⇒ transitive y⌝);

Finally we prove that all members of an ordinal are ordinals.
xl-sml
set_goal([], ⌜∀ x:GS• ordinal x ⇒ ∀ y:GS• y ∈g x ⇒ ordinal y⌝);

Galaxies are Closed under the Successor Relationship
We need this result later to show that the natural numbers are a set.
xl-sml
set_goal([], ⌜∀g x• galaxy g ∧ x ∈g g ⇒ suco x ∈g g⌝);
a (REPEAT strip_tac THEN rewrite_tac [get_spec ⌜suco⌝]);
a (REPEAT (all_asm_fc_tac [GCloseUnit, GClose∪g]));
val GCloseSuco = save_pop_thm "GCloseSuco";

Theorem 2.4
We prove that the ordinals are linearly ordered by $<o.
First we prove some lemmas:
xl-sml
set_goal([], ⌜∀ x y:GS• transitive x ∧ transitive y ⇒ transitive (x ∩g y)⌝);


xl-sml
set_goal([], ⌜∀ x y:GS• transitive x ∧ transitive y ⇒ transitive (x ∪g y)⌝);


xl-sml
set_goal([], ⌜∀ x y:GS• connected x ∧ connected y ⇒ connected (x ∩g y)⌝);


xl-sml
set_goal([], ⌜∀ x y:GS• ordinal x ∧ ordinal y ⇒ ordinal (x ∩g y)⌝);


xl-sml
set_goal([], ⌜∀ x y:GS• ordinal x ∧ ordinal y ∧ x ⊆g y ∧ ¬ x = y ⇒ x ∈g y⌝);


xl-sml
set_goal([], ⌜∀ x y:GS• ordinal x ∧ ordinal y ⇒ ordinal (x ∪g y)⌝);


xl-sml
set_goal([], ⌜∀ x y:GS• ordinal x ∧ ordinal y ⇒ x <o y ∨ x = y ∨ y <o x⌝);

Definition 2.6
Successor and limit ordinals are defined. Natural numbers are defined.
These definitions are not the ones used by Drake, and not only the names but the concepts differ. My successor predicate does not hold of the empty set. I use the name "natural number" where he talks of integers, and generally I'm chosing longer names.
xl-holconst
successor : GS → BOOL
∀s :GS• successor s ⇔ ∃t• ordinal t ∧ s = suco t

xl-holconst
limit_ordinal : GS → BOOL
∀s :GS• limit_ordinal s ⇔ ordinal s ∧ ¬ successor s ∧ ¬ s = ∅g

xl-holconst
natural_number : GS → BOOL
∀s :GS• natural_number s ⇔ s = ∅g ∨ (successor s ∧ ∀t• t∈g s ⇒ t = ∅g ∨ successor t)
Theorem 2.7
Induction theorems over ordinals and natural numbers.
Successors are Ordinals

xl-sml
set_goal([],⌜fttab∀ x:GS• successor x ⇒ ordinal xfttab⌝);
a (rewrite_tac[get_spec ⌜successor⌝]
fttabTHEN REPEAT strip_tac
fttabTHEN fc_tac [ord_suc_ord_thm]
fttabTHEN asm_rewrite_tac[]);
val successor_ord_thm = save_pop_thm "successor_ord_thm";

Well-foundedness of the ordinals
First we prove that <o is well-founded.
xl-sml
set_goal([],⌜well_founded $<o⌝);
a (asm_tac gs_wf_axiom);
a (fc_tac [wf_restrict_wf_thm]);
a (SPEC_NTH_ASM_T 1 ⌜λx y• ordinal x ∧ ordinal y⌝ ante_tac
fttabTHEN rewrite_tac[]);
a (lemma_tac ⌜$<o = (λ x y• (ordinal x ∧ ordinal y) ∧ x ∈g y)⌝);
(* *** Goal "1" *** *)
a (once_rewrite_tac [ext_thm]);
a (once_rewrite_tac [ext_thm]);
a (prove_tac[get_spec ⌜$<o⌝]);
(* *** Goal "2" *** *)
a (asm_rewrite_tac[]);
val wf_ordinals_thm = save_pop_thm "wf_ordinals_thm";

Ordering the Natural Numbers
To get an induction principle for the natural numbers we first define a well-founded ordering over them. Since I don't plan to use this a lot I use the name <gn (less than over the natural numbers defined in galactic set theory).
xl-sml
declare_infix(240,"<gn");


xl-holconst
$<gn : GS → GS → BOOL
∀x y:GS• x <gn y ⇔ natural_number x ∧ natural_number y ∧ x ∈g y
Now we try to find a better proof that the one above that this is well-founded. And fail, this is just a more compact rendition of the same proof.
xl-sml
set_goal([],⌜well_founded $<gn⌝);
a (asm_tac gs_wf_axiom);
a (fc_tac [wf_restrict_wf_thm]);
a (SPEC_NTH_ASM_T 1 ⌜λx y• natural_number x ∧ natural_number y⌝ ante_tac
fttabTHEN rewrite_tac[]);
a (lemma_tac ⌜$<gn = (λ x y• (natural_number x ∧ natural_number y) ∧ x ∈g y)⌝
fttabTHEN1 (REPEAT_N 2 (once_rewrite_tac [ext_thm])
fttabfttabTHEN prove_tac[get_spec ⌜$<gn⌝]));
a (asm_rewrite_tac[]);
val wf_nat_thm = save_pop_thm "wf_nat_thm";

This allows us to do well-founded induction over the natural number which the way I have implemented it is "course-of-values" induction. However, for the sake of form I will prove that induction principle as an explicit theorem. This is just what you get by expanding the definition of well-foundedness in the above theorem.
xl-sml
val nat_induct_thm = save_thm ("nat_induct_thm",
fttab(rewrite_rule [get_spec ⌜well_founded⌝] wf_nat_thm));

Note that this theorem can only be used to prove properties which are true of all sets, so you have to make it conditional (natural_number n ⇒ whatever). I suppose I'd better do another one.
xl-sml
set_goal([], ⌜∀ p• (∀ x• natural_number x ∧ (∀ y• y <gn x ⇒ p y) ⇒ p x)
fttab⇒ (∀ x• natural_number x ⇒ p x)⌝);
a (asm_tac (rewrite_rule []
fttab(all_∀_intro (∀_elim ⌜λx• natural_number x ⇒ p x⌝ nat_induct_thm))));
a (rewrite_tac [all_∀_intro (taut_rule ⌜a ∧ b ⇒ c ⇔ b ⇒ a ⇒ c⌝)]);
a (lemma_tac ⌜∀ p x• (∀ y• y <gn x ⇒ p y) ⇔ (∀ y• y <gn x ⇒ natural_number y ⇒ p y)⌝);
(* *** Goal "1" *** *)
a (rewrite_tac [get_spec ⌜$<gn⌝]);
a (REPEAT strip_tac THEN all_asm_fc_tac[]);
(* *** Goal "2" *** *)
a (asm_rewrite_tac[]);
val nat_induct_thm2 = save_pop_thm "nat_induct_thm2";

I've tried using that principle and it too has disadvantages. Because <gn is used the induction hypothesis is more awkward to use (weaker) than it would have been if ∈g had been used. Unfortunately the proof of an induction theorem using plain set membership is not entirely trivial, so its proof has to be left til later.
xl-sml
set_goal([], ⌜∀ p• (∀ x• natural_number x ∧ (∀ y• y ∈g x ⇒ p y) ⇒ p x)
fttab⇒ (∀ x• natural_number x ⇒ p x)⌝);

Theorem 2.8
The set of natural numbers.
Natural Numbers are Ordinals

xl-sml
set_goal ([], ⌜∀n• natural_number n ⇒ ordinal n⌝);
a (rewrite_tac [get_spec ⌜natural_number⌝, get_spec ⌜successor⌝]);
a (REPEAT strip_tac THEN_TRY asm_rewrite_tac[ordinal_∅g]);
a (all_fc_tac [ord_suc_ord_thm]);
val ord_nat_thm = save_pop_thm "ord_nat_thm";

Members of Natural Numbers are Ordinals

xl-sml
set_goal ([], ⌜∀n• natural_number n ⇒ ∀m• m ∈g n ⇒ ordinal m⌝);
a (REPEAT strip_tac);
a (REPEAT (all_fc_tac[ord_nat_thm, ord_mem_ord]));
val mem_nat_ord_thm = save_pop_thm "mem_nat_ord_thm";

An Ordinal is Zero, a successor or a limit

xl-sml
set_goal ([], ⌜∀n• ordinal n ⇒ n = ∅g ∨ successor n ∨ limit_ordinal n⌝);
a (rewrite_tac [get_spec ⌜limit_ordinal⌝, get_spec ⌜successor⌝]);
a (REPEAT strip_tac);
a (spec_nth_asm_tac 2 ⌜t⌝);
val ordinal_kind_thm = save_pop_thm "ordinal_kind_thm";

A Natural Number is not a Limit Ordinal

xl-sml
set_goal ([], ⌜∀n• natural_number n ⇒ ¬ limit_ordinal n⌝);
a (rewrite_tac [get_spec ⌜limit_ordinal⌝, get_spec ⌜natural_number⌝]);
a (REPEAT strip_tac);
val nat_not_lim_thm = save_pop_thm "nat_not_lim_thm";

A Natural Number is zero or a successor

xl-sml
set_goal ([], ⌜∀n• natural_number n ⇒ successor n ∨ n = ∅g⌝);
a (rewrite_tac [get_spec ⌜natural_number⌝]);
a (REPEAT strip_tac);
val nat_zero_or_suc_thm = save_pop_thm "nat_zero_or_suc_thm";

A Non-empty set is not the Empty Set

xl-sml
set_goal ([], ⌜∀m n• m ∈g n ⇒ ¬ n = ∅g⌝);
a (prove_tac [gst_opext_clauses, gst_relext_clauses]);
val mem_not_empty_thm = save_pop_thm "mem_not_empty_thm";

A Natural Number does not contain a Limit Ordinal

xl-sml
set_goal ([], ⌜∀m n• natural_number n ∧ m ∈g n ⇒ ¬ limit_ordinal m⌝);
a (rewrite_tac [get_spec ⌜limit_ordinal⌝, get_spec ⌜natural_number⌝]);
a (REPEAT strip_tac);
(* *** Goal "1" *** *)
a (all_fc_tac [mem_not_empty_thm]);
(* *** Goal "2" *** *)
a (all_asm_fc_tac[]);
val mem_nat_not_lim_thm = save_pop_thm "mem_nat_not_lim_thm";

All Members of Natural Numbers are Natural Numbers

xl-sml
set_goal ([], ⌜∀n• natural_number n ⇒ ∀m• m ∈g n ⇒ natural_number m⌝);
a (rewrite_tac [get_spec ⌜natural_number⌝]);
a (REPEAT strip_tac THEN_TRY all_asm_fc_tac [mem_not_empty_thm]);
a (lemma_tac ⌜transitive n⌝ THEN1
fttab (REPEAT (all_fc_tac [get_spec ⌜ordinal⌝, successor_ord_thm])));
a (lemma_tac ⌜t ∈g n⌝ THEN1 (EVERY [all_fc_tac [get_spec ⌜transitive⌝],
fttabPOP_ASM_T ante_tac, rewrite_tac [gst_relext_clauses], asm_prove_tac[]]));
a (all_asm_fc_tac[]);
val mem_nat_nat_thm = save_pop_thm "mem_nat_nat_thm";

Galaxies are Closed under suc

xl-sml
set_goal ([], ⌜∀g• galaxy g ⇒ ∀x• x ∈g g ⇒ suco x ∈g g⌝);
a (rewrite_tac [get_spec ⌜suco⌝]);
a (REPEAT strip_tac);
a (REPEAT (all_fc_tac [GClose∪g, GCloseUnit]));
val GCloseSuc = save_pop_thm "GCloseSuc";

Natural Numbers are in the Smallest Galaxy

xl-sml
set_goal ([], ⌜∀n• natural_number n ⇒ n ∈g Gx ∅g⌝);
a (strip_tac THEN gen_induction_tac1 nat_induct_thm2);
a (fc_tac [nat_zero_or_suc_thm]);
(* *** Goal "1" *** *)
a (fc_tac [get_spec ⌜successor⌝]);
a (lemma_tac ⌜t <gn n⌝
fttabTHEN1 asm_rewrite_tac [get_spec ⌜$<gn⌝, get_spec ⌜suco⌝]);
(* *** Goal "1.1" *** *)
a (lemma_tac ⌜t ∈g n⌝
fttabTHEN1 asm_rewrite_tac [get_spec ⌜suco⌝]);
a (all_fc_tac [mem_nat_nat_thm]);
(* *** Goal "1.2" *** *)
a (asm_tac (∀_elim ⌜∅g⌝ galaxy_Gx));
a (asm_rewrite_tac[]);
a (REPEAT (all_asm_fc_tac[GCloseSuc]));
(* *** Goal "2" *** *)
a (asm_rewrite_tac[]);
a (asm_tac (∀_elim ⌜∅g⌝ galaxy_Gx));
a (all_asm_fc_tac[G∅gC]);
val nat_in_G∅g_thm = save_pop_thm "nat_in_G∅g_thm";

The Existence of w
This comes from the axiom of infinity, however, in galactic set theory we get that from the existence of galaxies, so the following proof is a little unusual.
xl-sml
set_goal ([], ⌜∃w• ∀z• z ∈g w ⇔ natural_number z⌝);
a (∃_tac ⌜Sep (Gx ∅g) natural_number⌝
fttabTHEN rewrite_tac [gst_opext_clauses]);
a (rewrite_tac [all_∀_intro (taut_rule ⌜(a ∧ b ⇔ b) ⇔ b ⇒ a⌝)]);
a strip_tac;
a (gen_induction_tac1 nat_induct_thm2);
a (fc_tac [nat_zero_or_suc_thm]);
(* *** Goal "1" *** *)
a (fc_tac [get_spec ⌜successor⌝, nat_in_G∅g_thm]);
(* *** Goal "2" *** *)
a (asm_rewrite_tac []);
a (asm_tac (∀_elim ⌜∅g⌝ galaxy_Gx));
a (all_asm_fc_tac[G∅gC]);
val w_exists_thm = save_pop_thm "w_exists_thm";

The Definition of Rank
We define the rank of a set.
The Consistency Proof
Before introducing the definition of rank we undertake the proof necessary to establish that the definition is conservative. The key lemma in this proof is the proof that the relevant functional "respects" the membership relation.
xl-sml
set_goal([],⌜(λf• λx• ⋃g (Imagep (suco o f) x)) respects $∈g⌝);
a (rewrite_tac [get_spec ⌜$respects⌝]
fttabTHEN REPEAT strip_tac);
a (once_rewrite_tac [gst_relext_clauses]
fttabTHEN REPEAT strip_tac);
(* *** Goal "1" *** *)
a (∃_tac ⌜e'⌝ THEN REPEAT strip_tac);
a (∃_tac ⌜e''⌝ THEN REPEAT strip_tac);
a (POP_ASM_T ante_tac
fttabTHEN rewrite_tac[get_spec⌜$o⌝]
fttabTHEN strip_tac);
a (lemma_tac ⌜h e'' = g e''⌝
fttabTHEN1 (REPEAT_N 2 (asm_fc_tac[tc_incr_thm])
fttabfttabTHEN asm_rewrite_tac[]));
a (asm_rewrite_tac[]);
(* *** Goal "2" *** *)
a (∃_tac ⌜e'⌝ THEN REPEAT strip_tac);
a (∃_tac ⌜e''⌝ THEN REPEAT strip_tac);
a (POP_ASM_T ante_tac
fttabTHEN rewrite_tac[get_spec⌜$o⌝]
fttabTHEN strip_tac);
a (lemma_tac ⌜h e'' = g e''⌝
fttabTHEN1 (REPEAT_N 2 (asm_fc_tac[tc_incr_thm])
fttabfttabTHEN asm_rewrite_tac[]));
a (asm_rewrite_tac[]);
val respect_lemma = pop_thm();

Armed with that lemma we can now prove that the function which we will call "rank" exists.
xl-sml
set_goal([],⌜∃rank• ∀x• rank x = ⋃g (Imagep (suco o rank) x)⌝);
a (∃_tac ⌜fix (λf• λx• ⋃g (Imagep (suco o f) x))⌝
fttabTHEN strip_tac);
a (asm_tac gs_wf_axiom);
a (asm_tac respect_lemma);
a (fc_tac [∀_elim ⌜λf• λx• ⋃g (Imagep (suco o f) x)⌝ (get_spec ⌜fix⌝)]);
a (asm_fc_tac []);
a (POP_ASM_T (rewrite_thm_tac o rewrite_rule [ext_thm]));
val _ = xl_set_cs_∃_thm (pop_thm());


xl-holconst
rank : GS → GS
∀x• rank x = ⋃g (Imagep (suco o rank) x)
Proof Context
In this section we define a proof context for ordinals.
Proof Context

xl-sml
add_pc_thms "ord" ([]);
set_merge_pcs ["basic_hol", "gst-ax", "ord"];
commit_pc "ord";


up quick index © RBJ

privacy policy

Created:

$Id: ordinals.xml,v 1.4 2011/02/20 16:11:48 rbj Exp $

V