Library ZFskol

Require Import basic.
Require Export ZFdef.

Module Skolem (Z : IZF_Ex_sig) <: IZF_sig.

Instance Zsetoid: Equivalence Z.eq_set.

Instance Zin_morph : Proper (Z.eq_set ==> Z.eq_set ==> iff) Z.in_set.

Definition set :=
  { f : Z.set -> Prop |
    (exists u, f u) /\
    (forall a a', f a -> f a' -> Z.eq_set a a') }.

Lemma set_intro : forall (f:Z.set->Prop) (P:set->Prop),
  (exists u, f u) ->
  (forall a a', f a -> f a' -> Z.eq_set a a') ->
  (forall Hex Huniq, P (exist _ f (conj Hex Huniq))) ->
  sig P.

Inductive in_set_ (x y:set) : Prop :=
 InSet
  (_:exists2 x', proj1_sig x x' &
     exists2 y', proj1_sig y y' & Z.in_set x' y').

Definition in_set := in_set_.

Lemma in_set_elim : forall x y, in_set x y <->
  exists2 x', proj1_sig x x' &
  exists2 y', proj1_sig y y' & Z.in_set x' y'.

Notation "x \in y" := (in_set x y) (at level 60).

Definition eq_set a b := forall x, x \in a <-> x \in b.

Notation "x == y" := (eq_set x y) (at level 70).

Lemma eq_set_ax : forall a b, a == b <-> (forall x, x \in a <-> x \in b).

Instance eq_setoid: Equivalence eq_set.

Lemma In_intro: forall x y: set,
  (forall x' y', proj1_sig x x' -> proj1_sig y y' -> Z.in_set x' y') ->
  x \in y.

Definition Z2set (x:Z.set) : set.
Defined.

Lemma Z2set_surj : forall x, exists y, x == Z2set y.

Lemma Eq_proj : forall (x:set) x', proj1_sig x x' -> x == Z2set x'.

Lemma inZ_in : forall a b, Z.in_set a b -> Z2set a \in Z2set b.

Lemma in_inZ : forall a b, Z2set a \in Z2set b -> Z.in_set a b.

Lemma eq_Zeq : forall x y, Z2set x == Z2set y -> Z.eq_set x y.

Lemma Zeq_eq : forall x y, Z.eq_set x y -> Z2set x == Z2set y.

Instance Z2set_morph : Proper (Z.eq_set ==> eq_set) Z2set.
Qed.

Lemma in_reg : forall a a' b, a == a' -> a \in b -> a' \in b.

Instance in_morph : Proper (eq_set ==> eq_set ==> iff) in_set.


Lemma empty_sig : { empty | forall x, ~ x \in empty }.

Definition empty := proj1_sig empty_sig.
Lemma empty_ax: forall x, ~ x \in empty.
Lemma pair_sig : forall a b,
  { pair | forall x, x \in pair <-> (x == a \/ x == b) }.

Definition pair a b := proj1_sig (pair_sig a b).
Lemma pair_ax: forall a b x, x \in pair a b <-> (x == a \/ x == b).
Lemma union_sig: forall a,
  { union | forall x, x \in union <-> (exists2 y, x \in y & y \in a) }.

Definition union a := proj1_sig (union_sig a).
Lemma union_ax: forall a x,
  x \in union a <-> (exists2 y, x \in y & y \in a).
Lemma power_sig: forall a,
  { power | forall x, x \in power <-> (forall y, y \in x -> y \in a) }.

Definition power a := proj1_sig (power_sig a).
Lemma power_ax:
  forall a x, x \in power a <-> (forall y, y \in x -> y \in a).
Definition funDom (R:set -> set -> Prop) x :=
  forall x' y y', R x y -> R x' y' -> x == x' -> y == y'.
Definition downR (R:set -> set -> Prop) x' y' :=
  exists2 x, x == Z2set x' /\ funDom R x & exists2 y, y == Z2set y' & R x y.

Lemma downR_morph : Proper
  ((eq_set ==> eq_set ==> iff) ==> Z.eq_set ==> Z.eq_set ==> iff) downR.

Lemma downR_fun : forall R x x' y y',
  downR R x y ->
  downR R x' y' ->
  Z.eq_set x x' ->
  Z.eq_set y y'.

Lemma repl0 : forall (a:set) (R:set->set->Prop), set.

Definition incl_set x y := forall z, z \in x -> z \in y.

Lemma repl0_mono :
  Proper (incl_set ==> (eq_set ==> eq_set ==> iff) ==> incl_set) repl0.

Lemma repl_sig :
  { repl |
    Proper (incl_set ==> (eq_set ==> eq_set ==> iff) ==> incl_set) repl /\
    forall a (R:set->set->Prop),
    (forall x x' y y', x \in a -> R x y -> R x' y' -> x == x' -> y == y') ->
    forall x, x \in repl a R <-> (exists2 y, y \in a & exists2 x', x == x' & R y x') }.

Definition repl := proj1_sig repl_sig.
Lemma repl_mono :
  Proper (incl_set ==> (eq_set ==> eq_set ==> iff) ==> incl_set) repl.
Lemma repl_ax:
    forall a (R:set->set->Prop),
    (forall x x' y y', x \in a -> R x y -> R x' y' -> x == x' -> y == y') ->
    forall x, x \in repl a R <-> (exists2 y, y \in a & exists2 x', x == x' & R y x').
Definition Nat x :=
  forall (P:set),
  empty \in P ->
  (forall x, x \in P -> union (pair x (pair x x)) \in P) ->
  x \in P.

Instance Nat_morph : Proper (eq_set ==> iff) Nat.
Qed.

Lemma Nat_S : forall x,
  Nat x -> Nat (union (pair x (pair x x))).

Definition infinite_sig :
  { infty | empty \in infty /\
      forall x, x \in infty -> union (pair x (pair x x)) \in infty }.


















Qed.
Definition infinite := proj1_sig infinite_sig.
Lemma infinity_ax1: empty \in infinite.
Lemma infinity_ax2: forall x,
  x \in infinite -> union (pair x (pair x x)) \in infinite.
Lemma regularity_ax: forall a a0, a0 \in a ->
  exists2 b, b \in a & ~(exists2 c, c \in a & c \in b).

End Skolem.