Library ZFlimit

Require Import ZF ZFpairs ZFnats ZFord.
Require ZFfix.
Section Limit.

Variable o : set.
Variable F : set -> set.
Hypothesis oord : isOrd o.
Hypothesis Fm : ext_fun o F.

Definition lim :=
  subset (sup o F) (fun z => exists2 o', o' ∈ o & ∀ w, o' ⊆ w -> w ∈ o -> z ∈ F w).

Lemma lim_def z :
  z ∈ lim <-> exists2 o', o' ∈ o &∀ w, o' ⊆ w -> w ∈ o -> z ∈ F w.

Lemma lim_cst o' :
  o' ∈ o ->
  (∀ w, o' ⊆ w -> w ∈ o -> F w == F o') ->
  lim == F o'.

End Limit.

Lemma lim_oucc o F :
  isOrd o ->
  ext_fun (osucc o) F ->
  lim (osucc o) F == F o.

Lemma lim_ext :
  ∀ o o', isOrd o -> o == o' -> ∀ f f', eq_fun o f f' -> lim o f == lim o' f'.

Instance lim_morph : Proper (eq_set==>(eq_set==>eq_set)==>eq_set) lim.


Qed.

Section LimitMono.

Variable F:set->set.
Variable o : set.
Hypothesis oord : isOrd o.
Hypothesis Fmono : increasing F.

Let os := fun y => isOrd_inv _ y oord.

Let Fext : ext_fun o F.
Qed.

Lemma lim_def_mono : lim o F == sup o F.

Lemma lim_mono z :
  z ∈ lim o F <-> exists2 o', o' ∈ o & z ∈ F o'.

End LimitMono.

Section LimitTI.

Variable F : set->set.
Hypothesis Fm : Proper (incl_set==>incl_set) F.

Lemma TIlim o :
  isOrd o ->
  TI F o == lim o (fun o' => F(TI F o')).

End LimitTI.

Section TRF.

Hypothesis F:(set->set->set)->set->set->set.
Hypothesis Fext : ∀ o o' f f' x x',
  isOrd o ->
  (∀ o' o'' x x', o' ∈ o -> o'==o'' -> x==x' -> f o' x == f' o'' x') ->
  o == o' ->
  x == x' ->
  F f o x == F f' o' x'.

Fixpoint TR_acc (o:set) (H:Acc in_set o) (H':isOrd o) (x:set) : set :=
  F (fun o' x' => ZFrepl.uchoice (fun y' => exists h:o' ∈ o, y' == TR_acc o' (Acc_inv H h) (isOrd_inv _ _ H' h) x')) o x.

Lemma TR_acc_morph o o' h h' oo oo' x x' :
  o == o' ->
  x == x' ->
  TR_acc o h oo x == TR_acc o' h' oo' x'.

Lemma isOrd_acc o : isOrd o -> Acc in_set o.

Definition TR o x := ZFrepl.uchoice (fun y => exists h:isOrd o, y == TR_acc o (isOrd_acc _ h) h x).

Lemma TR_acc_eqn o h h' x :
  TR_acc o h h' x == F TR o x.

Lemma TR_eqn o x :
  isOrd o ->
  TR o x == F TR o x.

Global Instance TR_morph : morph2 TR.

Qed.

End TRF.

Section TR_irrel.

Variable F : (set->set->set)->set->set->set.

Variable T : set -> set.
Variable Tcont : ∀ o z, isOrd o ->
  (z ∈ T o <-> exists2 o', o' ∈ o & z ∈ T (osucc o')).

Hypothesis Fext : ∀ o o' f f' x x',
  isOrd o ->
  (∀ o' o'' x x', o' ∈ o -> o'==o'' -> x==x' -> f o' x == f' o'' x') ->
  o == o' ->
  x == x' ->
  F f o x == F f' o' x'.

Hypothesis Firr : ∀ o o' f f' x x',
  morph2 f ->
  morph2 f' ->
  isOrd o ->
  isOrd o' ->
  (∀ o1 o1' x x',
   o1 ∈ o -> o1' ∈ o' -> o1 ⊆ o1' -> x ∈ T o1 -> x==x' ->
   f o1 x == f' o1' x') ->
  o ⊆ o' ->
  x ∈ T o ->
  x == x' ->
  F f o x == F f' o' x'.

Lemma TR_irrel : ∀ o o' x,
  isOrd o ->
  isOrd o' ->
  o' ⊆ o ->
  x ∈ T o' ->
  TR F o x == TR F o' x.

End TR_irrel.

Section TRirr.

Variable F : (set->set)->set->set.
Hypothesis Fm : Proper ((eq_set==>eq_set)==>eq_set==>eq_set) F.
Variable T : set -> set.
Variable Tcont : ∀ o z, isOrd o ->
  (z ∈ T o <-> exists2 o', o' ∈ o & z ∈ T (osucc o')).
Hypothesis Fext : ∀ o f f',
  isOrd o ->
  eq_fun (T o) f f' ->
  eq_fun (T (osucc o)) (F f) (F f').

Lemma Tmono o o': isOrd o -> isOrd o' -> o ⊆ o' -> T o ⊆ T o'.

Let G f o x := F (fun x => lim o (fun o' => f o' x)) x.
Definition TRF := TR G.

Let Gext : ∀ o o' f f' x x',
  isOrd o ->
  (∀ o' o'' x x', o' ∈ o -> o'==o'' -> x==x' -> f o' x == f' o'' x') ->
  o == o' ->
  x == x' ->
  G f o x == G f' o' x'.
Qed.

Let Girr : ∀ o o' f f' x x',
  morph2 f ->
  morph2 f' ->
  isOrd o ->
  isOrd o' ->
  (∀ o1 o1' x x',
   o1 ∈ o -> o1' ∈ o' -> o1 ⊆ o1' -> x ∈ T o1 -> x==x' ->
   f o1 x == f' o1' x') ->
  o ⊆ o' ->
  x ∈ T o ->
  x == x' ->
  G f o x == G f' o' x'.






Qed.

Instance TRF_morph : morph2 TRF.
Qed.

Lemma TRF_indep : ∀ o o' x,
  isOrd o ->
  o' ∈ o ->
  x ∈ T (osucc o') ->
  TRF o x == F (TRF o') x.

End TRirr.