Library ZFnats
Require Export ZF.
Import IZF.
Definition zero := empty.
Definition succ n := union2 n (singl n).
Instance succ_morph : morph1 succ.
Definition pred := union.
Instance pred_morph : morph1 pred.
Qed.
Lemma discr : forall k, ~ succ k == zero.
Definition lt := in_set.
Definition le m n := lt m (succ n).
Instance lt_morph : Proper (eq_set ==> eq_set ==> iff) lt.
Qed.
Instance le_morph : Proper (eq_set ==> eq_set ==> iff) le.
Lemma le_case : forall m n, le m n -> m == n \/ lt m n.
Lemma succ_intro1 : forall x n, x == n -> lt x (succ n).
Lemma succ_intro2 : forall x n, lt x n -> lt x (succ n).
Lemma lt_is_le : forall x y, lt x y -> le x y.
Lemma le_refl : forall n, le n n.
Hint Resolve lt_is_le le_refl.
Definition is_nat n : Prop :=
forall nat:set,
zero \in nat ->
(forall k, k \in nat -> succ k \in nat) ->
n \in nat.
Lemma is_nat_zero : is_nat zero.
Lemma is_nat_succ : forall n, is_nat n -> is_nat (succ n).
Definition N := subset infinite is_nat.
Lemma zero_typ: zero \in N.
Lemma succ_typ: forall n, n \in N -> succ n \in N.
Lemma N_ind : forall (P: set->Prop),
(forall n n', n \in N -> n == n' -> P n -> P n') ->
P zero ->
(forall n, n \in N -> P n -> P (succ n)) ->
forall n, n \in N -> P n.
Lemma lt_trans : forall m n p, p \in N -> lt m n -> lt n p -> lt m p.
Lemma pred_succ_eq : forall n, n \in N -> pred (succ n) == n.
Lemma pred_typ : forall n, n \in N -> pred n \in N.
Lemma succ_inj : forall m n, m \in N -> n \in N -> succ m == succ n -> m == n.
Definition max := union2.
Instance max_morph : morph2 max.
Qed.
Lemma lt_0_succ : forall n, n \in N -> lt zero (succ n).
Lemma lt_mono : forall m n, m \in N -> n \in N ->
lt m n -> lt (succ m) (succ n).
Lemma le_total : forall m, m \in N -> forall n, n \in N ->
lt m n \/ m == n \/ lt n m.
Lemma max_sym : forall m n, max m n == max n m.
Lemma max_eq : forall m n, m == n -> max m n == m.
Lemma max_lt : forall m n, n \in N -> lt m n -> max m n == n.
Lemma max_typ : forall m n, m \in N -> n \in N -> max m n \in N.
Fixpoint nat2set (n:nat) : set :=
match n with
| 0 => zero
| S k => succ (nat2set k)
end.
Lemma nat2set_typ : forall n, nat2set n \in N.
Lemma nat2set_inj : forall n m, nat2set n == nat2set m -> n = m.
Lemma nat2set_reflect : forall x, x \in N -> exists n, x == nat2set n.