1 (* Title: CCL/subsetI |
|
2 ID: $Id$ |
|
3 |
|
4 Derived rules involving subsets. |
|
5 Union and Intersection as lattice operations. |
|
6 *) |
|
7 |
|
8 (*** Big Union -- least upper bound of a set ***) |
|
9 |
|
10 val prems = goal (the_context ()) |
|
11 "B:A ==> B <= Union(A)"; |
|
12 by (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1)); |
|
13 qed "Union_upper"; |
|
14 |
|
15 val prems = goal (the_context ()) |
|
16 "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C"; |
|
17 by (REPEAT (ares_tac [subsetI] 1 |
|
18 ORELSE eresolve_tac ([UnionE] @ (prems RL [subsetD])) 1)); |
|
19 qed "Union_least"; |
|
20 |
|
21 |
|
22 (*** Big Intersection -- greatest lower bound of a set ***) |
|
23 |
|
24 val prems = goal (the_context ()) |
|
25 "B:A ==> Inter(A) <= B"; |
|
26 by (REPEAT (resolve_tac (prems@[subsetI]) 1 |
|
27 ORELSE etac InterD 1)); |
|
28 qed "Inter_lower"; |
|
29 |
|
30 val prems = goal (the_context ()) |
|
31 "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)"; |
|
32 by (REPEAT (ares_tac [subsetI,InterI] 1 |
|
33 ORELSE eresolve_tac (prems RL [subsetD]) 1)); |
|
34 qed "Inter_greatest"; |
|
35 |
|
36 (*** Finite Union -- the least upper bound of 2 sets ***) |
|
37 |
|
38 goal (the_context ()) "A <= A Un B"; |
|
39 by (REPEAT (ares_tac [subsetI,UnI1] 1)); |
|
40 qed "Un_upper1"; |
|
41 |
|
42 goal (the_context ()) "B <= A Un B"; |
|
43 by (REPEAT (ares_tac [subsetI,UnI2] 1)); |
|
44 qed "Un_upper2"; |
|
45 |
|
46 val prems = goal (the_context ()) "[| A<=C; B<=C |] ==> A Un B <= C"; |
|
47 by (cut_facts_tac prems 1); |
|
48 by (DEPTH_SOLVE (ares_tac [subsetI] 1 |
|
49 ORELSE eresolve_tac [UnE,subsetD] 1)); |
|
50 qed "Un_least"; |
|
51 |
|
52 (*** Finite Intersection -- the greatest lower bound of 2 sets *) |
|
53 |
|
54 goal (the_context ()) "A Int B <= A"; |
|
55 by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)); |
|
56 qed "Int_lower1"; |
|
57 |
|
58 goal (the_context ()) "A Int B <= B"; |
|
59 by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)); |
|
60 qed "Int_lower2"; |
|
61 |
|
62 val prems = goal (the_context ()) "[| C<=A; C<=B |] ==> C <= A Int B"; |
|
63 by (cut_facts_tac prems 1); |
|
64 by (REPEAT (ares_tac [subsetI,IntI] 1 |
|
65 ORELSE etac subsetD 1)); |
|
66 qed "Int_greatest"; |
|
67 |
|
68 (*** Monotonicity ***) |
|
69 |
|
70 val [prem] = goalw (the_context ()) [mono_def] |
|
71 "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)"; |
|
72 by (REPEAT (ares_tac [allI, impI, prem] 1)); |
|
73 qed "monoI"; |
|
74 |
|
75 val [major,minor] = goalw (the_context ()) [mono_def] |
|
76 "[| mono(f); A <= B |] ==> f(A) <= f(B)"; |
|
77 by (rtac (major RS spec RS spec RS mp) 1); |
|
78 by (rtac minor 1); |
|
79 qed "monoD"; |
|
80 |
|
81 val [prem] = goal (the_context ()) "mono(f) ==> f(A) Un f(B) <= f(A Un B)"; |
|
82 by (rtac Un_least 1); |
|
83 by (rtac (Un_upper1 RS (prem RS monoD)) 1); |
|
84 by (rtac (Un_upper2 RS (prem RS monoD)) 1); |
|
85 qed "mono_Un"; |
|
86 |
|
87 val [prem] = goal (the_context ()) "mono(f) ==> f(A Int B) <= f(A) Int f(B)"; |
|
88 by (rtac Int_greatest 1); |
|
89 by (rtac (Int_lower1 RS (prem RS monoD)) 1); |
|
90 by (rtac (Int_lower2 RS (prem RS monoD)) 1); |
|
91 qed "mono_Int"; |
|
92 |
|
93 (****) |
|
94 |
|
95 val set_cs = FOL_cs |
|
96 addSIs [ballI, subsetI, InterI, INT_I, CollectI, |
|
97 ComplI, IntI, UnCI, singletonI] |
|
98 addIs [bexI, UnionI, UN_I] |
|
99 addSEs [bexE, UnionE, UN_E, |
|
100 CollectE, ComplE, IntE, UnE, emptyE, singletonE] |
|
101 addEs [ballE, InterD, InterE, INT_D, INT_E, subsetD, subsetCE]; |
|
102 |
|
103 fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac set_cs; |
|
104 |
|
105 fun prover s = prove_goal (the_context ()) s (fn _=>[fast_tac set_cs 1]); |
|
106 |
|
107 val mem_rews = [trivial_set,empty_eq] @ (map prover |
|
108 [ "(a : A Un B) <-> (a:A | a:B)", |
|
109 "(a : A Int B) <-> (a:A & a:B)", |
|
110 "(a : Compl(B)) <-> (~a:B)", |
|
111 "(a : {b}) <-> (a=b)", |
|
112 "(a : {}) <-> False", |
|
113 "(a : {x. P(x)}) <-> P(a)" ]); |
|
114 |
|
115 val set_congs = [ball_cong, bex_cong, INT_cong, UN_cong]; |
|
116 |
|
117 val set_ss = FOL_ss addcongs set_congs |
|
118 addsimps mem_rews; |
|