Library ZFord2
Require Import ZFnats ZFord ZFfix.
Import IZF.
Definition isPOrd x :=
exists2 o, isOrd o & x == VN o.
Instance isPOrd_morph : Proper (eq_set ==> iff) isPOrd.
Qed.
Lemma isPOrd_zero : isPOrd zero.
Definition osucc := power.
Lemma isPOrd_succ : forall o, isPOrd o -> isPOrd (osucc o).
Definition HF := VN N.
Lemma isPOrd_HF : isPOrd HF.
Definition olt x y := isPOrd x /\ isPOrd y /\ x \in y.
Instance olt_morph : Proper (eq_set ==> eq_set ==> iff) olt.
Qed.
Lemma olt_ord1 : forall x y, olt x y -> isPOrd x.
Lemma olt_ord2 : forall x y, olt x y -> isPOrd y.
Lemma olt_succ : forall x y,
olt x y -> olt (osucc x) (osucc y).
Lemma olt_trans : forall x y z, olt x y -> olt y z -> olt x z.
Lemma HF_limit : forall o,
olt o HF ->
olt (osucc o) HF.
Definition ole x y := isPOrd x /\ isPOrd y /\ x \incl y.
Instance ole_morph : Proper (eq_set ==> eq_set ==> iff) ole.
Qed.
Lemma olt_weak : forall x y, olt x y -> ole x y.
Lemma ole_refl : forall x, isPOrd x -> ole x x.
Hint Resolve olt_weak ole_refl.
Lemma ole_olt_trans :
forall x y z, ole x y -> olt y z -> olt x z.
Lemma olt_ole_trans :
forall x y z, olt x y -> ole y z -> olt x z.
Lemma isPOrd_ind : forall x (P:set->Prop),
(forall y y', ole y x -> y == y' -> P y -> P y') ->
(forall y, ole y x ->
(forall z, olt z y -> P z) -> P y) ->
isPOrd x -> P x.
Lemma isOrd_intro : forall x,
(forall a b, a \in b -> b \in x -> a \in x) ->
(forall y, y \in x -> isOrd y) ->
isOrd x.
Lemma isOrd_elim : forall x (P:set->Prop),
(forall x x', isOrd x -> x == x' -> P x -> P x') ->
(forall y,
(forall a b, a \in b -> b \in y -> a \in y) ->
(forall z, z \in y -> isOrd z) ->
(forall z, z \in y -> P z) -> P y) ->
isOrd x -> P x.
Lemma isOrd_inv : forall x y,
isOrd x -> lt y x -> isOrd y.
Lemma isOrd_le : forall x y,
isOrd x -> le y x -> isOrd y.
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 isOrd_zero : isOrd zero.
Lemma isOrd_succ : forall n, isOrd n -> isOrd (succ n).
Lemma le_lt_trans : forall x y z, isOrd z -> le x y -> lt y z -> lt x z.
Lemma lt_le_trans : forall x y z, isOrd z -> lt x y -> le y z -> lt x z.
Lemma lt_antirefl : forall x, isOrd x -> ~ lt x x.
Lemma isOrd_eq : forall o, isOrd o -> o == sup o succ.
Module ClassicOrdinal.
Axiom EM : forall A, A \/ ~A.
Lemma ord_total : forall x y,
isOrd x -> isOrd y -> le x y \/ lt y x.
Lemma ord_incl_le : forall x y, isOrd x -> isOrd y -> x \incl y -> le x y.
End ClassicOrdinal.
Lemma ord_le_incl : forall x y, isOrd x -> isOrd y -> le x y -> x \incl y.
Definition increasing F :=
forall x y, isOrd x -> isOrd y -> y \incl x -> F y \incl F x.
Lemma increasing_le : forall F x y,
increasing F -> isOrd x -> le y x -> F y \incl F x.
Lemma isOrd_N : isOrd N.
Lemma natOrd : forall n, n \in N -> isOrd n.
Hint Resolve natOrd isOrd_N.
Definition succOrd o := exists2 o', isOrd o' & o == succ o'.
Definition limitOrd o := isOrd o /\ union o == o.
Definition limitOrd' o := isOrd o /\ (forall x, lt x o -> lt (succ x) o).
Lemma limit_equiv : forall o, limitOrd' o -> limitOrd o.
Lemma N_limit_ord : limitOrd' N.
Lemma limit_is_ord : forall o, limitOrd o -> isOrd o.
Hint Resolve limit_is_ord.
Lemma limit'_is_ord : forall o, limitOrd' o -> isOrd o.
Hint Resolve limit'_is_ord.
Lemma discr_lim_succ : forall o, limitOrd o -> succOrd o -> False.
Definition least_ord o (P:set->Prop) :=
union (subset o (fun y => P y /\ forall x, isOrd x -> P x -> le y x)).
Lemma least_ord_morph : forall o o' (P P':set->Prop),
isOrd o -> o == o' ->
(forall x x', isOrd x -> x == x' -> (P x <-> P' x')) ->
least_ord o P == least_ord o' P'.
Lemma least_ord1 : forall o (P:set->Prop),
(forall x x', isOrd x -> x == x' -> P x -> P x') ->
isOrd o ->
forall x,
lt x o ->
P x ->
P (least_ord o P) /\ isOrd (least_ord o P) /\ le (least_ord o P) x /\
forall y, lt y (least_ord o P) -> ~ P y.
Import ClassicOrdinal.
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.
Inductive ord : Set := OO | OS (o:ord) | OL (f:nat->ord).
Fixpoint ord2set (o:ord) : set :=
match o with
| OO => zero
| OS k => succ (ord2set k)
| OL f => ord_sup (fun k => ord2set (f k))
end.
Lemma ord2set_typ : forall o, isOrd (ord2set o).
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 succ.
Definition mult_w := iter_w plus_w.
Definition pow_w := iter_w mult_w.
Definition epsilon0 : set := iter_w pow_w N.
Lemma isOrd_epsilon0: isOrd epsilon0.
Lemma zero_typ_e0 : zero \in epsilon0.
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'.
Lemma TR_rel_repl_rel :
forall o, isOrd o -> repl_rel o 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).
Lemma TR_morph0 : forall o o', isOrd o -> o == o' -> TR o == TR o'.
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,
isOrd n ->
(forall y f, isOrd y -> y \incl n ->
(forall z, lt z y -> f z \in X) -> F f y \in X) ->
TR n \in X.
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.
Lemma TI_morph0 : forall x x', isOrd x -> x == x' ->
TI x == TI x'.
Lemma TI_fun_ext : forall o, isOrd o ->
ext_fun o (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, le m 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.
Import IZF.
Definition isPOrd x :=
exists2 o, isOrd o & x == VN o.
Instance isPOrd_morph : Proper (eq_set ==> iff) isPOrd.
Qed.
Lemma isPOrd_zero : isPOrd zero.
Definition osucc := power.
Lemma isPOrd_succ : forall o, isPOrd o -> isPOrd (osucc o).
Definition HF := VN N.
Lemma isPOrd_HF : isPOrd HF.
Definition olt x y := isPOrd x /\ isPOrd y /\ x \in y.
Instance olt_morph : Proper (eq_set ==> eq_set ==> iff) olt.
Qed.
Lemma olt_ord1 : forall x y, olt x y -> isPOrd x.
Lemma olt_ord2 : forall x y, olt x y -> isPOrd y.
Lemma olt_succ : forall x y,
olt x y -> olt (osucc x) (osucc y).
Lemma olt_trans : forall x y z, olt x y -> olt y z -> olt x z.
Lemma HF_limit : forall o,
olt o HF ->
olt (osucc o) HF.
Definition ole x y := isPOrd x /\ isPOrd y /\ x \incl y.
Instance ole_morph : Proper (eq_set ==> eq_set ==> iff) ole.
Qed.
Lemma olt_weak : forall x y, olt x y -> ole x y.
Lemma ole_refl : forall x, isPOrd x -> ole x x.
Hint Resolve olt_weak ole_refl.
Lemma ole_olt_trans :
forall x y z, ole x y -> olt y z -> olt x z.
Lemma olt_ole_trans :
forall x y z, olt x y -> ole y z -> olt x z.
Lemma isPOrd_ind : forall x (P:set->Prop),
(forall y y', ole y x -> y == y' -> P y -> P y') ->
(forall y, ole y x ->
(forall z, olt z y -> P z) -> P y) ->
isPOrd x -> P x.
Lemma isOrd_intro : forall x,
(forall a b, a \in b -> b \in x -> a \in x) ->
(forall y, y \in x -> isOrd y) ->
isOrd x.
Lemma isOrd_elim : forall x (P:set->Prop),
(forall x x', isOrd x -> x == x' -> P x -> P x') ->
(forall y,
(forall a b, a \in b -> b \in y -> a \in y) ->
(forall z, z \in y -> isOrd z) ->
(forall z, z \in y -> P z) -> P y) ->
isOrd x -> P x.
Lemma isOrd_inv : forall x y,
isOrd x -> lt y x -> isOrd y.
Lemma isOrd_le : forall x y,
isOrd x -> le y x -> isOrd y.
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 isOrd_zero : isOrd zero.
Lemma isOrd_succ : forall n, isOrd n -> isOrd (succ n).
Lemma le_lt_trans : forall x y z, isOrd z -> le x y -> lt y z -> lt x z.
Lemma lt_le_trans : forall x y z, isOrd z -> lt x y -> le y z -> lt x z.
Lemma lt_antirefl : forall x, isOrd x -> ~ lt x x.
Lemma isOrd_eq : forall o, isOrd o -> o == sup o succ.
Module ClassicOrdinal.
Axiom EM : forall A, A \/ ~A.
Lemma ord_total : forall x y,
isOrd x -> isOrd y -> le x y \/ lt y x.
Lemma ord_incl_le : forall x y, isOrd x -> isOrd y -> x \incl y -> le x y.
End ClassicOrdinal.
Lemma ord_le_incl : forall x y, isOrd x -> isOrd y -> le x y -> x \incl y.
Definition increasing F :=
forall x y, isOrd x -> isOrd y -> y \incl x -> F y \incl F x.
Lemma increasing_le : forall F x y,
increasing F -> isOrd x -> le y x -> F y \incl F x.
Lemma isOrd_N : isOrd N.
Lemma natOrd : forall n, n \in N -> isOrd n.
Hint Resolve natOrd isOrd_N.
Definition succOrd o := exists2 o', isOrd o' & o == succ o'.
Definition limitOrd o := isOrd o /\ union o == o.
Definition limitOrd' o := isOrd o /\ (forall x, lt x o -> lt (succ x) o).
Lemma limit_equiv : forall o, limitOrd' o -> limitOrd o.
Lemma N_limit_ord : limitOrd' N.
Lemma limit_is_ord : forall o, limitOrd o -> isOrd o.
Hint Resolve limit_is_ord.
Lemma limit'_is_ord : forall o, limitOrd' o -> isOrd o.
Hint Resolve limit'_is_ord.
Lemma discr_lim_succ : forall o, limitOrd o -> succOrd o -> False.
Definition least_ord o (P:set->Prop) :=
union (subset o (fun y => P y /\ forall x, isOrd x -> P x -> le y x)).
Lemma least_ord_morph : forall o o' (P P':set->Prop),
isOrd o -> o == o' ->
(forall x x', isOrd x -> x == x' -> (P x <-> P' x')) ->
least_ord o P == least_ord o' P'.
Lemma least_ord1 : forall o (P:set->Prop),
(forall x x', isOrd x -> x == x' -> P x -> P x') ->
isOrd o ->
forall x,
lt x o ->
P x ->
P (least_ord o P) /\ isOrd (least_ord o P) /\ le (least_ord o P) x /\
forall y, lt y (least_ord o P) -> ~ P y.
Import ClassicOrdinal.
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.
Inductive ord : Set := OO | OS (o:ord) | OL (f:nat->ord).
Fixpoint ord2set (o:ord) : set :=
match o with
| OO => zero
| OS k => succ (ord2set k)
| OL f => ord_sup (fun k => ord2set (f k))
end.
Lemma ord2set_typ : forall o, isOrd (ord2set o).
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 succ.
Definition mult_w := iter_w plus_w.
Definition pow_w := iter_w mult_w.
Definition epsilon0 : set := iter_w pow_w N.
Lemma isOrd_epsilon0: isOrd epsilon0.
Lemma zero_typ_e0 : zero \in epsilon0.
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'.
Lemma TR_rel_repl_rel :
forall o, isOrd o -> repl_rel o 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).
Lemma TR_morph0 : forall o o', isOrd o -> o == o' -> TR o == TR o'.
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,
isOrd n ->
(forall y f, isOrd y -> y \incl n ->
(forall z, lt z y -> f z \in X) -> F f y \in X) ->
TR n \in X.
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.
Lemma TI_morph0 : forall x x', isOrd x -> x == x' ->
TI x == TI x'.
Lemma TI_fun_ext : forall o, isOrd o ->
ext_fun o (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, le m 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.