Require Export Omega Classical.
Global Set Implicit Arguments.
Global Unset Strict Implicit.
Global Unset Printing Implicit Defensive.

Ltac contra A :=
  match goal with
  |[ |- ?t] => destruct (classic t) as [A|A]; [exact A|exfalso]
  end.

(* Some definitions for relations *)

Definition functional {X Y} (R : X -> Y -> Prop) :=
  forall x y y', R x y -> R x y' -> y = y'.

Definition injective {X Y} (R : X -> Y -> Prop) :=
  forall x x' y, R x y -> R x' y -> x = x'.

Definition total {X Y} (R : X -> Y -> Prop) :=
  forall x, exists y, R x y.

Definition surjective {X Y} (R : X -> Y -> Prop) :=
  forall y, exists x, R x y.

(* Definition of ZF-structures and notation *)

Class SetStruct :=
  {
    set : Type;
    elem : set -> set -> Prop;
    
    eset : set;
    union : set -> set;
    power : set -> set;
    rep : (set -> set -> Prop) -> set -> set;
  }.

Coercion set : SetStruct >-> Sortclass.

Definition sub {M : SetStruct} (x y : M) :=
  forall z, elem z x -> elem z y.

Notation "x 'el' y" := (elem x y) (at level 70).
Notation "x 'nel' y" := (~ elem x y) (at level 70).

Notation "x '<<=' y" := (sub x y) (at level 70).
Notation "x << y" := (x <<= y /\ x <> y) (at level 70).

Notation "p '<=p' q" := (forall z, p z -> q z) (at level 70).
Notation "x '<=c' p" := (forall z, z el x -> p z) (at level 70).
Notation "p '<=s' x" := (forall z, p z -> z el x) (at level 70).

Notation "0" := eset.

Notation inhab x := (exists y, y el x).
Notation upbnd x u := (forall z, z el x -> z <<= u).
Notation gel x u := (u el x /\ upbnd x u).

Definition agree {M : SetStruct} p x :=
  forall z, z el x <-> p z.

Definition small {M : SetStruct} p :=
  exists x, agree p x.

Definition trans {M : SetStruct} x :=
  forall y, y el x -> y <<= x.

Definition swelled {M : SetStruct} x :=
  forall y z, y el x -> z <<= y -> z el x.

Inductive WF {M : SetStruct} : set -> Prop :=
| WFI x : x <=c WF -> WF x.

(* ZF is the usual set of axioms (without infinity) *)

Class ZF (M : SetStruct) :=
  {
    Ext : forall x y, x <<= y -> y <<= x -> x = y;
    Eset : forall z, z nel 0;
    Union : forall x z, z el union x <-> exists y, y el x /\ z el y;
    Power : forall x z, z el power x <-> z <<= x;
    Rep : forall R, functional R -> forall x z, z el rep R x <-> exists y, y el x /\ R y z;
    AxWF : forall x, WF x;
  }.

Arguments AxWF {_} {_} _.
Existing Class ZF.