author | wenzelm |
Sat, 15 Apr 2000 15:00:57 +0200 | |
changeset 8717 | 20c42415c07d |
parent 5325 | f7a5e06adea1 |
child 9180 | 3bda56c0d70d |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/subset |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
6 |
Derived rules involving subsets |
|
7 |
Union and Intersection as lattice operations |
|
8 |
*) |
|
9 |
||
10 |
(*** cons ***) |
|
11 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
12 |
qed_goal "cons_subsetI" thy "!!a. [| a:C; B<=C |] ==> cons(a,B) <= C" |
2877 | 13 |
(fn _ => [ Blast_tac 1 ]); |
0 | 14 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
15 |
qed_goal "subset_consI" thy "B <= cons(a,B)" |
2877 | 16 |
(fn _ => [ Blast_tac 1 ]); |
0 | 17 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
18 |
qed_goal "cons_subset_iff" thy "cons(a,B)<=C <-> a:C & B<=C" |
2877 | 19 |
(fn _ => [ Blast_tac 1 ]); |
0 | 20 |
|
21 |
(*A safe special case of subset elimination, adding no new variables |
|
22 |
[| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *) |
|
2469 | 23 |
bind_thm ("cons_subsetE", cons_subset_iff RS iffD1 RS conjE); |
0 | 24 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
25 |
qed_goal "subset_empty_iff" thy "A<=0 <-> A=0" |
2877 | 26 |
(fn _=> [ (Blast_tac 1) ]); |
0 | 27 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
28 |
qed_goal "subset_cons_iff" thy |
0 | 29 |
"C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)" |
2877 | 30 |
(fn _=> [ (Blast_tac 1) ]); |
0 | 31 |
|
32 |
(*** succ ***) |
|
33 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
34 |
qed_goal "subset_succI" thy "i <= succ(i)" |
2877 | 35 |
(fn _=> [ (Blast_tac 1) ]); |
0 | 36 |
|
37 |
(*But if j is an ordinal or is transitive, then i:j implies i<=j! |
|
38 |
See ordinal/Ord_succ_subsetI*) |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
39 |
qed_goalw "succ_subsetI" thy [succ_def] |
2469 | 40 |
"!!i j. [| i:j; i<=j |] ==> succ(i)<=j" |
2877 | 41 |
(fn _=> [ (Blast_tac 1) ]); |
0 | 42 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
43 |
qed_goalw "succ_subsetE" thy [succ_def] |
0 | 44 |
"[| succ(i) <= j; [| i:j; i<=j |] ==> P \ |
45 |
\ |] ==> P" |
|
46 |
(fn major::prems=> |
|
47 |
[ (rtac (major RS cons_subsetE) 1), |
|
48 |
(REPEAT (ares_tac prems 1)) ]); |
|
49 |
||
50 |
(*** singletons ***) |
|
51 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
52 |
qed_goal "singleton_subsetI" thy "!!a c. a:C ==> {a} <= C" |
2877 | 53 |
(fn _=> [ (Blast_tac 1) ]); |
0 | 54 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
55 |
qed_goal "singleton_subsetD" thy "!!a C. {a} <= C ==> a:C" |
2877 | 56 |
(fn _=> [ (Blast_tac 1) ]); |
0 | 57 |
|
58 |
(*** Big Union -- least upper bound of a set ***) |
|
59 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
60 |
qed_goal "Union_subset_iff" thy "Union(A) <= C <-> (ALL x:A. x <= C)" |
2877 | 61 |
(fn _ => [ Blast_tac 1 ]); |
0 | 62 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
63 |
qed_goal "Union_upper" thy |
2469 | 64 |
"!!B A. B:A ==> B <= Union(A)" |
2877 | 65 |
(fn _ => [ Blast_tac 1 ]); |
0 | 66 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
67 |
qed_goal "Union_least" thy |
0 | 68 |
"[| !!x. x:A ==> x<=C |] ==> Union(A) <= C" |
69 |
(fn [prem]=> |
|
70 |
[ (rtac (ballI RS (Union_subset_iff RS iffD2)) 1), |
|
71 |
(etac prem 1) ]); |
|
72 |
||
73 |
(*** Union of a family of sets ***) |
|
74 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
75 |
Goal "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))"; |
4091 | 76 |
by (blast_tac (claset() addSEs [equalityE]) 1); |
760 | 77 |
qed "subset_UN_iff_eq"; |
0 | 78 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
79 |
qed_goal "UN_subset_iff" thy |
3840 | 80 |
"(UN x:A. B(x)) <= C <-> (ALL x:A. B(x) <= C)" |
2877 | 81 |
(fn _ => [ Blast_tac 1 ]); |
0 | 82 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
83 |
qed_goal "UN_upper" thy |
3840 | 84 |
"!!x A. x:A ==> B(x) <= (UN x:A. B(x))" |
0 | 85 |
(fn _ => [ etac (RepFunI RS Union_upper) 1 ]); |
86 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
87 |
qed_goal "UN_least" thy |
3840 | 88 |
"[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C" |
0 | 89 |
(fn [prem]=> |
90 |
[ (rtac (ballI RS (UN_subset_iff RS iffD2)) 1), |
|
91 |
(etac prem 1) ]); |
|
92 |
||
93 |
||
94 |
(*** Big Intersection -- greatest lower bound of a nonempty set ***) |
|
95 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
96 |
qed_goal "Inter_subset_iff" thy |
0 | 97 |
"!!a A. a: A ==> C <= Inter(A) <-> (ALL x:A. C <= x)" |
2877 | 98 |
(fn _ => [ Blast_tac 1 ]); |
0 | 99 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
100 |
qed_goal "Inter_lower" thy "!!B A. B:A ==> Inter(A) <= B" |
2877 | 101 |
(fn _ => [ Blast_tac 1 ]); |
0 | 102 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
103 |
qed_goal "Inter_greatest" thy |
0 | 104 |
"[| a:A; !!x. x:A ==> C<=x |] ==> C <= Inter(A)" |
105 |
(fn [prem1,prem2]=> |
|
106 |
[ (rtac ([prem1, ballI] MRS (Inter_subset_iff RS iffD2)) 1), |
|
107 |
(etac prem2 1) ]); |
|
108 |
||
109 |
(*** Intersection of a family of sets ***) |
|
110 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
111 |
qed_goal "INT_lower" thy |
3840 | 112 |
"!!x. x:A ==> (INT x:A. B(x)) <= B(x)" |
2877 | 113 |
(fn _ => [ Blast_tac 1 ]); |
0 | 114 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
115 |
qed_goal "INT_greatest" thy |
3840 | 116 |
"[| a:A; !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))" |
0 | 117 |
(fn [nonempty,prem] => |
118 |
[ rtac (nonempty RS RepFunI RS Inter_greatest) 1, |
|
119 |
REPEAT (eresolve_tac [RepFunE, prem, ssubst] 1) ]); |
|
120 |
||
121 |
||
122 |
(*** Finite Union -- the least upper bound of 2 sets ***) |
|
123 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
124 |
qed_goal "Un_subset_iff" thy "A Un B <= C <-> A <= C & B <= C" |
2877 | 125 |
(fn _ => [ Blast_tac 1 ]); |
0 | 126 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
127 |
qed_goal "Un_upper1" thy "A <= A Un B" |
2877 | 128 |
(fn _ => [ Blast_tac 1 ]); |
0 | 129 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
130 |
qed_goal "Un_upper2" thy "B <= A Un B" |
2877 | 131 |
(fn _ => [ Blast_tac 1 ]); |
0 | 132 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
133 |
qed_goal "Un_least" thy "!!A B C. [| A<=C; B<=C |] ==> A Un B <= C" |
2877 | 134 |
(fn _ => [ Blast_tac 1 ]); |
2469 | 135 |
|
0 | 136 |
|
137 |
(*** Finite Intersection -- the greatest lower bound of 2 sets *) |
|
138 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
139 |
qed_goal "Int_subset_iff" thy "C <= A Int B <-> C <= A & C <= B" |
2877 | 140 |
(fn _ => [ Blast_tac 1 ]); |
0 | 141 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
142 |
qed_goal "Int_lower1" thy "A Int B <= A" |
2877 | 143 |
(fn _ => [ Blast_tac 1 ]); |
0 | 144 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
145 |
qed_goal "Int_lower2" thy "A Int B <= B" |
2877 | 146 |
(fn _ => [ Blast_tac 1 ]); |
0 | 147 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
148 |
qed_goal "Int_greatest" thy "!!A B C. [| C<=A; C<=B |] ==> C <= A Int B" |
2877 | 149 |
(fn _ => [ Blast_tac 1 ]); |
2469 | 150 |
|
0 | 151 |
|
152 |
(*** Set difference *) |
|
153 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
154 |
qed_goal "Diff_subset" thy "A-B <= A" |
2877 | 155 |
(fn _ => [ Blast_tac 1 ]); |
0 | 156 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
157 |
qed_goal "Diff_contains" thy |
2469 | 158 |
"!!C. [| C<=A; C Int B = 0 |] ==> C <= A-B" |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
159 |
(fn _ => [ Blast_tac 1 ]); |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
160 |
|
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
161 |
Goal "B <= A - cons(c,C) <-> B<=A-C & c ~: B"; |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
162 |
by (Blast_tac 1); |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
163 |
qed "subset_Diff_cons_iff"; |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
164 |
|
2469 | 165 |
|
0 | 166 |
|
167 |
(** Collect **) |
|
168 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
169 |
qed_goal "Collect_subset" thy "Collect(A,P) <= A" |
2877 | 170 |
(fn _ => [ Blast_tac 1 ]); |
2469 | 171 |
|
0 | 172 |
|
173 |
(** RepFun **) |
|
174 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
4091
diff
changeset
|
175 |
val prems = Goal "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B"; |
4091 | 176 |
by (blast_tac (claset() addIs prems) 1); |
760 | 177 |
qed "RepFun_subset"; |
689 | 178 |
|
2469 | 179 |
val subset_SIs = |
180 |
[subset_refl, cons_subsetI, subset_consI, |
|
181 |
Union_least, UN_least, Un_least, |
|
182 |
Inter_greatest, Int_greatest, RepFun_subset, |
|
183 |
Un_upper1, Un_upper2, Int_lower1, Int_lower2]; |
|
184 |
||
689 | 185 |
|
2469 | 186 |
(*A claset for subset reasoning*) |
4091 | 187 |
val subset_cs = claset() |
2469 | 188 |
delrules [subsetI, subsetCE] |
189 |
addSIs subset_SIs |
|
190 |
addIs [Union_upper, Inter_lower] |
|
191 |
addSEs [cons_subsetE]; |
|
192 |