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