author  clasohm 
Wed, 14 Dec 1994 11:41:49 +0100  
changeset 782  200a16083201 
parent 760  f0200e91b272 
child 1461  6bcb44e4d6e5 
permissions  rwrr 
0  1 
(* Title: ZF/subset 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1991 University of Cambridge 

5 

6 
Derived rules involving subsets 

7 
Union and Intersection as lattice operations 

8 
*) 

9 

10 
(*** cons ***) 

11 

760  12 
qed_goal "cons_subsetI" ZF.thy "[ a:C; B<=C ] ==> cons(a,B) <= C" 
0  13 
(fn prems=> 
14 
[ (cut_facts_tac prems 1), 

15 
(REPEAT (ares_tac [subsetI] 1 

16 
ORELSE eresolve_tac [consE,ssubst,subsetD] 1)) ]); 

17 

760  18 
qed_goal "subset_consI" ZF.thy "B <= cons(a,B)" 
0  19 
(fn _=> [ (rtac subsetI 1), (etac consI2 1) ]); 
20 

21 
(*Useful for rewriting!*) 

760  22 
qed_goal "cons_subset_iff" ZF.thy "cons(a,B)<=C <> a:C & B<=C" 
0  23 
(fn _=> [ (fast_tac upair_cs 1) ]); 
24 

25 
(*A safe special case of subset elimination, adding no new variables 

26 
[ cons(a,B) <= C; [ a : C; B <= C ] ==> R ] ==> R *) 

782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset

27 
bind_thm ("cons_subsetE", (cons_subset_iff RS iffD1 RS conjE)); 
0  28 

760  29 
qed_goal "subset_empty_iff" ZF.thy "A<=0 <> A=0" 
0  30 
(fn _=> [ (fast_tac (upair_cs addIs [equalityI]) 1) ]); 
31 

760  32 
qed_goal "subset_cons_iff" ZF.thy 
0  33 
"C<=cons(a,B) <> C<=B  (a:C & C{a} <= B)" 
34 
(fn _=> [ (fast_tac upair_cs 1) ]); 

35 

36 
(*** succ ***) 

37 

760  38 
qed_goal "subset_succI" ZF.thy "i <= succ(i)" 
0  39 
(fn _=> [ (rtac subsetI 1), (etac succI2 1) ]); 
40 

41 
(*But if j is an ordinal or is transitive, then i:j implies i<=j! 

42 
See ordinal/Ord_succ_subsetI*) 

760  43 
qed_goalw "succ_subsetI" ZF.thy [succ_def] 
0  44 
"[ i:j; i<=j ] ==> succ(i)<=j" 
45 
(fn prems=> 

46 
[ (REPEAT (ares_tac (prems@[cons_subsetI]) 1)) ]); 

47 

760  48 
qed_goalw "succ_subsetE" ZF.thy [succ_def] 
0  49 
"[ succ(i) <= j; [ i:j; i<=j ] ==> P \ 
50 
\ ] ==> P" 

51 
(fn major::prems=> 

52 
[ (rtac (major RS cons_subsetE) 1), 

53 
(REPEAT (ares_tac prems 1)) ]); 

54 

55 
(*** singletons ***) 

56 

760  57 
qed_goal "singleton_subsetI" ZF.thy 
0  58 
"a:C ==> {a} <= C" 
59 
(fn prems=> 

60 
[ (REPEAT (resolve_tac (prems@[cons_subsetI,empty_subsetI]) 1)) ]); 

61 

760  62 
qed_goal "singleton_subsetD" ZF.thy 
0  63 
"{a} <= C ==> a:C" 
64 
(fn prems=> [ (REPEAT (ares_tac (prems@[cons_subsetE]) 1)) ]); 

65 

66 
(*** Big Union  least upper bound of a set ***) 

67 

760  68 
qed_goal "Union_subset_iff" ZF.thy "Union(A) <= C <> (ALL x:A. x <= C)" 
0  69 
(fn _ => [ fast_tac upair_cs 1 ]); 
70 

760  71 
qed_goal "Union_upper" ZF.thy 
0  72 
"B:A ==> B <= Union(A)" 
73 
(fn prems=> [ (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1)) ]); 

74 

760  75 
qed_goal "Union_least" ZF.thy 
0  76 
"[ !!x. x:A ==> x<=C ] ==> Union(A) <= C" 
77 
(fn [prem]=> 

78 
[ (rtac (ballI RS (Union_subset_iff RS iffD2)) 1), 

79 
(etac prem 1) ]); 

80 

81 
(*** Union of a family of sets ***) 

82 

83 
goal ZF.thy "A <= (UN i:I. B(i)) <> A = (UN i:I. A Int B(i))"; 

84 
by (fast_tac (upair_cs addSIs [equalityI] addSEs [equalityE]) 1); 

760  85 
qed "subset_UN_iff_eq"; 
0  86 

760  87 
qed_goal "UN_subset_iff" ZF.thy 
0  88 
"(UN x:A.B(x)) <= C <> (ALL x:A. B(x) <= C)" 
89 
(fn _ => [ fast_tac upair_cs 1 ]); 

90 

760  91 
qed_goal "UN_upper" ZF.thy 
0  92 
"!!x A. x:A ==> B(x) <= (UN x:A.B(x))" 
93 
(fn _ => [ etac (RepFunI RS Union_upper) 1 ]); 

94 

760  95 
qed_goal "UN_least" ZF.thy 
0  96 
"[ !!x. x:A ==> B(x)<=C ] ==> (UN x:A.B(x)) <= C" 
97 
(fn [prem]=> 

98 
[ (rtac (ballI RS (UN_subset_iff RS iffD2)) 1), 

99 
(etac prem 1) ]); 

100 

101 

102 
(*** Big Intersection  greatest lower bound of a nonempty set ***) 

103 

760  104 
qed_goal "Inter_subset_iff" ZF.thy 
0  105 
"!!a A. a: A ==> C <= Inter(A) <> (ALL x:A. C <= x)" 
106 
(fn _ => [ fast_tac upair_cs 1 ]); 

107 

760  108 
qed_goal "Inter_lower" ZF.thy "B:A ==> Inter(A) <= B" 
0  109 
(fn prems=> 
110 
[ (REPEAT (resolve_tac (prems@[subsetI]) 1 

111 
ORELSE etac InterD 1)) ]); 

112 

760  113 
qed_goal "Inter_greatest" ZF.thy 
0  114 
"[ a:A; !!x. x:A ==> C<=x ] ==> C <= Inter(A)" 
115 
(fn [prem1,prem2]=> 

116 
[ (rtac ([prem1, ballI] MRS (Inter_subset_iff RS iffD2)) 1), 

117 
(etac prem2 1) ]); 

118 

119 
(*** Intersection of a family of sets ***) 

120 

760  121 
qed_goal "INT_lower" ZF.thy 
0  122 
"x:A ==> (INT x:A.B(x)) <= B(x)" 
123 
(fn [prem] => 

124 
[ rtac (prem RS RepFunI RS Inter_lower) 1 ]); 

125 

760  126 
qed_goal "INT_greatest" ZF.thy 
0  127 
"[ a:A; !!x. x:A ==> C<=B(x) ] ==> C <= (INT x:A.B(x))" 
128 
(fn [nonempty,prem] => 

129 
[ rtac (nonempty RS RepFunI RS Inter_greatest) 1, 

130 
REPEAT (eresolve_tac [RepFunE, prem, ssubst] 1) ]); 

131 

132 

133 
(*** Finite Union  the least upper bound of 2 sets ***) 

134 

760  135 
qed_goal "Un_subset_iff" ZF.thy "A Un B <= C <> A <= C & B <= C" 
0  136 
(fn _ => [ fast_tac upair_cs 1 ]); 
137 

760  138 
qed_goal "Un_upper1" ZF.thy "A <= A Un B" 
0  139 
(fn _ => [ (REPEAT (ares_tac [subsetI,UnI1] 1)) ]); 
140 

760  141 
qed_goal "Un_upper2" ZF.thy "B <= A Un B" 
0  142 
(fn _ => [ (REPEAT (ares_tac [subsetI,UnI2] 1)) ]); 
143 

760  144 
qed_goal "Un_least" ZF.thy "!!A B C. [ A<=C; B<=C ] ==> A Un B <= C" 
0  145 
(fn _ => 
146 
[ (rtac (Un_subset_iff RS iffD2) 1), 

147 
(REPEAT (ares_tac [conjI] 1)) ]); 

148 

149 
(*** Finite Intersection  the greatest lower bound of 2 sets *) 

150 

760  151 
qed_goal "Int_subset_iff" ZF.thy "C <= A Int B <> C <= A & C <= B" 
0  152 
(fn _ => [ fast_tac upair_cs 1 ]); 
153 

760  154 
qed_goal "Int_lower1" ZF.thy "A Int B <= A" 
0  155 
(fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)) ]); 
156 

760  157 
qed_goal "Int_lower2" ZF.thy "A Int B <= B" 
0  158 
(fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)) ]); 
159 

760  160 
qed_goal "Int_greatest" ZF.thy 
0  161 
"!!A B C. [ C<=A; C<=B ] ==> C <= A Int B" 
162 
(fn prems=> 

163 
[ (rtac (Int_subset_iff RS iffD2) 1), 

164 
(REPEAT (ares_tac [conjI] 1)) ]); 

165 

166 
(*** Set difference *) 

167 

760  168 
qed_goal "Diff_subset" ZF.thy "AB <= A" 
0  169 
(fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac DiffE 1)) ]); 
170 

760  171 
qed_goal "Diff_contains" ZF.thy 
0  172 
"[ C<=A; C Int B = 0 ] ==> C <= AB" 
173 
(fn prems=> 

174 
[ (cut_facts_tac prems 1), 

175 
(rtac subsetI 1), 

176 
(REPEAT (ares_tac [DiffI,IntI,notI] 1 

177 
ORELSE eresolve_tac [subsetD,equals0D] 1)) ]); 

178 

179 
(** Collect **) 

180 

760  181 
qed_goal "Collect_subset" ZF.thy "Collect(A,P) <= A" 
0  182 
(fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac CollectD1 1)) ]); 
183 

184 
(** RepFun **) 

185 

186 
val prems = goal ZF.thy "[ !!x. x:A ==> f(x): B ] ==> {f(x). x:A} <= B"; 

187 
by (rtac subsetI 1); 

188 
by (etac RepFunE 1); 

189 
by (etac ssubst 1); 

190 
by (eresolve_tac prems 1); 

760  191 
qed "RepFun_subset"; 
689  192 

193 
(*A more powerful claset for subset reasoning*) 

194 
val subset_cs = subset0_cs 

195 
addSIs [subset_refl,cons_subsetI,subset_consI,Union_least,UN_least,Un_least, 

196 
Inter_greatest,Int_greatest,RepFun_subset] 

197 
addSIs [Un_upper1,Un_upper2,Int_lower1,Int_lower2] 

198 
addIs [Union_upper,Inter_lower] 

199 
addSEs [cons_subsetE]; 

200 