Quelle ZF_Base.thy Sprache: Isabelle

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

section \<open>Base of Zermelo-Fraenkel Set Theory\<close>

theory ZF_Base
imports FOL
begin

subsection \<open>Signature\<close>

declare [[eta_contract = false]]

typedecl i
instance i :: "term" ..

axiomatization mem :: "[i, i] \ o" (infixl \\\ 50) \ \membership relation\
  and zero :: "i"  (\<open>0\<close>)  \<comment> \<open>the empty set\<close>
  and Pow :: "i \ i" \ \power sets\
  and Inf :: "i"  \<comment> \<open>infinite set\<close>
  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 \<open>Bounded Quantifiers\<close>

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" \<rightleftharpoons> Ball and
  "_Bex" \<rightleftharpoons> Bex
translations
  "\x\A. P" \ "CONST Ball(A, \x. P)"
  "\x\A. P" \ "CONST Bex(A, \x. P)"

subsection \<open>Variations on Replacement\<close>

(* 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" \<rightleftharpoons> 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" \<rightleftharpoons> 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" \<rightleftharpoons> Collect
translations
  "{x\A. P}" \ "CONST Collect(A, \x. P)"

subsection \<open>General union and intersection\<close>

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 \<open>Finite sets and binary operations\<close>

(*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 \<open>Axioms\<close>

(* 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 \<in> PrimReplace(A,P) \<longleftrightarrow> (\<exists>x\<in>A. P(x,b))"

subsection \<open>Definite descriptions -- via Replace over the set "1"\<close>

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 \<open>Ordered Pairing\<close>

(* 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 \<open>Relations and Functions\<close>

(*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 \<open>ASCII syntax\<close>

notation (ASCII)
  cart_prod       (infixr \<open>*\<close> 80) and
  Int             (infixl \<open>Int\<close> 70) and
  Un              (infixl \<open>Un\<close> 65) and
  function_space  (infixr \<open>->\<close> 60) and
  Subset          (infixl \<open><=\<close> 50) and
  mem             (infixl \<open>:\<close> 50) and
  not_mem         (infixl \<open>\<not>:\<close> 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 \<open>Substitution\<close>

(*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\<open>Bounded universal quantifier\<close>

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\<open>Bounded existential quantifier\<close>

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)\
     \<Longrightarrow> (\<exists>x\<in>A. P(x)) \<longleftrightarrow> (\<exists>x\<in>A'. P'(x))"
by (simp add: Bex_def cong: conj_cong)

subsection\<open>Rules for subsets\<close>

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\<open>For calculations\<close>
declare subsetD [trans] rev_subsetD [trans] subset_trans [trans]

subsection\<open>Rules for equality\<close>

(*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\<open>Rules for Replace -- the derived form of replacement\<close>

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 \<in> {y. x\<in>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)};
        \<And>x. \<lbrakk>x: A;  P(x,b);  \<forall>y. P(x,y)\<longrightarrow>y=b\<rbrakk> \<Longrightarrow> R
\<rbrakk> \<Longrightarrow> 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)};
        \<And>x. \<lbrakk>x: A;  P(x,b)\<rbrakk> \<Longrightarrow> R
   \<rbrakk> \<Longrightarrow> 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\<open>Rules for RepFun\<close>

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};
        \<And>x.\<lbrakk>x\<in>A;  b=f(x)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow>
     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\<open>Rules for Collect -- forming a subset by separation\<close>

(*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)\
     \<Longrightarrow> Collect(A, \<lambda>x. P(x)) = Collect(B, \<lambda>x. Q(x))"
  by (simp add: Collect_def)

subsection\<open>Rules for Unions\<close>

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\<open>Rules for Unions of families\<close>
(* @{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\<open>Rules for the empty set\<close>

(*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\<open>Rules for Inter\<close>

(*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\<open>Rules for Intersections of families\<close>

(* @{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\<open>Rules for Powersets\<close>

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]    \<comment> \<open>\<^term>\<open>0 \<in> Pow(B)\<close>\<close>
lemmas Pow_top = subset_refl [THEN PowI]         \<comment> \<open>\<^term>\<open>A \<in> Pow(A)\<close>\<close>

subsection\<open>Cantor's Theorem: There is no surjection from a set to its powerset.\<close>

(*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

quality94%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.