|
1 (* Title: ZF/subset |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 Derived rules involving subsets |
|
7 Union and Intersection as lattice operations |
|
8 *) |
|
9 |
|
10 (*** cons ***) |
|
11 |
|
12 val cons_subsetI = prove_goal ZF.thy "[| a:C; B<=C |] ==> cons(a,B) <= C" |
|
13 (fn prems=> |
|
14 [ (cut_facts_tac prems 1), |
|
15 (REPEAT (ares_tac [subsetI] 1 |
|
16 ORELSE eresolve_tac [consE,ssubst,subsetD] 1)) ]); |
|
17 |
|
18 val subset_consI = prove_goal ZF.thy "B <= cons(a,B)" |
|
19 (fn _=> [ (rtac subsetI 1), (etac consI2 1) ]); |
|
20 |
|
21 (*Useful for rewriting!*) |
|
22 val cons_subset_iff = prove_goal ZF.thy "cons(a,B)<=C <-> a:C & B<=C" |
|
23 (fn _=> [ (fast_tac upair_cs 1) ]); |
|
24 |
|
25 (*A safe special case of subset elimination, adding no new variables |
|
26 [| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *) |
|
27 val cons_subsetE = standard (cons_subset_iff RS iffD1 RS conjE); |
|
28 |
|
29 val subset_empty_iff = prove_goal ZF.thy "A<=0 <-> A=0" |
|
30 (fn _=> [ (fast_tac (upair_cs addIs [equalityI]) 1) ]); |
|
31 |
|
32 val subset_cons_iff = prove_goal ZF.thy |
|
33 "C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)" |
|
34 (fn _=> [ (fast_tac upair_cs 1) ]); |
|
35 |
|
36 (*** succ ***) |
|
37 |
|
38 val subset_succI = prove_goal ZF.thy "i <= succ(i)" |
|
39 (fn _=> [ (rtac subsetI 1), (etac succI2 1) ]); |
|
40 |
|
41 (*But if j is an ordinal or is transitive, then i:j implies i<=j! |
|
42 See ordinal/Ord_succ_subsetI*) |
|
43 val succ_subsetI = prove_goalw ZF.thy [succ_def] |
|
44 "[| i:j; i<=j |] ==> succ(i)<=j" |
|
45 (fn prems=> |
|
46 [ (REPEAT (ares_tac (prems@[cons_subsetI]) 1)) ]); |
|
47 |
|
48 val succ_subsetE = prove_goalw ZF.thy [succ_def] |
|
49 "[| succ(i) <= j; [| i:j; i<=j |] ==> P \ |
|
50 \ |] ==> P" |
|
51 (fn major::prems=> |
|
52 [ (rtac (major RS cons_subsetE) 1), |
|
53 (REPEAT (ares_tac prems 1)) ]); |
|
54 |
|
55 (*** singletons ***) |
|
56 |
|
57 val singleton_subsetI = prove_goal ZF.thy |
|
58 "a:C ==> {a} <= C" |
|
59 (fn prems=> |
|
60 [ (REPEAT (resolve_tac (prems@[cons_subsetI,empty_subsetI]) 1)) ]); |
|
61 |
|
62 val singleton_subsetD = prove_goal ZF.thy |
|
63 "{a} <= C ==> a:C" |
|
64 (fn prems=> [ (REPEAT (ares_tac (prems@[cons_subsetE]) 1)) ]); |
|
65 |
|
66 (*** Big Union -- least upper bound of a set ***) |
|
67 |
|
68 val Union_subset_iff = prove_goal ZF.thy "Union(A) <= C <-> (ALL x:A. x <= C)" |
|
69 (fn _ => [ fast_tac upair_cs 1 ]); |
|
70 |
|
71 val Union_upper = prove_goal ZF.thy |
|
72 "B:A ==> B <= Union(A)" |
|
73 (fn prems=> [ (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1)) ]); |
|
74 |
|
75 val Union_least = prove_goal ZF.thy |
|
76 "[| !!x. x:A ==> x<=C |] ==> Union(A) <= C" |
|
77 (fn [prem]=> |
|
78 [ (rtac (ballI RS (Union_subset_iff RS iffD2)) 1), |
|
79 (etac prem 1) ]); |
|
80 |
|
81 (*** Union of a family of sets ***) |
|
82 |
|
83 goal ZF.thy "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))"; |
|
84 by (fast_tac (upair_cs addSIs [equalityI] addSEs [equalityE]) 1); |
|
85 val subset_UN_iff_eq = result(); |
|
86 |
|
87 val UN_subset_iff = prove_goal ZF.thy |
|
88 "(UN x:A.B(x)) <= C <-> (ALL x:A. B(x) <= C)" |
|
89 (fn _ => [ fast_tac upair_cs 1 ]); |
|
90 |
|
91 val UN_upper = prove_goal ZF.thy |
|
92 "!!x A. x:A ==> B(x) <= (UN x:A.B(x))" |
|
93 (fn _ => [ etac (RepFunI RS Union_upper) 1 ]); |
|
94 |
|
95 val UN_least = prove_goal ZF.thy |
|
96 "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A.B(x)) <= C" |
|
97 (fn [prem]=> |
|
98 [ (rtac (ballI RS (UN_subset_iff RS iffD2)) 1), |
|
99 (etac prem 1) ]); |
|
100 |
|
101 |
|
102 (*** Big Intersection -- greatest lower bound of a nonempty set ***) |
|
103 |
|
104 val Inter_subset_iff = prove_goal ZF.thy |
|
105 "!!a A. a: A ==> C <= Inter(A) <-> (ALL x:A. C <= x)" |
|
106 (fn _ => [ fast_tac upair_cs 1 ]); |
|
107 |
|
108 val Inter_lower = prove_goal ZF.thy "B:A ==> Inter(A) <= B" |
|
109 (fn prems=> |
|
110 [ (REPEAT (resolve_tac (prems@[subsetI]) 1 |
|
111 ORELSE etac InterD 1)) ]); |
|
112 |
|
113 val Inter_greatest = prove_goal ZF.thy |
|
114 "[| a:A; !!x. x:A ==> C<=x |] ==> C <= Inter(A)" |
|
115 (fn [prem1,prem2]=> |
|
116 [ (rtac ([prem1, ballI] MRS (Inter_subset_iff RS iffD2)) 1), |
|
117 (etac prem2 1) ]); |
|
118 |
|
119 (*** Intersection of a family of sets ***) |
|
120 |
|
121 val INT_lower = prove_goal ZF.thy |
|
122 "x:A ==> (INT x:A.B(x)) <= B(x)" |
|
123 (fn [prem] => |
|
124 [ rtac (prem RS RepFunI RS Inter_lower) 1 ]); |
|
125 |
|
126 val INT_greatest = prove_goal ZF.thy |
|
127 "[| a:A; !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A.B(x))" |
|
128 (fn [nonempty,prem] => |
|
129 [ rtac (nonempty RS RepFunI RS Inter_greatest) 1, |
|
130 REPEAT (eresolve_tac [RepFunE, prem, ssubst] 1) ]); |
|
131 |
|
132 |
|
133 (*** Finite Union -- the least upper bound of 2 sets ***) |
|
134 |
|
135 val Un_subset_iff = prove_goal ZF.thy "A Un B <= C <-> A <= C & B <= C" |
|
136 (fn _ => [ fast_tac upair_cs 1 ]); |
|
137 |
|
138 val Un_upper1 = prove_goal ZF.thy "A <= A Un B" |
|
139 (fn _ => [ (REPEAT (ares_tac [subsetI,UnI1] 1)) ]); |
|
140 |
|
141 val Un_upper2 = prove_goal ZF.thy "B <= A Un B" |
|
142 (fn _ => [ (REPEAT (ares_tac [subsetI,UnI2] 1)) ]); |
|
143 |
|
144 val Un_least = prove_goal ZF.thy "!!A B C. [| A<=C; B<=C |] ==> A Un B <= C" |
|
145 (fn _ => |
|
146 [ (rtac (Un_subset_iff RS iffD2) 1), |
|
147 (REPEAT (ares_tac [conjI] 1)) ]); |
|
148 |
|
149 (*** Finite Intersection -- the greatest lower bound of 2 sets *) |
|
150 |
|
151 val Int_subset_iff = prove_goal ZF.thy "C <= A Int B <-> C <= A & C <= B" |
|
152 (fn _ => [ fast_tac upair_cs 1 ]); |
|
153 |
|
154 val Int_lower1 = prove_goal ZF.thy "A Int B <= A" |
|
155 (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)) ]); |
|
156 |
|
157 val Int_lower2 = prove_goal ZF.thy "A Int B <= B" |
|
158 (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)) ]); |
|
159 |
|
160 val Int_greatest = prove_goal ZF.thy |
|
161 "!!A B C. [| C<=A; C<=B |] ==> C <= A Int B" |
|
162 (fn prems=> |
|
163 [ (rtac (Int_subset_iff RS iffD2) 1), |
|
164 (REPEAT (ares_tac [conjI] 1)) ]); |
|
165 |
|
166 (*** Set difference *) |
|
167 |
|
168 val Diff_subset = prove_goal ZF.thy "A-B <= A" |
|
169 (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac DiffE 1)) ]); |
|
170 |
|
171 val Diff_contains = prove_goal ZF.thy |
|
172 "[| C<=A; C Int B = 0 |] ==> C <= A-B" |
|
173 (fn prems=> |
|
174 [ (cut_facts_tac prems 1), |
|
175 (rtac subsetI 1), |
|
176 (REPEAT (ares_tac [DiffI,IntI,notI] 1 |
|
177 ORELSE eresolve_tac [subsetD,equals0D] 1)) ]); |
|
178 |
|
179 (** Collect **) |
|
180 |
|
181 val Collect_subset = prove_goal ZF.thy "Collect(A,P) <= A" |
|
182 (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac CollectD1 1)) ]); |
|
183 |
|
184 (** RepFun **) |
|
185 |
|
186 val prems = goal ZF.thy "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B"; |
|
187 by (rtac subsetI 1); |
|
188 by (etac RepFunE 1); |
|
189 by (etac ssubst 1); |
|
190 by (eresolve_tac prems 1); |
|
191 val RepFun_subset = result(); |