equal
deleted
inserted
replaced
1 (* Title: HOL/LessThan/LessThan |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 *) |
|
7 |
|
8 |
|
9 (*** Finally, a few set-theoretic laws... |
|
10 CAN BOOLEAN SIMPLIFICATION BE AUTOMATED? ***) |
|
11 |
|
12 (** Rewrite rules to eliminate A. Conditions can be satisfied by letting B |
|
13 be any set including A Int C and contained in A Un C, such as B=A or B=C. |
|
14 **) |
|
15 |
|
16 Goal "[| A Int C <= B; B <= A Un C |] \ |
|
17 \ ==> (A Int B) Un (-A Int C) = B Un C"; |
|
18 by (Blast_tac 1); |
|
19 qed "set_cancel1"; |
|
20 |
|
21 Goal "[| A Int C <= B; B <= A Un C |] \ |
|
22 \ ==> (A Un B) Int (-A Un C) = B Int C"; |
|
23 by (Blast_tac 1); |
|
24 qed "set_cancel2"; |
|
25 |
|
26 (*The base B=A*) |
|
27 Goal "A Un (-A Int C) = A Un C"; |
|
28 by (Blast_tac 1); |
|
29 qed "set_cancel3"; |
|
30 |
|
31 Goal "A Int (-A Un C) = A Int C"; |
|
32 by (Blast_tac 1); |
|
33 qed "set_cancel4"; |
|
34 |
|
35 (*The base B=C*) |
|
36 Goal "(A Int C) Un (-A Int C) = C"; |
|
37 by (Blast_tac 1); |
|
38 qed "set_cancel5"; |
|
39 |
|
40 Goal "(A Un C) Int (-A Un C) = C"; |
|
41 by (Blast_tac 1); |
|
42 qed "set_cancel6"; |
|
43 |
|
44 Addsimps [set_cancel1, set_cancel2, set_cancel3, |
|
45 set_cancel4, set_cancel5, set_cancel6]; |
|
46 |
|
47 |
|