equal
deleted
inserted
replaced
16 Goal "{s. P} = (if P then UNIV else {})"; |
16 Goal "{s. P} = (if P then UNIV else {})"; |
17 by (Force_tac 1); |
17 by (Force_tac 1); |
18 qed "Collect_const"; |
18 qed "Collect_const"; |
19 Addsimps [Collect_const]; |
19 Addsimps [Collect_const]; |
20 |
20 |
|
21 (*If added as a simprule it can cause looping when equalityE is also present: |
|
22 A={} goes to {}<=A and A<={} and then back to A={} !*) |
21 Goal "(A <= {}) = (A = {})"; |
23 Goal "(A <= {}) = (A = {})"; |
22 by (Blast_tac 1); |
24 by (Blast_tac 1); |
23 qed "subset_empty"; |
25 qed "subset_empty"; |
24 Addsimps [subset_empty]; |
|
25 |
26 |
26 Goalw [psubset_def] "~ (A < {})"; |
27 Goalw [psubset_def] "~ (A < {})"; |
27 by (Blast_tac 1); |
28 by (Blast_tac 1); |
28 qed "not_psubset_empty"; |
29 qed "not_psubset_empty"; |
29 AddIffs [not_psubset_empty]; |
30 AddIffs [not_psubset_empty]; |