author | wenzelm |
Tue, 13 Jun 2006 23:41:39 +0200 | |
changeset 19876 | 11d447d5d68c |
parent 17456 | bcf7544875b2 |
permissions | -rw-r--r-- |
17456 | 1 |
(* Title: CCL/subsetI |
0 | 2 |
ID: $Id$ |
3 |
||
17456 | 4 |
Derived rules involving subsets. |
5 |
Union and Intersection as lattice operations. |
|
0 | 6 |
*) |
7 |
||
8 |
(*** Big Union -- least upper bound of a set ***) |
|
9 |
||
17456 | 10 |
val prems = goal (the_context ()) |
0 | 11 |
"B:A ==> B <= Union(A)"; |
12 |
by (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1)); |
|
757 | 13 |
qed "Union_upper"; |
0 | 14 |
|
17456 | 15 |
val prems = goal (the_context ()) |
0 | 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)); |
|
757 | 19 |
qed "Union_least"; |
0 | 20 |
|
21 |
||
22 |
(*** Big Intersection -- greatest lower bound of a set ***) |
|
23 |
||
17456 | 24 |
val prems = goal (the_context ()) |
0 | 25 |
"B:A ==> Inter(A) <= B"; |
26 |
by (REPEAT (resolve_tac (prems@[subsetI]) 1 |
|
27 |
ORELSE etac InterD 1)); |
|
757 | 28 |
qed "Inter_lower"; |
0 | 29 |
|
17456 | 30 |
val prems = goal (the_context ()) |
0 | 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)); |
|
757 | 34 |
qed "Inter_greatest"; |
0 | 35 |
|
36 |
(*** Finite Union -- the least upper bound of 2 sets ***) |
|
37 |
||
17456 | 38 |
goal (the_context ()) "A <= A Un B"; |
0 | 39 |
by (REPEAT (ares_tac [subsetI,UnI1] 1)); |
757 | 40 |
qed "Un_upper1"; |
0 | 41 |
|
17456 | 42 |
goal (the_context ()) "B <= A Un B"; |
0 | 43 |
by (REPEAT (ares_tac [subsetI,UnI2] 1)); |
757 | 44 |
qed "Un_upper2"; |
0 | 45 |
|
17456 | 46 |
val prems = goal (the_context ()) "[| A<=C; B<=C |] ==> A Un B <= C"; |
0 | 47 |
by (cut_facts_tac prems 1); |
48 |
by (DEPTH_SOLVE (ares_tac [subsetI] 1 |
|
49 |
ORELSE eresolve_tac [UnE,subsetD] 1)); |
|
757 | 50 |
qed "Un_least"; |
0 | 51 |
|
52 |
(*** Finite Intersection -- the greatest lower bound of 2 sets *) |
|
53 |
||
17456 | 54 |
goal (the_context ()) "A Int B <= A"; |
0 | 55 |
by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)); |
757 | 56 |
qed "Int_lower1"; |
0 | 57 |
|
17456 | 58 |
goal (the_context ()) "A Int B <= B"; |
0 | 59 |
by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)); |
757 | 60 |
qed "Int_lower2"; |
0 | 61 |
|
17456 | 62 |
val prems = goal (the_context ()) "[| C<=A; C<=B |] ==> C <= A Int B"; |
0 | 63 |
by (cut_facts_tac prems 1); |
64 |
by (REPEAT (ares_tac [subsetI,IntI] 1 |
|
65 |
ORELSE etac subsetD 1)); |
|
757 | 66 |
qed "Int_greatest"; |
0 | 67 |
|
68 |
(*** Monotonicity ***) |
|
69 |
||
17456 | 70 |
val [prem] = goalw (the_context ()) [mono_def] |
0 | 71 |
"[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)"; |
72 |
by (REPEAT (ares_tac [allI, impI, prem] 1)); |
|
757 | 73 |
qed "monoI"; |
0 | 74 |
|
17456 | 75 |
val [major,minor] = goalw (the_context ()) [mono_def] |
0 | 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); |
|
757 | 79 |
qed "monoD"; |
0 | 80 |
|
17456 | 81 |
val [prem] = goal (the_context ()) "mono(f) ==> f(A) Un f(B) <= f(A Un B)"; |
0 | 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); |
|
757 | 85 |
qed "mono_Un"; |
0 | 86 |
|
17456 | 87 |
val [prem] = goal (the_context ()) "mono(f) ==> f(A Int B) <= f(A) Int f(B)"; |
0 | 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); |
|
757 | 91 |
qed "mono_Int"; |
0 | 92 |
|
93 |
(****) |
|
94 |
||
95 |
val set_cs = FOL_cs |
|
96 |
addSIs [ballI, subsetI, InterI, INT_I, CollectI, |
|
1459 | 97 |
ComplI, IntI, UnCI, singletonI] |
0 | 98 |
addIs [bexI, UnionI, UN_I] |
99 |
addSEs [bexE, UnionE, UN_E, |
|
1459 | 100 |
CollectE, ComplE, IntE, UnE, emptyE, singletonE] |
0 | 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 |
||
17456 | 105 |
fun prover s = prove_goal (the_context ()) s (fn _=>[fast_tac set_cs 1]); |
0 | 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", |
|
3837 | 113 |
"(a : {x. P(x)}) <-> P(a)" ]); |
0 | 114 |
|
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset
|
115 |
val set_congs = [ball_cong, bex_cong, INT_cong, UN_cong]; |
0 | 116 |
|
1963 | 117 |
val set_ss = FOL_ss addcongs set_congs |
2035 | 118 |
addsimps mem_rews; |