# Library ZFord

Require Import ZFnats.
Require Export ZF.
Import IZF.

Fixpoint plump ub (p:Acc in_set ub) x : Prop :=
(forall y (q: y \in ub), y \in x -> plump y (Acc_inv p _ q) y) /\
(forall z y (q: y \in ub), plump y (Acc_inv p _ q) z ->
z \incl y -> y \in x -> z \in x).

Instance wf_morph : Proper (eq_set ==> iff) (Acc in_set).

Qed.

Scheme Acc_indd := Induction for Acc Sort Prop.

Lemma plump_morph : forall x x' p p' y y',
x == x' -> y == y' -> (plump x p y <-> plump x' p' y').

Lemma plump_bound : forall ub1 ub2 p1 p2 x,
x \incl ub1 ->
plump ub1 p1 x -> plump ub2 p2 x.

Lemma plump_Acc : forall ub p x,
plump ub p x -> x \incl ub -> Acc in_set x.

Definition isOrd x :=
{ p:Acc in_set x | plump x p x }.

Lemma isOrd_ext : forall x y, x == y -> isOrd x -> isOrd y.

Instance isOrd_morph : Proper (eq_set ==> iff) isOrd.

Qed.

Lemma isOrd_inv : forall x y,
isOrd x -> lt y x -> isOrd y.

Lemma isOrd_plump : forall z, isOrd z ->
forall x y, isOrd x -> x \incl y -> y \in z -> x \in z.

Lemma isOrd_intro : forall x,
(forall a b, isOrd a -> a \incl b -> b \in x -> a \in x) ->
(forall y, y \in x -> isOrd y) ->
isOrd x.

Lemma isOrd_trans : forall x y z,
isOrd x -> lt z y -> lt y x -> lt z x.

Lemma isOrd_ind : forall x (P:set->Prop),
(forall y y', isOrd y -> y \incl x -> y == y' -> P y -> P y') ->
(forall y, isOrd y ->
y \incl x ->
(forall z, lt z y -> P z) -> P y) ->
isOrd x -> P x.

Lemma lt_antirefl : forall x, isOrd x -> ~ lt x x.

Lemma isOrd_zero : isOrd zero.

Definition osucc x := subset (power x) isOrd.

Instance osucc_morph : morph1 osucc.

Qed.

Lemma lt_osucc : forall x, isOrd x -> lt x (osucc x).

Hint Resolve isOrd_zero lt_osucc.

Lemma olts_le : forall x y, lt x (osucc y) -> x \incl y.

Lemma ole_lts : forall x y, isOrd x -> x \incl y -> lt x (osucc y).

Lemma le_lt_trans : forall x y z, isOrd z -> lt x (osucc y) -> lt y z -> lt x z.

Lemma isOrd_succ : forall n, isOrd n -> isOrd (osucc n).
Hint Resolve isOrd_succ.

Lemma lt_osucc_compat : forall n m, isOrd m -> lt n m -> lt (osucc n) (osucc m).

Lemma isOrd_eq : forall o, isOrd o -> o == sup o osucc.

Definition increasing F :=
forall x y, isOrd x -> isOrd y -> y \incl x -> F y \incl F x.
Definition increasing_bounded o F :=
forall x x', lt x' o -> lt x x' -> F x \incl F x'.

Definition succOrd o := exists2 o', isOrd o' & o == osucc o'.

Definition limitOrd o := isOrd o /\ (forall x, lt x o -> lt (osucc x) o).

Lemma limit_is_ord : forall o, limitOrd o -> isOrd o.
Hint Resolve limit_is_ord.

Lemma limit_union : forall o, limitOrd o -> union o == o.

Lemma limit_union_intro : forall o, isOrd o -> union o == o -> limitOrd o.

Lemma discr_lim_succ : forall o, limitOrd o -> succOrd o -> False.

Section OrdinalUpperBound.

Variable I : set.
Variable f : set -> set.
Hypothesis f_ext : ext_fun I f.
Hypothesis f_ord : forall x, x \in I -> isOrd (f x).

Lemma isOrd_supf_intro : forall n, n \in I -> f n \incl sup I f.

Lemma isOrd_supf_elim : forall x, lt x (sup I f) -> exists2 n, n \in I & lt x (f n).

Lemma isOrd_supf : isOrd (sup I f).

End OrdinalUpperBound.

Definition toOrd (x : set) :=
sup (subset x isOrd) osucc.

Instance toOrd_morph : morph1 toOrd.

Qed.

Lemma toOrd_isOrd : forall x, isOrd (toOrd x).

Lemma toOrd_ord : forall o, isOrd o -> toOrd o == o.

Section TransfiniteRecursion.

Variable F : (set -> set) -> set -> set.
Hypothesis Fmorph : forall o o' f f',
o == o' -> eq_fun o f f' -> F f o == F f' o'.

Definition TR_rel o y :=
forall P,
Proper (eq_set ==> eq_set ==> iff) P ->
(forall o' f, ext_fun o' f ->
(forall n, lt n o' -> P n (f n)) ->
P o' (F f o')) ->
P o y.

Instance TR_rel_morph : Proper (eq_set ==> eq_set ==> iff) TR_rel.

Qed.

Lemma TR_rel_intro : forall x f,
ext_fun x f ->
(forall y, y \in x -> TR_rel y (f y)) ->
TR_rel x (F f x).

Lemma TR_rel_inv : forall x y,
TR_rel x y ->
exists2 f,
ext_fun x f /\ (forall y, y \in x -> TR_rel y (f y)) &
y == F f x.

Lemma TR_rel_fun :
forall x y, TR_rel x y -> forall y', TR_rel x y' -> y == y'.

Require Import ZFrepl.

Lemma TR_rel_repl_rel :
forall x, repl_rel x TR_rel.

Lemma TR_rel_def : forall o, isOrd o -> exists y, TR_rel o y.

Lemma TR_rel_choice_pred : forall o, isOrd o ->
uchoice_pred (fun y => TR_rel o y).

Definition TR o := uchoice (fun y => TR_rel o y).

Instance TR_morph : morph1 TR.
Qed.

Lemma TR_eqn : forall o, isOrd o -> TR o == F TR o.

Lemma TR_ind : forall o (P:set->set->Prop),
(forall x x', isOrd x -> x \incl o -> x == x' ->
forall y y', y == y' -> P x y -> P x' y') ->
isOrd o ->
(forall y, isOrd y -> y \incl o ->
(forall x, lt x y -> P x (TR x)) ->
P y (F TR y)) ->
P o (TR o).

Lemma TR_typ : forall n X,
morph1 X ->
isOrd n ->
(forall y f, isOrd y -> y \incl n ->
(forall z, lt z y -> f z \in X z) -> F f y \in X y) ->
TR n \in X n.

End TransfiniteRecursion.

Section TransfiniteIteration.

Variable F : set -> set.
Hypothesis Fmorph : Proper (eq_set ==> eq_set) F.

Let G f o := sup o (fun o' => F (f o')).

Lemma Gmorph : forall o o' f f',
o == o' -> eq_fun o f f' -> G f o == G f' o'.
Hint Resolve Gmorph.

Definition TI := TR G.

Instance TI_morph : morph1 TI.
Qed.

Lemma TI_fun_ext : forall x, ext_fun x (fun y => F (TI y)).
Hint Resolve TI_fun_ext.

Lemma TI_eq : forall o,
isOrd o ->
TI o == sup o (fun o' => F (TI o')).

Lemma TI_intro : forall o o' x,
isOrd o ->
lt o' o ->
x \in F (TI o') ->
x \in TI o.

Lemma TI_elim : forall o x,
isOrd o ->
x \in TI o ->
exists2 o', lt o' o & x \in F (TI o').

Lemma TI_initial : TI zero == empty.

Lemma TI_typ : forall n X,
(forall a, a \in X -> F a \in X) ->
isOrd n ->
(forall m G, isOrd m -> m \incl n ->
ext_fun m G ->
(forall x, lt x m -> G x \in X) -> sup m G \in X) ->
TI n \in X.

End TransfiniteIteration.
Hint Resolve TI_fun_ext.

Require Import ZFrepl.

Section LimOrd.

Variable f : nat -> set.
Variable ford : forall n, isOrd (f n).

Definition ord_sup :=
union (repl N (fun x y => exists2 n, x == nat2set n & f n == y)).

Lemma repl_sup :
repl_rel N (fun x y => exists2 n, x == nat2set n & f n == y).

Lemma isOrd_sup_intro : forall n, f n \incl ord_sup.

Lemma isOrd_sup_elim : forall x, lt x ord_sup -> exists n, lt x (f n).

Lemma isOrd_sup : isOrd ord_sup.

End LimOrd.

Section LimOrdRel.

Variable R : nat -> set -> Prop.
Variable Rmorph : forall n x x', isOrd x -> x == x' -> R n x -> R n x'.
Variable Rtot : forall n, exists x, R n x.
Variable Rfun : forall n x x',
isOrd x -> isOrd x' -> R n x -> R n x' -> x == x'.
Variable Rord : forall n x, R n x -> isOrd x.

Definition sup_rel :=
union (repl N (fun x y => exists2 n, x == nat2set n & R n y)).

Lemma repl_sup_rel :
repl_rel N (fun x y => exists2 n, x == nat2set n & R n y).

Lemma isOrd_sup_rel_intro2 : forall n y, R n y -> y \incl sup_rel.

Lemma isOrd_sup_rel_intro : forall n,
exists2 y, R n y & y \incl sup_rel.

Lemma isOrd_sup_rel_elim :
forall x, lt x sup_rel -> exists n, exists2 y, R n y & lt x y.

Lemma isOrd_sup_rel : isOrd sup_rel.

End LimOrdRel.

Fixpoint nat2ordset n :=
match n with
| 0 => zero
| S k => osucc (nat2ordset k)
end.

Lemma nat2ordset_typ : forall n, isOrd (nat2ordset n).
Hint Resolve nat2ordset_typ.

Definition omega := ord_sup nat2ordset.

Lemma isOrd_omega : isOrd omega.
Hint Resolve isOrd_omega.

Lemma zero_omega : lt zero omega.
Hint Resolve zero_omega.

Lemma osucc_omega : forall n, lt n omega -> lt (osucc n) omega.
Hint Resolve osucc_omega.

Lemma omega_limit_ord : limitOrd omega.
Hint Resolve omega_limit_ord.

Inductive ord : Set := OO | OS (o:ord) | OL (f:nat->ord).

Fixpoint ord2set (o:ord) : set :=
match o with
| OO => zero
| OS k => osucc (ord2set k)
| OL f => ord_sup (fun k => ord2set (f k))
end.

Lemma ord2set_typ : forall o, isOrd (ord2set o).
Hint Resolve ord2set_typ.

Definition iter_w (f:set->set) o :=
ord_sup(nat_rect(fun _=>set) o (fun _ => f)).

Lemma isOrd_iter_w : forall f o,
(forall x, isOrd x -> isOrd (f x)) ->
isOrd o ->
isOrd (iter_w f o).

Definition plus_w := iter_w osucc.
Definition mult_w := iter_w plus_w.
Definition pow_w := iter_w mult_w.
Definition epsilon0 : set := iter_w pow_w omega.

Lemma isOrd_epsilon0: isOrd epsilon0.

Lemma zero_typ_e0 : zero \in epsilon0.