Quelle  ZF_Base.thy

(*  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:›\› 10)
  "_Bex"      :: "[pttrn, i, o] ==> o"        (‹(‹indent=3 notation=‹binder 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"(\<forall>x\<in>A.P)\<longleftrightarrow>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\<in>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"(\<exists>x\<in>A. True) \<longleftrightarrow> True"} unless @{term"A" is nonempty\<And>*)
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\<subseteq>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"\<Union>x\<in>A. B(x)"} abbreviates @{term"\<Union>({B(x). x\<in>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\<Union>} 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\<in>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\<in>B can hold when B\<in>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\<in>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"\<Inter>x\<in>A. B(x)"} abbreviates @{term"\<Inter>({B(x). x\<in>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\<Inter>} 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]    🍋 ‹🍋‹0 ∈ Pow(B)›\ lemmas Pow_top = subset_refl [THEN PowI]         🍋 ‹🍋‹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\<in>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