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. x∈A ⟶ P(x)"

definition Bex :: "[i, i ⇒ o] ⇒ o"
  where "Bex(A, P) ≡ ∃x. x∈A ∧ P(x)"

syntax
  "_Ball" :: "[pttrn, i, o] ⇒ o"  (‹(3∀_∈_./ _)› 10)
  "_Bex" :: "[pttrn, i, o] ⇒ o"  (‹(3∃_∈_./ _)› 10)
translations
  "∀x∈A. P" ⇌ "CONST Ball(A, λx. P)"
  "∃x∈A. 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. x∈A, 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 . x∈A, y=f(x)}"

syntax
  "_RepFun" :: "[i, pttrn, i] => i"  (‹(1{_ ./ _ ∈ _})› [51,0,51])
translations
  "{b. x∈A}" ⇌ "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 . x∈A, x=y & P(x)}"

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


subsection ‹General union and intersection›

definition Inter :: "i => i"  (‹⋂_› [90] 90)
  where "⋂(A) == { x∈⋃(A) . ∀y∈A. x∈y}"

syntax
  "_UNION" :: "[pttrn, i, i] => i"  (‹(3⋃_∈_./ _)› 10)
  "_INTER" :: "[pttrn, i, i] => i"  (‹(3⋂_∈_./ _)› 10)
translations
  "⋃x∈A. B" == "CONST Union({B. x∈A})"
  "⋂x∈A. B" == "CONST Inter({B. x∈A})"


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. x∈Pow(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 ≡ ∀x∈A. x∈B"

definition Diff :: "[i, i] ⇒ i"  (infixl ‹-› 65)  ― ‹set difference›
  where "A - B == { x∈A . ~(x∈B) }"

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) ⟷ (∃B∈C. A∈B)" and
  Pow_iff:       "A ∈ Pow(B) ⟷ A ⊆ B" and

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

  (*This formulation facilitates case analysis on A.*)
  foundation:    "A = 0 ∨ (∃x∈A. ∀y∈x. y∉A)" and

  (*Schema axiom since predicate P is a higher-order variable*)
  replacement:   "(∀x∈A. ∀y z. P(x,y) ∧ P(x,z) ⟶ y = z) ⟹
                         b ∈ PrimReplace(A,P) ⟷ (∃x∈A. 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) == ⋃x∈A. ⋃y∈B(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. w∈r, ∃x y. w=⟨x,y⟩ ∧ z=⟨y,x⟩}"

definition domain :: "i ⇒ i"
  where "domain(r) == {x. w∈r, ∃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) == ∀z∈r. ∃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). ∃x∈A. ⟨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. ∃x∈A. ∃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)⟩. x∈A}"

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

definition Pi :: "[i, i ⇒ i] ⇒ i"
  where "Pi(A,B) == {f∈Pow(Sigma(A,B)). A⊆domain(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
  "∏x∈A. B"   == "CONST Pi(A, λx. B)"
  "∑x∈A. B"   == "CONST Sigma(A, λx. B)"
  "λx∈A. 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: "[| b∈A;  a=b |] ==> a∈A"
by (erule ssubst, assumption)


subsection‹Bounded universal quantifier›

lemma ballI [intro!]: "[| !!x. x∈A ==> P(x) |] ==> ∀x∈A. P(x)"
by (simp add: Ball_def)

lemmas strip = impI allI ballI

lemma bspec [dest?]: "[| ∀x∈A. P(x);  x: A |] ==> P(x)"
by (simp add: Ball_def)

(*Instantiates x first: better for automatic theorem proving?*)
lemma rev_ballE [elim]:
    "[| ∀x∈A. P(x);  x∉A ==> Q;  P(x) ==> Q |] ==> Q"
by (simp add: Ball_def, blast)

lemma ballE: "[| ∀x∈A. P(x);  P(x) ==> Q;  x∉A ==> Q |] ==> Q"
by blast

(*Used in the datatype package*)
lemma rev_bspec: "[| x: A;  ∀x∈A. 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]: "(∀x∈A. P) <-> ((∃x. x∈A) ⟶ P)"
by (simp add: Ball_def)

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

lemma atomize_ball:
    "(!!x. x ∈ A ==> P(x)) == Trueprop (∀x∈A. P(x))"
  by (simp only: Ball_def atomize_all atomize_imp)

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


subsection‹Bounded existential quantifier›

lemma bexI [intro]: "[| P(x);  x: A |] ==> ∃x∈A. P(x)"
by (simp add: Bex_def, blast)

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

(*Not of the general form for such rules. The existential quanitifer becomes universal. *)
lemma bexCI: "[| ∀x∈A. ~P(x) ==> P(a);  a: A |] ==> ∃x∈A. P(x)"
by blast

lemma bexE [elim!]: "[| ∃x∈A. P(x);  !!x. [| x∈A; 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]: "(∃x∈A. P) <-> ((∃x. x∈A) & P)"
by (simp add: Bex_def)

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



subsection‹Rules for subsets›

lemma subsetI [intro!]:
    "(!!x. x∈A ==> x∈B) ==> A ⊆ B"
by (simp add: subset_def)

(*Rule in Modus Ponens style [was called subsetE] *)
lemma subsetD [elim]: "[| A ⊆ B;  c∈A |] ==> c∈B"
apply (unfold subset_def)
apply (erule bspec, assumption)
done

(*Classical elimination rule*)
lemma subsetCE [elim]:
    "[| A ⊆ B;  c∉A ==> P;  c∈B ==> P |] ==> P"
by (simp add: subset_def, blast)

(*Sometimes useful with premises in this order*)
lemma rev_subsetD: "[| c∈A; A<=B |] ==> c∈B"
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. x∈A ⟶ x∈B)"
apply (unfold subset_def Ball_def)
apply (rule iff_refl)
done

text‹For calculations›
declare subsetD [trans] rev_subsetD [trans] subset_trans [trans]


subsection‹Rules 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. x∈A <-> x∈B) ==> 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;  [| c∈A; c∈B |] ==> P;  [| c∉A; c∉B |] ==> P |]  ==>  P"
by (erule equalityE, blast)

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


subsection‹Rules for Replace -- the derived form of replacement›

lemma Replace_iff:
    "b ∈ {y. x∈A, P(x,y)}  <->  (∃x∈A. P(x,b) & (∀y. P(x,y) ⟶ y=b))"
apply (unfold 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. x∈A, 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. x∈A, 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. x∈A, P(x,y)};
        !!x. [| x: A;  P(x,b) |] ==> R
     |] ==> R"
by (erule ReplaceE, blast)

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


subsection‹Rules for RepFun›

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

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

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

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

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

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


subsection‹Rules for Collect -- forming a subset by separation›

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

lemma CollectI [intro!]: "[| a∈A;  P(a) |] ==> a ∈ {x∈A. P(x)}"
by simp

lemma CollectE [elim!]: "[| a ∈ {x∈A. P(x)};  [| a∈A; P(a) |] ==> R |] ==> R"
by simp

lemma CollectD1: "a ∈ {x∈A. P(x)} ==> a∈A"
by (erule CollectE, assumption)

lemma CollectD2: "a ∈ {x∈A. P(x)} ==> P(a)"
by (erule CollectE, assumption)

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


subsection‹Rules 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)


subsection‹Rules for Unions of families›
(* @{term"⋃x∈A. B(x)"} abbreviates @{term"⋃({B(x). x∈A})"} *)

lemma UN_iff [simp]: "b ∈ (⋃x∈A. B(x)) <-> (∃x∈A. 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: (⋃x∈A. B(x))"
by (simp, blast)


lemma UN_E [elim!]:
    "[| b ∈ (⋃x∈A. B(x));  !!x.[| x: A;  b: B(x) |] ==> R |] ==> R"
by blast

lemma UN_cong:
    "[| A=B;  !!x. x∈B ==> C(x)=D(x) |] ==> (⋃x∈A. C(x)) = (⋃x∈B. 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.*)


subsection‹Rules 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. y∈A ==> False |] ==> A=0"
by blast

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

declare sym [THEN equals0D, dest]

lemma not_emptyI: "a∈A ==> A ≠ 0"
by blast

lemma not_emptyE:  "[| A ≠ 0;  !!x. x∈A ==> R |] ==> R"
by blast


subsection‹Rules for Inter›

(*Not obviously useful for proving InterI, InterD, InterE*)
lemma Inter_iff: "A ∈ ⋂(C) <-> (∀x∈C. A: x) & C≠0"
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;  C≠0 |] ==> 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);  B∉C ==> R;  A∈B ==> R |] ==> R"
by (simp add: Inter_def, blast)


subsection‹Rules for Intersections of families›

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

lemma INT_iff: "b ∈ (⋂x∈A. B(x)) <-> (∀x∈A. b ∈ B(x)) & A≠0"
by (force simp add: Inter_def)

lemma INT_I: "[| !!x. x: A ==> b: B(x);  A≠0 |] ==> b: (⋂x∈A. B(x))"
by blast

lemma INT_E: "[| b ∈ (⋂x∈A. B(x));  a: A |] ==> b ∈ B(a)"
by blast

lemma INT_cong:
    "[| A=B;  !!x. x∈B ==> C(x)=D(x) |] ==> (⋂x∈A. C(x)) = (⋂x∈B. D(x))"
by simp

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


subsection‹Rules 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]    ― ‹\<^term>‹0 ∈ Pow(B)››
lemmas Pow_top = subset_refl [THEN PowI]         ― ‹\<^term>‹A ∈ Pow(A)››


subsection‹Cantor'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). ∀x∈A. b(x) ≠ S"
by (best elim!: equalityCE del: ReplaceI RepFun_eqI)

end