author | nipkow |
Fri, 17 Jan 1997 18:32:24 +0100 | |
changeset 2523 | 0ccea141409b |
parent 2515 | 6ff9bd353121 |
child 2893 | 2ee005e46d6d |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/subset |
923 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
923 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
6 |
Derived rules involving subsets |
|
7 |
Union and Intersection as lattice operations |
|
8 |
*) |
|
9 |
||
10 |
(*** insert ***) |
|
11 |
||
12 |
qed_goal "subset_insertI" Set.thy "B <= insert a B" |
|
13 |
(fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]); |
|
14 |
||
1531 | 15 |
goal Set.thy "!!x. x ~: A ==> (A <= insert x B) = (A <= B)"; |
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1631
diff
changeset
|
16 |
by (Fast_tac 1); |
1531 | 17 |
qed "subset_insert"; |
18 |
||
923 | 19 |
(*** Big Union -- least upper bound of a set ***) |
20 |
||
21 |
val prems = goal Set.thy |
|
22 |
"B:A ==> B <= Union(A)"; |
|
23 |
by (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1)); |
|
24 |
qed "Union_upper"; |
|
25 |
||
26 |
val [prem] = goal Set.thy |
|
27 |
"[| !!X. X:A ==> X<=C |] ==> Union(A) <= C"; |
|
1465 | 28 |
by (rtac subsetI 1); |
923 | 29 |
by (REPEAT (eresolve_tac [asm_rl, UnionE, prem RS subsetD] 1)); |
30 |
qed "Union_least"; |
|
31 |
||
32 |
(** General union **) |
|
33 |
||
34 |
val prems = goal Set.thy |
|
35 |
"a:A ==> B(a) <= (UN x:A. B(x))"; |
|
36 |
by (REPEAT (ares_tac (prems@[UN_I RS subsetI]) 1)); |
|
37 |
qed "UN_upper"; |
|
38 |
||
39 |
val [prem] = goal Set.thy |
|
40 |
"[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C"; |
|
1465 | 41 |
by (rtac subsetI 1); |
923 | 42 |
by (REPEAT (eresolve_tac [asm_rl, UN_E, prem RS subsetD] 1)); |
43 |
qed "UN_least"; |
|
44 |
||
45 |
goal Set.thy "B(a) <= (UN x. B(x))"; |
|
46 |
by (REPEAT (ares_tac [UN1_I RS subsetI] 1)); |
|
47 |
qed "UN1_upper"; |
|
48 |
||
49 |
val [prem] = goal Set.thy "[| !!x. B(x)<=C |] ==> (UN x. B(x)) <= C"; |
|
1465 | 50 |
by (rtac subsetI 1); |
923 | 51 |
by (REPEAT (eresolve_tac [asm_rl, UN1_E, prem RS subsetD] 1)); |
52 |
qed "UN1_least"; |
|
53 |
||
54 |
||
55 |
(*** Big Intersection -- greatest lower bound of a set ***) |
|
56 |
||
57 |
val prems = goal Set.thy "B:A ==> Inter(A) <= B"; |
|
1465 | 58 |
by (rtac subsetI 1); |
923 | 59 |
by (REPEAT (resolve_tac prems 1 ORELSE etac InterD 1)); |
60 |
qed "Inter_lower"; |
|
61 |
||
62 |
val [prem] = goal Set.thy |
|
63 |
"[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)"; |
|
1465 | 64 |
by (rtac (InterI RS subsetI) 1); |
923 | 65 |
by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1)); |
66 |
qed "Inter_greatest"; |
|
67 |
||
68 |
val prems = goal Set.thy "a:A ==> (INT x:A. B(x)) <= B(a)"; |
|
1465 | 69 |
by (rtac subsetI 1); |
923 | 70 |
by (REPEAT (resolve_tac prems 1 ORELSE etac INT_D 1)); |
71 |
qed "INT_lower"; |
|
72 |
||
73 |
val [prem] = goal Set.thy |
|
74 |
"[| !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))"; |
|
1465 | 75 |
by (rtac (INT_I RS subsetI) 1); |
923 | 76 |
by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1)); |
77 |
qed "INT_greatest"; |
|
78 |
||
79 |
goal Set.thy "(INT x. B(x)) <= B(a)"; |
|
1465 | 80 |
by (rtac subsetI 1); |
923 | 81 |
by (REPEAT (resolve_tac prems 1 ORELSE etac INT1_D 1)); |
82 |
qed "INT1_lower"; |
|
83 |
||
84 |
val [prem] = goal Set.thy |
|
85 |
"[| !!x. C<=B(x) |] ==> C <= (INT x. B(x))"; |
|
1465 | 86 |
by (rtac (INT1_I RS subsetI) 1); |
923 | 87 |
by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1)); |
88 |
qed "INT1_greatest"; |
|
89 |
||
90 |
(*** Finite Union -- the least upper bound of 2 sets ***) |
|
91 |
||
92 |
goal Set.thy "A <= A Un B"; |
|
93 |
by (REPEAT (ares_tac [subsetI,UnI1] 1)); |
|
94 |
qed "Un_upper1"; |
|
95 |
||
96 |
goal Set.thy "B <= A Un B"; |
|
97 |
by (REPEAT (ares_tac [subsetI,UnI2] 1)); |
|
98 |
qed "Un_upper2"; |
|
99 |
||
100 |
val prems = goal Set.thy "[| A<=C; B<=C |] ==> A Un B <= C"; |
|
101 |
by (cut_facts_tac prems 1); |
|
102 |
by (DEPTH_SOLVE (ares_tac [subsetI] 1 |
|
103 |
ORELSE eresolve_tac [UnE,subsetD] 1)); |
|
104 |
qed "Un_least"; |
|
105 |
||
106 |
(*** Finite Intersection -- the greatest lower bound of 2 sets *) |
|
107 |
||
108 |
goal Set.thy "A Int B <= A"; |
|
109 |
by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)); |
|
110 |
qed "Int_lower1"; |
|
111 |
||
112 |
goal Set.thy "A Int B <= B"; |
|
113 |
by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)); |
|
114 |
qed "Int_lower2"; |
|
115 |
||
116 |
val prems = goal Set.thy "[| C<=A; C<=B |] ==> C <= A Int B"; |
|
117 |
by (cut_facts_tac prems 1); |
|
118 |
by (REPEAT (ares_tac [subsetI,IntI] 1 |
|
119 |
ORELSE etac subsetD 1)); |
|
120 |
qed "Int_greatest"; |
|
121 |
||
122 |
(*** Set difference ***) |
|
123 |
||
124 |
qed_goal "Diff_subset" Set.thy "A-B <= (A::'a set)" |
|
125 |
(fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac DiffE 1)) ]); |
|
126 |
||
127 |
(*** Monotonicity ***) |
|
128 |
||
129 |
val [prem] = goal Set.thy "mono(f) ==> f(A) Un f(B) <= f(A Un B)"; |
|
130 |
by (rtac Un_least 1); |
|
131 |
by (rtac (Un_upper1 RS (prem RS monoD)) 1); |
|
132 |
by (rtac (Un_upper2 RS (prem RS monoD)) 1); |
|
133 |
qed "mono_Un"; |
|
134 |
||
135 |
val [prem] = goal Set.thy "mono(f) ==> f(A Int B) <= f(A) Int f(B)"; |
|
136 |
by (rtac Int_greatest 1); |
|
137 |
by (rtac (Int_lower1 RS (prem RS monoD)) 1); |
|
138 |
by (rtac (Int_lower2 RS (prem RS monoD)) 1); |
|
139 |
qed "mono_Int"; |