1 (* Title: Psubset.ML |
|
2 Author: Martin Coen, Cambridge University Computer Laboratory |
|
3 Copyright 1993 University of Cambridge |
|
4 |
|
5 Properties of subsets and empty sets. |
|
6 *) |
|
7 |
|
8 open Psubset; |
|
9 |
|
10 (*********) |
|
11 |
|
12 (*** Rules for subsets ***) |
|
13 |
|
14 goal Set.thy "A <= B = (! t.t:A --> t:B)"; |
|
15 by (Blast_tac 1); |
|
16 qed "subset_iff"; |
|
17 |
|
18 goalw thy [psubset_def] "!!A::'a set. [| A <= B; A ~= B |] ==> A<B"; |
|
19 by (Blast_tac 1); |
|
20 qed "psubsetI"; |
|
21 |
|
22 |
|
23 goalw thy [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))"; |
|
24 by (Blast_tac 1); |
|
25 qed "subset_iff_psubset_eq"; |
|
26 |
|
27 |
|
28 goal Set.thy "!!a. insert a A ~= insert a B ==> A ~= B"; |
|
29 by (Blast_tac 1); |
|
30 qed "insert_lim"; |
|
31 |
|
32 (* This is an adaptation of the proof for the "<=" version in Finite. *) |
|
33 |
|
34 goalw thy [psubset_def] |
|
35 "!!B. finite B ==> !A. A < B --> card(A) < card(B)"; |
|
36 by (etac finite_induct 1); |
|
37 by (Simp_tac 1); |
|
38 by (Blast_tac 1); |
|
39 by (strip_tac 1); |
|
40 by (etac conjE 1); |
|
41 by (case_tac "x:A" 1); |
|
42 (*1*) |
|
43 by (dtac mk_disjoint_insert 1); |
|
44 by (etac exE 1); |
|
45 by (etac conjE 1); |
|
46 by (hyp_subst_tac 1); |
|
47 by (rotate_tac ~1 1); |
|
48 by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1); |
|
49 by (dtac insert_lim 1); |
|
50 by (Asm_full_simp_tac 1); |
|
51 (*2*) |
|
52 by (rotate_tac ~1 1); |
|
53 by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1); |
|
54 by (case_tac "A=F" 1); |
|
55 by (Asm_simp_tac 1); |
|
56 by (Asm_simp_tac 1); |
|
57 by (subgoal_tac "card A <= card F" 1); |
|
58 by (Asm_simp_tac 2); |
|
59 by (Auto_tac()); |
|
60 qed_spec_mp "psubset_card" ; |
|
61 |
|
62 |
|
63 goal Set.thy "(A = B) = ((A <= (B::'a set)) & (B<=A))"; |
|
64 by (Blast_tac 1); |
|
65 qed "set_eq_subset"; |
|
66 |
|
67 |
|
68 goalw thy [psubset_def] "~ (A < {})"; |
|
69 by (Blast_tac 1); |
|
70 qed "not_psubset_empty"; |
|
71 |
|
72 AddIffs [not_psubset_empty]; |
|
73 |
|
74 goalw thy [psubset_def] |
|
75 "!!x. A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B"; |
|
76 by (Auto_tac()); |
|
77 qed "psubset_insertD"; |
|
78 |
|
79 |
|
80 (*NB we do not have [| A < B; C < D |] ==> A Un C < B Un D |
|
81 even for finite sets: consider A={1}, C={2}, B=D={1,2} *) |
|
82 |
|
83 |
|