author  lcp 
Mon, 31 Oct 1994 18:09:32 +0100  
changeset 673  023cef668158 
parent 572  13c30ac40f8f 
child 686  be908d8d41ef 
permissions  rwrr 
0  1 
(* Title: ZF/upair 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1991 University of Cambridge 

5 

6 
UNORDERED pairs in ZermeloFraenkel Set Theory 

7 

8 
Observe the order of dependence: 

9 
Upair is defined in terms of Replace 

10 
Un is defined in terms of Upair and Union (similarly for Int) 

11 
cons is defined in terms of Upair and Un 

12 
Ordered pairs and descriptions are defined using cons ("set notation") 

13 
*) 

14 

15 
(*** Lemmas about power sets ***) 

16 

17 
val Pow_bottom = empty_subsetI RS PowI; (* 0 : Pow(B) *) 

18 
val Pow_top = subset_refl RS PowI; (* A : Pow(A) *) 

19 
val Pow_neq_0 = Pow_top RSN (2,equals0D); (* Pow(a)=0 ==> P *) 

20 

21 

22 
(*** Unordered pairs  Upair ***) 

23 

24 
val pairing = prove_goalw ZF.thy [Upair_def] 

25 
"c : Upair(a,b) <> (c=a  c=b)" 

26 
(fn _ => [ (fast_tac (lemmas_cs addEs [Pow_neq_0, sym RS Pow_neq_0]) 1) ]); 

27 

28 
val UpairI1 = prove_goal ZF.thy "a : Upair(a,b)" 

29 
(fn _ => [ (rtac (refl RS disjI1 RS (pairing RS iffD2)) 1) ]); 

30 

31 
val UpairI2 = prove_goal ZF.thy "b : Upair(a,b)" 

32 
(fn _ => [ (rtac (refl RS disjI2 RS (pairing RS iffD2)) 1) ]); 

33 

34 
val UpairE = prove_goal ZF.thy 

35 
"[ a : Upair(b,c); a=b ==> P; a=c ==> P ] ==> P" 

36 
(fn major::prems=> 

37 
[ (rtac (major RS (pairing RS iffD1 RS disjE)) 1), 

38 
(REPEAT (eresolve_tac prems 1)) ]); 

39 

40 
(*** Rules for binary union  Un  defined via Upair ***) 

41 

42 
val UnI1 = prove_goalw ZF.thy [Un_def] "c : A ==> c : A Un B" 

43 
(fn [prem]=> [ (rtac (prem RS (UpairI1 RS UnionI)) 1) ]); 

44 

45 
val UnI2 = prove_goalw ZF.thy [Un_def] "c : B ==> c : A Un B" 

46 
(fn [prem]=> [ (rtac (prem RS (UpairI2 RS UnionI)) 1) ]); 

47 

48 
val UnE = prove_goalw ZF.thy [Un_def] 

49 
"[ c : A Un B; c:A ==> P; c:B ==> P ] ==> P" 

50 
(fn major::prems=> 

51 
[ (rtac (major RS UnionE) 1), 

52 
(etac UpairE 1), 

53 
(REPEAT (EVERY1 [resolve_tac prems, etac subst, assume_tac])) ]); 

54 

572  55 
(*Stronger version of the rule above*) 
56 
val UnE' = prove_goal ZF.thy 

57 
"[ c : A Un B; c:A ==> P; [ c:B; c~:A ] ==> P ] ==> P" 

58 
(fn major::prems => 

59 
[(rtac (major RS UnE) 1), 

60 
(eresolve_tac prems 1), 

61 
(rtac classical 1), 

62 
(eresolve_tac prems 1), 

63 
(swap_res_tac prems 1), 

64 
(etac notnotD 1)]); 

65 

0  66 
val Un_iff = prove_goal ZF.thy "c : A Un B <> (c:A  c:B)" 
67 
(fn _ => [ (fast_tac (lemmas_cs addIs [UnI1,UnI2] addSEs [UnE]) 1) ]); 

68 

69 
(*Classical introduction rule: no commitment to A vs B*) 

37  70 
val UnCI = prove_goal ZF.thy "(c ~: B ==> c : A) ==> c : A Un B" 
0  71 
(fn [prem]=> 
72 
[ (rtac (disjCI RS (Un_iff RS iffD2)) 1), 

73 
(etac prem 1) ]); 

74 

75 

76 
(*** Rules for small intersection  Int  defined via Upair ***) 

77 

78 
val IntI = prove_goalw ZF.thy [Int_def] 

79 
"[ c : A; c : B ] ==> c : A Int B" 

80 
(fn prems=> 

81 
[ (REPEAT (resolve_tac (prems @ [UpairI1,InterI]) 1 

82 
ORELSE eresolve_tac [UpairE, ssubst] 1)) ]); 

83 

84 
val IntD1 = prove_goalw ZF.thy [Int_def] "c : A Int B ==> c : A" 

85 
(fn [major]=> 

86 
[ (rtac (UpairI1 RS (major RS InterD)) 1) ]); 

87 

88 
val IntD2 = prove_goalw ZF.thy [Int_def] "c : A Int B ==> c : B" 

89 
(fn [major]=> 

90 
[ (rtac (UpairI2 RS (major RS InterD)) 1) ]); 

91 

92 
val IntE = prove_goal ZF.thy 

93 
"[ c : A Int B; [ c:A; c:B ] ==> P ] ==> P" 

94 
(fn prems=> 

95 
[ (resolve_tac prems 1), 

96 
(REPEAT (resolve_tac (prems RL [IntD1,IntD2]) 1)) ]); 

97 

98 
val Int_iff = prove_goal ZF.thy "c : A Int B <> (c:A & c:B)" 

99 
(fn _ => [ (fast_tac (lemmas_cs addSIs [IntI] addSEs [IntE]) 1) ]); 

100 

101 

102 
(*** Rules for set difference  defined via Upair ***) 

103 

104 
val DiffI = prove_goalw ZF.thy [Diff_def] 

37  105 
"[ c : A; c ~: B ] ==> c : A  B" 
0  106 
(fn prems=> [ (REPEAT (resolve_tac (prems @ [CollectI]) 1)) ]); 
107 

108 
val DiffD1 = prove_goalw ZF.thy [Diff_def] 

109 
"c : A  B ==> c : A" 

110 
(fn [major]=> [ (rtac (major RS CollectD1) 1) ]); 

111 

112 
val DiffD2 = prove_goalw ZF.thy [Diff_def] 

485  113 
"c : A  B ==> c ~: B" 
114 
(fn [major]=> [ (rtac (major RS CollectD2) 1) ]); 

0  115 

116 
val DiffE = prove_goal ZF.thy 

37  117 
"[ c : A  B; [ c:A; c~:B ] ==> P ] ==> P" 
0  118 
(fn prems=> 
119 
[ (resolve_tac prems 1), 

485  120 
(REPEAT (ares_tac (prems RL [DiffD1, DiffD2]) 1)) ]); 
0  121 

37  122 
val Diff_iff = prove_goal ZF.thy "c : AB <> (c:A & c~:B)" 
0  123 
(fn _ => [ (fast_tac (lemmas_cs addSIs [DiffI] addSEs [DiffE]) 1) ]); 
124 

125 
(*** Rules for cons  defined via Un and Upair ***) 

126 

127 
val consI1 = prove_goalw ZF.thy [cons_def] "a : cons(a,B)" 

128 
(fn _ => [ (rtac (UpairI1 RS UnI1) 1) ]); 

129 

130 
val consI2 = prove_goalw ZF.thy [cons_def] "a : B ==> a : cons(b,B)" 

131 
(fn [prem]=> [ (rtac (prem RS UnI2) 1) ]); 

132 

133 
val consE = prove_goalw ZF.thy [cons_def] 

134 
"[ a : cons(b,A); a=b ==> P; a:A ==> P ] ==> P" 

135 
(fn major::prems=> 

136 
[ (rtac (major RS UnE) 1), 

137 
(REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ]); 

138 

572  139 
(*Stronger version of the rule above*) 
140 
val consE' = prove_goal ZF.thy 

141 
"[ a : cons(b,A); a=b ==> P; [ a:A; a~=b ] ==> P ] ==> P" 

142 
(fn major::prems => 

143 
[(rtac (major RS consE) 1), 

144 
(eresolve_tac prems 1), 

145 
(rtac classical 1), 

146 
(eresolve_tac prems 1), 

147 
(swap_res_tac prems 1), 

148 
(etac notnotD 1)]); 

149 

0  150 
val cons_iff = prove_goal ZF.thy "a : cons(b,A) <> (a=b  a:A)" 
151 
(fn _ => [ (fast_tac (lemmas_cs addIs [consI1,consI2] addSEs [consE]) 1) ]); 

152 

153 
(*Classical introduction rule*) 

37  154 
val consCI = prove_goal ZF.thy "(a~:B ==> a=b) ==> a: cons(b,B)" 
0  155 
(fn [prem]=> 
156 
[ (rtac (disjCI RS (cons_iff RS iffD2)) 1), 

157 
(etac prem 1) ]); 

158 

159 
(*** Singletons  using cons ***) 

160 

161 
val singletonI = prove_goal ZF.thy "a : {a}" 

162 
(fn _=> [ (rtac consI1 1) ]); 

163 

164 
val singletonE = prove_goal ZF.thy "[ a: {b}; a=b ==> P ] ==> P" 

165 
(fn major::prems=> 

166 
[ (rtac (major RS consE) 1), 

167 
(REPEAT (eresolve_tac (prems @ [emptyE]) 1)) ]); 

168 

169 

170 
(*** Rules for Descriptions ***) 

171 

172 
val the_equality = prove_goalw ZF.thy [the_def] 

173 
"[ P(a); !!x. P(x) ==> x=a ] ==> (THE x. P(x)) = a" 

174 
(fn prems=> 

175 
[ (fast_tac (lemmas_cs addIs ([equalityI,singletonI]@prems) 

176 
addEs (prems RL [subst])) 1) ]); 

177 

178 
(* Only use this if you already know EX!x. P(x) *) 

179 
val the_equality2 = prove_goal ZF.thy 

673  180 
"!!P. [ EX! x. P(x); P(a) ] ==> (THE x. P(x)) = a" 
181 
(fn _ => 

182 
[ (deepen_tac (lemmas_cs addSIs [the_equality]) 1 1) ]); 

0  183 

184 
val theI = prove_goal ZF.thy "EX! x. P(x) ==> P(THE x. P(x))" 

185 
(fn [major]=> 

186 
[ (rtac (major RS ex1E) 1), 

187 
(resolve_tac [major RS the_equality2 RS ssubst] 1), 

188 
(REPEAT (assume_tac 1)) ]); 

189 

435  190 
(*the_cong is no longer necessary: if (ALL y.P(y)<>Q(y)) then 
191 
(THE x.P(x)) rewrites to (THE x. Q(x)) *) 

192 

193 
(*If it's "undefined", it's zero!*) 

194 
val the_0 = prove_goalw ZF.thy [the_def] 

195 
"!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0" 

196 
(fn _ => 

485  197 
[ (fast_tac (lemmas_cs addIs [equalityI] addSEs [ReplaceE]) 1) ]); 
435  198 

0  199 

200 
(*** if  a conditional expression for formulae ***) 

201 

202 
goalw ZF.thy [if_def] "if(True,a,b) = a"; 

203 
by (fast_tac (lemmas_cs addIs [the_equality]) 1); 

204 
val if_true = result(); 

205 

206 
goalw ZF.thy [if_def] "if(False,a,b) = b"; 

207 
by (fast_tac (lemmas_cs addIs [the_equality]) 1); 

208 
val if_false = result(); 

209 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

210 
(*Never use with case splitting, or if P is known to be true or false*) 
0  211 
val prems = goalw ZF.thy [if_def] 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

212 
"[ P<>Q; Q ==> a=c; ~Q ==> b=d ] ==> if(P,a,b) = if(Q,c,d)"; 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

213 
by (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1); 
0  214 
val if_cong = result(); 
215 

216 
(*Not needed for rewriting, since P would rewrite to True anyway*) 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

217 
goalw ZF.thy [if_def] "!!P. P ==> if(P,a,b) = a"; 
0  218 
by (fast_tac (lemmas_cs addSIs [the_equality]) 1); 
219 
val if_P = result(); 

220 

221 
(*Not needed for rewriting, since P would rewrite to False anyway*) 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

222 
goalw ZF.thy [if_def] "!!P. ~P ==> if(P,a,b) = b"; 
0  223 
by (fast_tac (lemmas_cs addSIs [the_equality]) 1); 
224 
val if_not_P = result(); 

225 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

226 
val if_ss = FOL_ss addsimps [if_true,if_false]; 
0  227 

228 
val expand_if = prove_goal ZF.thy 

229 
"P(if(Q,x,y)) <> ((Q > P(x)) & (~Q > P(y)))" 

437  230 
(fn _=> [ (excluded_middle_tac "Q" 1), 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

231 
(asm_simp_tac if_ss 1), 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

232 
(asm_simp_tac if_ss 1) ]); 
0  233 

234 
val prems = goal ZF.thy 

235 
"[ P ==> a: A; ~P ==> b: A ] ==> if(P,a,b): A"; 

437  236 
by (excluded_middle_tac "P" 1); 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

237 
by (ALLGOALS (asm_simp_tac (if_ss addsimps prems))); 
0  238 
val if_type = result(); 
239 

240 

241 
(*** Foundation lemmas ***) 

242 

437  243 
(*was called mem_anti_sym*) 
673  244 
val mem_asym = prove_goal ZF.thy "!!P. [ a:b; b:a ] ==> P" 
245 
(fn _=> 

246 
[ (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1), 

0  247 
(etac equals0D 1), 
248 
(rtac consI1 1), 

673  249 
(fast_tac (lemmas_cs addIs [consI1,consI2] 
0  250 
addSEs [consE,equalityE]) 1) ]); 
251 

437  252 
(*was called mem_anti_refl*) 
253 
val mem_irrefl = prove_goal ZF.thy "a:a ==> P" 

254 
(fn [major]=> [ (rtac (major RS (major RS mem_asym)) 1) ]); 

0  255 

437  256 
val mem_not_refl = prove_goal ZF.thy "a ~: a" 
257 
(K [ (rtac notI 1), (etac mem_irrefl 1) ]); 

0  258 

435  259 
(*Good for proving inequalities by rewriting*) 
260 
val mem_imp_not_eq = prove_goal ZF.thy "!!a A. a:A ==> a ~= A" 

437  261 
(fn _=> [ fast_tac (lemmas_cs addSEs [mem_irrefl]) 1 ]); 
435  262 

0  263 
(*** Rules for succ ***) 
264 

265 
val succI1 = prove_goalw ZF.thy [succ_def] "i : succ(i)" 

266 
(fn _=> [ (rtac consI1 1) ]); 

267 

268 
val succI2 = prove_goalw ZF.thy [succ_def] 

269 
"i : j ==> i : succ(j)" 

270 
(fn [prem]=> [ (rtac (prem RS consI2) 1) ]); 

271 

272 
val succE = prove_goalw ZF.thy [succ_def] 

273 
"[ i : succ(j); i=j ==> P; i:j ==> P ] ==> P" 

274 
(fn major::prems=> 

275 
[ (rtac (major RS consE) 1), 

276 
(REPEAT (eresolve_tac prems 1)) ]); 

277 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

278 
val succ_iff = prove_goal ZF.thy "i : succ(j) <> i=j  i:j" 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

279 
(fn _ => [ (fast_tac (lemmas_cs addIs [succI1,succI2] addSEs [succE]) 1) ]); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

280 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

281 
(*Classical introduction rule*) 
37  282 
val succCI = prove_goal ZF.thy "(i~:j ==> i=j) ==> i: succ(j)" 
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

283 
(fn [prem]=> 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

284 
[ (rtac (disjCI RS (succ_iff RS iffD2)) 1), 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

285 
(etac prem 1) ]); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

286 

0  287 
val succ_neq_0 = prove_goal ZF.thy "succ(n)=0 ==> P" 
288 
(fn [major]=> 

289 
[ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1), 

290 
(rtac succI1 1) ]); 

291 

292 
(*Useful for rewriting*) 

37  293 
val succ_not_0 = prove_goal ZF.thy "succ(n) ~= 0" 
0  294 
(fn _=> [ (rtac notI 1), (etac succ_neq_0 1) ]); 
295 

296 
(* succ(c) <= B ==> c : B *) 

297 
val succ_subsetD = succI1 RSN (2,subsetD); 

298 

673  299 
val succ_inject = prove_goal ZF.thy "!!m n. succ(m) = succ(n) ==> m=n" 
300 
(fn _ => 

301 
[ (fast_tac (lemmas_cs addSEs [succE, equalityE, make_elim succ_subsetD] 

302 
addEs [mem_asym]) 1) ]); 

0  303 

304 
val succ_inject_iff = prove_goal ZF.thy "succ(m) = succ(n) <> m=n" 

305 
(fn _=> [ (fast_tac (FOL_cs addSEs [succ_inject]) 1) ]); 

306 

437  307 
(*UpairI1/2 should become UpairCI; mem_irrefl as a hazE? *) 
0  308 
val upair_cs = lemmas_cs 
309 
addSIs [singletonI, DiffI, IntI, UnCI, consCI, succCI, UpairI1,UpairI2] 

310 
addSEs [singletonE, DiffE, IntE, UnE, consE, succE, UpairE]; 

311 