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.