Theory ZF_Base

(*  Title:      ZF/ZF_Base.thy
    Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
    Copyright   1993  University of Cambridge
*)

section Base of Zermelo-Fraenkel Set Theory

theory ZF_Base
imports FOL
begin

subsection Signature

declare [[eta_contract = false]]

typedecl i
instance i :: "term" ..

axiomatization mem :: "[i, i]  o"  (infixl  50)  ― ‹membership relation
  and zero :: "i"  (0)  ― ‹the empty set
  and Pow :: "i  i"  ― ‹power sets
  and Inf :: "i"  ― ‹infinite set
  and Union :: "i  i"  (_ [90] 90)
  and PrimReplace :: "[i, [i, i]  o]  i"

abbreviation not_mem :: "[i, i]  o"  (infixl  50)  ― ‹negated membership relation
  where "x  y  ¬ (x  y)"


subsection Bounded Quantifiers

definition Ball :: "[i, i  o]  o"
  where "Ball(A, P)  x. xA  P(x)"

definition Bex :: "[i, i  o]  o"
  where "Bex(A, P)  x. xA  P(x)"

syntax
  "_Ball" :: "[pttrn, i, o]  o"  ((3__./ _) 10)
  "_Bex" :: "[pttrn, i, o]  o"  ((3__./ _) 10)
translations
  "xA. P"  "CONST Ball(A, λx. P)"
  "xA. P"  "CONST Bex(A, λx. P)"


subsection Variations on Replacement

(* Derived form of replacement, restricting P to its functional part.
   The resulting set (for functional P) is the same as with
   PrimReplace, but the rules are simpler. *)
definition Replace :: "[i, [i, i]  o]  i"
  where "Replace(A,P)  PrimReplace(A, λx y. (∃!z. P(x,z))  P(x,y))"

syntax
  "_Replace"  :: "[pttrn, pttrn, i, o]  i"  ((1{_ ./ _  _, _}))
translations
  "{y. xA, Q}"  "CONST Replace(A, λx y. Q)"


(* Functional form of replacement -- analgous to ML's map functional *)

definition RepFun :: "[i, i  i]  i"
  where "RepFun(A,f)  {y . xA, y=f(x)}"

syntax
  "_RepFun" :: "[i, pttrn, i]  i"  ((1{_ ./ _  _}) [51,0,51])
translations
  "{b. xA}"  "CONST RepFun(A, λx. b)"


(* Separation and Pairing can be derived from the Replacement
   and Powerset Axioms using the following definitions. *)
definition Collect :: "[i, i  o]  i"
  where "Collect(A,P)  {y . xA, x=y  P(x)}"

syntax
  "_Collect" :: "[pttrn, i, o]  i"  ((1{_  _ ./ _}))
translations
  "{xA. P}"  "CONST Collect(A, λx. P)"


subsection General union and intersection

definition Inter :: "i  i"  (_ [90] 90)
  where "(A)  { x(A) . yA. xy}"

syntax
  "_UNION" :: "[pttrn, i, i]  i"  ((3__./ _) 10)
  "_INTER" :: "[pttrn, i, i]  i"  ((3__./ _) 10)
translations
  "xA. B" == "CONST Union({B. xA})"
  "xA. B" == "CONST Inter({B. xA})"


subsection Finite sets and binary operations

(*Unordered pairs (Upair) express binary union/intersection and cons;
  set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)

definition Upair :: "[i, i]  i"
  where "Upair(a,b)  {y. xPow(Pow(0)), (x=0  y=a) | (x=Pow(0)  y=b)}"

definition Subset :: "[i, i]  o"  (infixl  50)  ― ‹subset relation
  where subset_def: "A  B  xA. xB"

definition Diff :: "[i, i]  i"  (infixl - 65)  ― ‹set difference
  where "A - B  { xA . ¬(xB) }"

definition Un :: "[i, i]  i"  (infixl  65)  ― ‹binary union
  where "A  B  (Upair(A,B))"

definition Int :: "[i, i]  i"  (infixl  70)  ― ‹binary intersection
  where "A  B  (Upair(A,B))"

definition cons :: "[i, i]  i"
  where "cons(a,A)  Upair(a,a)  A"

definition succ :: "i  i"
  where "succ(i)  cons(i, i)"

nonterminal "is"
syntax
  "" :: "i  is"  (_)
  "_Enum" :: "[i, is]  is"  (_,/ _)
  "_Finset" :: "is  i"  ({(_)})
translations
  "{x, xs}" == "CONST cons(x, {xs})"
  "{x}" == "CONST cons(x, 0)"


subsection Axioms

(* ZF axioms -- see Suppes p.238
   Axioms for Union, Pow and Replace state existence only,
   uniqueness is derivable using extensionality. *)

axiomatization
where
  extension:     "A = B  A  B  B  A" and
  Union_iff:     "A  (C)  (BC. AB)" and
  Pow_iff:       "A  Pow(B)  A  B" and

  (*We may name this set, though it is not uniquely defined.*)
  infinity:      "0  Inf  (yInf. succ(y)  Inf)" and

  (*This formulation facilitates case analysis on A.*)
  foundation:    "A = 0  (xA. yx. yA)" and

  (*Schema axiom since predicate P is a higher-order variable*)
  replacement:   "(xA. y z. P(x,y)  P(x,z)  y = z) 
                         b  PrimReplace(A,P)  (xA. P(x,b))"


subsection Definite descriptions -- via Replace over the set "1"

definition The :: "(i  o)  i"  (binder THE  10)
  where the_def: "The(P)     ({y . x  {0}, P(y)})"

definition If :: "[o, i, i]  i"  ((if (_)/ then (_)/ else (_)) [10] 10)
  where if_def: "if P then a else b  THE z. P  z=a | ¬P  z=b"

abbreviation (input)
  old_if :: "[o, i, i]  i"  (if '(_,_,_'))
  where "if(P,a,b)  If(P,a,b)"


subsection Ordered Pairing

(* this "symmetric" definition works better than {{a}, {a,b}} *)
definition Pair :: "[i, i]  i"
  where "Pair(a,b)  {{a,a}, {a,b}}"

definition fst :: "i  i"
  where "fst(p)  THE a. b. p = Pair(a, b)"

definition snd :: "i  i"
  where "snd(p)  THE b. a. p = Pair(a, b)"

definition split :: "[[i, i]  'a, i]  'a::{}"  ― ‹for pattern-matching
  where "split(c)  λp. c(fst(p), snd(p))"

(* Patterns -- extends pre-defined type "pttrn" used in abstractions *)
nonterminal patterns
syntax
  "_pattern"  :: "patterns  pttrn"         (_)
  ""          :: "pttrn  patterns"         (_)
  "_patterns" :: "[pttrn, patterns]  patterns"  (_,/_)
  "_Tuple"    :: "[i, is]  i"              ((_,/ _))
translations
  "x, y, z"   == "x, y, z"
  "x, y"      == "CONST Pair(x, y)"
  "λx,y,zs.b" == "CONST split(λx y,zs.b)"
  "λx,y.b"    == "CONST split(λx y. b)"

definition Sigma :: "[i, i  i]  i"
  where "Sigma(A,B)  xA. yB(x). {x,y}"

abbreviation cart_prod :: "[i, i]  i"  (infixr × 80)  ― ‹Cartesian product
  where "A × B  Sigma(A, λ_. B)"


subsection Relations and Functions

(*converse of relation r, inverse of function*)
definition converse :: "i  i"
  where "converse(r)  {z. wr, x y. w=x,y  z=y,x}"

definition domain :: "i  i"
  where "domain(r)  {x. wr, y. w=x,y}"

definition range :: "i  i"
  where "range(r)  domain(converse(r))"

definition field :: "i  i"
  where "field(r)  domain(r)  range(r)"

definition relation :: "i  o"  ― ‹recognizes sets of pairs
  where "relation(r)  zr. x y. z = x,y"

definition "function" :: "i  o"  ― ‹recognizes functions; can have non-pairs
  where "function(r)  x y. x,y  r  (y'. x,y'  r  y = y')"

definition Image :: "[i, i]  i"  (infixl `` 90)  ― ‹image
  where image_def: "r `` A   {y  range(r). xA. x,y  r}"

definition vimage :: "[i, i]  i"  (infixl -`` 90)  ― ‹inverse image
  where vimage_def: "r -`` A  converse(r)``A"

(* Restrict the relation r to the domain A *)
definition restrict :: "[i, i]  i"
  where "restrict(r,A)  {z  r. xA. y. z = x,y}"


(* Abstraction, application and Cartesian product of a family of sets *)

definition Lambda :: "[i, i  i]  i"
  where lam_def: "Lambda(A,b)  {x,b(x). xA}"

definition "apply" :: "[i, i]  i"  (infixl ` 90)  ― ‹function application
  where "f`a  (f``{a})"

definition Pi :: "[i, i  i]  i"
  where "Pi(A,B)  {fPow(Sigma(A,B)). Adomain(f)  function(f)}"

abbreviation function_space :: "[i, i]  i"  (infixr  60)  ― ‹function space
  where "A  B  Pi(A, λ_. B)"


(* binder syntax *)

syntax
  "_PROD"     :: "[pttrn, i, i]  i"        ((3__./ _) 10)
  "_SUM"      :: "[pttrn, i, i]  i"        ((3__./ _) 10)
  "_lam"      :: "[pttrn, i, i]  i"        ((3λ__./ _) 10)
translations
  "xA. B"   == "CONST Pi(A, λx. B)"
  "xA. B"   == "CONST Sigma(A, λx. B)"
  "λxA. f"    == "CONST Lambda(A, λx. f)"


subsection ASCII syntax

notation (ASCII)
  cart_prod       (infixr * 80) and
  Int             (infixl Int 70) and
  Un              (infixl Un 65) and
  function_space  (infixr -> 60) and
  Subset          (infixl <= 50) and
  mem             (infixl : 50) and
  not_mem         (infixl ¬: 50)

syntax (ASCII)
  "_Ball"     :: "[pttrn, i, o]  o"        ((3ALL _:_./ _) 10)
  "_Bex"      :: "[pttrn, i, o]  o"        ((3EX _:_./ _) 10)
  "_Collect"  :: "[pttrn, i, o]  i"        ((1{_: _ ./ _}))
  "_Replace"  :: "[pttrn, pttrn, i, o]  i" ((1{_ ./ _: _, _}))
  "_RepFun"   :: "[i, pttrn, i]  i"        ((1{_ ./ _: _}) [51,0,51])
  "_UNION"    :: "[pttrn, i, i]  i"        ((3UN _:_./ _) 10)
  "_INTER"    :: "[pttrn, i, i]  i"        ((3INT _:_./ _) 10)
  "_PROD"     :: "[pttrn, i, i]  i"        ((3PROD _:_./ _) 10)
  "_SUM"      :: "[pttrn, i, i]  i"        ((3SUM _:_./ _) 10)
  "_lam"      :: "[pttrn, i, i]  i"        ((3lam _:_./ _) 10)
  "_Tuple"    :: "[i, is]  i"              (<(_,/ _)>)
  "_pattern"  :: "patterns  pttrn"         (<_>)


subsection Substitution

(*Useful examples:  singletonI RS subst_elem,  subst_elem RSN (2,IntI) *)
lemma subst_elem: "bA;  a=b  aA"
by (erule ssubst, assumption)


subsectionBounded universal quantifier

lemma ballI [intro!]: "x. xA  P(x)  xA. P(x)"
by (simp add: Ball_def)

lemmas strip = impI allI ballI

lemma bspec [dest?]: "xA. P(x);  x: A  P(x)"
by (simp add: Ball_def)

(*Instantiates x first: better for automatic theorem proving?*)
lemma rev_ballE [elim]:
    "xA. P(x);  xA  Q;  P(x)  Q  Q"
by (simp add: Ball_def, blast)

lemma ballE: "xA. P(x);  P(x)  Q;  xA  Q  Q"
by blast

(*Used in the datatype package*)
lemma rev_bspec: "x: A;  xA. P(x)  P(x)"
by (simp add: Ball_def)

(*Trival rewrite rule;   @{term"(∀x∈A.P)<->P"} holds only if A is nonempty!*)
lemma ball_triv [simp]: "(xA. P) <-> ((x. xA)  P)"
by (simp add: Ball_def)

(*Congruence rule for rewriting*)
lemma ball_cong [cong]:
    "A=A';  x. xA'  P(x) <-> P'(x)  (xA. P(x)) <-> (xA'. P'(x))"
by (simp add: Ball_def)

lemma atomize_ball:
    "(x. x  A  P(x))  Trueprop (xA. P(x))"
  by (simp only: Ball_def atomize_all atomize_imp)

lemmas [symmetric, rulify] = atomize_ball
  and [symmetric, defn] = atomize_ball


subsectionBounded existential quantifier

lemma bexI [intro]: "P(x);  x: A  xA. P(x)"
by (simp add: Bex_def, blast)

(*The best argument order when there is only one @{term"x∈A"}*)
lemma rev_bexI: "xA;  P(x)  xA. P(x)"
by blast

(*Not of the general form for such rules. The existential quanitifer becomes universal. *)
lemma bexCI: "xA. ¬P(x)  P(a);  a: A  xA. P(x)"
by blast

lemma bexE [elim!]: "xA. P(x);  x. xA; P(x)  Q  Q"
by (simp add: Bex_def, blast)

(*We do not even have @{term"(∃x∈A. True) <-> True"} unless @{term"A" is nonempty⋀*)
lemma bex_triv [simp]: "(xA. P) <-> ((x. xA)  P)"
by (simp add: Bex_def)

lemma bex_cong [cong]:
    "A=A';  x. xA'  P(x) <-> P'(x)
      (xA. P(x)) <-> (xA'. P'(x))"
by (simp add: Bex_def cong: conj_cong)



subsectionRules for subsets

lemma subsetI [intro!]:
    "(x. xA  xB)  A  B"
by (simp add: subset_def)

(*Rule in Modus Ponens style [was called subsetE] *)
lemma subsetD [elim]: "A  B;  cA  cB"
  unfolding subset_def
apply (erule bspec, assumption)
done

(*Classical elimination rule*)
lemma subsetCE [elim]:
    "A  B;  cA  P;  cB  P  P"
by (simp add: subset_def, blast)

(*Sometimes useful with premises in this order*)
lemma rev_subsetD: "cA; A<=B  cB"
by blast

lemma contra_subsetD: "A  B; c  B  c  A"
by blast

lemma rev_contra_subsetD: "c  B;  A  B  c  A"
by blast

lemma subset_refl [simp]: "A  A"
by blast

lemma subset_trans: "A<=B;  B<=C  A<=C"
by blast

(*Useful for proving A<=B by rewriting in some cases*)
lemma subset_iff:
     "A<=B <-> (x. xA  xB)"
  unfolding subset_def Ball_def
apply (rule iff_refl)
done

textFor calculations
declare subsetD [trans] rev_subsetD [trans] subset_trans [trans]


subsectionRules for equality

(*Anti-symmetry of the subset relation*)
lemma equalityI [intro]: "A  B;  B  A  A = B"
by (rule extension [THEN iffD2], rule conjI)


lemma equality_iffI: "(x. xA <-> xB)  A = B"
by (rule equalityI, blast+)

lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1]
lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2]

lemma equalityE: "A = B;  A<=B; B<=A  P    P"
by (blast dest: equalityD1 equalityD2)

lemma equalityCE:
    "A = B;  cA; cB  P;  cA; cB  P    P"
by (erule equalityE, blast)

lemma equality_iffD:
  "A = B  (x. x  A <-> x  B)"
  by auto


subsectionRules for Replace -- the derived form of replacement

lemma Replace_iff:
    "b  {y. xA, P(x,y)}  <->  (xA. P(x,b)  (y. P(x,y)  y=b))"
  unfolding Replace_def
apply (rule replacement [THEN iff_trans], blast+)
done

(*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
lemma ReplaceI [intro]:
    "P(x,b);  x: A;  y. P(x,y)  y=b 
     b  {y. xA, P(x,y)}"
by (rule Replace_iff [THEN iffD2], blast)

(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *)
lemma ReplaceE:
    "b  {y. xA, P(x,y)};
        x. x: A;  P(x,b);  y. P(x,y)y=b  R
  R"
by (rule Replace_iff [THEN iffD1, THEN bexE], simp+)

(*As above but without the (generally useless) 3rd assumption*)
lemma ReplaceE2 [elim!]:
    "b  {y. xA, P(x,y)};
        x. x: A;  P(x,b)  R
  R"
by (erule ReplaceE, blast)

lemma Replace_cong [cong]:
    "A=B;  x y. xB  P(x,y) <-> Q(x,y) 
     Replace(A,P) = Replace(B,Q)"
apply (rule equality_iffI)
apply (simp add: Replace_iff)
done


subsectionRules for RepFun

lemma RepFunI: "a  A  f(a)  {f(x). xA}"
by (simp add: RepFun_def Replace_iff, blast)

(*Useful for coinduction proofs*)
lemma RepFun_eqI [intro]: "b=f(a);  a  A  b  {f(x). xA}"
apply (erule ssubst)
apply (erule RepFunI)
done

lemma RepFunE [elim!]:
    "b  {f(x). xA};
        x.xA;  b=f(x)  P 
     P"
by (simp add: RepFun_def Replace_iff, blast)

lemma RepFun_cong [cong]:
    "A=B;  x. xB  f(x)=g(x)  RepFun(A,f) = RepFun(B,g)"
by (simp add: RepFun_def)

lemma RepFun_iff [simp]: "b  {f(x). xA} <-> (xA. b=f(x))"
by (unfold Bex_def, blast)

lemma triv_RepFun [simp]: "{x. xA} = A"
by blast


subsectionRules for Collect -- forming a subset by separation

(*Separation is derivable from Replacement*)
lemma separation [simp]: "a  {xA. P(x)} <-> aA  P(a)"
by (unfold Collect_def, blast)

lemma CollectI [intro!]: "aA;  P(a)  a  {xA. P(x)}"
by simp

lemma CollectE [elim!]: "a  {xA. P(x)};  aA; P(a)  R  R"
by simp

lemma CollectD1: "a  {xA. P(x)}  aA"
by (erule CollectE, assumption)

lemma CollectD2: "a  {xA. P(x)}  P(a)"
by (erule CollectE, assumption)

lemma Collect_cong [cong]:
    "A=B;  x. xB  P(x) <-> Q(x)
      Collect(A, λx. P(x)) = Collect(B, λx. Q(x))"
by (simp add: Collect_def)


subsectionRules for Unions

declare Union_iff [simp]

(*The order of the premises presupposes that C is rigid; A may be flexible*)
lemma UnionI [intro]: "B: C;  A: B  A: (C)"
by (simp, blast)

lemma UnionE [elim!]: "A  (C);  B.A: B;  B: C  R  R"
by (simp, blast)


subsectionRules for Unions of families
(* @{term"⋃x∈A. B(x)"} abbreviates @{term"⋃({B(x). x∈A})"} *)

lemma UN_iff [simp]: "b  (xA. B(x)) <-> (xA. b  B(x))"
by (simp add: Bex_def, blast)

(*The order of the premises presupposes that A is rigid; b may be flexible*)
lemma UN_I: "a: A;  b: B(a)  b: (xA. B(x))"
by (simp, blast)


lemma UN_E [elim!]:
    "b  (xA. B(x));  x.x: A;  b: B(x)  R  R"
by blast

lemma UN_cong:
    "A=B;  x. xB  C(x)=D(x)  (xA. C(x)) = (xB. D(x))"
by simp


(*No "Addcongs [UN_cong]" because @{term⋃} is a combination of constants*)

(* UN_E appears before UnionE so that it is tried first, to avoid expensive
  calls to hyp_subst_tac.  Cannot include UN_I as it is unsafe: would enlarge
  the search space.*)


subsectionRules for the empty set

(*The set @{term"{x∈0. False}"} is empty; by foundation it equals 0
  See Suppes, page 21.*)
lemma not_mem_empty [simp]: "a  0"
apply (cut_tac foundation)
apply (best dest: equalityD2)
done

lemmas emptyE [elim!] = not_mem_empty [THEN notE]


lemma empty_subsetI [simp]: "0  A"
by blast

lemma equals0I: "y. yA  False  A=0"
by blast

lemma equals0D [dest]: "A=0  a  A"
by blast

declare sym [THEN equals0D, dest]

lemma not_emptyI: "aA  A  0"
by blast

lemma not_emptyE:  "A  0;  x. xA  R  R"
by blast


subsectionRules for Inter

(*Not obviously useful for proving InterI, InterD, InterE*)
lemma Inter_iff: "A  (C) <-> (xC. A: x)  C0"
by (simp add: Inter_def Ball_def, blast)

(* Intersection is well-behaved only if the family is non-empty! *)
lemma InterI [intro!]:
    "x. x: C  A: x;  C0  A  (C)"
by (simp add: Inter_iff)

(*A "destruct" rule -- every B in C contains A as an element, but
  A∈B can hold when B∈C does not!  This rule is analogous to "spec". *)
lemma InterD [elim, Pure.elim]: "A  (C);  B  C  A  B"
by (unfold Inter_def, blast)

(*"Classical" elimination rule -- does not require exhibiting @{term"B∈C"} *)
lemma InterE [elim]:
    "A  (C);  BC  R;  AB  R  R"
by (simp add: Inter_def, blast)


subsectionRules for Intersections of families

(* @{term"⋂x∈A. B(x)"} abbreviates @{term"⋂({B(x). x∈A})"} *)

lemma INT_iff: "b  (xA. B(x)) <-> (xA. b  B(x))  A0"
by (force simp add: Inter_def)

lemma INT_I: "x. x: A  b: B(x);  A0  b: (xA. B(x))"
by blast

lemma INT_E: "b  (xA. B(x));  a: A  b  B(a)"
by blast

lemma INT_cong:
    "A=B;  x. xB  C(x)=D(x)  (xA. C(x)) = (xB. D(x))"
by simp

(*No "Addcongs [INT_cong]" because @{term⋂} is a combination of constants*)


subsectionRules for Powersets

lemma PowI: "A  B  A  Pow(B)"
by (erule Pow_iff [THEN iffD2])

lemma PowD: "A  Pow(B)    A<=B"
by (erule Pow_iff [THEN iffD1])

declare Pow_iff [iff]

lemmas Pow_bottom = empty_subsetI [THEN PowI]    ― ‹term0  Pow(B)
lemmas Pow_top = subset_refl [THEN PowI]         ― ‹termA  Pow(A)


subsectionCantor's Theorem: There is no surjection from a set to its powerset.

(*The search is undirected.  Allowing redundant introduction rules may
  make it diverge.  Variable b represents ANY map, such as
  (lam x∈A.b(x)): A->Pow(A). *)
lemma cantor: "S  Pow(A). xA. b(x)  S"
by (best elim!: equalityCE del: ReplaceI RepFun_eqI)

end