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"  (‹(‹open_block notation=‹prefix ⋃››⋃_)› [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"  (‹(‹indent=3 notation=‹binder ∀∈››∀_∈_./ _)› 10)
  "_Bex" :: "[pttrn, i, o] ⇒ o"  (‹(‹indent=3 notation=‹binder ∃∈››∃_∈_./ _)› 10)
syntax_consts
  "_Ball" ⇌ Ball and
  "_Bex" ⇌ Bex
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"  (‹(‹indent=1 notation=‹mixfix relational replacement››{_ ./ _ ∈ _, _})›)
syntax_consts
  "_Replace" ⇌ Replace
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"  (‹(‹indent=1 notation=‹mixfix functional replacement››{_ ./ _ ∈ _})› [51,0,51])
syntax_consts
  "_RepFun" ⇌ RepFun
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"  (‹(‹indent=1 notation=‹mixfix set comprehension››{_ ∈ _ ./ _})›)
syntax_consts
  "_Collect" ⇌ Collect
translations
  "{x∈A. P}" ⇌ "CONST Collect(A, λx. P)"


subsection ‹General union and intersection›

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

syntax
  "_UNION" :: "[pttrn, i, i] ⇒ i"  (‹(‹indent=3 notation=‹binder ⋃∈››⋃_∈_./ _)› 10)
  "_INTER" :: "[pttrn, i, i] ⇒ i"  (‹(‹indent=3 notation=‹binder ⋂∈››⋂_∈_./ _)› 10)
syntax_consts
  "_UNION" == Union and
  "_INTER" == Inter
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"  (‹(‹indent=1 notation=‹mixfix set enumeration››{_})›)
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"  (‹(‹notation=‹mixfix if then else››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))"

nonterminal "tuple_args"
syntax
  "" :: "i ⇒ tuple_args"  (‹_›)
  "_Tuple_args" :: "[i, tuple_args] ⇒ tuple_args"  (‹_,/ _›)
  "_Tuple" :: "[i, tuple_args] ⇒ i"  (‹(‹indent=1 notation=‹mixfix tuple enumeration››⟨_,/ _⟩)›)
translations
  "⟨x, y, z⟩"   == "⟨x, ⟨y, z⟩⟩"
  "⟨x, y⟩"      == "CONST Pair(x, y)"

(* Patterns -- extends pre-defined type "pttrn" used in abstractions *)
nonterminal patterns
syntax
  "_pattern"  :: "patterns ⇒ pttrn"  (‹(‹open_block notation=‹pattern tuple››⟨_⟩)›)
  ""          :: "pttrn ⇒ patterns"  (‹_›)
  "_patterns" :: "[pttrn, patterns] ⇒ patterns"  (‹_,/_›)
syntax_consts
  "_pattern" "_patterns" == split
translations
  "λ⟨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"        (‹(‹indent=3 notation=‹mixfix ∏∈››∏_∈_./ _)› 10)
  "_SUM"      :: "[pttrn, i, i] ⇒ i"        (‹(‹indent=3 notation=‹mixfix ∑∈››∑_∈_./ _)› 10)
  "_lam"      :: "[pttrn, i, i] ⇒ i"        (‹(‹indent=3 notation=‹mixfix λ∈››λ_∈_./ _)› 10)
syntax_consts
  "_PROD" == Pi and
  "_SUM" == Sigma and
  "_lam" == Lambda
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"        (‹(‹indent=3 notation=‹binder ALL:››ALL _:_./ _)› 10)
  "_Bex"      :: "[pttrn, i, o] ⇒ o"        (‹(‹indent=3 notation=‹binder EX:››EX _:_./ _)› 10)
  "_Collect"  :: "[pttrn, i, o] ⇒ i"        (‹(‹indent=1 notation=‹mixfix set comprehension››{_: _ ./ _})›)
  "_Replace"  :: "[pttrn, pttrn, i, o] ⇒ i" (‹(‹indent=1 notation=‹mixfix relational replacement››{_ ./ _: _, _})›)
  "_RepFun"   :: "[i, pttrn, i] ⇒ i"        (‹(‹indent=1 notation=‹mixfix functional replacement››{_ ./ _: _})› [51,0,51])
  "_UNION"    :: "[pttrn, i, i] ⇒ i"        (‹(‹indent=3 notation=‹binder UN:››UN _:_./ _)› 10)
  "_INTER"    :: "[pttrn, i, i] ⇒ i"        (‹(‹indent=3 notation=‹binder INT:››INT _:_./ _)› 10)
  "_PROD"     :: "[pttrn, i, i] ⇒ i"        (‹(‹indent=3 notation=‹binder PROD:››PROD _:_./ _)› 10)
  "_SUM"      :: "[pttrn, i, i] ⇒ i"        (‹(‹indent=3 notation=‹binder SUM:››SUM _:_./ _)› 10)
  "_lam"      :: "[pttrn, i, i] ⇒ i"        (‹(‹indent=3 notation=‹binder lam:››lam _:_./ _)› 10)
  "_Tuple"    :: "[i, tuple_args] ⇒ i"      (‹(‹indent=1 notation=‹mixfix tuple enumeration››<_,/ _>)›)
  "_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"
  unfolding 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)"
  by auto

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))"
  unfolding Replace_def
  by (rule replacement [THEN iff_trans], blast+)

(*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}"
  by (blast intro: RepFunI)

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 (auto simp: Collect_def)

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" and CollectD2: "a ∈ {x∈A. P(x)} ⟹ P(a)"
  by auto

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 auto

lemma UnionE [elim!]: "⟦A ∈ ⋃(C);  ⋀B.⟦A: B;  B: C⟧ ⟹ R⟧ ⟹ R"
  by auto


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 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 force


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"
  using foundation by (best dest: equalityD2)

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 (force simp: Inter_def)

(* 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 (force simp: Inter_def)

(*"Classical" elimination rule -- does not require exhibiting @{term"B∈C"} *)
lemma InterE [elim]:
  "⟦A ∈ ⋂(C);  B∉C ⟹ R;  A∈B ⟹ R⟧ ⟹ R"
  by (auto simp: Inter_def)


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