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