author | wenzelm |
Fri, 06 May 2011 17:52:08 +0200 | |
changeset 42711 | 159c4d1d4c42 |
parent 41779 | a68f503805ed |
child 44147 | f3058e539e3a |
permissions | -rw-r--r-- |
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{*Zermelo-Fraenkel 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 |
uses "~~/src/Tools/misc_legacy.ML" |
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
37405
diff
changeset
|
11 |
begin |
0 | 12 |
|
39128
93a7365fb4ee
turned eta_contract into proper configuration option;
wenzelm
parents:
38798
diff
changeset
|
13 |
declare [[eta_contract = false]] |
23168 | 14 |
|
14076 | 15 |
typedecl i |
16 |
arities i :: "term" |
|
0 | 17 |
|
18 |
consts |
|
19 |
||
41310 | 20 |
zero :: "i" ("0") --{*the empty set*} |
14076 | 21 |
Pow :: "i => i" --{*power sets*} |
22 |
Inf :: "i" --{*infinite set*} |
|
0 | 23 |
|
14076 | 24 |
text {*Bounded Quantifiers *} |
25 |
consts |
|
13780 | 26 |
Ball :: "[i, i => o] => o" |
27 |
Bex :: "[i, i => o] => o" |
|
0 | 28 |
|
14076 | 29 |
text {*General Union and Intersection *} |
30 |
consts |
|
13780 | 31 |
Union :: "i => i" |
32 |
Inter :: "i => i" |
|
0 | 33 |
|
14076 | 34 |
text {*Variations on Replacement *} |
35 |
consts |
|
13144 | 36 |
PrimReplace :: "[i, [i, i] => o] => i" |
37 |
Replace :: "[i, [i, i] => o] => i" |
|
38 |
RepFun :: "[i, i => i] => i" |
|
39 |
Collect :: "[i, i => o] => i" |
|
0 | 40 |
|
14883 | 41 |
text{*Definite descriptions -- via Replace over the set "1"*} |
14076 | 42 |
consts |
13780 | 43 |
The :: "(i => o) => i" (binder "THE " 10) |
13144 | 44 |
If :: "[o, i, i] => i" ("(if (_)/ then (_)/ else (_))" [10] 10) |
6068 | 45 |
|
24826 | 46 |
abbreviation (input) |
47 |
old_if :: "[o, i, i] => i" ("if '(_,_,_')") where |
|
48 |
"if(P,a,b) == If(P,a,b)" |
|
6068 | 49 |
|
50 |
||
14076 | 51 |
text {*Finite Sets *} |
6068 | 52 |
consts |
13780 | 53 |
Upair :: "[i, i] => i" |
54 |
cons :: "[i, i] => i" |
|
55 |
succ :: "i => i" |
|
0 | 56 |
|
14076 | 57 |
text {*Ordered Pairing *} |
58 |
consts |
|
13780 | 59 |
Pair :: "[i, i] => i" |
60 |
fst :: "i => i" |
|
61 |
snd :: "i => i" |
|
14854 | 62 |
split :: "[[i, i] => 'a, i] => 'a::{}" --{*for pattern-matching*} |
0 | 63 |
|
14076 | 64 |
text {*Sigma and Pi Operators *} |
65 |
consts |
|
13780 | 66 |
Sigma :: "[i, i => i] => i" |
67 |
Pi :: "[i, i => i] => i" |
|
0 | 68 |
|
14076 | 69 |
text {*Relations and Functions *} |
70 |
consts |
|
71 |
"domain" :: "i => i" |
|
13144 | 72 |
range :: "i => i" |
73 |
field :: "i => i" |
|
74 |
converse :: "i => i" |
|
14076 | 75 |
relation :: "i => o" --{*recognizes sets of pairs*} |
24826 | 76 |
"function" :: "i => o" --{*recognizes functions; can have non-pairs*} |
13144 | 77 |
Lambda :: "[i, i => i] => i" |
78 |
restrict :: "[i, i] => i" |
|
0 | 79 |
|
14076 | 80 |
text {*Infixes in order of decreasing precedence *} |
81 |
consts |
|
0 | 82 |
|
24826 | 83 |
Image :: "[i, i] => i" (infixl "``" 90) --{*image*} |
84 |
vimage :: "[i, i] => i" (infixl "-``" 90) --{*inverse image*} |
|
85 |
"apply" :: "[i, i] => i" (infixl "`" 90) --{*function application*} |
|
86 |
"Int" :: "[i, i] => i" (infixl "Int" 70) --{*binary intersection*} |
|
87 |
"Un" :: "[i, i] => i" (infixl "Un" 65) --{*binary union*} |
|
88 |
Diff :: "[i, i] => i" (infixl "-" 65) --{*set difference*} |
|
89 |
Subset :: "[i, i] => o" (infixl "<=" 50) --{*subset relation*} |
|
90 |
mem :: "[i, i] => o" (infixl ":" 50) --{*membership relation*} |
|
91 |
||
92 |
abbreviation |
|
93 |
not_mem :: "[i, i] => o" (infixl "~:" 50) --{*negated membership relation*} |
|
94 |
where "x ~: y == ~ (x : y)" |
|
95 |
||
96 |
abbreviation |
|
97 |
cart_prod :: "[i, i] => i" (infixr "*" 80) --{*Cartesian product*} |
|
98 |
where "A * B == Sigma(A, %_. B)" |
|
99 |
||
100 |
abbreviation |
|
101 |
function_space :: "[i, i] => i" (infixr "->" 60) --{*function space*} |
|
102 |
where "A -> B == Pi(A, %_. B)" |
|
0 | 103 |
|
104 |
||
41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
40714
diff
changeset
|
105 |
nonterminal "is" and patterns |
615 | 106 |
|
107 |
syntax |
|
13144 | 108 |
"" :: "i => is" ("_") |
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
109 |
"_Enum" :: "[i, is] => is" ("_,/ _") |
24826 | 110 |
|
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
111 |
"_Finset" :: "is => i" ("{(_)}") |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
112 |
"_Tuple" :: "[i, is] => i" ("<(_,/ _)>") |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
113 |
"_Collect" :: "[pttrn, i, o] => i" ("(1{_: _ ./ _})") |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
114 |
"_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})") |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
115 |
"_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _: _})" [51,0,51]) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
116 |
"_INTER" :: "[pttrn, i, i] => i" ("(3INT _:_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
117 |
"_UNION" :: "[pttrn, i, i] => i" ("(3UN _:_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
118 |
"_PROD" :: "[pttrn, i, i] => i" ("(3PROD _:_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
119 |
"_SUM" :: "[pttrn, i, i] => i" ("(3SUM _:_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
120 |
"_lam" :: "[pttrn, i, i] => i" ("(3lam _:_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
121 |
"_Ball" :: "[pttrn, i, o] => o" ("(3ALL _:_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
122 |
"_Bex" :: "[pttrn, i, o] => o" ("(3EX _:_./ _)" 10) |
1106
62bdb9e5722b
Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset
|
123 |
|
62bdb9e5722b
Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset
|
124 |
(** Patterns -- extends pre-defined type "pttrn" used in abstractions **) |
62bdb9e5722b
Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset
|
125 |
|
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
126 |
"_pattern" :: "patterns => pttrn" ("<_>") |
13144 | 127 |
"" :: "pttrn => patterns" ("_") |
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
128 |
"_patterns" :: "[pttrn, patterns] => patterns" ("_,/_") |
615 | 129 |
|
0 | 130 |
translations |
35068 | 131 |
"{x, xs}" == "CONST cons(x, {xs})" |
132 |
"{x}" == "CONST cons(x, 0)" |
|
133 |
"{x:A. P}" == "CONST Collect(A, %x. P)" |
|
134 |
"{y. x:A, Q}" == "CONST Replace(A, %x y. Q)" |
|
135 |
"{b. x:A}" == "CONST RepFun(A, %x. b)" |
|
136 |
"INT x:A. B" == "CONST Inter({B. x:A})" |
|
137 |
"UN x:A. B" == "CONST Union({B. x:A})" |
|
138 |
"PROD x:A. B" == "CONST Pi(A, %x. B)" |
|
139 |
"SUM x:A. B" == "CONST Sigma(A, %x. B)" |
|
140 |
"lam x:A. f" == "CONST Lambda(A, %x. f)" |
|
141 |
"ALL x:A. P" == "CONST Ball(A, %x. P)" |
|
142 |
"EX x:A. P" == "CONST Bex(A, %x. P)" |
|
37 | 143 |
|
1106
62bdb9e5722b
Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset
|
144 |
"<x, y, z>" == "<x, <y, z>>" |
35068 | 145 |
"<x, y>" == "CONST Pair(x, y)" |
146 |
"%<x,y,zs>.b" == "CONST split(%x <y,zs>.b)" |
|
147 |
"%<x,y>.b" == "CONST split(%x y. b)" |
|
2286 | 148 |
|
0 | 149 |
|
24826 | 150 |
notation (xsymbols) |
151 |
cart_prod (infixr "\<times>" 80) and |
|
152 |
Int (infixl "\<inter>" 70) and |
|
153 |
Un (infixl "\<union>" 65) and |
|
154 |
function_space (infixr "\<rightarrow>" 60) and |
|
155 |
Subset (infixl "\<subseteq>" 50) and |
|
156 |
mem (infixl "\<in>" 50) and |
|
157 |
not_mem (infixl "\<notin>" 50) and |
|
158 |
Union ("\<Union>_" [90] 90) and |
|
159 |
Inter ("\<Inter>_" [90] 90) |
|
160 |
||
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
11322
diff
changeset
|
161 |
syntax (xsymbols) |
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
162 |
"_Collect" :: "[pttrn, i, o] => i" ("(1{_ \<in> _ ./ _})") |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
163 |
"_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})") |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
164 |
"_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \<in> _})" [51,0,51]) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
165 |
"_UNION" :: "[pttrn, i, i] => i" ("(3\<Union>_\<in>_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
166 |
"_INTER" :: "[pttrn, i, i] => i" ("(3\<Inter>_\<in>_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
167 |
"_PROD" :: "[pttrn, i, i] => i" ("(3\<Pi>_\<in>_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
168 |
"_SUM" :: "[pttrn, i, i] => i" ("(3\<Sigma>_\<in>_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
169 |
"_lam" :: "[pttrn, i, i] => i" ("(3\<lambda>_\<in>_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
170 |
"_Ball" :: "[pttrn, i, o] => o" ("(3\<forall>_\<in>_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
171 |
"_Bex" :: "[pttrn, i, o] => o" ("(3\<exists>_\<in>_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
172 |
"_Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>") |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
173 |
"_pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>") |
2540 | 174 |
|
24826 | 175 |
notation (HTML output) |
176 |
cart_prod (infixr "\<times>" 80) and |
|
177 |
Int (infixl "\<inter>" 70) and |
|
178 |
Un (infixl "\<union>" 65) and |
|
179 |
Subset (infixl "\<subseteq>" 50) and |
|
180 |
mem (infixl "\<in>" 50) and |
|
181 |
not_mem (infixl "\<notin>" 50) and |
|
182 |
Union ("\<Union>_" [90] 90) and |
|
183 |
Inter ("\<Inter>_" [90] 90) |
|
184 |
||
6340 | 185 |
syntax (HTML output) |
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
186 |
"_Collect" :: "[pttrn, i, o] => i" ("(1{_ \<in> _ ./ _})") |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
187 |
"_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})") |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
188 |
"_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \<in> _})" [51,0,51]) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
189 |
"_UNION" :: "[pttrn, i, i] => i" ("(3\<Union>_\<in>_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
190 |
"_INTER" :: "[pttrn, i, i] => i" ("(3\<Inter>_\<in>_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
191 |
"_PROD" :: "[pttrn, i, i] => i" ("(3\<Pi>_\<in>_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
192 |
"_SUM" :: "[pttrn, i, i] => i" ("(3\<Sigma>_\<in>_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
193 |
"_lam" :: "[pttrn, i, i] => i" ("(3\<lambda>_\<in>_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
194 |
"_Ball" :: "[pttrn, i, o] => o" ("(3\<forall>_\<in>_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
195 |
"_Bex" :: "[pttrn, i, o] => o" ("(3\<exists>_\<in>_./ _)" 10) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
196 |
"_Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>") |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35068
diff
changeset
|
197 |
"_pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>") |
6340 | 198 |
|
2540 | 199 |
|
14227 | 200 |
finalconsts |
24826 | 201 |
0 Pow Inf Union PrimReplace mem |
14227 | 202 |
|
37405 | 203 |
defs (* Bounded Quantifiers *) |
14227 | 204 |
Ball_def: "Ball(A, P) == \<forall>x. x\<in>A --> P(x)" |
205 |
Bex_def: "Bex(A, P) == \<exists>x. x\<in>A & P(x)" |
|
690 | 206 |
|
14227 | 207 |
subset_def: "A <= B == \<forall>x\<in>A. x\<in>B" |
690 | 208 |
|
3906 | 209 |
|
41779 | 210 |
axiomatization where |
0 | 211 |
|
615 | 212 |
(* ZF axioms -- see Suppes p.238 |
213 |
Axioms for Union, Pow and Replace state existence only, |
|
214 |
uniqueness is derivable using extensionality. *) |
|
0 | 215 |
|
41779 | 216 |
extension: "A = B <-> A <= B & B <= A" and |
217 |
Union_iff: "A \<in> Union(C) <-> (\<exists>B\<in>C. A\<in>B)" and |
|
218 |
Pow_iff: "A \<in> Pow(B) <-> A <= B" and |
|
0 | 219 |
|
615 | 220 |
(*We may name this set, though it is not uniquely defined.*) |
41779 | 221 |
infinity: "0\<in>Inf & (\<forall>y\<in>Inf. succ(y): Inf)" and |
0 | 222 |
|
615 | 223 |
(*This formulation facilitates case analysis on A.*) |
41779 | 224 |
foundation: "A=0 | (\<exists>x\<in>A. \<forall>y\<in>x. y~:A)" and |
0 | 225 |
|
615 | 226 |
(*Schema axiom since predicate P is a higher-order variable*) |
14227 | 227 |
replacement: "(\<forall>x\<in>A. \<forall>y z. P(x,y) & P(x,z) --> y=z) ==> |
228 |
b \<in> PrimReplace(A,P) <-> (\<exists>x\<in>A. P(x,b))" |
|
615 | 229 |
|
14883 | 230 |
|
690 | 231 |
defs |
232 |
||
615 | 233 |
(* Derived form of replacement, restricting P to its functional part. |
234 |
The resulting set (for functional P) is the same as with |
|
235 |
PrimReplace, but the rules are simpler. *) |
|
0 | 236 |
|
13780 | 237 |
Replace_def: "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))" |
615 | 238 |
|
239 |
(* Functional form of replacement -- analgous to ML's map functional *) |
|
0 | 240 |
|
14227 | 241 |
RepFun_def: "RepFun(A,f) == {y . x\<in>A, y=f(x)}" |
0 | 242 |
|
615 | 243 |
(* Separation and Pairing can be derived from the Replacement |
244 |
and Powerset Axioms using the following definitions. *) |
|
0 | 245 |
|
14227 | 246 |
Collect_def: "Collect(A,P) == {y . x\<in>A, x=y & P(x)}" |
0 | 247 |
|
615 | 248 |
(*Unordered pairs (Upair) express binary union/intersection and cons; |
249 |
set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*) |
|
0 | 250 |
|
14227 | 251 |
Upair_def: "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}" |
13780 | 252 |
cons_def: "cons(a,A) == Upair(a,a) Un A" |
253 |
succ_def: "succ(i) == cons(i, i)" |
|
615 | 254 |
|
2872
ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset
|
255 |
(* 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
|
256 |
|
14227 | 257 |
Diff_def: "A - B == { x\<in>A . ~(x\<in>B) }" |
258 |
Inter_def: "Inter(A) == { x\<in>Union(A) . \<forall>y\<in>A. x\<in>y}" |
|
13780 | 259 |
Un_def: "A Un B == Union(Upair(A,B))" |
260 |
Int_def: "A Int B == Inter(Upair(A,B))" |
|
2872
ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset
|
261 |
|
14883 | 262 |
(* definite descriptions *) |
14227 | 263 |
the_def: "The(P) == Union({y . x \<in> {0}, P(y)})" |
13780 | 264 |
if_def: "if(P,a,b) == THE z. P & z=a | ~P & z=b" |
0 | 265 |
|
615 | 266 |
(* this "symmetric" definition works better than {{a}, {a,b}} *) |
13780 | 267 |
Pair_def: "<a,b> == {{a,a}, {a,b}}" |
14227 | 268 |
fst_def: "fst(p) == THE a. \<exists>b. p=<a,b>" |
269 |
snd_def: "snd(p) == THE b. \<exists>a. p=<a,b>" |
|
13780 | 270 |
split_def: "split(c) == %p. c(fst(p), snd(p))" |
14227 | 271 |
Sigma_def: "Sigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {<x,y>}" |
0 | 272 |
|
615 | 273 |
(* Operations on relations *) |
0 | 274 |
|
615 | 275 |
(*converse of relation r, inverse of function*) |
14227 | 276 |
converse_def: "converse(r) == {z. w\<in>r, \<exists>x y. w=<x,y> & z=<y,x>}" |
0 | 277 |
|
14227 | 278 |
domain_def: "domain(r) == {x. w\<in>r, \<exists>y. w=<x,y>}" |
13780 | 279 |
range_def: "range(r) == domain(converse(r))" |
280 |
field_def: "field(r) == domain(r) Un range(r)" |
|
14227 | 281 |
relation_def: "relation(r) == \<forall>z\<in>r. \<exists>x y. z = <x,y>" |
13780 | 282 |
function_def: "function(r) == |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
283 |
\<forall>x y. <x,y>:r --> (\<forall>y'. <x,y'>:r --> y=y')" |
14227 | 284 |
image_def: "r `` A == {y : range(r) . \<exists>x\<in>A. <x,y> : r}" |
13780 | 285 |
vimage_def: "r -`` A == converse(r)``A" |
0 | 286 |
|
615 | 287 |
(* Abstraction, application and Cartesian product of a family of sets *) |
0 | 288 |
|
14227 | 289 |
lam_def: "Lambda(A,b) == {<x,b(x)> . x\<in>A}" |
13780 | 290 |
apply_def: "f`a == Union(f``{a})" |
14227 | 291 |
Pi_def: "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A<=domain(f) & function(f)}" |
0 | 292 |
|
12891 | 293 |
(* Restrict the relation r to the domain A *) |
14227 | 294 |
restrict_def: "restrict(r,A) == {z : r. \<exists>x\<in>A. \<exists>y. z = <x,y>}" |
13780 | 295 |
|
296 |
||
297 |
subsection {* Substitution*} |
|
298 |
||
299 |
(*Useful examples: singletonI RS subst_elem, subst_elem RSN (2,IntI) *) |
|
14227 | 300 |
lemma subst_elem: "[| b\<in>A; a=b |] ==> a\<in>A" |
13780 | 301 |
by (erule ssubst, assumption) |
302 |
||
303 |
||
304 |
subsection{*Bounded universal quantifier*} |
|
305 |
||
14227 | 306 |
lemma ballI [intro!]: "[| !!x. x\<in>A ==> P(x) |] ==> \<forall>x\<in>A. P(x)" |
13780 | 307 |
by (simp add: Ball_def) |
308 |
||
15481 | 309 |
lemmas strip = impI allI ballI |
310 |
||
14227 | 311 |
lemma bspec [dest?]: "[| \<forall>x\<in>A. P(x); x: A |] ==> P(x)" |
13780 | 312 |
by (simp add: Ball_def) |
313 |
||
314 |
(*Instantiates x first: better for automatic theorem proving?*) |
|
315 |
lemma rev_ballE [elim]: |
|
14227 | 316 |
"[| \<forall>x\<in>A. P(x); x~:A ==> Q; P(x) ==> Q |] ==> Q" |
13780 | 317 |
by (simp add: Ball_def, blast) |
318 |
||
14227 | 319 |
lemma ballE: "[| \<forall>x\<in>A. P(x); P(x) ==> Q; x~:A ==> Q |] ==> Q" |
13780 | 320 |
by blast |
321 |
||
322 |
(*Used in the datatype package*) |
|
14227 | 323 |
lemma rev_bspec: "[| x: A; \<forall>x\<in>A. P(x) |] ==> P(x)" |
13780 | 324 |
by (simp add: Ball_def) |
325 |
||
14227 | 326 |
(*Trival rewrite rule; (\<forall>x\<in>A.P)<->P holds only if A is nonempty!*) |
327 |
lemma ball_triv [simp]: "(\<forall>x\<in>A. P) <-> ((\<exists>x. x\<in>A) --> P)" |
|
13780 | 328 |
by (simp add: Ball_def) |
329 |
||
330 |
(*Congruence rule for rewriting*) |
|
331 |
lemma ball_cong [cong]: |
|
14227 | 332 |
"[| A=A'; !!x. x\<in>A' ==> P(x) <-> P'(x) |] ==> (\<forall>x\<in>A. P(x)) <-> (\<forall>x\<in>A'. P'(x))" |
13780 | 333 |
by (simp add: Ball_def) |
334 |
||
18845 | 335 |
lemma atomize_ball: |
336 |
"(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))" |
|
337 |
by (simp only: Ball_def atomize_all atomize_imp) |
|
338 |
||
339 |
lemmas [symmetric, rulify] = atomize_ball |
|
340 |
and [symmetric, defn] = atomize_ball |
|
341 |
||
13780 | 342 |
|
343 |
subsection{*Bounded existential quantifier*} |
|
344 |
||
14227 | 345 |
lemma bexI [intro]: "[| P(x); x: A |] ==> \<exists>x\<in>A. P(x)" |
13780 | 346 |
by (simp add: Bex_def, blast) |
347 |
||
14227 | 348 |
(*The best argument order when there is only one x\<in>A*) |
349 |
lemma rev_bexI: "[| x\<in>A; P(x) |] ==> \<exists>x\<in>A. P(x)" |
|
13780 | 350 |
by blast |
351 |
||
14227 | 352 |
(*Not of the general form for such rules; ~\<exists>has become ALL~ *) |
353 |
lemma bexCI: "[| \<forall>x\<in>A. ~P(x) ==> P(a); a: A |] ==> \<exists>x\<in>A. P(x)" |
|
13780 | 354 |
by blast |
355 |
||
14227 | 356 |
lemma bexE [elim!]: "[| \<exists>x\<in>A. P(x); !!x. [| x\<in>A; P(x) |] ==> Q |] ==> Q" |
13780 | 357 |
by (simp add: Bex_def, blast) |
358 |
||
14227 | 359 |
(*We do not even have (\<exists>x\<in>A. True) <-> True unless A is nonempty!!*) |
360 |
lemma bex_triv [simp]: "(\<exists>x\<in>A. P) <-> ((\<exists>x. x\<in>A) & P)" |
|
13780 | 361 |
by (simp add: Bex_def) |
362 |
||
363 |
lemma bex_cong [cong]: |
|
14227 | 364 |
"[| A=A'; !!x. x\<in>A' ==> P(x) <-> P'(x) |] |
365 |
==> (\<exists>x\<in>A. P(x)) <-> (\<exists>x\<in>A'. P'(x))" |
|
13780 | 366 |
by (simp add: Bex_def cong: conj_cong) |
367 |
||
368 |
||
369 |
||
370 |
subsection{*Rules for subsets*} |
|
371 |
||
372 |
lemma subsetI [intro!]: |
|
14227 | 373 |
"(!!x. x\<in>A ==> x\<in>B) ==> A <= B" |
13780 | 374 |
by (simp add: subset_def) |
375 |
||
376 |
(*Rule in Modus Ponens style [was called subsetE] *) |
|
14227 | 377 |
lemma subsetD [elim]: "[| A <= B; c\<in>A |] ==> c\<in>B" |
13780 | 378 |
apply (unfold subset_def) |
379 |
apply (erule bspec, assumption) |
|
380 |
done |
|
381 |
||
382 |
(*Classical elimination rule*) |
|
383 |
lemma subsetCE [elim]: |
|
14227 | 384 |
"[| A <= B; c~:A ==> P; c\<in>B ==> P |] ==> P" |
13780 | 385 |
by (simp add: subset_def, blast) |
386 |
||
387 |
(*Sometimes useful with premises in this order*) |
|
14227 | 388 |
lemma rev_subsetD: "[| c\<in>A; A<=B |] ==> c\<in>B" |
13780 | 389 |
by blast |
390 |
||
391 |
lemma contra_subsetD: "[| A <= B; c ~: B |] ==> c ~: A" |
|
392 |
by blast |
|
393 |
||
394 |
lemma rev_contra_subsetD: "[| c ~: B; A <= B |] ==> c ~: A" |
|
395 |
by blast |
|
396 |
||
397 |
lemma subset_refl [simp]: "A <= A" |
|
398 |
by blast |
|
399 |
||
400 |
lemma subset_trans: "[| A<=B; B<=C |] ==> A<=C" |
|
401 |
by blast |
|
402 |
||
403 |
(*Useful for proving A<=B by rewriting in some cases*) |
|
404 |
lemma subset_iff: |
|
14227 | 405 |
"A<=B <-> (\<forall>x. x\<in>A --> x\<in>B)" |
13780 | 406 |
apply (unfold subset_def Ball_def) |
407 |
apply (rule iff_refl) |
|
408 |
done |
|
409 |
||
410 |
||
411 |
subsection{*Rules for equality*} |
|
412 |
||
413 |
(*Anti-symmetry of the subset relation*) |
|
414 |
lemma equalityI [intro]: "[| A <= B; B <= A |] ==> A = B" |
|
415 |
by (rule extension [THEN iffD2], rule conjI) |
|
416 |
||
417 |
||
14227 | 418 |
lemma equality_iffI: "(!!x. x\<in>A <-> x\<in>B) ==> A = B" |
13780 | 419 |
by (rule equalityI, blast+) |
420 |
||
421 |
lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1, standard] |
|
422 |
lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2, standard] |
|
423 |
||
424 |
lemma equalityE: "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P" |
|
425 |
by (blast dest: equalityD1 equalityD2) |
|
426 |
||
427 |
lemma equalityCE: |
|
14227 | 428 |
"[| A = B; [| c\<in>A; c\<in>B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P" |
13780 | 429 |
by (erule equalityE, blast) |
430 |
||
27702 | 431 |
lemma equality_iffD: |
432 |
"A = B ==> (!!x. x : A <-> x : B)" |
|
433 |
by auto |
|
434 |
||
13780 | 435 |
|
436 |
subsection{*Rules for Replace -- the derived form of replacement*} |
|
437 |
||
438 |
lemma Replace_iff: |
|
14227 | 439 |
"b : {y. x\<in>A, P(x,y)} <-> (\<exists>x\<in>A. P(x,b) & (\<forall>y. P(x,y) --> y=b))" |
13780 | 440 |
apply (unfold Replace_def) |
441 |
apply (rule replacement [THEN iff_trans], blast+) |
|
442 |
done |
|
443 |
||
444 |
(*Introduction; there must be a unique y such that P(x,y), namely y=b. *) |
|
445 |
lemma ReplaceI [intro]: |
|
446 |
"[| P(x,b); x: A; !!y. P(x,y) ==> y=b |] ==> |
|
14227 | 447 |
b : {y. x\<in>A, P(x,y)}" |
13780 | 448 |
by (rule Replace_iff [THEN iffD2], blast) |
449 |
||
450 |
(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *) |
|
451 |
lemma ReplaceE: |
|
14227 | 452 |
"[| b : {y. x\<in>A, P(x,y)}; |
453 |
!!x. [| x: A; P(x,b); \<forall>y. P(x,y)-->y=b |] ==> R |
|
13780 | 454 |
|] ==> R" |
455 |
by (rule Replace_iff [THEN iffD1, THEN bexE], simp+) |
|
456 |
||
457 |
(*As above but without the (generally useless) 3rd assumption*) |
|
458 |
lemma ReplaceE2 [elim!]: |
|
14227 | 459 |
"[| b : {y. x\<in>A, P(x,y)}; |
13780 | 460 |
!!x. [| x: A; P(x,b) |] ==> R |
461 |
|] ==> R" |
|
462 |
by (erule ReplaceE, blast) |
|
463 |
||
464 |
lemma Replace_cong [cong]: |
|
14227 | 465 |
"[| A=B; !!x y. x\<in>B ==> P(x,y) <-> Q(x,y) |] ==> |
13780 | 466 |
Replace(A,P) = Replace(B,Q)" |
467 |
apply (rule equality_iffI) |
|
468 |
apply (simp add: Replace_iff) |
|
469 |
done |
|
470 |
||
471 |
||
472 |
subsection{*Rules for RepFun*} |
|
473 |
||
14227 | 474 |
lemma RepFunI: "a \<in> A ==> f(a) : {f(x). x\<in>A}" |
13780 | 475 |
by (simp add: RepFun_def Replace_iff, blast) |
476 |
||
477 |
(*Useful for coinduction proofs*) |
|
14227 | 478 |
lemma RepFun_eqI [intro]: "[| b=f(a); a \<in> A |] ==> b : {f(x). x\<in>A}" |
13780 | 479 |
apply (erule ssubst) |
480 |
apply (erule RepFunI) |
|
481 |
done |
|
482 |
||
483 |
lemma RepFunE [elim!]: |
|
14227 | 484 |
"[| b : {f(x). x\<in>A}; |
485 |
!!x.[| x\<in>A; b=f(x) |] ==> P |] ==> |
|
13780 | 486 |
P" |
487 |
by (simp add: RepFun_def Replace_iff, blast) |
|
488 |
||
489 |
lemma RepFun_cong [cong]: |
|
14227 | 490 |
"[| A=B; !!x. x\<in>B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)" |
13780 | 491 |
by (simp add: RepFun_def) |
492 |
||
14227 | 493 |
lemma RepFun_iff [simp]: "b : {f(x). x\<in>A} <-> (\<exists>x\<in>A. b=f(x))" |
13780 | 494 |
by (unfold Bex_def, blast) |
495 |
||
14227 | 496 |
lemma triv_RepFun [simp]: "{x. x\<in>A} = A" |
13780 | 497 |
by blast |
498 |
||
499 |
||
500 |
subsection{*Rules for Collect -- forming a subset by separation*} |
|
501 |
||
502 |
(*Separation is derivable from Replacement*) |
|
14227 | 503 |
lemma separation [simp]: "a : {x\<in>A. P(x)} <-> a\<in>A & P(a)" |
13780 | 504 |
by (unfold Collect_def, blast) |
505 |
||
14227 | 506 |
lemma CollectI [intro!]: "[| a\<in>A; P(a) |] ==> a : {x\<in>A. P(x)}" |
13780 | 507 |
by simp |
508 |
||
14227 | 509 |
lemma CollectE [elim!]: "[| a : {x\<in>A. P(x)}; [| a\<in>A; P(a) |] ==> R |] ==> R" |
13780 | 510 |
by simp |
511 |
||
14227 | 512 |
lemma CollectD1: "a : {x\<in>A. P(x)} ==> a\<in>A" |
13780 | 513 |
by (erule CollectE, assumption) |
514 |
||
14227 | 515 |
lemma CollectD2: "a : {x\<in>A. P(x)} ==> P(a)" |
13780 | 516 |
by (erule CollectE, assumption) |
517 |
||
518 |
lemma Collect_cong [cong]: |
|
14227 | 519 |
"[| A=B; !!x. x\<in>B ==> P(x) <-> Q(x) |] |
13780 | 520 |
==> Collect(A, %x. P(x)) = Collect(B, %x. Q(x))" |
521 |
by (simp add: Collect_def) |
|
522 |
||
523 |
||
524 |
subsection{*Rules for Unions*} |
|
525 |
||
526 |
declare Union_iff [simp] |
|
527 |
||
528 |
(*The order of the premises presupposes that C is rigid; A may be flexible*) |
|
529 |
lemma UnionI [intro]: "[| B: C; A: B |] ==> A: Union(C)" |
|
530 |
by (simp, blast) |
|
531 |
||
14227 | 532 |
lemma UnionE [elim!]: "[| A \<in> Union(C); !!B.[| A: B; B: C |] ==> R |] ==> R" |
13780 | 533 |
by (simp, blast) |
534 |
||
535 |
||
536 |
subsection{*Rules for Unions of families*} |
|
14227 | 537 |
(* \<Union>x\<in>A. B(x) abbreviates Union({B(x). x\<in>A}) *) |
13780 | 538 |
|
14227 | 539 |
lemma UN_iff [simp]: "b : (\<Union>x\<in>A. B(x)) <-> (\<exists>x\<in>A. b \<in> B(x))" |
13780 | 540 |
by (simp add: Bex_def, blast) |
541 |
||
542 |
(*The order of the premises presupposes that A is rigid; b may be flexible*) |
|
14227 | 543 |
lemma UN_I: "[| a: A; b: B(a) |] ==> b: (\<Union>x\<in>A. B(x))" |
13780 | 544 |
by (simp, blast) |
545 |
||
546 |
||
547 |
lemma UN_E [elim!]: |
|
14227 | 548 |
"[| b : (\<Union>x\<in>A. B(x)); !!x.[| x: A; b: B(x) |] ==> R |] ==> R" |
13780 | 549 |
by blast |
550 |
||
551 |
lemma UN_cong: |
|
14227 | 552 |
"[| A=B; !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Union>x\<in>A. C(x)) = (\<Union>x\<in>B. D(x))" |
13780 | 553 |
by simp |
554 |
||
555 |
||
14227 | 556 |
(*No "Addcongs [UN_cong]" because \<Union>is a combination of constants*) |
13780 | 557 |
|
558 |
(* UN_E appears before UnionE so that it is tried first, to avoid expensive |
|
559 |
calls to hyp_subst_tac. Cannot include UN_I as it is unsafe: would enlarge |
|
560 |
the search space.*) |
|
561 |
||
562 |
||
563 |
subsection{*Rules for the empty set*} |
|
564 |
||
14227 | 565 |
(*The set {x\<in>0. False} is empty; by foundation it equals 0 |
13780 | 566 |
See Suppes, page 21.*) |
567 |
lemma not_mem_empty [simp]: "a ~: 0" |
|
568 |
apply (cut_tac foundation) |
|
569 |
apply (best dest: equalityD2) |
|
570 |
done |
|
571 |
||
572 |
lemmas emptyE [elim!] = not_mem_empty [THEN notE, standard] |
|
573 |
||
574 |
||
575 |
lemma empty_subsetI [simp]: "0 <= A" |
|
576 |
by blast |
|
577 |
||
14227 | 578 |
lemma equals0I: "[| !!y. y\<in>A ==> False |] ==> A=0" |
13780 | 579 |
by blast |
580 |
||
581 |
lemma equals0D [dest]: "A=0 ==> a ~: A" |
|
582 |
by blast |
|
583 |
||
584 |
declare sym [THEN equals0D, dest] |
|
585 |
||
14227 | 586 |
lemma not_emptyI: "a\<in>A ==> A ~= 0" |
13780 | 587 |
by blast |
588 |
||
14227 | 589 |
lemma not_emptyE: "[| A ~= 0; !!x. x\<in>A ==> R |] ==> R" |
13780 | 590 |
by blast |
591 |
||
592 |
||
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
593 |
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
|
594 |
|
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
595 |
(*Not obviously useful for proving InterI, InterD, InterE*) |
14227 | 596 |
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
|
597 |
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
|
598 |
|
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
599 |
(* Intersection is well-behaved only if the family is non-empty! *) |
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
600 |
lemma InterI [intro!]: |
14227 | 601 |
"[| !!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
|
602 |
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
|
603 |
|
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
604 |
(*A "destruct" rule -- every B in C contains A as an element, but |
14227 | 605 |
A\<in>B can hold when B\<in>C does not! This rule is analogous to "spec". *) |
40714
4c17bfdf6f84
prefer non-classical eliminations in Pure reasoning, notably "rule" steps;
wenzelm
parents:
39128
diff
changeset
|
606 |
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
|
607 |
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
|
608 |
|
14227 | 609 |
(*"Classical" elimination rule -- does not require exhibiting B\<in>C *) |
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
610 |
lemma InterE [elim]: |
14227 | 611 |
"[| A \<in> Inter(C); B~:C ==> R; A\<in>B ==> R |] ==> R" |
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
612 |
by (simp add: Inter_def, blast) |
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 |
|
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
615 |
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
|
616 |
|
14227 | 617 |
(* \<Inter>x\<in>A. B(x) abbreviates 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
|
618 |
|
14227 | 619 |
lemma INT_iff: "b : (\<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
|
620 |
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
|
621 |
|
14227 | 622 |
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
|
623 |
by blast |
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
624 |
|
14227 | 625 |
lemma INT_E: "[| b : (\<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
|
626 |
by blast |
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
627 |
|
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
628 |
lemma INT_cong: |
14227 | 629 |
"[| 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
|
630 |
by simp |
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
631 |
|
14227 | 632 |
(*No "Addcongs [INT_cong]" because \<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
|
633 |
|
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
634 |
|
13780 | 635 |
subsection{*Rules for Powersets*} |
636 |
||
14227 | 637 |
lemma PowI: "A <= B ==> A \<in> Pow(B)" |
13780 | 638 |
by (erule Pow_iff [THEN iffD2]) |
639 |
||
14227 | 640 |
lemma PowD: "A \<in> Pow(B) ==> A<=B" |
13780 | 641 |
by (erule Pow_iff [THEN iffD1]) |
642 |
||
643 |
declare Pow_iff [iff] |
|
644 |
||
14227 | 645 |
lemmas Pow_bottom = empty_subsetI [THEN PowI] (* 0 \<in> Pow(B) *) |
646 |
lemmas Pow_top = subset_refl [THEN PowI] (* A \<in> Pow(A) *) |
|
13780 | 647 |
|
648 |
||
649 |
subsection{*Cantor's Theorem: There is no surjection from a set to its powerset.*} |
|
650 |
||
651 |
(*The search is undirected. Allowing redundant introduction rules may |
|
652 |
make it diverge. Variable b represents ANY map, such as |
|
14227 | 653 |
(lam x\<in>A.b(x)): A->Pow(A). *) |
654 |
lemma cantor: "\<exists>S \<in> Pow(A). \<forall>x\<in>A. b(x) ~= S" |
|
13780 | 655 |
by (best elim!: equalityCE del: ReplaceI RepFun_eqI) |
656 |
||
657 |
(*Functions for ML scripts*) |
|
658 |
ML |
|
659 |
{* |
|
14227 | 660 |
(*Converts A<=B to x\<in>A ==> x\<in>B*) |
24893 | 661 |
fun impOfSubs th = th RSN (2, @{thm rev_subsetD}); |
13780 | 662 |
|
14227 | 663 |
(*Takes assumptions \<forall>x\<in>A.P(x) and a\<in>A; creates assumption P(a)*) |
24893 | 664 |
val ball_tac = dtac @{thm bspec} THEN' assume_tac |
13780 | 665 |
*} |
0 | 666 |
|
667 |
end |
|
668 |