(* 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" (\\_\ [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" (\(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 \<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" (\<open>(1{_ ./ _ \<in> _, _})\<close>)
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" (\<open>(1{_ ./ _ \<in> _})\<close> [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 \<open>General union and intersection\<close>
definition Inter :: "i => i" (\<open>\<Inter>_\<close> [90] 90)
where "\(A) == { x\\(A) . \y\A. x\y}"
syntax
"_UNION" :: "[pttrn, i, i] => i" (\<open>(3\<Union>_\<in>_./ _)\<close> 10)
"_INTER" :: "[pttrn, i, i] => i" (\<open>(3\<Inter>_\<in>_./ _)\<close> 10)
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" (\{(_)}\)
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" (\(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" (\<open>if '(_,_,_')\<close>)
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))"
(* Patterns -- extends pre-defined type "pttrn" used in abstractions *)
nonterminal patterns
syntax
"_pattern" :: "patterns => pttrn" (\<open>\<langle>_\<rangle>\<close>)
"" :: "pttrn => patterns" (\<open>_\<close>)
"_patterns" :: "[pttrn, patterns] => patterns" (\<open>_,/_\<close>)
"_Tuple" :: "[i, is] => i" (\<open>\<langle>(_,/ _)\<rangle>\<close>)
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 \<open>\<times>\<close> 80) \<comment> \<open>Cartesian product\<close>
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" (\<open>(3\<Prod>_\<in>_./ _)\<close> 10)
"_SUM" :: "[pttrn, i, i] => i" (\<open>(3\<Sum>_\<in>_./ _)\<close> 10)
"_lam" :: "[pttrn, i, i] => i" (\<open>(3\<lambda>_\<in>_./ _)\<close> 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 \<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>~:\<close> 50)
syntax (ASCII)
"_Ball" :: "[pttrn, i, o] => o" (\<open>(3ALL _:_./ _)\<close> 10)
"_Bex" :: "[pttrn, i, o] => o" (\<open>(3EX _:_./ _)\<close> 10)
"_Collect" :: "[pttrn, i, o] => i" (\<open>(1{_: _ ./ _})\<close>)
"_Replace" :: "[pttrn, pttrn, i, o] => i" (\<open>(1{_ ./ _: _, _})\<close>)
"_RepFun" :: "[i, pttrn, i] => i" (\<open>(1{_ ./ _: _})\<close> [51,0,51])
"_UNION" :: "[pttrn, i, i] => i" (\<open>(3UN _:_./ _)\<close> 10)
"_INTER" :: "[pttrn, i, i] => i" (\<open>(3INT _:_./ _)\<close> 10)
"_PROD" :: "[pttrn, i, i] => i" (\<open>(3PROD _:_./ _)\<close> 10)
"_SUM" :: "[pttrn, i, i] => i" (\<open>(3SUM _:_./ _)\<close> 10)
"_lam" :: "[pttrn, i, i] => i" (\<open>(3lam _:_./ _)\<close> 10)
"_Tuple" :: "[i, is] => i" (\<open><(_,/ _)>\<close>)
"_pattern" :: "patterns => pttrn" (\<open><_>\<close>)
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)<->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) <-> 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) |]
==> (\<exists>x\<in>A. P(x)) <-> (\<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"
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\<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))"
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 \<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)};
!!x. [| x: A; P(x,b); \<forall>y. P(x,y)\<longrightarrow>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\<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}"
apply (erule ssubst)
apply (erule RepFunI)
done
lemma RepFunE [elim!]:
"[| b \ {f(x). x\A};
!!x.[| x\<in>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\<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 (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\<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 (simp, blast)
lemma UnionE [elim!]: "[| A \ \(C); !!B.[| A: B; B: C |] ==> R |] ==> R"
by (simp, blast)
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 (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\<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"
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\<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 (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\<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 (unfold Inter_def, blast)
(*"Classical" elimination rule -- does not require exhibiting @{term"B\<in>C"} *)
lemma InterE [elim]:
"[| A \ \(C); B\C ==> R; A\B ==> R |] ==> R"
by (simp add: Inter_def, blast)
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
¤ Dauer der Verarbeitung: 0.9 Sekunden
(vorverarbeitet)
¤
|
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.
|
