Library ZFfix
Section IterMonotone.
Variable F : set -> set.
Variable Fmono : Proper (incl_set ==> incl_set) F.
Let Fm := Fmono_morph _ Fmono.
Lemma TI_mono : increasing (TI F).
Lemma TI_incl : ∀ o, isOrd o ->
∀ o', o' < o ->
TI F o' ⊆ TI F o.
Lemma TI_mono_succ : ∀ o,
isOrd o ->
TI F (osucc o) == F (TI F o).
Lemma TI_mono_eq : ∀ o,
isOrd o ->
TI F o == sup o (fun o' => TI F (osucc o')).
Lemma TI_pre_fix : ∀ fx o,
isOrd o ->
F fx ⊆ fx ->
TI F o ⊆ fx.
Variable F : set -> set.
Variable Fmono : Proper (incl_set ==> incl_set) F.
Let Fm := Fmono_morph _ Fmono.
Lemma TI_mono : increasing (TI F).
Lemma TI_incl : ∀ o, isOrd o ->
∀ o', o' < o ->
TI F o' ⊆ TI F o.
Lemma TI_mono_succ : ∀ o,
isOrd o ->
TI F (osucc o) == F (TI F o).
Lemma TI_mono_eq : ∀ o,
isOrd o ->
TI F o == sup o (fun o' => TI F (osucc o')).
Lemma TI_pre_fix : ∀ fx o,
isOrd o ->
F fx ⊆ fx ->
TI F o ⊆ fx.
The union of all stages. We will show it is a fixpoint.
Definition Ffix := subset A (fun a => exists2 o, isOrd o & a ∈ TI F o).
Lemma Ffix_inA : Ffix ⊆ A.
Lemma TI_Ffix : ∀ o, isOrd o -> TI F o ⊆ Ffix.
Lemma Ffix_def : ∀ a, a ∈ Ffix <-> exists2 o, isOrd o & a ∈ TI F o.
Subterms of a
Definition fsub a :=
subset Ffix (fun b => ∀ X, X ⊆ Ffix -> a ∈ F X -> b ∈ X).
Instance fsub_morph : morph1 fsub.
Qed.
Lemma fsub_elim : ∀ x y o,
isOrd o ->
y ∈ TI F o ->
x ∈ fsub y ->
exists2 o', lt o' o & x ∈ TI F o'.
Lemma Ffix_fsub_inv : ∀ x y,
x ∈ Ffix ->
y ∈ fsub x ->
y ∈ Ffix.
subset Ffix (fun b => ∀ X, X ⊆ Ffix -> a ∈ F X -> b ∈ X).
Instance fsub_morph : morph1 fsub.
Qed.
Lemma fsub_elim : ∀ x y o,
isOrd o ->
y ∈ TI F o ->
x ∈ fsub y ->
exists2 o', lt o' o & x ∈ TI F o'.
Lemma Ffix_fsub_inv : ∀ x y,
x ∈ Ffix ->
y ∈ fsub x ->
y ∈ Ffix.
Functions defined by recursion on subterms
Section Iter.
Variable G : (set -> set) -> set -> set.
Hypothesis Gm : ∀ x x' g g',
x ∈ Ffix ->
eq_fun (fsub x) g g' ->
x == x' -> G g x == G g' x'.
Definition Ffix_rel a y :=
∀ R:set->set->Prop,
Proper (eq_set ==> eq_set ==> iff) R ->
(∀ x g,
ext_fun (fsub x) g ->
(∀ y, y ∈ fsub x -> R y (g y)) ->
R x (G g x)) ->
R a y.
Instance Ffix_rel_morph :
Proper (eq_set ==> eq_set ==> iff) Ffix_rel.
Qed.
Lemma Ffix_rel_intro : ∀ x g,
ext_fun (fsub x) g ->
(∀ y, y ∈ fsub x -> Ffix_rel y (g y)) ->
Ffix_rel x (G g x).
Lemma Ffix_rel_inv : ∀ x o,
x ∈ Ffix ->
Ffix_rel x o ->
exists2 g,
ext_fun (fsub x) g /\
(∀ y, y ∈ fsub x -> Ffix_rel y (g y)) &
o == G g x.
Lemma Ffix_rel_fun :
∀ x y, Ffix_rel x y ->
∀ y', Ffix_rel x y' -> x ∈ Ffix -> y == y'.
Require Import ZFrepl.
Lemma Ffix_rel_def : ∀ o a, isOrd o -> a ∈ TI F o -> exists y, Ffix_rel a y.
Lemma Ffix_rel_choice_pred : ∀ o a, isOrd o -> a ∈ TI F o ->
uchoice_pred (fun o => Ffix_rel a o).
Variable G : (set -> set) -> set -> set.
Hypothesis Gm : ∀ x x' g g',
x ∈ Ffix ->
eq_fun (fsub x) g g' ->
x == x' -> G g x == G g' x'.
Definition Ffix_rel a y :=
∀ R:set->set->Prop,
Proper (eq_set ==> eq_set ==> iff) R ->
(∀ x g,
ext_fun (fsub x) g ->
(∀ y, y ∈ fsub x -> R y (g y)) ->
R x (G g x)) ->
R a y.
Instance Ffix_rel_morph :
Proper (eq_set ==> eq_set ==> iff) Ffix_rel.
Qed.
Lemma Ffix_rel_intro : ∀ x g,
ext_fun (fsub x) g ->
(∀ y, y ∈ fsub x -> Ffix_rel y (g y)) ->
Ffix_rel x (G g x).
Lemma Ffix_rel_inv : ∀ x o,
x ∈ Ffix ->
Ffix_rel x o ->
exists2 g,
ext_fun (fsub x) g /\
(∀ y, y ∈ fsub x -> Ffix_rel y (g y)) &
o == G g x.
Lemma Ffix_rel_fun :
∀ x y, Ffix_rel x y ->
∀ y', Ffix_rel x y' -> x ∈ Ffix -> y == y'.
Require Import ZFrepl.
Lemma Ffix_rel_def : ∀ o a, isOrd o -> a ∈ TI F o -> exists y, Ffix_rel a y.
Lemma Ffix_rel_choice_pred : ∀ o a, isOrd o -> a ∈ TI F o ->
uchoice_pred (fun o => Ffix_rel a o).
The recursion operator
Definition Fix_rec a := uchoice (fun o => Ffix_rel a o).
Lemma Fr_eqn : ∀ a o,
isOrd o ->
a ∈ TI F o ->
Fix_rec a == G Fix_rec a.
Lemma Fix_rec_typ U2 a :
(∀ x g, ext_fun (fsub x) g -> x ∈ Ffix -> (∀ y, y ∈ fsub x -> g y ∈ U2) -> G g x ∈ U2) ->
a ∈ Ffix ->
Fix_rec a ∈ U2.
End Iter.
Definition F_a g x := osup (fsub x) (fun a => osucc (g a)).
Lemma F_a_morph : ∀ x x' g g',
eq_fun (fsub x) g g' ->
x == x' -> F_a g x == F_a g' x'.
Hint Resolve F_a_morph.
Lemma Fe1 : ∀ X, ext_fun X (fun b => osucc (Fix_rec F_a b)).
Hint Resolve Fe1.
Lemma F_a_ord : ∀ a, a ∈ Ffix -> isOrd (Fix_rec F_a a).
Hint Resolve F_a_ord.
Lemma Fr_eqn : ∀ a o,
isOrd o ->
a ∈ TI F o ->
Fix_rec a == G Fix_rec a.
Lemma Fix_rec_typ U2 a :
(∀ x g, ext_fun (fsub x) g -> x ∈ Ffix -> (∀ y, y ∈ fsub x -> g y ∈ U2) -> G g x ∈ U2) ->
a ∈ Ffix ->
Fix_rec a ∈ U2.
End Iter.
Definition F_a g x := osup (fsub x) (fun a => osucc (g a)).
Lemma F_a_morph : ∀ x x' g g',
eq_fun (fsub x) g g' ->
x == x' -> F_a g x == F_a g' x'.
Hint Resolve F_a_morph.
Lemma Fe1 : ∀ X, ext_fun X (fun b => osucc (Fix_rec F_a b)).
Hint Resolve Fe1.
Lemma F_a_ord : ∀ a, a ∈ Ffix -> isOrd (Fix_rec F_a a).
Hint Resolve F_a_ord.
We need stability to prove that Ffix is a fixpoint
Hypothesis Fstab : ∀ X,
X ⊆ power A ->
inter (replf X F) ⊆ F (inter X).
Lemma F_intro : ∀ w,
isOrd w ->
∀ a, a ∈ TI F w ->
a ∈ F (fsub a).
Lemma F_a_tot : ∀ a,
a ∈ Ffix ->
a ∈ TI F (osucc (Fix_rec F_a a)).
X ⊆ power A ->
inter (replf X F) ⊆ F (inter X).
Lemma F_intro : ∀ w,
isOrd w ->
∀ a, a ∈ TI F w ->
a ∈ F (fsub a).
Lemma F_a_tot : ∀ a,
a ∈ Ffix ->
a ∈ TI F (osucc (Fix_rec F_a a)).
The closure ordinal
Definition Ffix_ord :=
osup Ffix (fun a => osucc (Fix_rec F_a a)).
Lemma Ffix_o_o : isOrd Ffix_ord.
Hint Resolve Ffix_o_o.
Lemma Ffix_post : ∀ a,
a ∈ Ffix ->
a ∈ TI F Ffix_ord.
Lemma Ffix_closure : Ffix == TI F Ffix_ord.
osup Ffix (fun a => osucc (Fix_rec F_a a)).
Lemma Ffix_o_o : isOrd Ffix_ord.
Hint Resolve Ffix_o_o.
Lemma Ffix_post : ∀ a,
a ∈ Ffix ->
a ∈ TI F Ffix_ord.
Lemma Ffix_closure : Ffix == TI F Ffix_ord.
We prove it is a fixpoint
Lemma Ffix_eqn : Ffix == F Ffix.
End BoundedOperator.
Section BoundIndep.
Variable A : set.
Hypothesis Ftyp : ∀ X, X ⊆ A -> F X ⊆ A.
Variable A' : set.
Hypothesis Ftyp' : ∀ X, X ⊆ A' -> F X ⊆ A'.
Lemma Ffix_indep : Ffix A == Ffix A'.
Lemma Ffix_ord_indep :
Ffix_ord A == Ffix_ord A'.
End BoundIndep.
End IterMonotone.
End BoundedOperator.
Section BoundIndep.
Variable A : set.
Hypothesis Ftyp : ∀ X, X ⊆ A -> F X ⊆ A.
Variable A' : set.
Hypothesis Ftyp' : ∀ X, X ⊆ A' -> F X ⊆ A'.
Lemma Ffix_indep : Ffix A == Ffix A'.
Lemma Ffix_ord_indep :
Ffix_ord A == Ffix_ord A'.
End BoundIndep.
End IterMonotone.
Section KnasterTarski.
Variable A : set.
Variable F : set -> set.
Hypothesis Fmono : Proper (incl_set==>incl_set) F.
Hypothesis Ftyp : ∀ x, x ⊆ A -> F x ⊆ A.
Definition is_lfp x :=
F x == x /\ ∀ y, F y ⊆ y -> x ⊆ y.
Definition pre_fix x := x ⊆ F x.
Definition post_fix x := F x ⊆ x.
Lemma post_fix_A : post_fix A.
Definition M' := subset (power A) post_fix.
Lemma member_A : A ∈ M'.
Lemma post_fix1 : ∀ x, x ∈ M' -> F x ⊆ x.
Definition FIX := inter M'.
Lemma lfp_typ : FIX ⊆ A.
Lemma lower_bound : ∀ x, x ∈ M' -> FIX ⊆ x.
Lemma post_fix2 : ∀ x, x ∈ M' -> F FIX ⊆ F x.
Lemma post_fix_lfp : post_fix FIX.
Lemma incl_f_lfp : F FIX ∈ M'.
Lemma FIX_eqn : F FIX == FIX.
Lemma knaster_tarski : is_lfp FIX.
Lemma TI_FIX : ∀ o, isOrd o -> TI F o ⊆ FIX.
End KnasterTarski.