author  paulson 
Tue, 06 Mar 2012 15:15:49 +0000  
changeset 46820  c656222c4dc1 
parent 46751  6b94c39b7366 
child 46907  eea3eb057fea 
permissions  rwrr 
615  1 
(* Title: ZF/ZF.thy 
0  2 
Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory 
3 
Copyright 1993 University of Cambridge 

14076  4 
*) 
0  5 

14076  6 
header{*ZermeloFraenkel Set Theory*} 
0  7 

37781
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
37405
diff
changeset

8 
theory ZF 
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
37405
diff
changeset

9 
imports FOL 
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
37405
diff
changeset

10 
begin 
0  11 

39128
93a7365fb4ee
turned eta_contract into proper configuration option;
wenzelm
parents:
38798
diff
changeset

12 
declare [[eta_contract = false]] 
23168  13 

14076  14 
typedecl i 
15 
arities i :: "term" 

0  16 

17 
consts 

18 

41310  19 
zero :: "i" ("0") {*the empty set*} 
14076  20 
Pow :: "i => i" {*power sets*} 
21 
Inf :: "i" {*infinite set*} 

0  22 

14076  23 
text {*Bounded Quantifiers *} 
24 
consts 

13780  25 
Ball :: "[i, i => o] => o" 
26 
Bex :: "[i, i => o] => o" 

0  27 

14076  28 
text {*General Union and Intersection *} 
29 
consts 

13780  30 
Union :: "i => i" 
31 
Inter :: "i => i" 

0  32 

14076  33 
text {*Variations on Replacement *} 
34 
consts 

13144  35 
PrimReplace :: "[i, [i, i] => o] => i" 
36 
Replace :: "[i, [i, i] => o] => i" 

37 
RepFun :: "[i, i => i] => i" 

38 
Collect :: "[i, i => o] => i" 

0  39 

14883  40 
text{*Definite descriptions  via Replace over the set "1"*} 
14076  41 
consts 
13780  42 
The :: "(i => o) => i" (binder "THE " 10) 
13144  43 
If :: "[o, i, i] => i" ("(if (_)/ then (_)/ else (_))" [10] 10) 
6068  44 

24826  45 
abbreviation (input) 
46 
old_if :: "[o, i, i] => i" ("if '(_,_,_')") where 

47 
"if(P,a,b) == If(P,a,b)" 

6068  48 

49 

14076  50 
text {*Finite Sets *} 
6068  51 
consts 
13780  52 
Upair :: "[i, i] => i" 
53 
cons :: "[i, i] => i" 

54 
succ :: "i => i" 

0  55 

14076  56 
text {*Ordered Pairing *} 
57 
consts 

13780  58 
Pair :: "[i, i] => i" 
59 
fst :: "i => i" 

60 
snd :: "i => i" 

14854  61 
split :: "[[i, i] => 'a, i] => 'a::{}" {*for patternmatching*} 
0  62 

14076  63 
text {*Sigma and Pi Operators *} 
64 
consts 

13780  65 
Sigma :: "[i, i => i] => i" 
66 
Pi :: "[i, i => i] => i" 

0  67 

14076  68 
text {*Relations and Functions *} 
69 
consts 

70 
"domain" :: "i => i" 

13144  71 
range :: "i => i" 
72 
field :: "i => i" 

73 
converse :: "i => i" 

14076  74 
relation :: "i => o" {*recognizes sets of pairs*} 
24826  75 
"function" :: "i => o" {*recognizes functions; can have nonpairs*} 
13144  76 
Lambda :: "[i, i => i] => i" 
77 
restrict :: "[i, i] => i" 

0  78 

14076  79 
text {*Infixes in order of decreasing precedence *} 
80 
consts 

0  81 

24826  82 
Image :: "[i, i] => i" (infixl "``" 90) {*image*} 
83 
vimage :: "[i, i] => i" (infixl "``" 90) {*inverse image*} 

84 
"apply" :: "[i, i] => i" (infixl "`" 90) {*function application*} 

85 
"Int" :: "[i, i] => i" (infixl "Int" 70) {*binary intersection*} 

86 
"Un" :: "[i, i] => i" (infixl "Un" 65) {*binary union*} 

87 
Diff :: "[i, i] => i" (infixl "" 65) {*set difference*} 

88 
Subset :: "[i, i] => o" (infixl "<=" 50) {*subset relation*} 

89 
mem :: "[i, i] => o" (infixl ":" 50) {*membership relation*} 

90 

91 
abbreviation 

92 
not_mem :: "[i, i] => o" (infixl "~:" 50) {*negated membership relation*} 

93 
where "x ~: y == ~ (x : y)" 

94 

95 
abbreviation 

96 
cart_prod :: "[i, i] => i" (infixr "*" 80) {*Cartesian product*} 

97 
where "A * B == Sigma(A, %_. B)" 

98 

99 
abbreviation 

100 
function_space :: "[i, i] => i" (infixr ">" 60) {*function space*} 

101 
where "A > B == Pi(A, %_. B)" 

0  102 

103 

41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
40714
diff
changeset

104 
nonterminal "is" and patterns 
615  105 

106 
syntax 

13144  107 
"" :: "i => is" ("_") 
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

108 
"_Enum" :: "[i, is] => is" ("_,/ _") 
24826  109 

35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

110 
"_Finset" :: "is => i" ("{(_)}") 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

111 
"_Tuple" :: "[i, is] => i" ("<(_,/ _)>") 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

112 
"_Collect" :: "[pttrn, i, o] => i" ("(1{_: _ ./ _})") 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

113 
"_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})") 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

114 
"_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _: _})" [51,0,51]) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

115 
"_INTER" :: "[pttrn, i, i] => i" ("(3INT _:_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

116 
"_UNION" :: "[pttrn, i, i] => i" ("(3UN _:_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

117 
"_PROD" :: "[pttrn, i, i] => i" ("(3PROD _:_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

118 
"_SUM" :: "[pttrn, i, i] => i" ("(3SUM _:_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

119 
"_lam" :: "[pttrn, i, i] => i" ("(3lam _:_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

120 
"_Ball" :: "[pttrn, i, o] => o" ("(3ALL _:_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

121 
"_Bex" :: "[pttrn, i, o] => o" ("(3EX _:_./ _)" 10) 
1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

122 

62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

123 
(** Patterns  extends predefined type "pttrn" used in abstractions **) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

124 

35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

125 
"_pattern" :: "patterns => pttrn" ("<_>") 
13144  126 
"" :: "pttrn => patterns" ("_") 
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

127 
"_patterns" :: "[pttrn, patterns] => patterns" ("_,/_") 
615  128 

0  129 
translations 
35068  130 
"{x, xs}" == "CONST cons(x, {xs})" 
131 
"{x}" == "CONST cons(x, 0)" 

132 
"{x:A. P}" == "CONST Collect(A, %x. P)" 

133 
"{y. x:A, Q}" == "CONST Replace(A, %x y. Q)" 

134 
"{b. x:A}" == "CONST RepFun(A, %x. b)" 

135 
"INT x:A. B" == "CONST Inter({B. x:A})" 

136 
"UN x:A. B" == "CONST Union({B. x:A})" 

137 
"PROD x:A. B" == "CONST Pi(A, %x. B)" 

138 
"SUM x:A. B" == "CONST Sigma(A, %x. B)" 

139 
"lam x:A. f" == "CONST Lambda(A, %x. f)" 

140 
"ALL x:A. P" == "CONST Ball(A, %x. P)" 

141 
"EX x:A. P" == "CONST Bex(A, %x. P)" 

37  142 

1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

143 
"<x, y, z>" == "<x, <y, z>>" 
35068  144 
"<x, y>" == "CONST Pair(x, y)" 
145 
"%<x,y,zs>.b" == "CONST split(%x <y,zs>.b)" 

146 
"%<x,y>.b" == "CONST split(%x y. b)" 

2286  147 

0  148 

24826  149 
notation (xsymbols) 
150 
cart_prod (infixr "\<times>" 80) and 

151 
Int (infixl "\<inter>" 70) and 

152 
Un (infixl "\<union>" 65) and 

153 
function_space (infixr "\<rightarrow>" 60) and 

154 
Subset (infixl "\<subseteq>" 50) and 

155 
mem (infixl "\<in>" 50) and 

156 
not_mem (infixl "\<notin>" 50) and 

157 
Union ("\<Union>_" [90] 90) and 

158 
Inter ("\<Inter>_" [90] 90) 

159 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
11322
diff
changeset

160 
syntax (xsymbols) 
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

161 
"_Collect" :: "[pttrn, i, o] => i" ("(1{_ \<in> _ ./ _})") 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

162 
"_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})") 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

163 
"_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \<in> _})" [51,0,51]) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

164 
"_UNION" :: "[pttrn, i, i] => i" ("(3\<Union>_\<in>_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

165 
"_INTER" :: "[pttrn, i, i] => i" ("(3\<Inter>_\<in>_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

166 
"_PROD" :: "[pttrn, i, i] => i" ("(3\<Pi>_\<in>_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

167 
"_SUM" :: "[pttrn, i, i] => i" ("(3\<Sigma>_\<in>_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

168 
"_lam" :: "[pttrn, i, i] => i" ("(3\<lambda>_\<in>_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

169 
"_Ball" :: "[pttrn, i, o] => o" ("(3\<forall>_\<in>_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

170 
"_Bex" :: "[pttrn, i, o] => o" ("(3\<exists>_\<in>_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

171 
"_Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>") 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

172 
"_pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>") 
2540  173 

24826  174 
notation (HTML output) 
175 
cart_prod (infixr "\<times>" 80) and 

176 
Int (infixl "\<inter>" 70) and 

177 
Un (infixl "\<union>" 65) and 

178 
Subset (infixl "\<subseteq>" 50) and 

179 
mem (infixl "\<in>" 50) and 

180 
not_mem (infixl "\<notin>" 50) and 

181 
Union ("\<Union>_" [90] 90) and 

182 
Inter ("\<Inter>_" [90] 90) 

183 

6340  184 
syntax (HTML output) 
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

185 
"_Collect" :: "[pttrn, i, o] => i" ("(1{_ \<in> _ ./ _})") 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

186 
"_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})") 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

187 
"_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \<in> _})" [51,0,51]) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

188 
"_UNION" :: "[pttrn, i, i] => i" ("(3\<Union>_\<in>_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

189 
"_INTER" :: "[pttrn, i, i] => i" ("(3\<Inter>_\<in>_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

190 
"_PROD" :: "[pttrn, i, i] => i" ("(3\<Pi>_\<in>_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

191 
"_SUM" :: "[pttrn, i, i] => i" ("(3\<Sigma>_\<in>_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

192 
"_lam" :: "[pttrn, i, i] => i" ("(3\<lambda>_\<in>_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

193 
"_Ball" :: "[pttrn, i, o] => o" ("(3\<forall>_\<in>_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

194 
"_Bex" :: "[pttrn, i, o] => o" ("(3\<exists>_\<in>_./ _)" 10) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

195 
"_Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>") 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

196 
"_pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>") 
6340  197 

2540  198 

14227  199 
finalconsts 
24826  200 
0 Pow Inf Union PrimReplace mem 
14227  201 

37405  202 
defs (* Bounded Quantifiers *) 
46820  203 
Ball_def: "Ball(A, P) == \<forall>x. x\<in>A \<longrightarrow> P(x)" 
14227  204 
Bex_def: "Bex(A, P) == \<exists>x. x\<in>A & P(x)" 
690  205 

46820  206 
subset_def: "A \<subseteq> B == \<forall>x\<in>A. x\<in>B" 
690  207 

3906  208 

41779  209 
axiomatization where 
0  210 

615  211 
(* ZF axioms  see Suppes p.238 
212 
Axioms for Union, Pow and Replace state existence only, 

213 
uniqueness is derivable using extensionality. *) 

0  214 

46820  215 
extension: "A = B <> A \<subseteq> B & B \<subseteq> A" and 
216 
Union_iff: "A \<in> \<Union>(C) <> (\<exists>B\<in>C. A\<in>B)" and 

217 
Pow_iff: "A \<in> Pow(B) <> A \<subseteq> B" and 

0  218 

615  219 
(*We may name this set, though it is not uniquely defined.*) 
41779  220 
infinity: "0\<in>Inf & (\<forall>y\<in>Inf. succ(y): Inf)" and 
0  221 

615  222 
(*This formulation facilitates case analysis on A.*) 
46820  223 
foundation: "A=0  (\<exists>x\<in>A. \<forall>y\<in>x. y\<notin>A)" and 
0  224 

615  225 
(*Schema axiom since predicate P is a higherorder variable*) 
46820  226 
replacement: "(\<forall>x\<in>A. \<forall>y z. P(x,y) & P(x,z) \<longrightarrow> y=z) ==> 
14227  227 
b \<in> PrimReplace(A,P) <> (\<exists>x\<in>A. P(x,b))" 
615  228 

14883  229 

690  230 
defs 
231 

615  232 
(* Derived form of replacement, restricting P to its functional part. 
233 
The resulting set (for functional P) is the same as with 

234 
PrimReplace, but the rules are simpler. *) 

0  235 

13780  236 
Replace_def: "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))" 
615  237 

238 
(* Functional form of replacement  analgous to ML's map functional *) 

0  239 

14227  240 
RepFun_def: "RepFun(A,f) == {y . x\<in>A, y=f(x)}" 
0  241 

615  242 
(* Separation and Pairing can be derived from the Replacement 
243 
and Powerset Axioms using the following definitions. *) 

0  244 

14227  245 
Collect_def: "Collect(A,P) == {y . x\<in>A, x=y & P(x)}" 
0  246 

615  247 
(*Unordered pairs (Upair) express binary union/intersection and cons; 
248 
set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*) 

0  249 

14227  250 
Upair_def: "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a)  (x=Pow(0) & y=b)}" 
46820  251 
cons_def: "cons(a,A) == Upair(a,a) \<union> A" 
13780  252 
succ_def: "succ(i) == cons(i, i)" 
615  253 

2872
ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset

254 
(* Difference, general intersection, binary union and small intersection *) 
ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset

255 

14227  256 
Diff_def: "A  B == { x\<in>A . ~(x\<in>B) }" 
46820  257 
Inter_def: "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}" 
258 
Un_def: "A \<union> B == \<Union>(Upair(A,B))" 

259 
Int_def: "A \<inter> B == \<Inter>(Upair(A,B))" 

2872
ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset

260 

14883  261 
(* definite descriptions *) 
46820  262 
the_def: "The(P) == \<Union>({y . x \<in> {0}, P(y)})" 
13780  263 
if_def: "if(P,a,b) == THE z. P & z=a  ~P & z=b" 
0  264 

615  265 
(* this "symmetric" definition works better than {{a}, {a,b}} *) 
13780  266 
Pair_def: "<a,b> == {{a,a}, {a,b}}" 
14227  267 
fst_def: "fst(p) == THE a. \<exists>b. p=<a,b>" 
268 
snd_def: "snd(p) == THE b. \<exists>a. p=<a,b>" 

13780  269 
split_def: "split(c) == %p. c(fst(p), snd(p))" 
14227  270 
Sigma_def: "Sigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {<x,y>}" 
0  271 

615  272 
(* Operations on relations *) 
0  273 

615  274 
(*converse of relation r, inverse of function*) 
14227  275 
converse_def: "converse(r) == {z. w\<in>r, \<exists>x y. w=<x,y> & z=<y,x>}" 
0  276 

14227  277 
domain_def: "domain(r) == {x. w\<in>r, \<exists>y. w=<x,y>}" 
13780  278 
range_def: "range(r) == domain(converse(r))" 
46820  279 
field_def: "field(r) == domain(r) \<union> range(r)" 
14227  280 
relation_def: "relation(r) == \<forall>z\<in>r. \<exists>x y. z = <x,y>" 
13780  281 
function_def: "function(r) == 
46820  282 
\<forall>x y. <x,y>:r \<longrightarrow> (\<forall>y'. <x,y'>:r \<longrightarrow> y=y')" 
283 
image_def: "r `` A == {y \<in> range(r) . \<exists>x\<in>A. <x,y> \<in> r}" 

13780  284 
vimage_def: "r `` A == converse(r)``A" 
0  285 

615  286 
(* Abstraction, application and Cartesian product of a family of sets *) 
0  287 

14227  288 
lam_def: "Lambda(A,b) == {<x,b(x)> . x\<in>A}" 
46820  289 
apply_def: "f`a == \<Union>(f``{a})" 
14227  290 
Pi_def: "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A<=domain(f) & function(f)}" 
0  291 

12891  292 
(* Restrict the relation r to the domain A *) 
46820  293 
restrict_def: "restrict(r,A) == {z \<in> r. \<exists>x\<in>A. \<exists>y. z = <x,y>}" 
13780  294 

295 

296 
subsection {* Substitution*} 

297 

298 
(*Useful examples: singletonI RS subst_elem, subst_elem RSN (2,IntI) *) 

14227  299 
lemma subst_elem: "[ b\<in>A; a=b ] ==> a\<in>A" 
13780  300 
by (erule ssubst, assumption) 
301 

302 

303 
subsection{*Bounded universal quantifier*} 

304 

14227  305 
lemma ballI [intro!]: "[ !!x. x\<in>A ==> P(x) ] ==> \<forall>x\<in>A. P(x)" 
13780  306 
by (simp add: Ball_def) 
307 

15481  308 
lemmas strip = impI allI ballI 
309 

14227  310 
lemma bspec [dest?]: "[ \<forall>x\<in>A. P(x); x: A ] ==> P(x)" 
13780  311 
by (simp add: Ball_def) 
312 

313 
(*Instantiates x first: better for automatic theorem proving?*) 

46820  314 
lemma rev_ballE [elim]: 
315 
"[ \<forall>x\<in>A. P(x); x\<notin>A ==> Q; P(x) ==> Q ] ==> Q" 

316 
by (simp add: Ball_def, blast) 

13780  317 

46820  318 
lemma ballE: "[ \<forall>x\<in>A. P(x); P(x) ==> Q; x\<notin>A ==> Q ] ==> Q" 
13780  319 
by blast 
320 

321 
(*Used in the datatype package*) 

14227  322 
lemma rev_bspec: "[ x: A; \<forall>x\<in>A. P(x) ] ==> P(x)" 
13780  323 
by (simp add: Ball_def) 
324 

46820  325 
(*Trival rewrite rule; @{term"(\<forall>x\<in>A.P)<>P"} holds only if A is nonempty!*) 
326 
lemma ball_triv [simp]: "(\<forall>x\<in>A. P) <> ((\<exists>x. x\<in>A) \<longrightarrow> P)" 

13780  327 
by (simp add: Ball_def) 
328 

329 
(*Congruence rule for rewriting*) 

330 
lemma ball_cong [cong]: 

14227  331 
"[ A=A'; !!x. x\<in>A' ==> P(x) <> P'(x) ] ==> (\<forall>x\<in>A. P(x)) <> (\<forall>x\<in>A'. P'(x))" 
13780  332 
by (simp add: Ball_def) 
333 

18845  334 
lemma atomize_ball: 
335 
"(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))" 

336 
by (simp only: Ball_def atomize_all atomize_imp) 

337 

338 
lemmas [symmetric, rulify] = atomize_ball 

339 
and [symmetric, defn] = atomize_ball 

340 

13780  341 

342 
subsection{*Bounded existential quantifier*} 

343 

14227  344 
lemma bexI [intro]: "[ P(x); x: A ] ==> \<exists>x\<in>A. P(x)" 
13780  345 
by (simp add: Bex_def, blast) 
346 

46820  347 
(*The best argument order when there is only one @{term"x\<in>A"}*) 
14227  348 
lemma rev_bexI: "[ x\<in>A; P(x) ] ==> \<exists>x\<in>A. P(x)" 
13780  349 
by blast 
350 

46820  351 
(*Not of the general form for such rules. The existential quanitifer becomes universal. *) 
14227  352 
lemma bexCI: "[ \<forall>x\<in>A. ~P(x) ==> P(a); a: A ] ==> \<exists>x\<in>A. P(x)" 
13780  353 
by blast 
354 

14227  355 
lemma bexE [elim!]: "[ \<exists>x\<in>A. P(x); !!x. [ x\<in>A; P(x) ] ==> Q ] ==> Q" 
13780  356 
by (simp add: Bex_def, blast) 
357 

46820  358 
(*We do not even have @{term"(\<exists>x\<in>A. True) <> True"} unless @{term"A" is nonempty!!*) 
14227  359 
lemma bex_triv [simp]: "(\<exists>x\<in>A. P) <> ((\<exists>x. x\<in>A) & P)" 
13780  360 
by (simp add: Bex_def) 
361 

362 
lemma bex_cong [cong]: 

46820  363 
"[ A=A'; !!x. x\<in>A' ==> P(x) <> P'(x) ] 
14227  364 
==> (\<exists>x\<in>A. P(x)) <> (\<exists>x\<in>A'. P'(x))" 
13780  365 
by (simp add: Bex_def cong: conj_cong) 
366 

367 

368 

369 
subsection{*Rules for subsets*} 

370 

371 
lemma subsetI [intro!]: 

46820  372 
"(!!x. x\<in>A ==> x\<in>B) ==> A \<subseteq> B" 
373 
by (simp add: subset_def) 

13780  374 

375 
(*Rule in Modus Ponens style [was called subsetE] *) 

46820  376 
lemma subsetD [elim]: "[ A \<subseteq> B; c\<in>A ] ==> c\<in>B" 
13780  377 
apply (unfold subset_def) 
378 
apply (erule bspec, assumption) 

379 
done 

380 

381 
(*Classical elimination rule*) 

382 
lemma subsetCE [elim]: 

46820  383 
"[ A \<subseteq> B; c\<notin>A ==> P; c\<in>B ==> P ] ==> P" 
384 
by (simp add: subset_def, blast) 

13780  385 

386 
(*Sometimes useful with premises in this order*) 

14227  387 
lemma rev_subsetD: "[ c\<in>A; A<=B ] ==> c\<in>B" 
13780  388 
by blast 
389 

46820  390 
lemma contra_subsetD: "[ A \<subseteq> B; c \<notin> B ] ==> c \<notin> A" 
13780  391 
by blast 
392 

46820  393 
lemma rev_contra_subsetD: "[ c \<notin> B; A \<subseteq> B ] ==> c \<notin> A" 
13780  394 
by blast 
395 

46820  396 
lemma subset_refl [simp]: "A \<subseteq> A" 
13780  397 
by blast 
398 

399 
lemma subset_trans: "[ A<=B; B<=C ] ==> A<=C" 

400 
by blast 

401 

402 
(*Useful for proving A<=B by rewriting in some cases*) 

46820  403 
lemma subset_iff: 
404 
"A<=B <> (\<forall>x. x\<in>A \<longrightarrow> x\<in>B)" 

13780  405 
apply (unfold subset_def Ball_def) 
406 
apply (rule iff_refl) 

407 
done 

408 

409 

410 
subsection{*Rules for equality*} 

411 

412 
(*Antisymmetry of the subset relation*) 

46820  413 
lemma equalityI [intro]: "[ A \<subseteq> B; B \<subseteq> A ] ==> A = B" 
414 
by (rule extension [THEN iffD2], rule conjI) 

13780  415 

416 

14227  417 
lemma equality_iffI: "(!!x. x\<in>A <> x\<in>B) ==> A = B" 
13780  418 
by (rule equalityI, blast+) 
419 

45602  420 
lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1] 
421 
lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2] 

13780  422 

423 
lemma equalityE: "[ A = B; [ A<=B; B<=A ] ==> P ] ==> P" 

46820  424 
by (blast dest: equalityD1 equalityD2) 
13780  425 

426 
lemma equalityCE: 

46820  427 
"[ A = B; [ c\<in>A; c\<in>B ] ==> P; [ c\<notin>A; c\<notin>B ] ==> P ] ==> P" 
428 
by (erule equalityE, blast) 

13780  429 

27702  430 
lemma equality_iffD: 
46820  431 
"A = B ==> (!!x. x \<in> A <> x \<in> B)" 
27702  432 
by auto 
433 

13780  434 

435 
subsection{*Rules for Replace  the derived form of replacement*} 

436 

46820  437 
lemma Replace_iff: 
438 
"b \<in> {y. x\<in>A, P(x,y)} <> (\<exists>x\<in>A. P(x,b) & (\<forall>y. P(x,y) \<longrightarrow> y=b))" 

13780  439 
apply (unfold Replace_def) 
440 
apply (rule replacement [THEN iff_trans], blast+) 

441 
done 

442 

443 
(*Introduction; there must be a unique y such that P(x,y), namely y=b. *) 

46820  444 
lemma ReplaceI [intro]: 
445 
"[ P(x,b); x: A; !!y. P(x,y) ==> y=b ] ==> 

446 
b \<in> {y. x\<in>A, P(x,y)}" 

447 
by (rule Replace_iff [THEN iffD2], blast) 

13780  448 

449 
(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *) 

46820  450 
lemma ReplaceE: 
451 
"[ b \<in> {y. x\<in>A, P(x,y)}; 

452 
!!x. [ x: A; P(x,b); \<forall>y. P(x,y)\<longrightarrow>y=b ] ==> R 

13780  453 
] ==> R" 
454 
by (rule Replace_iff [THEN iffD1, THEN bexE], simp+) 

455 

456 
(*As above but without the (generally useless) 3rd assumption*) 

46820  457 
lemma ReplaceE2 [elim!]: 
458 
"[ b \<in> {y. x\<in>A, P(x,y)}; 

459 
!!x. [ x: A; P(x,b) ] ==> R 

13780  460 
] ==> R" 
46820  461 
by (erule ReplaceE, blast) 
13780  462 

463 
lemma Replace_cong [cong]: 

46820  464 
"[ A=B; !!x y. x\<in>B ==> P(x,y) <> Q(x,y) ] ==> 
13780  465 
Replace(A,P) = Replace(B,Q)" 
46820  466 
apply (rule equality_iffI) 
467 
apply (simp add: Replace_iff) 

13780  468 
done 
469 

470 

471 
subsection{*Rules for RepFun*} 

472 

46820  473 
lemma RepFunI: "a \<in> A ==> f(a) \<in> {f(x). x\<in>A}" 
13780  474 
by (simp add: RepFun_def Replace_iff, blast) 
475 

476 
(*Useful for coinduction proofs*) 

46820  477 
lemma RepFun_eqI [intro]: "[ b=f(a); a \<in> A ] ==> b \<in> {f(x). x\<in>A}" 
13780  478 
apply (erule ssubst) 
479 
apply (erule RepFunI) 

480 
done 

481 

482 
lemma RepFunE [elim!]: 

46820  483 
"[ b \<in> {f(x). x\<in>A}; 
484 
!!x.[ x\<in>A; b=f(x) ] ==> P ] ==> 

13780  485 
P" 
46820  486 
by (simp add: RepFun_def Replace_iff, blast) 
13780  487 

46820  488 
lemma RepFun_cong [cong]: 
14227  489 
"[ A=B; !!x. x\<in>B ==> f(x)=g(x) ] ==> RepFun(A,f) = RepFun(B,g)" 
13780  490 
by (simp add: RepFun_def) 
491 

46820  492 
lemma RepFun_iff [simp]: "b \<in> {f(x). x\<in>A} <> (\<exists>x\<in>A. b=f(x))" 
13780  493 
by (unfold Bex_def, blast) 
494 

14227  495 
lemma triv_RepFun [simp]: "{x. x\<in>A} = A" 
13780  496 
by blast 
497 

498 

499 
subsection{*Rules for Collect  forming a subset by separation*} 

500 

501 
(*Separation is derivable from Replacement*) 

46820  502 
lemma separation [simp]: "a \<in> {x\<in>A. P(x)} <> a\<in>A & P(a)" 
13780  503 
by (unfold Collect_def, blast) 
504 

46820  505 
lemma CollectI [intro!]: "[ a\<in>A; P(a) ] ==> a \<in> {x\<in>A. P(x)}" 
13780  506 
by simp 
507 

46820  508 
lemma CollectE [elim!]: "[ a \<in> {x\<in>A. P(x)}; [ a\<in>A; P(a) ] ==> R ] ==> R" 
13780  509 
by simp 
510 

46820  511 
lemma CollectD1: "a \<in> {x\<in>A. P(x)} ==> a\<in>A" 
13780  512 
by (erule CollectE, assumption) 
513 

46820  514 
lemma CollectD2: "a \<in> {x\<in>A. P(x)} ==> P(a)" 
13780  515 
by (erule CollectE, assumption) 
516 

517 
lemma Collect_cong [cong]: 

46820  518 
"[ A=B; !!x. x\<in>B ==> P(x) <> Q(x) ] 
13780  519 
==> Collect(A, %x. P(x)) = Collect(B, %x. Q(x))" 
520 
by (simp add: Collect_def) 

521 

522 

523 
subsection{*Rules for Unions*} 

524 

525 
declare Union_iff [simp] 

526 

527 
(*The order of the premises presupposes that C is rigid; A may be flexible*) 

46820  528 
lemma UnionI [intro]: "[ B: C; A: B ] ==> A: \<Union>(C)" 
13780  529 
by (simp, blast) 
530 

46820  531 
lemma UnionE [elim!]: "[ A \<in> \<Union>(C); !!B.[ A: B; B: C ] ==> R ] ==> R" 
13780  532 
by (simp, blast) 
533 

534 

535 
subsection{*Rules for Unions of families*} 

46820  536 
(* @{term"\<Union>x\<in>A. B(x)"} abbreviates @{term"\<Union>({B(x). x\<in>A})"} *) 
13780  537 

46820  538 
lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B(x)) <> (\<exists>x\<in>A. b \<in> B(x))" 
13780  539 
by (simp add: Bex_def, blast) 
540 

541 
(*The order of the premises presupposes that A is rigid; b may be flexible*) 

14227  542 
lemma UN_I: "[ a: A; b: B(a) ] ==> b: (\<Union>x\<in>A. B(x))" 
13780  543 
by (simp, blast) 
544 

545 

46820  546 
lemma UN_E [elim!]: 
547 
"[ b \<in> (\<Union>x\<in>A. B(x)); !!x.[ x: A; b: B(x) ] ==> R ] ==> R" 

548 
by blast 

13780  549 

46820  550 
lemma UN_cong: 
14227  551 
"[ A=B; !!x. x\<in>B ==> C(x)=D(x) ] ==> (\<Union>x\<in>A. C(x)) = (\<Union>x\<in>B. D(x))" 
46820  552 
by simp 
13780  553 

554 

46820  555 
(*No "Addcongs [UN_cong]" because @{term\<Union>} is a combination of constants*) 
13780  556 

557 
(* UN_E appears before UnionE so that it is tried first, to avoid expensive 

558 
calls to hyp_subst_tac. Cannot include UN_I as it is unsafe: would enlarge 

559 
the search space.*) 

560 

561 

562 
subsection{*Rules for the empty set*} 

563 

46820  564 
(*The set @{term"{x\<in>0. False}"} is empty; by foundation it equals 0 
13780  565 
See Suppes, page 21.*) 
46820  566 
lemma not_mem_empty [simp]: "a \<notin> 0" 
13780  567 
apply (cut_tac foundation) 
568 
apply (best dest: equalityD2) 

569 
done 

570 

45602  571 
lemmas emptyE [elim!] = not_mem_empty [THEN notE] 
13780  572 

573 

46820  574 
lemma empty_subsetI [simp]: "0 \<subseteq> A" 
575 
by blast 

13780  576 

14227  577 
lemma equals0I: "[ !!y. y\<in>A ==> False ] ==> A=0" 
13780  578 
by blast 
579 

46820  580 
lemma equals0D [dest]: "A=0 ==> a \<notin> A" 
13780  581 
by blast 
582 

583 
declare sym [THEN equals0D, dest] 

584 

46820  585 
lemma not_emptyI: "a\<in>A ==> A \<noteq> 0" 
13780  586 
by blast 
587 

46820  588 
lemma not_emptyE: "[ A \<noteq> 0; !!x. x\<in>A ==> R ] ==> R" 
13780  589 
by blast 
590 

591 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

592 
subsection{*Rules for Inter*} 
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

593 

a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

594 
(*Not obviously useful for proving InterI, InterD, InterE*) 
46820  595 
lemma Inter_iff: "A \<in> \<Inter>(C) <> (\<forall>x\<in>C. A: x) & C\<noteq>0" 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

596 
by (simp add: Inter_def Ball_def, blast) 
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

597 

a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

598 
(* Intersection is wellbehaved only if the family is nonempty! *) 
46820  599 
lemma InterI [intro!]: 
600 
"[ !!x. x: C ==> A: x; C\<noteq>0 ] ==> A \<in> \<Inter>(C)" 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

601 
by (simp add: Inter_iff) 
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

602 

a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

603 
(*A "destruct" rule  every B in C contains A as an element, but 
14227  604 
A\<in>B can hold when B\<in>C does not! This rule is analogous to "spec". *) 
46820  605 
lemma InterD [elim, Pure.elim]: "[ A \<in> \<Inter>(C); B \<in> C ] ==> A \<in> B" 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

606 
by (unfold Inter_def, blast) 
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

607 

46820  608 
(*"Classical" elimination rule  does not require exhibiting @{term"B\<in>C"} *) 
609 
lemma InterE [elim]: 

610 
"[ A \<in> \<Inter>(C); B\<notin>C ==> R; A\<in>B ==> R ] ==> R" 

611 
by (simp add: Inter_def, blast) 

612 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

613 

a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

614 
subsection{*Rules for Intersections of families*} 
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

615 

46820  616 
(* @{term"\<Inter>x\<in>A. B(x)"} abbreviates @{term"\<Inter>({B(x). x\<in>A})"} *) 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

617 

46820  618 
lemma INT_iff: "b \<in> (\<Inter>x\<in>A. B(x)) <> (\<forall>x\<in>A. b \<in> B(x)) & A\<noteq>0" 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

619 
by (force simp add: Inter_def) 
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

620 

14227  621 
lemma INT_I: "[ !!x. x: A ==> b: B(x); A\<noteq>0 ] ==> b: (\<Inter>x\<in>A. B(x))" 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

622 
by blast 
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

623 

46820  624 
lemma INT_E: "[ b \<in> (\<Inter>x\<in>A. B(x)); a: A ] ==> b \<in> B(a)" 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

625 
by blast 
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

626 

a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

627 
lemma INT_cong: 
14227  628 
"[ A=B; !!x. x\<in>B ==> C(x)=D(x) ] ==> (\<Inter>x\<in>A. C(x)) = (\<Inter>x\<in>B. D(x))" 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

629 
by simp 
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

630 

46820  631 
(*No "Addcongs [INT_cong]" because @{term\<Inter>} is a combination of constants*) 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

632 

a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

633 

13780  634 
subsection{*Rules for Powersets*} 
635 

46820  636 
lemma PowI: "A \<subseteq> B ==> A \<in> Pow(B)" 
13780  637 
by (erule Pow_iff [THEN iffD2]) 
638 

14227  639 
lemma PowD: "A \<in> Pow(B) ==> A<=B" 
13780  640 
by (erule Pow_iff [THEN iffD1]) 
641 

642 
declare Pow_iff [iff] 

643 

46820  644 
lemmas Pow_bottom = empty_subsetI [THEN PowI] {* @{term"0 \<in> Pow(B)"} *} 
645 
lemmas Pow_top = subset_refl [THEN PowI] {* @{term"A \<in> Pow(A)"} *} 

13780  646 

647 

648 
subsection{*Cantor's Theorem: There is no surjection from a set to its powerset.*} 

649 

46820  650 
(*The search is undirected. Allowing redundant introduction rules may 
13780  651 
make it diverge. Variable b represents ANY map, such as 
14227  652 
(lam x\<in>A.b(x)): A>Pow(A). *) 
46820  653 
lemma cantor: "\<exists>S \<in> Pow(A). \<forall>x\<in>A. b(x) \<noteq> S" 
13780  654 
by (best elim!: equalityCE del: ReplaceI RepFun_eqI) 
655 

0  656 
end 
657 