author | paulson |
Tue, 21 May 2002 13:06:36 +0200 | |
changeset 13168 | afcbca3498b0 |
parent 12552 | d2d2ab3f1f37 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/subset |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
6 |
Derived rules involving subsets |
|
7 |
Union and Intersection as lattice operations |
|
8 |
*) |
|
9 |
||
10 |
(*** cons ***) |
|
11 |
||
9180 | 12 |
Goal "[| a:C; B<=C |] ==> cons(a,B) <= C"; |
13 |
by (Blast_tac 1); |
|
14 |
qed "cons_subsetI"; |
|
0 | 15 |
|
9180 | 16 |
Goal "B <= cons(a,B)"; |
17 |
by (Blast_tac 1); |
|
18 |
qed "subset_consI"; |
|
0 | 19 |
|
9180 | 20 |
Goal "cons(a,B)<=C <-> a:C & B<=C"; |
21 |
by (Blast_tac 1); |
|
22 |
qed "cons_subset_iff"; |
|
9304 | 23 |
AddIffs [cons_subset_iff]; |
0 | 24 |
|
25 |
(*A safe special case of subset elimination, adding no new variables |
|
26 |
[| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *) |
|
2469 | 27 |
bind_thm ("cons_subsetE", cons_subset_iff RS iffD1 RS conjE); |
0 | 28 |
|
9180 | 29 |
Goal "A<=0 <-> A=0"; |
30 |
by (Blast_tac 1) ; |
|
31 |
qed "subset_empty_iff"; |
|
0 | 32 |
|
9180 | 33 |
Goal "C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)"; |
34 |
by (Blast_tac 1) ; |
|
35 |
qed "subset_cons_iff"; |
|
0 | 36 |
|
37 |
(*** succ ***) |
|
38 |
||
9180 | 39 |
Goal "i <= succ(i)"; |
40 |
by (Blast_tac 1) ; |
|
41 |
qed "subset_succI"; |
|
0 | 42 |
|
43 |
(*But if j is an ordinal or is transitive, then i:j implies i<=j! |
|
44 |
See ordinal/Ord_succ_subsetI*) |
|
9211 | 45 |
Goalw [succ_def] "[| i:j; i<=j |] ==> succ(i)<=j"; |
46 |
by (Blast_tac 1) ; |
|
47 |
qed "succ_subsetI"; |
|
0 | 48 |
|
9211 | 49 |
val major::prems= Goalw [succ_def] |
0 | 50 |
"[| succ(i) <= j; [| i:j; i<=j |] ==> P \ |
9211 | 51 |
\ |] ==> P"; |
52 |
by (rtac (major RS cons_subsetE) 1); |
|
53 |
by (REPEAT (ares_tac prems 1)) ; |
|
54 |
qed "succ_subsetE"; |
|
0 | 55 |
|
12552
d2d2ab3f1f37
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
paulson
parents:
9907
diff
changeset
|
56 |
Goalw [succ_def] "succ(a) <= B <-> (a <= B & a : B)"; |
d2d2ab3f1f37
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
paulson
parents:
9907
diff
changeset
|
57 |
by (Blast_tac 1) ; |
d2d2ab3f1f37
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
paulson
parents:
9907
diff
changeset
|
58 |
qed "succ_subset_iff"; |
d2d2ab3f1f37
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
paulson
parents:
9907
diff
changeset
|
59 |
|
0 | 60 |
(*** singletons ***) |
61 |
||
9180 | 62 |
Goal "a:C ==> {a} <= C"; |
63 |
by (Blast_tac 1) ; |
|
64 |
qed "singleton_subsetI"; |
|
0 | 65 |
|
9180 | 66 |
Goal "{a} <= C ==> a:C"; |
67 |
by (Blast_tac 1) ; |
|
68 |
qed "singleton_subsetD"; |
|
0 | 69 |
|
70 |
(*** Big Union -- least upper bound of a set ***) |
|
71 |
||
9180 | 72 |
Goal "Union(A) <= C <-> (ALL x:A. x <= C)"; |
73 |
by (Blast_tac 1); |
|
74 |
qed "Union_subset_iff"; |
|
0 | 75 |
|
9180 | 76 |
Goal "B:A ==> B <= Union(A)"; |
77 |
by (Blast_tac 1); |
|
78 |
qed "Union_upper"; |
|
0 | 79 |
|
9180 | 80 |
val [prem]= Goal |
81 |
"[| !!x. x:A ==> x<=C |] ==> Union(A) <= C"; |
|
82 |
by (rtac (ballI RS (Union_subset_iff RS iffD2)) 1); |
|
83 |
by (etac prem 1) ; |
|
84 |
qed "Union_least"; |
|
0 | 85 |
|
86 |
(*** Union of a family of sets ***) |
|
87 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
88 |
Goal "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))"; |
4091 | 89 |
by (blast_tac (claset() addSEs [equalityE]) 1); |
760 | 90 |
qed "subset_UN_iff_eq"; |
0 | 91 |
|
9180 | 92 |
Goal "(UN x:A. B(x)) <= C <-> (ALL x:A. B(x) <= C)"; |
93 |
by (Blast_tac 1); |
|
94 |
qed "UN_subset_iff"; |
|
0 | 95 |
|
9180 | 96 |
Goal "x:A ==> B(x) <= (UN x:A. B(x))"; |
97 |
by (etac (RepFunI RS Union_upper) 1); |
|
98 |
qed "UN_upper"; |
|
0 | 99 |
|
9180 | 100 |
val [prem]= Goal |
101 |
"[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C"; |
|
102 |
by (rtac (ballI RS (UN_subset_iff RS iffD2)) 1); |
|
103 |
by (etac prem 1) ; |
|
104 |
qed "UN_least"; |
|
0 | 105 |
|
106 |
||
107 |
(*** Big Intersection -- greatest lower bound of a nonempty set ***) |
|
108 |
||
9180 | 109 |
Goal "a: A ==> C <= Inter(A) <-> (ALL x:A. C <= x)"; |
110 |
by (Blast_tac 1); |
|
111 |
qed "Inter_subset_iff"; |
|
0 | 112 |
|
9180 | 113 |
Goal "B:A ==> Inter(A) <= B"; |
114 |
by (Blast_tac 1); |
|
115 |
qed "Inter_lower"; |
|
0 | 116 |
|
9180 | 117 |
val [prem1,prem2]= Goal |
118 |
"[| a:A; !!x. x:A ==> C<=x |] ==> C <= Inter(A)"; |
|
119 |
by (rtac ([prem1, ballI] MRS (Inter_subset_iff RS iffD2)) 1); |
|
120 |
by (etac prem2 1) ; |
|
121 |
qed "Inter_greatest"; |
|
0 | 122 |
|
123 |
(*** Intersection of a family of sets ***) |
|
124 |
||
9180 | 125 |
Goal "x:A ==> (INT x:A. B(x)) <= B(x)"; |
126 |
by (Blast_tac 1); |
|
127 |
qed "INT_lower"; |
|
0 | 128 |
|
9180 | 129 |
val [nonempty,prem] = Goal |
130 |
"[| a:A; !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))"; |
|
131 |
by (rtac (nonempty RS RepFunI RS Inter_greatest) 1); |
|
132 |
by (REPEAT (eresolve_tac [RepFunE, prem, ssubst] 1)); |
|
133 |
qed "INT_greatest"; |
|
0 | 134 |
|
135 |
||
136 |
(*** Finite Union -- the least upper bound of 2 sets ***) |
|
137 |
||
9180 | 138 |
Goal "A Un B <= C <-> A <= C & B <= C"; |
139 |
by (Blast_tac 1); |
|
140 |
qed "Un_subset_iff"; |
|
0 | 141 |
|
9180 | 142 |
Goal "A <= A Un B"; |
143 |
by (Blast_tac 1); |
|
144 |
qed "Un_upper1"; |
|
0 | 145 |
|
9180 | 146 |
Goal "B <= A Un B"; |
147 |
by (Blast_tac 1); |
|
148 |
qed "Un_upper2"; |
|
0 | 149 |
|
9180 | 150 |
Goal "[| A<=C; B<=C |] ==> A Un B <= C"; |
151 |
by (Blast_tac 1); |
|
152 |
qed "Un_least"; |
|
2469 | 153 |
|
0 | 154 |
|
155 |
(*** Finite Intersection -- the greatest lower bound of 2 sets *) |
|
156 |
||
9180 | 157 |
Goal "C <= A Int B <-> C <= A & C <= B"; |
158 |
by (Blast_tac 1); |
|
159 |
qed "Int_subset_iff"; |
|
0 | 160 |
|
9180 | 161 |
Goal "A Int B <= A"; |
162 |
by (Blast_tac 1); |
|
163 |
qed "Int_lower1"; |
|
0 | 164 |
|
9180 | 165 |
Goal "A Int B <= B"; |
166 |
by (Blast_tac 1); |
|
167 |
qed "Int_lower2"; |
|
0 | 168 |
|
9180 | 169 |
Goal "[| C<=A; C<=B |] ==> C <= A Int B"; |
170 |
by (Blast_tac 1); |
|
171 |
qed "Int_greatest"; |
|
2469 | 172 |
|
0 | 173 |
|
174 |
(*** Set difference *) |
|
175 |
||
9180 | 176 |
Goal "A-B <= A"; |
177 |
by (Blast_tac 1); |
|
178 |
qed "Diff_subset"; |
|
0 | 179 |
|
9180 | 180 |
Goal "[| C<=A; C Int B = 0 |] ==> C <= A-B"; |
181 |
by (Blast_tac 1); |
|
182 |
qed "Diff_contains"; |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
183 |
|
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
184 |
Goal "B <= A - cons(c,C) <-> B<=A-C & c ~: B"; |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
185 |
by (Blast_tac 1); |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
186 |
qed "subset_Diff_cons_iff"; |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
187 |
|
2469 | 188 |
|
0 | 189 |
|
190 |
(** Collect **) |
|
191 |
||
9180 | 192 |
Goal "Collect(A,P) <= A"; |
193 |
by (Blast_tac 1); |
|
194 |
qed "Collect_subset"; |
|
2469 | 195 |
|
0 | 196 |
|
197 |
(** RepFun **) |
|
198 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
199 |
val prems = Goal "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B"; |
4091 | 200 |
by (blast_tac (claset() addIs prems) 1); |
760 | 201 |
qed "RepFun_subset"; |
689 | 202 |
|
9907 | 203 |
bind_thms ("subset_SIs", |
2469 | 204 |
[subset_refl, cons_subsetI, subset_consI, |
205 |
Union_least, UN_least, Un_least, |
|
206 |
Inter_greatest, Int_greatest, RepFun_subset, |
|
9907 | 207 |
Un_upper1, Un_upper2, Int_lower1, Int_lower2]); |
2469 | 208 |
|
689 | 209 |
|
2469 | 210 |
(*A claset for subset reasoning*) |
4091 | 211 |
val subset_cs = claset() |
2469 | 212 |
delrules [subsetI, subsetCE] |
213 |
addSIs subset_SIs |
|
214 |
addIs [Union_upper, Inter_lower] |
|
215 |
addSEs [cons_subsetE]; |
|
216 |