Library e_recursion
initial import of the development
Lemma worder_ind M R (P: set -> Prop): wordering R M
-> (forall x, x <e M -> (forall y, y <e (iseg M R x) -> P y) -> P x)
-> forall x, x <e M -> P x.
Lemma trans_ind_b a (P: set -> Prop): ordinal a
-> (forall b, b <e a -> (forall c, c <e b -> P c) -> P b)
-> forall b, b <e a -> P b.
Lemma ordinal_wf (P: set -> Prop): ~(forall a, ordinal a -> P a)
-> exists a, ordinal a /\ ~ P a /\ forall b, b <e a -> P b.
Theorem trans_ind (P: set -> Prop):
(forall a, ordinal a -> (forall b, b <e a -> P b) -> P a)
-> forall a, ordinal a -> P a.
Lemma iseg_oisoeq M R x x': wordering R M -> x <e M -> x' <e M
-> oiso (iseg M R x) (iseg M R x') R R -> (iseg M R x) = (iseg M R x').
Lemma ordinal_ordiso a b: ordinal a -> ordinal b ->
oiso a b (elorder a) (elorder b) -> a = b.
Corollary ordiso_eq a b M R: ordiso M a R -> ordiso M b R -> a = b.
Corollary ordinal_iso M R: (exists a, ordiso M a R) -> (exists! a, ordiso M a R).
We first define the notion of a computation.
Definition compB t a B :=
function t (succ a) B /\ forall b, b <e (succ a) -> t[b] = G (t|b).
Definition comp t a :=
exists B, compB t a B.
Lemma comp_res x y t: ordinal x -> comp t x -> y <e x -> comp (t|(succ y)) y.
Lemma comp_eq t1 t2 x: ordinal x -> comp t1 x -> comp t2 x -> t1 = t2.
Lemma comp_unique t x: ordinal x -> comp t x -> exists! u, comp u x.
Lemma comp_subs t1 x1 t2 x2: ordinal x1 -> x2 <e x1 -> comp t1 x1 -> comp t2 x2 ->
t2 c= t1.
Lemma comp_linear t1 x1 t2 x2: ordinal x1 -> ordinal x2 -> comp t1 x1 -> comp t2 x2 ->
t1 c= t2 \/ t2 c= t1.
Lemma comp_res_eq x y t u: ordinal x -> y <e x -> comp t x -> comp u y ->
t|(succ y) = u.
Lemma comp_agree x y z t u i1 i2: ordinal x -> ordinal y -> comp t x -> comp u y ->
(z,i1) <e t -> (z,i2) <e u -> i1=i2.
Step 1: we define tao x, which will serve as the
unique computation of length x.
Definition t x := desc (fun t => comp t x).
Definition T x := replacement x t.
Definition TU x := union (T x).
Definition tao x := bunion (TU x) (singleton (x, G (TU x))).
Definition R1 x := replacement (TU x) pi2.
Definition R2 x := bunion (R1 x) (singleton (G (TU x))).
We begin with some simple statements.
Lemma T_el x b u: b <e x -> unique (fun t : set => comp t b) u -> u <e T x.
Lemma tao_T x t: t <e T x -> t c= tao x.
Lemma u_t x u: ordinal x -> comp u x -> u = t x.
Lemma TU_el t x y B a: (exists! t, comp t y) -> compB t y B ->
y <e x -> a <e succ y -> (a,t[a]) <e TU x.
Lemma R1_el t x y B a: (exists! t, comp t y) -> compB t y B ->
y <e x -> a <e succ y -> t[a] <e R1 x.
Lemma R1_subs t x y B: (exists! t, comp t y) ->
y <e x -> compB t y B -> compB t y (R1 x).
Lemma R2_subs t x y B: (exists! t : set, comp t y) ->
y <e x -> compB t y B -> compB t y (R2 x).
Now we prepare the inductive step,
meaning we assume all shorter computations to exist,
then we prove that TU is a function and tao a computation.
Lemma TU_rel x: (forall y, y <e x -> exists! t, comp t y) -> ordinal x ->
relation (TU x) x (R1 x).
Lemma TU_total x: (forall y, y <e x -> exists! t, comp t y) -> ordinal x ->
total (TU x) x (R1 x).
Lemma TU_functional x: (forall y, y <e x -> exists! t, comp t y) -> ordinal x ->
functional (TU x).
Lemma TU_fun1 x: (forall y, y <e x -> exists! t, comp t y) -> ordinal x ->
function (TU x) x (R1 x).
Lemma TU_fun2 x: (forall y, y <e x -> exists! t, comp t y) -> ordinal x ->
function (TU x) x (R2 x).
Lemma tao_fun x: (forall y, y <e x -> exists! t, comp t y) -> ordinal x ->
function (tao x) (succ x) (R2 x).
Lemma tao_x x: (forall y, y <e x -> exists! t, comp t y) -> ordinal x ->
(tao x) [x] = G (TU x).
Lemma tao_TU x: (forall y, y <e x -> exists! t, comp t y) -> ordinal x ->
(tao x)|x = TU x.
Lemma tao_compB_step x: (forall y, y <e x -> exists! t, comp t y) -> ordinal x ->
compB (tao x) x (R2 x).
Step 2: tao is a unique computation. We apply transfinite induction.
Lemma tao_compB x: ordinal x -> compB (tao x) x (R2 x).
Lemma tao_comp x: ordinal x -> comp (tao x) x.
Lemma tao_unique x sigma: ordinal x -> comp sigma x -> sigma = (tao x).
Lemma comp_exists x: ordinal x -> exists! t, comp t x.
Lemma tao_t x: ordinal x -> t x = tao x.
Lemma TU_fun x: ordinal x -> function (TU x) x (R1 x).
Lemma tao_app x: ordinal x -> (tao x) [x] = G (TU x).
Lemma tao_eq x y: ordinal x -> y <e x -> (tao x)|x [y] = (tao y) [y].
Lemma tao_res x: ordinal x -> function (tao x)|x x (R1 x).
Step 3: we define the recursive function F and prove it to satisfy
the Unbounded Transfinite Recursion Theorem.
Definition F x := tao x [x].
Lemma F_fun a: ordinal a -> function (lam F a) a (R1 a).
Lemma F_eq2 a: ordinal a -> (tao a)|a = (lam F a).
Theorem trans_rec: forall a, ordinal a -> F a = G (lam F a).
End TransRec.
Definition fset a' B := specification (power (product a' B)) (fun f => function f a' B).
Definition space a B := union (replacement a (fun a' => fset a' B)).
Section TransRecB.
Variable a: set.
Variable B: set.
Variable g: set.
Variable AO: ordinal a.
Variable GF: function g (space a B) B.
Definition G := app g.
Definition f := lam (F G) a.
Lemma B_tao_app1 b c: ordinal b -> c <e b -> function (tao G c) (succ c) B ->
(tao G b)[c] <e B.
Lemma B_tao_TU b: b <e a -> (forall c, c <e b -> function (tao G c) (succ c) B) ->
TU G b <e fset b B.
Lemma B_tao_app2 b: b <e a -> (forall c, c <e b -> function (tao G c) (succ c) B) ->
(tao G b)[b] <e B.
Lemma B_tao: forall b, b <e a -> function (tao G b) (succ b) B.
Lemma f_fun: function f a (R1 G a).
Lemma f_funB: function f a B.
Lemma f_rec: forall a', a' <e a -> f[a'] = g[f|a'].
Lemma f_unique f': function f' a B /\
(forall a', a' <e a -> f'[a'] = g[f'|a']) -> f = f'.
End TransRecB.
Theorem trans_rec_b a B g: ordinal a -> function g (space a B) B ->
exists! f, function f a B /\ forall a', a' <e a -> f[a'] = g[f|a'].