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.