|
11603
|
1 |
(* Title: HOL/subset.ML
|
|
923
|
2 |
ID: $Id$
|
|
1465
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
923
|
4 |
Copyright 1991 University of Cambridge
|
|
|
5 |
|
|
11603
|
6 |
Derived rules involving subsets. Union and Intersection as lattice
|
|
|
7 |
operations.
|
|
923
|
8 |
*)
|
|
|
9 |
|
|
11979
|
10 |
(* legacy ML bindings *)
|
|
|
11 |
|
|
|
12 |
val Ball_def = thm "Ball_def";
|
|
|
13 |
val Bex_def = thm "Bex_def";
|
|
|
14 |
val Collect_mem_eq = thm "Collect_mem_eq";
|
|
|
15 |
val Compl_def = thm "Compl_def";
|
|
|
16 |
val INTER_def = thm "INTER_def";
|
|
|
17 |
val Int_def = thm "Int_def";
|
|
|
18 |
val Inter_def = thm "Inter_def";
|
|
|
19 |
val Pow_def = thm "Pow_def";
|
|
|
20 |
val UNION_def = thm "UNION_def";
|
|
|
21 |
val UNIV_def = thm "UNIV_def";
|
|
|
22 |
val Un_def = thm "Un_def";
|
|
|
23 |
val Union_def = thm "Union_def";
|
|
|
24 |
val empty_def = thm "empty_def";
|
|
|
25 |
val image_def = thm "image_def";
|
|
|
26 |
val insert_def = thm "insert_def";
|
|
|
27 |
val mem_Collect_eq = thm "mem_Collect_eq";
|
|
|
28 |
val psubset_def = thm "psubset_def";
|
|
|
29 |
val set_diff_def = thm "set_diff_def";
|
|
|
30 |
val subset_def = thm "subset_def";
|
|
|
31 |
val CollectI = thm "CollectI";
|
|
|
32 |
val CollectD = thm "CollectD";
|
|
|
33 |
val set_ext = thm "set_ext";
|
|
|
34 |
val Collect_cong = thm "Collect_cong";
|
|
|
35 |
val CollectE = thm "CollectE";
|
|
|
36 |
val ballI = thm "ballI";
|
|
|
37 |
val strip = thms "strip";
|
|
|
38 |
val bspec = thm "bspec";
|
|
|
39 |
val ballE = thm "ballE";
|
|
|
40 |
val bexI = thm "bexI";
|
|
|
41 |
val rev_bexI = thm "rev_bexI";
|
|
|
42 |
val bexCI = thm "bexCI";
|
|
|
43 |
val bexE = thm "bexE";
|
|
|
44 |
val ball_triv = thm "ball_triv";
|
|
|
45 |
val bex_triv = thm "bex_triv";
|
|
|
46 |
val bex_triv_one_point1 = thm "bex_triv_one_point1";
|
|
|
47 |
val bex_triv_one_point2 = thm "bex_triv_one_point2";
|
|
|
48 |
val bex_one_point1 = thm "bex_one_point1";
|
|
|
49 |
val bex_one_point2 = thm "bex_one_point2";
|
|
|
50 |
val ball_one_point1 = thm "ball_one_point1";
|
|
|
51 |
val ball_one_point2 = thm "ball_one_point2";
|
|
|
52 |
val ball_cong = thm "ball_cong";
|
|
|
53 |
val bex_cong = thm "bex_cong";
|
|
|
54 |
val subsetI = thm "subsetI";
|
|
|
55 |
val subsetD = thm "subsetD";
|
|
|
56 |
val rev_subsetD = thm "rev_subsetD";
|
|
|
57 |
val subsetCE = thm "subsetCE";
|
|
|
58 |
val contra_subsetD = thm "contra_subsetD";
|
|
|
59 |
val subset_refl = thm "subset_refl";
|
|
|
60 |
val subset_trans = thm "subset_trans";
|
|
|
61 |
val subset_antisym = thm "subset_antisym";
|
|
|
62 |
val equalityI = thm "equalityI";
|
|
|
63 |
val equalityD1 = thm "equalityD1";
|
|
|
64 |
val equalityD2 = thm "equalityD2";
|
|
|
65 |
val equalityE = thm "equalityE";
|
|
|
66 |
val equalityCE = thm "equalityCE";
|
|
|
67 |
val setup_induction = thm "setup_induction";
|
|
|
68 |
val eqset_imp_iff = thm "eqset_imp_iff";
|
|
|
69 |
val UNIV_I = thm "UNIV_I";
|
|
|
70 |
val UNIV_witness = thm "UNIV_witness";
|
|
|
71 |
val subset_UNIV = thm "subset_UNIV";
|
|
|
72 |
val ball_UNIV = thm "ball_UNIV";
|
|
|
73 |
val bex_UNIV = thm "bex_UNIV";
|
|
|
74 |
val empty_iff = thm "empty_iff";
|
|
|
75 |
val emptyE = thm "emptyE";
|
|
|
76 |
val empty_subsetI = thm "empty_subsetI";
|
|
|
77 |
val equals0I = thm "equals0I";
|
|
|
78 |
val equals0D = thm "equals0D";
|
|
|
79 |
val ball_empty = thm "ball_empty";
|
|
|
80 |
val bex_empty = thm "bex_empty";
|
|
|
81 |
val UNIV_not_empty = thm "UNIV_not_empty";
|
|
|
82 |
val Pow_iff = thm "Pow_iff";
|
|
|
83 |
val PowI = thm "PowI";
|
|
|
84 |
val PowD = thm "PowD";
|
|
|
85 |
val Pow_bottom = thm "Pow_bottom";
|
|
|
86 |
val Pow_top = thm "Pow_top";
|
|
|
87 |
val Compl_iff = thm "Compl_iff";
|
|
|
88 |
val ComplI = thm "ComplI";
|
|
|
89 |
val ComplD = thm "ComplD";
|
|
|
90 |
val ComplE = thm "ComplE";
|
|
|
91 |
val Un_iff = thm "Un_iff";
|
|
|
92 |
val UnI1 = thm "UnI1";
|
|
|
93 |
val UnI2 = thm "UnI2";
|
|
|
94 |
val UnCI = thm "UnCI";
|
|
|
95 |
val UnE = thm "UnE";
|
|
|
96 |
val Int_iff = thm "Int_iff";
|
|
|
97 |
val IntI = thm "IntI";
|
|
|
98 |
val IntD1 = thm "IntD1";
|
|
|
99 |
val IntD2 = thm "IntD2";
|
|
|
100 |
val IntE = thm "IntE";
|
|
|
101 |
val Diff_iff = thm "Diff_iff";
|
|
|
102 |
val DiffI = thm "DiffI";
|
|
|
103 |
val DiffD1 = thm "DiffD1";
|
|
|
104 |
val DiffD2 = thm "DiffD2";
|
|
|
105 |
val DiffE = thm "DiffE";
|
|
|
106 |
val insert_iff = thm "insert_iff";
|
|
|
107 |
val insertI1 = thm "insertI1";
|
|
|
108 |
val insertI2 = thm "insertI2";
|
|
|
109 |
val insertE = thm "insertE";
|
|
|
110 |
val insertCI = thm "insertCI";
|
|
|
111 |
val subset_insert_iff = thm "subset_insert_iff";
|
|
|
112 |
val singletonI = thm "singletonI";
|
|
|
113 |
val singletonD = thm "singletonD";
|
|
|
114 |
val singletonE = thm "singletonE";
|
|
|
115 |
val singleton_iff = thm "singleton_iff";
|
|
|
116 |
val singleton_inject = thm "singleton_inject";
|
|
|
117 |
val singleton_insert_inj_eq = thm "singleton_insert_inj_eq";
|
|
|
118 |
val singleton_insert_inj_eq' = thm "singleton_insert_inj_eq'";
|
|
|
119 |
val subset_singletonD = thm "subset_singletonD";
|
|
|
120 |
val singleton_conv = thm "singleton_conv";
|
|
|
121 |
val singleton_conv2 = thm "singleton_conv2";
|
|
|
122 |
val diff_single_insert = thm "diff_single_insert";
|
|
|
123 |
val UN_iff = thm "UN_iff";
|
|
|
124 |
val UN_I = thm "UN_I";
|
|
|
125 |
val UN_E = thm "UN_E";
|
|
|
126 |
val UN_cong = thm "UN_cong";
|
|
|
127 |
val INT_iff = thm "INT_iff";
|
|
|
128 |
val INT_I = thm "INT_I";
|
|
|
129 |
val INT_D = thm "INT_D";
|
|
|
130 |
val INT_E = thm "INT_E";
|
|
|
131 |
val INT_cong = thm "INT_cong";
|
|
|
132 |
val Union_iff = thm "Union_iff";
|
|
|
133 |
val UnionI = thm "UnionI";
|
|
|
134 |
val UnionE = thm "UnionE";
|
|
|
135 |
val Inter_iff = thm "Inter_iff";
|
|
|
136 |
val InterI = thm "InterI";
|
|
|
137 |
val InterD = thm "InterD";
|
|
|
138 |
val InterE = thm "InterE";
|
|
|
139 |
val image_eqI = thm "image_eqI";
|
|
|
140 |
val imageI = thm "imageI";
|
|
|
141 |
val rev_image_eqI = thm "rev_image_eqI";
|
|
|
142 |
val imageE = thm "imageE";
|
|
|
143 |
val image_Un = thm "image_Un";
|
|
|
144 |
val image_iff = thm "image_iff";
|
|
|
145 |
val image_subset_iff = thm "image_subset_iff";
|
|
|
146 |
val subset_image_iff = thm "subset_image_iff";
|
|
|
147 |
val image_subsetI = thm "image_subsetI";
|
|
|
148 |
val range_eqI = thm "range_eqI";
|
|
|
149 |
val rangeI = thm "rangeI";
|
|
|
150 |
val rangeE = thm "rangeE";
|
|
|
151 |
val split_if_eq1 = thm "split_if_eq1";
|
|
|
152 |
val split_if_eq2 = thm "split_if_eq2";
|
|
|
153 |
val split_if_mem1 = thm "split_if_mem1";
|
|
|
154 |
val split_if_mem2 = thm "split_if_mem2";
|
|
|
155 |
val split_ifs = thms "split_ifs";
|
|
|
156 |
val mem_simps = thms "mem_simps";
|
|
|
157 |
val psubsetI = thm "psubsetI";
|
|
|
158 |
val psubset_insert_iff = thm "psubset_insert_iff";
|
|
|
159 |
val psubset_eq = thm "psubset_eq";
|
|
|
160 |
val psubset_imp_subset = thm "psubset_imp_subset";
|
|
|
161 |
val psubset_subset_trans = thm "psubset_subset_trans";
|
|
|
162 |
val subset_psubset_trans = thm "subset_psubset_trans";
|
|
|
163 |
val psubset_imp_ex_mem = thm "psubset_imp_ex_mem";
|
|
|
164 |
val atomize_ball = thm "atomize_ball";
|
|
|
165 |
|
|
|
166 |
|
|
923
|
167 |
(*** insert ***)
|
|
|
168 |
|
|
7007
|
169 |
Goal "B <= insert a B";
|
|
|
170 |
by (rtac subsetI 1);
|
|
|
171 |
by (etac insertI2 1) ;
|
|
|
172 |
qed "subset_insertI";
|
|
923
|
173 |
|
|
5316
|
174 |
Goal "x ~: A ==> (A <= insert x B) = (A <= B)";
|
|
2893
|
175 |
by (Blast_tac 1);
|
|
1531
|
176 |
qed "subset_insert";
|
|
|
177 |
|
|
923
|
178 |
(*** Big Union -- least upper bound of a set ***)
|
|
|
179 |
|
|
5316
|
180 |
Goal "B:A ==> B <= Union(A)";
|
|
|
181 |
by (REPEAT (ares_tac [subsetI,UnionI] 1));
|
|
923
|
182 |
qed "Union_upper";
|
|
|
183 |
|
|
5316
|
184 |
val [prem] = Goal "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C";
|
|
1465
|
185 |
by (rtac subsetI 1);
|
|
923
|
186 |
by (REPEAT (eresolve_tac [asm_rl, UnionE, prem RS subsetD] 1));
|
|
|
187 |
qed "Union_least";
|
|
|
188 |
|
|
|
189 |
(** General union **)
|
|
|
190 |
|
|
5316
|
191 |
Goal "a:A ==> B(a) <= (UN x:A. B(x))";
|
|
|
192 |
by (Blast_tac 1);
|
|
923
|
193 |
qed "UN_upper";
|
|
|
194 |
|
|
5316
|
195 |
val [prem] = Goal "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C";
|
|
1465
|
196 |
by (rtac subsetI 1);
|
|
923
|
197 |
by (REPEAT (eresolve_tac [asm_rl, UN_E, prem RS subsetD] 1));
|
|
|
198 |
qed "UN_least";
|
|
|
199 |
|
|
|
200 |
|
|
|
201 |
(*** Big Intersection -- greatest lower bound of a set ***)
|
|
|
202 |
|
|
5316
|
203 |
Goal "B:A ==> Inter(A) <= B";
|
|
2893
|
204 |
by (Blast_tac 1);
|
|
923
|
205 |
qed "Inter_lower";
|
|
|
206 |
|
|
5316
|
207 |
val [prem] = Goal "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)";
|
|
1465
|
208 |
by (rtac (InterI RS subsetI) 1);
|
|
923
|
209 |
by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
|
|
|
210 |
qed "Inter_greatest";
|
|
|
211 |
|
|
5316
|
212 |
Goal "a:A ==> (INT x:A. B(x)) <= B(a)";
|
|
|
213 |
by (Blast_tac 1);
|
|
923
|
214 |
qed "INT_lower";
|
|
|
215 |
|
|
5316
|
216 |
val [prem] = Goal "[| !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))";
|
|
1465
|
217 |
by (rtac (INT_I RS subsetI) 1);
|
|
923
|
218 |
by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
|
|
|
219 |
qed "INT_greatest";
|
|
|
220 |
|
|
|
221 |
(*** Finite Union -- the least upper bound of 2 sets ***)
|
|
|
222 |
|
|
5316
|
223 |
Goal "A <= A Un B";
|
|
2893
|
224 |
by (Blast_tac 1);
|
|
923
|
225 |
qed "Un_upper1";
|
|
|
226 |
|
|
5316
|
227 |
Goal "B <= A Un B";
|
|
2893
|
228 |
by (Blast_tac 1);
|
|
923
|
229 |
qed "Un_upper2";
|
|
|
230 |
|
|
5316
|
231 |
Goal "[| A<=C; B<=C |] ==> A Un B <= C";
|
|
2893
|
232 |
by (Blast_tac 1);
|
|
923
|
233 |
qed "Un_least";
|
|
|
234 |
|
|
|
235 |
(*** Finite Intersection -- the greatest lower bound of 2 sets *)
|
|
|
236 |
|
|
5316
|
237 |
Goal "A Int B <= A";
|
|
2893
|
238 |
by (Blast_tac 1);
|
|
923
|
239 |
qed "Int_lower1";
|
|
|
240 |
|
|
5316
|
241 |
Goal "A Int B <= B";
|
|
2893
|
242 |
by (Blast_tac 1);
|
|
923
|
243 |
qed "Int_lower2";
|
|
|
244 |
|
|
5316
|
245 |
Goal "[| C<=A; C<=B |] ==> C <= A Int B";
|
|
2893
|
246 |
by (Blast_tac 1);
|
|
923
|
247 |
qed "Int_greatest";
|
|
|
248 |
|
|
|
249 |
(*** Set difference ***)
|
|
|
250 |
|
|
7007
|
251 |
Goal "A-B <= (A::'a set)";
|
|
|
252 |
by (Blast_tac 1) ;
|
|
|
253 |
qed "Diff_subset";
|
|
923
|
254 |
|
|
|
255 |
(*** Monotonicity ***)
|
|
|
256 |
|
|
5316
|
257 |
Goal "mono(f) ==> f(A) Un f(B) <= f(A Un B)";
|
|
923
|
258 |
by (rtac Un_least 1);
|
|
5316
|
259 |
by (etac (Un_upper1 RSN (2,monoD)) 1);
|
|
|
260 |
by (etac (Un_upper2 RSN (2,monoD)) 1);
|
|
923
|
261 |
qed "mono_Un";
|
|
|
262 |
|
|
5316
|
263 |
Goal "mono(f) ==> f(A Int B) <= f(A) Int f(B)";
|
|
923
|
264 |
by (rtac Int_greatest 1);
|
|
5316
|
265 |
by (etac (Int_lower1 RSN (2,monoD)) 1);
|
|
|
266 |
by (etac (Int_lower2 RSN (2,monoD)) 1);
|
|
923
|
267 |
qed "mono_Int";
|