author  wenzelm 
Fri, 16 Sep 2016 21:28:09 +0200  
changeset 63901  4ce989e962e0 
parent 62149  a02b79ef2339 
child 65386  e3fb3036a00e 
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 

62149  6 
section \<open>ZermeloFraenkel Set Theory\<close> 
0  7 

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

8 
theory ZF 
48462
424fd5364f15
clarified "this_name" vs. former "reset" feature  imitate the latter by loading other session sources directly;
wenzelm
parents:
46972
diff
changeset

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

10 
begin 
0  11 

62149  12 
subsection \<open>Signature\<close> 
13 

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

14 
declare [[eta_contract = false]] 
23168  15 

14076  16 
typedecl i 
55380
4de48353034e
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
48733
diff
changeset

17 
instance i :: "term" .. 
0  18 

62149  19 
axiomatization mem :: "[i, i] \<Rightarrow> o" (infixl "\<in>" 50) \<comment> \<open>membership relation\<close> 
20 
and zero :: "i" ("0") \<comment> \<open>the empty set\<close> 

21 
and Pow :: "i \<Rightarrow> i" \<comment> \<open>power sets\<close> 

22 
and Inf :: "i" \<comment> \<open>infinite set\<close> 

23 
and Union :: "i \<Rightarrow> i" ("\<Union>_" [90] 90) 

24 
and PrimReplace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i" 

25 

26 
abbreviation not_mem :: "[i, i] \<Rightarrow> o" (infixl "\<notin>" 50) \<comment> \<open>negated membership relation\<close> 

27 
where "x \<notin> y \<equiv> \<not> (x \<in> y)" 

28 

29 

30 
subsection \<open>Bounded Quantifiers\<close> 

31 

32 
definition Ball :: "[i, i \<Rightarrow> o] \<Rightarrow> o" 

33 
where "Ball(A, P) \<equiv> \<forall>x. x\<in>A \<longrightarrow> P(x)" 

0  34 

62149  35 
definition Bex :: "[i, i \<Rightarrow> o] \<Rightarrow> o" 
36 
where "Bex(A, P) \<equiv> \<exists>x. x\<in>A \<and> P(x)" 

0  37 

62149  38 
syntax 
39 
"_Ball" :: "[pttrn, i, o] \<Rightarrow> o" ("(3\<forall>_\<in>_./ _)" 10) 

40 
"_Bex" :: "[pttrn, i, o] \<Rightarrow> o" ("(3\<exists>_\<in>_./ _)" 10) 

41 
translations 

42 
"\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball(A, \<lambda>x. P)" 

43 
"\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex(A, \<lambda>x. P)" 

44 

45 

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

47 

48 
(* Derived form of replacement, restricting P to its functional part. 

49 
The resulting set (for functional P) is the same as with 

50 
PrimReplace, but the rules are simpler. *) 

51 
definition Replace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i" 

63901  52 
where "Replace(A,P) == PrimReplace(A, %x y. (\<exists>!z. P(x,z)) & P(x,y))" 
0  53 

62149  54 
syntax 
55 
"_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})") 

56 
translations 

57 
"{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)" 

58 

59 

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

61 

62 
definition RepFun :: "[i, i \<Rightarrow> i] \<Rightarrow> i" 

63 
where "RepFun(A,f) == {y . x\<in>A, y=f(x)}" 

64 

65 
syntax 

66 
"_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \<in> _})" [51,0,51]) 

67 
translations 

68 
"{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)" 

69 

0  70 

62149  71 
(* Separation and Pairing can be derived from the Replacement 
72 
and Powerset Axioms using the following definitions. *) 

73 
definition Collect :: "[i, i \<Rightarrow> o] \<Rightarrow> i" 

74 
where "Collect(A,P) == {y . x\<in>A, x=y & P(x)}" 

75 

76 
syntax 

77 
"_Collect" :: "[pttrn, i, o] \<Rightarrow> i" ("(1{_ \<in> _ ./ _})") 

78 
translations 

79 
"{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)" 

80 

6068  81 

62149  82 
subsection \<open>General union and intersection\<close> 
83 

84 
definition Inter :: "i => i" ("\<Inter>_" [90] 90) 

85 
where "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}" 

86 

87 
syntax 

88 
"_UNION" :: "[pttrn, i, i] => i" ("(3\<Union>_\<in>_./ _)" 10) 

89 
"_INTER" :: "[pttrn, i, i] => i" ("(3\<Inter>_\<in>_./ _)" 10) 

90 
translations 

91 
"\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})" 

92 
"\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})" 

6068  93 

94 

62149  95 
subsection \<open>Finite sets and binary operations\<close> 
96 

97 
(*Unordered pairs (Upair) express binary union/intersection and cons; 

98 
set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*) 

99 

100 
definition Upair :: "[i, i] => i" 

101 
where "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a)  (x=Pow(0) & y=b)}" 

0  102 

62149  103 
definition Subset :: "[i, i] \<Rightarrow> o" (infixl "\<subseteq>" 50) \<comment> \<open>subset relation\<close> 
104 
where subset_def: "A \<subseteq> B \<equiv> \<forall>x\<in>A. x\<in>B" 

105 

106 
definition Diff :: "[i, i] \<Rightarrow> i" (infixl "" 65) \<comment> \<open>set difference\<close> 

107 
where "A  B == { x\<in>A . ~(x\<in>B) }" 

0  108 

62149  109 
definition Un :: "[i, i] \<Rightarrow> i" (infixl "\<union>" 65) \<comment> \<open>binary union\<close> 
110 
where "A \<union> B == \<Union>(Upair(A,B))" 

111 

112 
definition Int :: "[i, i] \<Rightarrow> i" (infixl "\<inter>" 70) \<comment> \<open>binary intersection\<close> 

113 
where "A \<inter> B == \<Inter>(Upair(A,B))" 

0  114 

62149  115 
definition cons :: "[i, i] => i" 
116 
where "cons(a,A) == Upair(a,a) \<union> A" 

117 

118 
definition succ :: "i => i" 

119 
where "succ(i) == cons(i, i)" 

0  120 

62149  121 
nonterminal "is" 
122 
syntax 

123 
"" :: "i \<Rightarrow> is" ("_") 

124 
"_Enum" :: "[i, is] \<Rightarrow> is" ("_,/ _") 

125 
"_Finset" :: "is \<Rightarrow> i" ("{(_)}") 

126 
translations 

127 
"{x, xs}" == "CONST cons(x, {xs})" 

128 
"{x}" == "CONST cons(x, 0)" 

129 

130 

131 
subsection \<open>Axioms\<close> 

132 

133 
(* ZF axioms  see Suppes p.238 

134 
Axioms for Union, Pow and Replace state existence only, 

135 
uniqueness is derivable using extensionality. *) 

48733
18e76e2db6d4
proper axiomatization of "mem"  do not leave it formally unspecified;
wenzelm
parents:
48462
diff
changeset

136 

18e76e2db6d4
proper axiomatization of "mem"  do not leave it formally unspecified;
wenzelm
parents:
48462
diff
changeset

137 
axiomatization 
62149  138 
where 
139 
extension: "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" and 

140 
Union_iff: "A \<in> \<Union>(C) \<longleftrightarrow> (\<exists>B\<in>C. A\<in>B)" and 

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

24826  142 

62149  143 
(*We may name this set, though it is not uniquely defined.*) 
144 
infinity: "0 \<in> Inf \<and> (\<forall>y\<in>Inf. succ(y) \<in> Inf)" and 

24826  145 

62149  146 
(*This formulation facilitates case analysis on A.*) 
147 
foundation: "A = 0 \<or> (\<exists>x\<in>A. \<forall>y\<in>x. y\<notin>A)" and 

148 

149 
(*Schema axiom since predicate P is a higherorder variable*) 

150 
replacement: "(\<forall>x\<in>A. \<forall>y z. P(x,y) \<and> P(x,z) \<longrightarrow> y = z) \<Longrightarrow> 

151 
b \<in> PrimReplace(A,P) \<longleftrightarrow> (\<exists>x\<in>A. P(x,b))" 

0  152 

153 

62149  154 
subsection \<open>Definite descriptions  via Replace over the set "1"\<close> 
155 

156 
definition The :: "(i \<Rightarrow> o) \<Rightarrow> i" (binder "THE " 10) 

157 
where the_def: "The(P) == \<Union>({y . x \<in> {0}, P(y)})" 

615  158 

62149  159 
definition If :: "[o, i, i] \<Rightarrow> i" ("(if (_)/ then (_)/ else (_))" [10] 10) 
160 
where if_def: "if P then a else b == THE z. P & z=a  ~P & z=b" 

161 

162 
abbreviation (input) 

163 
old_if :: "[o, i, i] => i" ("if '(_,_,_')") 

164 
where "if(P,a,b) == If(P,a,b)" 

165 

166 

167 
subsection \<open>Ordered Pairing\<close> 

24826  168 

62149  169 
(* this "symmetric" definition works better than {{a}, {a,b}} *) 
170 
definition Pair :: "[i, i] => i" 

171 
where "Pair(a,b) == {{a,a}, {a,b}}" 

172 

173 
definition fst :: "i \<Rightarrow> i" 

174 
where "fst(p) == THE a. \<exists>b. p = Pair(a, b)" 

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

175 

62149  176 
definition snd :: "i \<Rightarrow> i" 
177 
where "snd(p) == THE b. \<exists>a. p = Pair(a, b)" 

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

178 

62149  179 
definition split :: "[[i, i] \<Rightarrow> 'a, i] \<Rightarrow> 'a::{}" \<comment> \<open>for patternmatching\<close> 
180 
where "split(c) == \<lambda>p. c(fst(p), snd(p))" 

181 

182 
(* Patterns  extends predefined type "pttrn" used in abstractions *) 

183 
nonterminal patterns 

184 
syntax 

61979  185 
"_pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>") 
13144  186 
"" :: "pttrn => patterns" ("_") 
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset

187 
"_patterns" :: "[pttrn, patterns] => patterns" ("_,/_") 
62149  188 
"_Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>") 
0  189 
translations 
61979  190 
"\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>" 
191 
"\<langle>x, y\<rangle>" == "CONST Pair(x, y)" 

192 
"\<lambda>\<langle>x,y,zs\<rangle>.b" == "CONST split(\<lambda>x \<langle>y,zs\<rangle>.b)" 

193 
"\<lambda>\<langle>x,y\<rangle>.b" == "CONST split(\<lambda>x y. b)" 

2286  194 

62149  195 
definition Sigma :: "[i, i \<Rightarrow> i] \<Rightarrow> i" 
196 
where "Sigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {\<langle>x,y\<rangle>}" 

197 

198 
abbreviation cart_prod :: "[i, i] => i" (infixr "\<times>" 80) \<comment> \<open>Cartesian product\<close> 

199 
where "A \<times> B \<equiv> Sigma(A, \<lambda>_. B)" 

200 

201 

202 
subsection \<open>Relations and Functions\<close> 

203 

204 
(*converse of relation r, inverse of function*) 

205 
definition converse :: "i \<Rightarrow> i" 

206 
where "converse(r) == {z. w\<in>r, \<exists>x y. w=\<langle>x,y\<rangle> \<and> z=\<langle>y,x\<rangle>}" 

207 

208 
definition domain :: "i \<Rightarrow> i" 

209 
where "domain(r) == {x. w\<in>r, \<exists>y. w=\<langle>x,y\<rangle>}" 

210 

211 
definition range :: "i \<Rightarrow> i" 

212 
where "range(r) == domain(converse(r))" 

213 

214 
definition field :: "i \<Rightarrow> i" 

215 
where "field(r) == domain(r) \<union> range(r)" 

216 

217 
definition relation :: "i \<Rightarrow> o" \<comment> \<open>recognizes sets of pairs\<close> 

218 
where "relation(r) == \<forall>z\<in>r. \<exists>x y. z = \<langle>x,y\<rangle>" 

219 

220 
definition function :: "i \<Rightarrow> o" \<comment> \<open>recognizes functions; can have nonpairs\<close> 

221 
where "function(r) == \<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> (\<forall>y'. \<langle>x,y'\<rangle> \<in> r \<longrightarrow> y = y')" 

222 

223 
definition Image :: "[i, i] \<Rightarrow> i" (infixl "``" 90) \<comment> \<open>image\<close> 

224 
where image_def: "r `` A == {y \<in> range(r). \<exists>x\<in>A. \<langle>x,y\<rangle> \<in> r}" 

225 

226 
definition vimage :: "[i, i] \<Rightarrow> i" (infixl "``" 90) \<comment> \<open>inverse image\<close> 

227 
where vimage_def: "r `` A == converse(r)``A" 

228 

229 
(* Restrict the relation r to the domain A *) 

230 
definition restrict :: "[i, i] \<Rightarrow> i" 

231 
where "restrict(r,A) == {z \<in> r. \<exists>x\<in>A. \<exists>y. z = \<langle>x,y\<rangle>}" 

232 

233 

234 
(* Abstraction, application and Cartesian product of a family of sets *) 

235 

236 
definition Lambda :: "[i, i \<Rightarrow> i] \<Rightarrow> i" 

237 
where lam_def: "Lambda(A,b) == {\<langle>x,b(x)\<rangle>. x\<in>A}" 

238 

239 
definition "apply" :: "[i, i] \<Rightarrow> i" (infixl "`" 90) \<comment> \<open>function application\<close> 

240 
where "f`a == \<Union>(f``{a})" 

241 

242 
definition Pi :: "[i, i \<Rightarrow> i] \<Rightarrow> i" 

243 
where "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A\<subseteq>domain(f) & function(f)}" 

244 

245 
abbreviation function_space :: "[i, i] \<Rightarrow> i" (infixr ">" 60) \<comment> \<open>function space\<close> 

246 
where "A > B \<equiv> Pi(A, \<lambda>_. B)" 

247 

248 

249 
(* binder syntax *) 

250 

251 
syntax 

252 
"_PROD" :: "[pttrn, i, i] => i" ("(3\<Prod>_\<in>_./ _)" 10) 

253 
"_SUM" :: "[pttrn, i, i] => i" ("(3\<Sum>_\<in>_./ _)" 10) 

254 
"_lam" :: "[pttrn, i, i] => i" ("(3\<lambda>_\<in>_./ _)" 10) 

255 
translations 

256 
"\<Prod>x\<in>A. B" == "CONST Pi(A, \<lambda>x. B)" 

257 
"\<Sum>x\<in>A. B" == "CONST Sigma(A, \<lambda>x. B)" 

258 
"\<lambda>x\<in>A. f" == "CONST Lambda(A, \<lambda>x. f)" 

259 

260 

261 
subsection \<open>ASCII syntax\<close> 

0  262 

61979  263 
notation (ASCII) 
264 
cart_prod (infixr "*" 80) and 

265 
Int (infixl "Int" 70) and 

266 
Un (infixl "Un" 65) and 

24826  267 
function_space (infixr "\<rightarrow>" 60) and 
61979  268 
Subset (infixl "<=" 50) and 
269 
mem (infixl ":" 50) and 

270 
not_mem (infixl "~:" 50) 

24826  271 

61979  272 
syntax (ASCII) 
62149  273 
"_Ball" :: "[pttrn, i, o] => o" ("(3ALL _:_./ _)" 10) 
274 
"_Bex" :: "[pttrn, i, o] => o" ("(3EX _:_./ _)" 10) 

61979  275 
"_Collect" :: "[pttrn, i, o] => i" ("(1{_: _ ./ _})") 
276 
"_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})") 

277 
"_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _: _})" [51,0,51]) 

278 
"_UNION" :: "[pttrn, i, i] => i" ("(3UN _:_./ _)" 10) 

279 
"_INTER" :: "[pttrn, i, i] => i" ("(3INT _:_./ _)" 10) 

280 
"_PROD" :: "[pttrn, i, i] => i" ("(3PROD _:_./ _)" 10) 

281 
"_SUM" :: "[pttrn, i, i] => i" ("(3SUM _:_./ _)" 10) 

282 
"_lam" :: "[pttrn, i, i] => i" ("(3lam _:_./ _)" 10) 

283 
"_Tuple" :: "[i, is] => i" ("<(_,/ _)>") 

284 
"_pattern" :: "patterns => pttrn" ("<_>") 

2540  285 

13780  286 

60770  287 
subsection \<open>Substitution\<close> 
13780  288 

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

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

293 

60770  294 
subsection\<open>Bounded universal quantifier\<close> 
13780  295 

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

15481  299 
lemmas strip = impI allI ballI 
300 

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

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

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

307 
by (simp add: Ball_def, blast) 

13780  308 

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

312 
(*Used in the datatype package*) 

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

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

13780  318 
by (simp add: Ball_def) 
319 

320 
(*Congruence rule for rewriting*) 

321 
lemma ball_cong [cong]: 

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

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

327 
by (simp only: Ball_def atomize_all atomize_imp) 

328 

329 
lemmas [symmetric, rulify] = atomize_ball 

330 
and [symmetric, defn] = atomize_ball 

331 

13780  332 

60770  333 
subsection\<open>Bounded existential quantifier\<close> 
13780  334 

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

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

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

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

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

353 
lemma bex_cong [cong]: 

46820  354 
"[ A=A'; !!x. x\<in>A' ==> P(x) <> P'(x) ] 
14227  355 
==> (\<exists>x\<in>A. P(x)) <> (\<exists>x\<in>A'. P'(x))" 
13780  356 
by (simp add: Bex_def cong: conj_cong) 
357 

358 

359 

60770  360 
subsection\<open>Rules for subsets\<close> 
13780  361 

362 
lemma subsetI [intro!]: 

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

13780  365 

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

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

370 
done 

371 

372 
(*Classical elimination rule*) 

373 
lemma subsetCE [elim]: 

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

13780  376 

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

14227  378 
lemma rev_subsetD: "[ c\<in>A; A<=B ] ==> c\<in>B" 
13780  379 
by blast 
380 

46820  381 
lemma contra_subsetD: "[ A \<subseteq> B; c \<notin> B ] ==> c \<notin> A" 
13780  382 
by blast 
383 

46820  384 
lemma rev_contra_subsetD: "[ c \<notin> B; A \<subseteq> B ] ==> c \<notin> A" 
13780  385 
by blast 
386 

46820  387 
lemma subset_refl [simp]: "A \<subseteq> A" 
13780  388 
by blast 
389 

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

391 
by blast 

392 

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

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

13780  396 
apply (unfold subset_def Ball_def) 
397 
apply (rule iff_refl) 

398 
done 

399 

60770  400 
text\<open>For calculations\<close> 
46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46820
diff
changeset

401 
declare subsetD [trans] rev_subsetD [trans] subset_trans [trans] 
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46820
diff
changeset

402 

13780  403 

60770  404 
subsection\<open>Rules for equality\<close> 
13780  405 

406 
(*Antisymmetry of the subset relation*) 

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

13780  409 

410 

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

45602  414 
lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1] 
415 
lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2] 

13780  416 

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

46820  418 
by (blast dest: equalityD1 equalityD2) 
13780  419 

420 
lemma equalityCE: 

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

13780  423 

27702  424 
lemma equality_iffD: 
46820  425 
"A = B ==> (!!x. x \<in> A <> x \<in> B)" 
27702  426 
by auto 
427 

13780  428 

60770  429 
subsection\<open>Rules for Replace  the derived form of replacement\<close> 
13780  430 

46820  431 
lemma Replace_iff: 
432 
"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  433 
apply (unfold Replace_def) 
434 
apply (rule replacement [THEN iff_trans], blast+) 

435 
done 

436 

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

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

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

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

13780  442 

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

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

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

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

449 

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

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

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

13780  454 
] ==> R" 
46820  455 
by (erule ReplaceE, blast) 
13780  456 

457 
lemma Replace_cong [cong]: 

46820  458 
"[ A=B; !!x y. x\<in>B ==> P(x,y) <> Q(x,y) ] ==> 
13780  459 
Replace(A,P) = Replace(B,Q)" 
46820  460 
apply (rule equality_iffI) 
461 
apply (simp add: Replace_iff) 

13780  462 
done 
463 

464 

60770  465 
subsection\<open>Rules for RepFun\<close> 
13780  466 

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

470 
(*Useful for coinduction proofs*) 

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

474 
done 

475 

476 
lemma RepFunE [elim!]: 

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

13780  479 
P" 
46820  480 
by (simp add: RepFun_def Replace_iff, blast) 
13780  481 

46820  482 
lemma RepFun_cong [cong]: 
14227  483 
"[ A=B; !!x. x\<in>B ==> f(x)=g(x) ] ==> RepFun(A,f) = RepFun(B,g)" 
13780  484 
by (simp add: RepFun_def) 
485 

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

14227  489 
lemma triv_RepFun [simp]: "{x. x\<in>A} = A" 
13780  490 
by blast 
491 

492 

60770  493 
subsection\<open>Rules for Collect  forming a subset by separation\<close> 
13780  494 

495 
(*Separation is derivable from Replacement*) 

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

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

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

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

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

511 
lemma Collect_cong [cong]: 

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

515 

516 

60770  517 
subsection\<open>Rules for Unions\<close> 
13780  518 

519 
declare Union_iff [simp] 

520 

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

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

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

528 

60770  529 
subsection\<open>Rules for Unions of families\<close> 
46820  530 
(* @{term"\<Union>x\<in>A. B(x)"} abbreviates @{term"\<Union>({B(x). x\<in>A})"} *) 
13780  531 

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

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

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

539 

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

542 
by blast 

13780  543 

46820  544 
lemma UN_cong: 
14227  545 
"[ A=B; !!x. x\<in>B ==> C(x)=D(x) ] ==> (\<Union>x\<in>A. C(x)) = (\<Union>x\<in>B. D(x))" 
46820  546 
by simp 
13780  547 

548 

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

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

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

553 
the search space.*) 

554 

555 

60770  556 
subsection\<open>Rules for the empty set\<close> 
13780  557 

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

563 
done 

564 

45602  565 
lemmas emptyE [elim!] = not_mem_empty [THEN notE] 
13780  566 

567 

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

13780  570 

14227  571 
lemma equals0I: "[ !!y. y\<in>A ==> False ] ==> A=0" 
13780  572 
by blast 
573 

46820  574 
lemma equals0D [dest]: "A=0 ==> a \<notin> A" 
13780  575 
by blast 
576 

577 
declare sym [THEN equals0D, dest] 

578 

46820  579 
lemma not_emptyI: "a\<in>A ==> A \<noteq> 0" 
13780  580 
by blast 
581 

46820  582 
lemma not_emptyE: "[ A \<noteq> 0; !!x. x\<in>A ==> R ] ==> R" 
13780  583 
by blast 
584 

585 

60770  586 
subsection\<open>Rules for Inter\<close> 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

587 

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

588 
(*Not obviously useful for proving InterI, InterD, InterE*) 
46820  589 
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

590 
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

591 

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

592 
(* Intersection is wellbehaved only if the family is nonempty! *) 
46820  593 
lemma InterI [intro!]: 
594 
"[ !!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

595 
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

596 

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

597 
(*A "destruct" rule  every B in C contains A as an element, but 
14227  598 
A\<in>B can hold when B\<in>C does not! This rule is analogous to "spec". *) 
46820  599 
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

600 
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

601 

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

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

605 
by (simp add: Inter_def, blast) 

606 

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

607 

60770  608 
subsection\<open>Rules for Intersections of families\<close> 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

609 

46820  610 
(* @{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

611 

46820  612 
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

613 
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

614 

14227  615 
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

616 
by blast 
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_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

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

620 

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

621 
lemma INT_cong: 
14227  622 
"[ 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

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

624 

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

626 

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

627 

60770  628 
subsection\<open>Rules for Powersets\<close> 
13780  629 

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

14227  633 
lemma PowD: "A \<in> Pow(B) ==> A<=B" 
13780  634 
by (erule Pow_iff [THEN iffD1]) 
635 

636 
declare Pow_iff [iff] 

637 

61798  638 
lemmas Pow_bottom = empty_subsetI [THEN PowI] \<comment>\<open>@{term"0 \<in> Pow(B)"}\<close> 
639 
lemmas Pow_top = subset_refl [THEN PowI] \<comment>\<open>@{term"A \<in> Pow(A)"}\<close> 

13780  640 

641 

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

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

0  650 
end 