Library ZFindtypes
Require Export basic.
Require Import ZF ZFsum ZFfix ZFnats ZFord ZFrelations.
Import IZF ZFrepl.
Lemma cst_is_ext : forall X o, ext_fun o (fun _ => X).
Hint Resolve cst_is_ext.
Lemma sum_is_ext : forall o F G,
ext_fun o F ->
ext_fun o G ->
ext_fun o (fun y => sum (F y) (G y)).
Hint Resolve sum_is_ext.
Lemma func_is_ext : forall x X F,
ext_fun x F ->
ext_fun x (fun x => func X (F x)).
Hint Resolve func_is_ext.
Lemma cst_cont : forall X o y, lt y o -> X == sup o (fun _ => X).
Lemma sum_cont : forall o F G,
ext_fun o F ->
ext_fun o G ->
sum (sup o F) (sup o G) == sup o (fun y => sum (F y) (G y)).
Require Import ZFord_equiv ZFcard.
Section ProductContinuity.
Hypothesis mu : set.
Hypothesis mu_strong : stronglyInaccessibleCard mu.
Let mu_ord : isOrd mu.
Qed.
Let mu_regular : forall x F,
lt_card x mu ->
ext_fun x F ->
(forall y, y \in x -> lt (F y) mu) -> lt (sup x F) mu.
Qed.
Lemma func_cont : forall X F,
lt_card X mu ->
increasing F ->
func X (sup mu F) == sup mu (fun x => func X (F x)).
End ProductContinuity.
Definition UNIT := succ zero.
Lemma unit_typ : zero \in UNIT.
Lemma unit_elim : forall p, p \in UNIT -> p == zero.
Definition BOOL := succ (succ zero).
Definition TRUE := zero.
Definition FALSE := succ zero.
Lemma true_typ : TRUE \in BOOL.
Lemma false_typ : FALSE \in BOOL.
Lemma bool_elim : forall b, b \in BOOL -> b == TRUE \/ b == FALSE.
Section NatOrd_theory.
Definition NATf X := sum UNIT X.
Lemma sum_ext_natf : forall A, ext_fun A NATf.
Instance NATf_mono : Proper (incl_set ==> incl_set) NATf.
Qed.
Hint Resolve NATf_mono Fmono_morph.
Instance NATf_morph : Proper (eq_set ==> eq_set) NATf.
Qed.
Definition ZERO := inl zero.
Definition SUCC x := inr x.
Lemma NATf_discr : forall n, ~ ZERO == SUCC n.
Lemma SUCC_inj : forall n m, SUCC n == SUCC m -> n == m.
Lemma ZERO_typ_gen : forall X, ZERO \in sum UNIT X.
Lemma SUCC_typ_gen : forall x X, x \in X -> SUCC x \in sum UNIT X.
Lemma NATf_case : forall X (P:Prop) x,
(x == ZERO -> P) ->
(forall n, n \in X -> x == SUCC n -> P) ->
x \in NATf X -> P.
Section IterationNat.
Definition NATi := TI NATf.
Instance NATi_morph : morph1 NATi.
Qed.
Lemma NATfun_ext : forall x, ext_fun x (fun n => NATf (NATi n)).
Hint Resolve NATfun_ext.
Lemma NATi_case : forall (P:set->Prop) o n,
isOrd o ->
(forall x x', x \in NATi o -> x == x' -> P x -> P x') ->
P ZERO ->
(forall m o', lt o' o -> m \in NATi o' -> P (SUCC m)) ->
n \in NATi o -> P n.
Definition NATCASE_rel (fZ:set) (fS:set->set) (n:set) :=
fun y =>
(n == ZERO -> y == fZ) /\
(forall k, n == SUCC k -> y == fS k).
Lemma NATCASE_choice_pred :
forall o fZ fS n,
morph1 fS ->
isOrd o ->
n \in NATi o ->
uchoice_pred (NATCASE_rel fZ fS n).
Definition NATCASE (fZ:set) (fS:set->set) (n:set) :=
uchoice (NATCASE_rel fZ fS n).
Instance NATCASE_morph : Proper
(eq_set ==> (eq_set ==> eq_set) ==> eq_set ==> eq_set) NATCASE.
Qed.
Lemma NATCASE_def : forall o fZ fS n,
morph1 fS ->
isOrd o ->
n \in NATi o ->
NATCASE_rel fZ fS n (NATCASE fZ fS n).
Lemma NATCASE_ZERO : forall fZ fS,
morph1 fS ->
NATCASE fZ fS ZERO == fZ.
Lemma NATCASE_SUCC : forall o fZ fS n,
morph1 fS ->
isOrd o ->
n \in NATi o ->
NATCASE fZ fS (SUCC n) == fS n.
Lemma NATCASE_typ :
forall (P:set->set) o fZ fS,
morph1 P ->
morph1 fS ->
isOrd o ->
fZ \in P ZERO ->
(forall n, n \in NATi o -> fS n \in P (SUCC n)) ->
forall n,
n \in NATi (osucc o) ->
NATCASE fZ fS n \in P n.
Lemma NATi_fix :
forall (P:set->Prop) o,
isOrd o ->
(forall i, isOrd i -> i \incl o ->
(forall i' m, lt i' i -> m \in NATi i' -> P m) ->
forall n, n \in NATi i -> P n) ->
forall n, n \in NATi o -> P n.
End IterationNat.
Hint Resolve NATfun_ext.
Section NatFixpoint.
Definition NAT := NATi omega.
Lemma NAT_continuous : forall F,
ext_fun omega F ->
NATf (sup omega F) == sup omega (fun n => NATf (F n)).
Lemma NAT_eq : NAT == NATf NAT.
Lemma NATi_NAT : forall o,
isOrd o ->
NATi o \incl NAT.
Lemma ZERO_typ : ZERO \in NAT.
Lemma SUCC_typ : forall n, n \in NAT -> SUCC n \in NAT.
Lemma NAT_fix :
forall (P:set->Prop),
(forall o, isOrd o ->
(forall o' m, lt o' o -> m \in NATi o' -> P m) ->
forall n, n \in NATi o -> P n) ->
forall n, n \in NAT -> P n.
Lemma NAT_ind : forall (P:set->Prop),
(forall x x', x \in NAT -> x == x' -> P x -> P x') ->
P ZERO ->
(forall n, n \in NAT -> P n -> P (SUCC n)) ->
forall n, n \in NAT -> P n.
Fixpoint nat2NAT (n:nat) : set :=
match n with
| 0 => ZERO
| S k => SUCC (nat2NAT k)
end.
Lemma nat2NAT_reflect : forall x,
x \in NAT -> exists n, x == nat2NAT n.
End NatFixpoint.
Section NatUniverse.
Variable U : set.
Hypothesis has_cstr : forall X, X \in U -> sum UNIT X \in U.
Hypothesis has_empty : empty \in U.
Hypothesis has_limit : forall F,
ext_fun omega F ->
(forall n, n \in omega -> F n \in U) -> sup omega F \in U.
Lemma has_fin_limit : forall n F,
lt n omega ->
ext_fun n F ->
(forall m, lt m n -> F m \in U) -> sup n F \in U.
Lemma NATi_pre_typ : forall n, lt n omega -> NATi n \in U.
Lemma NAT_typ : NAT \in U.
End NatUniverse.
Definition ORDf X := sum UNIT (func NAT X).
Lemma sum_ext_ordf : forall A, ext_fun A ORDf.
Instance ORDf_mono : Proper (incl_set ==> incl_set) ORDf.
Qed.
Hint Resolve ORDf_mono.
Instance ORDf_morph : Proper (eq_set ==> eq_set) ORDf.
Qed.
Definition LIM f := inr f.
Lemma LIM_typ_gen : forall x X, x \in func NAT X -> LIM x \in sum UNIT (func NAT X).
Lemma ORDf_case : forall X (P:Prop) x,
(x == ZERO -> P) ->
(forall f, f \in func NAT X -> x == LIM f -> P) ->
x \in ORDf X -> P.
Section IterationOrd.
Definition ORDi := TI ORDf.
Instance ORDi_morph : morph1 ORDi.
Qed.
Lemma ORDfun_ext : forall x, ext_fun x (fun n => ORDf (ORDi n)).
Hint Resolve ORDfun_ext.
Lemma ORDi_case : forall (P:set->Prop) o n,
isOrd o ->
(forall x x', x \in ORDi o -> x == x' -> P x -> P x') ->
P ZERO ->
(forall f o', lt o' o -> f \in func NAT (ORDi o') -> P (LIM f)) ->
n \in ORDi o -> P n.
Lemma ORDi_fix :
forall (P:set->Prop) o,
isOrd o ->
(forall i, isOrd i -> i \incl o ->
(forall i' m, lt i' i -> m \in ORDi i' -> P m) ->
forall n, n \in ORDi i -> P n) ->
forall n, n \in ORDi o -> P n.
End IterationOrd.
Hint Resolve ORDfun_ext.
Section OrdFixpoint.
Hypothesis mu : set.
Hypothesis mu_strong : stronglyInaccessibleCard mu.
Hypothesis NAT_in_mu : lt_card NAT mu.
Let mu_ord : isOrd mu.
Qed.
Let mu_lim : forall x, lt x mu -> lt (osucc x) mu.
Qed.
Definition ORD := ORDi mu.
Lemma ORD_eq : ORD == ORDf ORD.
Lemma ORDi_ORD : forall o,
isOrd o ->
ORDi o \incl ORD.
Section OrdUniverse.
Variable U : set.
Hypothesis has_cstr : forall X, X \in U -> sum UNIT (func NAT X) \in U.
Hypothesis has_empty : empty \in U.
Hypothesis mu_clos : forall x F,
le x mu ->
ext_fun x F ->
(forall n, n \in x -> F n \in U) -> sup x F \in U.
Lemma ORDi_pre_typ : forall n, lt n mu -> ORDi n \in U.
Lemma ORD_typ : ORD \in U.
End OrdUniverse.
End OrdFixpoint.
End NatOrd_theory.
Hint Resolve NATf_mono Fmono_morph NATfun_ext.
Require Import ZF ZFsum ZFfix ZFnats ZFord ZFrelations.
Import IZF ZFrepl.
Lemma cst_is_ext : forall X o, ext_fun o (fun _ => X).
Hint Resolve cst_is_ext.
Lemma sum_is_ext : forall o F G,
ext_fun o F ->
ext_fun o G ->
ext_fun o (fun y => sum (F y) (G y)).
Hint Resolve sum_is_ext.
Lemma func_is_ext : forall x X F,
ext_fun x F ->
ext_fun x (fun x => func X (F x)).
Hint Resolve func_is_ext.
Lemma cst_cont : forall X o y, lt y o -> X == sup o (fun _ => X).
Lemma sum_cont : forall o F G,
ext_fun o F ->
ext_fun o G ->
sum (sup o F) (sup o G) == sup o (fun y => sum (F y) (G y)).
Require Import ZFord_equiv ZFcard.
Section ProductContinuity.
Hypothesis mu : set.
Hypothesis mu_strong : stronglyInaccessibleCard mu.
Let mu_ord : isOrd mu.
Qed.
Let mu_regular : forall x F,
lt_card x mu ->
ext_fun x F ->
(forall y, y \in x -> lt (F y) mu) -> lt (sup x F) mu.
Qed.
Lemma func_cont : forall X F,
lt_card X mu ->
increasing F ->
func X (sup mu F) == sup mu (fun x => func X (F x)).
End ProductContinuity.
Definition UNIT := succ zero.
Lemma unit_typ : zero \in UNIT.
Lemma unit_elim : forall p, p \in UNIT -> p == zero.
Definition BOOL := succ (succ zero).
Definition TRUE := zero.
Definition FALSE := succ zero.
Lemma true_typ : TRUE \in BOOL.
Lemma false_typ : FALSE \in BOOL.
Lemma bool_elim : forall b, b \in BOOL -> b == TRUE \/ b == FALSE.
Section NatOrd_theory.
Definition NATf X := sum UNIT X.
Lemma sum_ext_natf : forall A, ext_fun A NATf.
Instance NATf_mono : Proper (incl_set ==> incl_set) NATf.
Qed.
Hint Resolve NATf_mono Fmono_morph.
Instance NATf_morph : Proper (eq_set ==> eq_set) NATf.
Qed.
Definition ZERO := inl zero.
Definition SUCC x := inr x.
Lemma NATf_discr : forall n, ~ ZERO == SUCC n.
Lemma SUCC_inj : forall n m, SUCC n == SUCC m -> n == m.
Lemma ZERO_typ_gen : forall X, ZERO \in sum UNIT X.
Lemma SUCC_typ_gen : forall x X, x \in X -> SUCC x \in sum UNIT X.
Lemma NATf_case : forall X (P:Prop) x,
(x == ZERO -> P) ->
(forall n, n \in X -> x == SUCC n -> P) ->
x \in NATf X -> P.
Section IterationNat.
Definition NATi := TI NATf.
Instance NATi_morph : morph1 NATi.
Qed.
Lemma NATfun_ext : forall x, ext_fun x (fun n => NATf (NATi n)).
Hint Resolve NATfun_ext.
Lemma NATi_case : forall (P:set->Prop) o n,
isOrd o ->
(forall x x', x \in NATi o -> x == x' -> P x -> P x') ->
P ZERO ->
(forall m o', lt o' o -> m \in NATi o' -> P (SUCC m)) ->
n \in NATi o -> P n.
Definition NATCASE_rel (fZ:set) (fS:set->set) (n:set) :=
fun y =>
(n == ZERO -> y == fZ) /\
(forall k, n == SUCC k -> y == fS k).
Lemma NATCASE_choice_pred :
forall o fZ fS n,
morph1 fS ->
isOrd o ->
n \in NATi o ->
uchoice_pred (NATCASE_rel fZ fS n).
Definition NATCASE (fZ:set) (fS:set->set) (n:set) :=
uchoice (NATCASE_rel fZ fS n).
Instance NATCASE_morph : Proper
(eq_set ==> (eq_set ==> eq_set) ==> eq_set ==> eq_set) NATCASE.
Qed.
Lemma NATCASE_def : forall o fZ fS n,
morph1 fS ->
isOrd o ->
n \in NATi o ->
NATCASE_rel fZ fS n (NATCASE fZ fS n).
Lemma NATCASE_ZERO : forall fZ fS,
morph1 fS ->
NATCASE fZ fS ZERO == fZ.
Lemma NATCASE_SUCC : forall o fZ fS n,
morph1 fS ->
isOrd o ->
n \in NATi o ->
NATCASE fZ fS (SUCC n) == fS n.
Lemma NATCASE_typ :
forall (P:set->set) o fZ fS,
morph1 P ->
morph1 fS ->
isOrd o ->
fZ \in P ZERO ->
(forall n, n \in NATi o -> fS n \in P (SUCC n)) ->
forall n,
n \in NATi (osucc o) ->
NATCASE fZ fS n \in P n.
Lemma NATi_fix :
forall (P:set->Prop) o,
isOrd o ->
(forall i, isOrd i -> i \incl o ->
(forall i' m, lt i' i -> m \in NATi i' -> P m) ->
forall n, n \in NATi i -> P n) ->
forall n, n \in NATi o -> P n.
End IterationNat.
Hint Resolve NATfun_ext.
Section NatFixpoint.
Definition NAT := NATi omega.
Lemma NAT_continuous : forall F,
ext_fun omega F ->
NATf (sup omega F) == sup omega (fun n => NATf (F n)).
Lemma NAT_eq : NAT == NATf NAT.
Lemma NATi_NAT : forall o,
isOrd o ->
NATi o \incl NAT.
Lemma ZERO_typ : ZERO \in NAT.
Lemma SUCC_typ : forall n, n \in NAT -> SUCC n \in NAT.
Lemma NAT_fix :
forall (P:set->Prop),
(forall o, isOrd o ->
(forall o' m, lt o' o -> m \in NATi o' -> P m) ->
forall n, n \in NATi o -> P n) ->
forall n, n \in NAT -> P n.
Lemma NAT_ind : forall (P:set->Prop),
(forall x x', x \in NAT -> x == x' -> P x -> P x') ->
P ZERO ->
(forall n, n \in NAT -> P n -> P (SUCC n)) ->
forall n, n \in NAT -> P n.
Fixpoint nat2NAT (n:nat) : set :=
match n with
| 0 => ZERO
| S k => SUCC (nat2NAT k)
end.
Lemma nat2NAT_reflect : forall x,
x \in NAT -> exists n, x == nat2NAT n.
End NatFixpoint.
Section NatUniverse.
Variable U : set.
Hypothesis has_cstr : forall X, X \in U -> sum UNIT X \in U.
Hypothesis has_empty : empty \in U.
Hypothesis has_limit : forall F,
ext_fun omega F ->
(forall n, n \in omega -> F n \in U) -> sup omega F \in U.
Lemma has_fin_limit : forall n F,
lt n omega ->
ext_fun n F ->
(forall m, lt m n -> F m \in U) -> sup n F \in U.
Lemma NATi_pre_typ : forall n, lt n omega -> NATi n \in U.
Lemma NAT_typ : NAT \in U.
End NatUniverse.
Definition ORDf X := sum UNIT (func NAT X).
Lemma sum_ext_ordf : forall A, ext_fun A ORDf.
Instance ORDf_mono : Proper (incl_set ==> incl_set) ORDf.
Qed.
Hint Resolve ORDf_mono.
Instance ORDf_morph : Proper (eq_set ==> eq_set) ORDf.
Qed.
Definition LIM f := inr f.
Lemma LIM_typ_gen : forall x X, x \in func NAT X -> LIM x \in sum UNIT (func NAT X).
Lemma ORDf_case : forall X (P:Prop) x,
(x == ZERO -> P) ->
(forall f, f \in func NAT X -> x == LIM f -> P) ->
x \in ORDf X -> P.
Section IterationOrd.
Definition ORDi := TI ORDf.
Instance ORDi_morph : morph1 ORDi.
Qed.
Lemma ORDfun_ext : forall x, ext_fun x (fun n => ORDf (ORDi n)).
Hint Resolve ORDfun_ext.
Lemma ORDi_case : forall (P:set->Prop) o n,
isOrd o ->
(forall x x', x \in ORDi o -> x == x' -> P x -> P x') ->
P ZERO ->
(forall f o', lt o' o -> f \in func NAT (ORDi o') -> P (LIM f)) ->
n \in ORDi o -> P n.
Lemma ORDi_fix :
forall (P:set->Prop) o,
isOrd o ->
(forall i, isOrd i -> i \incl o ->
(forall i' m, lt i' i -> m \in ORDi i' -> P m) ->
forall n, n \in ORDi i -> P n) ->
forall n, n \in ORDi o -> P n.
End IterationOrd.
Hint Resolve ORDfun_ext.
Section OrdFixpoint.
Hypothesis mu : set.
Hypothesis mu_strong : stronglyInaccessibleCard mu.
Hypothesis NAT_in_mu : lt_card NAT mu.
Let mu_ord : isOrd mu.
Qed.
Let mu_lim : forall x, lt x mu -> lt (osucc x) mu.
Qed.
Definition ORD := ORDi mu.
Lemma ORD_eq : ORD == ORDf ORD.
Lemma ORDi_ORD : forall o,
isOrd o ->
ORDi o \incl ORD.
Section OrdUniverse.
Variable U : set.
Hypothesis has_cstr : forall X, X \in U -> sum UNIT (func NAT X) \in U.
Hypothesis has_empty : empty \in U.
Hypothesis mu_clos : forall x F,
le x mu ->
ext_fun x F ->
(forall n, n \in x -> F n \in U) -> sup x F \in U.
Lemma ORDi_pre_typ : forall n, lt n mu -> ORDi n \in U.
Lemma ORD_typ : ORD \in U.
End OrdUniverse.
End OrdFixpoint.
End NatOrd_theory.
Hint Resolve NATf_mono Fmono_morph NATfun_ext.