equal
deleted
inserted
replaced
150 qed "Int_assoc"; |
150 qed "Int_assoc"; |
151 |
151 |
152 (*Intersection is an AC-operator*) |
152 (*Intersection is an AC-operator*) |
153 val Int_ac = [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute]; |
153 val Int_ac = [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute]; |
154 |
154 |
|
155 goal thy "!!A B. B<=A ==> A Int B = B"; |
|
156 by (Blast_tac 1); |
|
157 qed "Int_absorb1"; |
|
158 |
|
159 goal thy "!!A B. A<=B ==> A Int B = A"; |
|
160 by (Blast_tac 1); |
|
161 qed "Int_absorb2"; |
|
162 |
155 goal thy "{} Int B = {}"; |
163 goal thy "{} Int B = {}"; |
156 by (Blast_tac 1); |
164 by (Blast_tac 1); |
157 qed "Int_empty_left"; |
165 qed "Int_empty_left"; |
158 Addsimps[Int_empty_left]; |
166 Addsimps[Int_empty_left]; |
159 |
167 |
221 qed "Un_assoc"; |
229 qed "Un_assoc"; |
222 |
230 |
223 (*Union is an AC-operator*) |
231 (*Union is an AC-operator*) |
224 val Un_ac = [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute]; |
232 val Un_ac = [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute]; |
225 |
233 |
|
234 goal thy "!!A B. A<=B ==> A Un B = B"; |
|
235 by (Blast_tac 1); |
|
236 qed "Un_absorb1"; |
|
237 |
|
238 goal thy "!!A B. B<=A ==> A Un B = A"; |
|
239 by (Blast_tac 1); |
|
240 qed "Un_absorb2"; |
|
241 |
226 goal thy "{} Un B = B"; |
242 goal thy "{} Un B = B"; |
227 by (Blast_tac 1); |
243 by (Blast_tac 1); |
228 qed "Un_empty_left"; |
244 qed "Un_empty_left"; |
229 Addsimps[Un_empty_left]; |
245 Addsimps[Un_empty_left]; |
230 |
246 |
548 |
564 |
549 section "-"; |
565 section "-"; |
550 |
566 |
551 goal thy "A-B = A Int Compl B"; |
567 goal thy "A-B = A Int Compl B"; |
552 by (Blast_tac 1); |
568 by (Blast_tac 1); |
553 qed "Diff_eq_Int_Compl"; |
569 qed "Diff_eq"; |
554 |
570 |
555 goal thy "A-A = {}"; |
571 goal thy "A-A = {}"; |
556 by (Blast_tac 1); |
572 by (Blast_tac 1); |
557 qed "Diff_cancel"; |
573 qed "Diff_cancel"; |
558 Addsimps[Diff_cancel]; |
574 Addsimps[Diff_cancel]; |
634 |
650 |
635 goal thy "(A Un B) - C = (A - C) Un (B - C)"; |
651 goal thy "(A Un B) - C = (A - C) Un (B - C)"; |
636 by (Blast_tac 1); |
652 by (Blast_tac 1); |
637 qed "Un_Diff"; |
653 qed "Un_Diff"; |
638 |
654 |
639 goal thy "(A Int B) - C = (A - C) Int (B - C)"; |
655 goal thy "(A Int B) - C = A Int (B - C)"; |
640 by (Blast_tac 1); |
656 by (Blast_tac 1); |
641 qed "Int_Diff"; |
657 qed "Int_Diff"; |
642 |
658 |
643 goal thy "(A-B) Int C = (A Int C) - (B Int C)"; |
659 goal thy "(A-B) Int C = (A Int C) - (B Int C)"; |
644 by (Blast_tac 1); |
660 by (Blast_tac 1); |