equal
deleted
inserted
replaced
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1998 University of Cambridge |
4 Copyright 1998 University of Cambridge |
5 |
5 |
6 lessThan, greaterThan, atLeast, atMost |
6 lessThan, greaterThan, atLeast, atMost |
7 *) |
7 *) |
8 |
|
9 |
|
10 open LessThan; |
|
11 |
8 |
12 |
9 |
13 (*** lessThan ***) |
10 (*** lessThan ***) |
14 |
11 |
15 Goalw [lessThan_def] "(i: lessThan k) = (i<k)"; |
12 Goalw [lessThan_def] "(i: lessThan k) = (i<k)"; |
142 Goal "atMost n Int atLeast n = {n}"; |
139 Goal "atMost n Int atLeast n = {n}"; |
143 by (blast_tac (claset() addIs [le_anti_sym]) 1); |
140 by (blast_tac (claset() addIs [le_anti_sym]) 1); |
144 qed "atMost_Int_atLeast"; |
141 qed "atMost_Int_atLeast"; |
145 |
142 |
146 |
143 |
|
144 |
|
145 |
|
146 (*** Finally, a few set-theoretic laws... |
|
147 CAN BOOLEAN SIMPLIFICATION BE AUTOMATED? ***) |
|
148 |
|
149 context Set.thy; |
|
150 |
|
151 (** Rewrites rules to eliminate A. Conditions can be satisfied by letting B |
|
152 be any set including A Int C and contained in A Un C, such as B=A or B=C. |
|
153 **) |
|
154 |
|
155 Goal "[| A Int C <= B; B <= A Un C |] \ |
|
156 \ ==> (A Int B) Un (Compl A Int C) = B Un C"; |
|
157 by (Blast_tac 1); |
|
158 |
|
159 Goal "[| A Int C <= B; B <= A Un C |] \ |
|
160 \ ==> (A Un B) Int (Compl A Un C) = B Int C"; |
|
161 by (Blast_tac 1); |
|
162 |
|
163 (*The base B=A*) |
|
164 Goal "A Un (Compl A Int C) = A Un C"; |
|
165 by (Blast_tac 1); |
|
166 |
|
167 Goal "A Int (Compl A Un C) = A Int C"; |
|
168 by (Blast_tac 1); |
|
169 |
|
170 (*The base B=C*) |
|
171 Goal "(A Int C) Un (Compl A Int C) = C"; |
|
172 by (Blast_tac 1); |
|
173 |
|
174 Goal "(A Un C) Int (Compl A Un C) = C"; |
|
175 by (Blast_tac 1); |
|
176 |
|
177 |
|
178 (** More ad-hoc rules **) |
|
179 |
|
180 Goal "A Un B - (A - B) = B"; |
|
181 by (Blast_tac 1); |
|
182 qed "Un_Diff_Diff"; |
|
183 |
|
184 Goal "A Int (B - C) Un C = A Int B Un C"; |
|
185 by (Blast_tac 1); |
|
186 qed "Int_Diff_Un"; |
|
187 |
|
188 Goal "Union(B) Int A = (UN C:B. C Int A)"; |
|
189 by (Blast_tac 1); |
|
190 qed "Int_Union2"; |
|
191 |
|
192 Goal "Union(B) Int A = Union((%C. C Int A)``B)"; |
|
193 by (Blast_tac 1); |
|
194 qed "Int_Union_Union"; |
|
195 |