author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 55  331d93292ee0 
permissions  rwrr 
0  1 
(* Title: ZF/qpair.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
For qpair.thy. 

7 

8 
Quineinspired ordered pairs and disjoint sums, for nonwellfounded data 

9 
structures in ZF. Does not precisely follow Quine's construction. Thanks 

10 
to Thomas Forster for suggesting this approach! 

11 

12 
W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers, 

13 
1966. 

14 

15 
Many proofs are borrowed from pair.ML and sum.ML 

16 

17 
Do we EVER have rank(a) < rank(<a;b>) ? Perhaps if the latter rank 

18 
is not a limit ordinal? 

19 
*) 

20 

21 

22 
open QPair; 

23 

24 
(**** Quine ordered pairing ****) 

25 

26 
(** Lemmas for showing that <a;b> uniquely determines a and b **) 

27 

28 
val QPair_iff = prove_goalw QPair.thy [QPair_def] 

29 
"<a;b> = <c;d> <> a=c & b=d" 

30 
(fn _=> [rtac sum_equal_iff 1]); 

31 

32 
val QPair_inject = standard (QPair_iff RS iffD1 RS conjE); 

33 

34 
val QPair_inject1 = prove_goal QPair.thy "<a;b> = <c;d> ==> a=c" 

35 
(fn [major]=> 

36 
[ (rtac (major RS QPair_inject) 1), (assume_tac 1) ]); 

37 

38 
val QPair_inject2 = prove_goal QPair.thy "<a;b> = <c;d> ==> b=d" 

39 
(fn [major]=> 

40 
[ (rtac (major RS QPair_inject) 1), (assume_tac 1) ]); 

41 

42 

43 
(*** QSigma: Disjoint union of a family of sets 

44 
Generalizes Cartesian product ***) 

45 

46 
val QSigmaI = prove_goalw QPair.thy [QSigma_def] 

47 
"[ a:A; b:B(a) ] ==> <a;b> : QSigma(A,B)" 

48 
(fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]); 

49 

50 
(*The general elimination rule*) 

51 
val QSigmaE = prove_goalw QPair.thy [QSigma_def] 

52 
"[ c: QSigma(A,B); \ 

53 
\ !!x y.[ x:A; y:B(x); c=<x;y> ] ==> P \ 

54 
\ ] ==> P" 

55 
(fn major::prems=> 

56 
[ (cut_facts_tac [major] 1), 

57 
(REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]); 

58 

59 
(** Elimination rules for <a;b>:A*B  introducing no eigenvariables **) 

60 

61 
val QSigmaE2 = 

62 
rule_by_tactic (REPEAT_FIRST (etac QPair_inject ORELSE' bound_hyp_subst_tac) 

63 
THEN prune_params_tac) 

64 
(read_instantiate [("c","<a;b>")] QSigmaE); 

65 

66 
val QSigmaD1 = prove_goal QPair.thy "<a;b> : QSigma(A,B) ==> a : A" 

67 
(fn [major]=> 

68 
[ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]); 

69 

70 
val QSigmaD2 = prove_goal QPair.thy "<a;b> : QSigma(A,B) ==> b : B(a)" 

71 
(fn [major]=> 

72 
[ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]); 

73 

74 
val QSigma_cong = prove_goalw QPair.thy [QSigma_def] 

75 
"[ A=A'; !!x. x:A' ==> B(x)=B'(x) ] ==> \ 

76 
\ QSigma(A,B) = QSigma(A',B')" 

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

77 
(fn prems=> [ (simp_tac (ZF_ss addsimps prems) 1) ]); 
0  78 

79 
val QSigma_empty1 = prove_goal QPair.thy "QSigma(0,B) = 0" 

80 
(fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]); 

81 

82 
val QSigma_empty2 = prove_goal QPair.thy "A <*> 0 = 0" 

83 
(fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]); 

84 

85 

86 
(*** Eliminator  qsplit ***) 

87 

88 
val qsplit = prove_goalw QPair.thy [qsplit_def] 

89 
"qsplit(%x y.c(x,y), <a;b>) = c(a,b)" 

90 
(fn _ => [ (fast_tac (ZF_cs addIs [the_equality] addEs [QPair_inject]) 1) ]); 

91 

92 
val qsplit_type = prove_goal QPair.thy 

93 
"[ p:QSigma(A,B); \ 

94 
\ !!x y.[ x:A; y:B(x) ] ==> c(x,y):C(<x;y>) \ 

95 
\ ] ==> qsplit(%x y.c(x,y), p) : C(p)" 

96 
(fn major::prems=> 

97 
[ (rtac (major RS QSigmaE) 1), 

98 
(etac ssubst 1), 

99 
(REPEAT (ares_tac (prems @ [qsplit RS ssubst]) 1)) ]); 

100 

101 

102 
val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject]; 

103 

104 
(*** qconverse ***) 

105 

106 
val qconverseI = prove_goalw QPair.thy [qconverse_def] 

107 
"!!a b r. <a;b>:r ==> <b;a>:qconverse(r)" 

108 
(fn _ => [ (fast_tac qpair_cs 1) ]); 

109 

110 
val qconverseD = prove_goalw QPair.thy [qconverse_def] 

111 
"!!a b r. <a;b> : qconverse(r) ==> <b;a> : r" 

112 
(fn _ => [ (fast_tac qpair_cs 1) ]); 

113 

114 
val qconverseE = prove_goalw QPair.thy [qconverse_def] 

115 
"[ yx : qconverse(r); \ 

116 
\ !!x y. [ yx=<y;x>; <x;y>:r ] ==> P \ 

117 
\ ] ==> P" 

118 
(fn [major,minor]=> 

119 
[ (rtac (major RS ReplaceE) 1), 

120 
(REPEAT (eresolve_tac [exE, conjE, minor] 1)), 

121 
(hyp_subst_tac 1), 

122 
(assume_tac 1) ]); 

123 

124 
val qconverse_cs = qpair_cs addSIs [qconverseI] 

125 
addSEs [qconverseD,qconverseE]; 

126 

127 
val qconverse_of_qconverse = prove_goal QPair.thy 

128 
"!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r" 

129 
(fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]); 

130 

131 
val qconverse_type = prove_goal QPair.thy 

132 
"!!A B r. r <= A <*> B ==> qconverse(r) <= B <*> A" 

133 
(fn _ => [ (fast_tac qconverse_cs 1) ]); 

134 

135 
val qconverse_of_prod = prove_goal QPair.thy "qconverse(A <*> B) = B <*> A" 

136 
(fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]); 

137 

138 
val qconverse_empty = prove_goal QPair.thy "qconverse(0) = 0" 

139 
(fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]); 

140 

141 

142 
(*** qsplit for predicates: result type o ***) 

143 

144 
goalw QPair.thy [qfsplit_def] "!!R a b. R(a,b) ==> qfsplit(R, <a;b>)"; 

145 
by (REPEAT (ares_tac [refl,exI,conjI] 1)); 

146 
val qfsplitI = result(); 

147 

148 
val major::prems = goalw QPair.thy [qfsplit_def] 

149 
"[ qfsplit(R,z); !!x y. [ z = <x;y>; R(x,y) ] ==> P ] ==> P"; 

150 
by (cut_facts_tac [major] 1); 

151 
by (REPEAT (eresolve_tac (prems@[asm_rl,exE,conjE]) 1)); 

152 
val qfsplitE = result(); 

153 

154 
goal QPair.thy "!!R a b. qfsplit(R,<a;b>) ==> R(a,b)"; 

155 
by (REPEAT (eresolve_tac [asm_rl,qfsplitE,QPair_inject,ssubst] 1)); 

156 
val qfsplitD = result(); 

157 

158 

159 
(**** The Quineinspired notion of disjoint sum ****) 

160 

161 
val qsum_defs = [qsum_def,QInl_def,QInr_def,qcase_def]; 

162 

163 
(** Introduction rules for the injections **) 

164 

165 
goalw QPair.thy qsum_defs "!!a A B. a : A ==> QInl(a) : A <+> B"; 

166 
by (REPEAT (ares_tac [UnI1,QSigmaI,singletonI] 1)); 

167 
val QInlI = result(); 

168 

169 
goalw QPair.thy qsum_defs "!!b A B. b : B ==> QInr(b) : A <+> B"; 

170 
by (REPEAT (ares_tac [UnI2,QSigmaI,singletonI] 1)); 

171 
val QInrI = result(); 

172 

173 
(** Elimination rules **) 

174 

175 
val major::prems = goalw QPair.thy qsum_defs 

176 
"[ u: A <+> B; \ 

177 
\ !!x. [ x:A; u=QInl(x) ] ==> P; \ 

178 
\ !!y. [ y:B; u=QInr(y) ] ==> P \ 

179 
\ ] ==> P"; 

180 
by (rtac (major RS UnE) 1); 

181 
by (REPEAT (rtac refl 1 

182 
ORELSE eresolve_tac (prems@[QSigmaE,singletonE,ssubst]) 1)); 

183 
val qsumE = result(); 

184 

185 
(** Injection and freeness equivalences, for rewriting **) 

186 

55  187 
goalw QPair.thy qsum_defs "QInl(a)=QInl(b) <> a=b"; 
188 
by (simp_tac (ZF_ss addsimps [QPair_iff]) 1); 

0  189 
val QInl_iff = result(); 
190 

55  191 
goalw QPair.thy qsum_defs "QInr(a)=QInr(b) <> a=b"; 
192 
by (simp_tac (ZF_ss addsimps [QPair_iff]) 1); 

0  193 
val QInr_iff = result(); 
194 

55  195 
goalw QPair.thy qsum_defs "QInl(a)=QInr(b) <> False"; 
196 
by (simp_tac (ZF_ss addsimps [QPair_iff, one_not_0 RS not_sym]) 1); 

0  197 
val QInl_QInr_iff = result(); 
198 

55  199 
goalw QPair.thy qsum_defs "QInr(b)=QInl(a) <> False"; 
200 
by (simp_tac (ZF_ss addsimps [QPair_iff, one_not_0]) 1); 

0  201 
val QInr_QInl_iff = result(); 
202 

55  203 
(*Injection and freeness rules*) 
204 

205 
val QInl_inject = standard (QInl_iff RS iffD1); 

206 
val QInr_inject = standard (QInr_iff RS iffD1); 

207 
val QInl_neq_QInr = standard (QInl_QInr_iff RS iffD1 RS FalseE); 

208 
val QInr_neq_QInl = standard (QInr_QInl_iff RS iffD1 RS FalseE); 

209 

0  210 
val qsum_cs = 
211 
ZF_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl] 

212 
addSDs [QInl_inject,QInr_inject]; 

213 

55  214 
goal QPair.thy "!!A B. QInl(a): A<+>B ==> a: A"; 
215 
by (fast_tac qsum_cs 1); 

216 
val QInlD = result(); 

217 

218 
goal QPair.thy "!!A B. QInr(b): A<+>B ==> b: B"; 

219 
by (fast_tac qsum_cs 1); 

220 
val QInrD = result(); 

221 

0  222 
(** <+> is itself injective... who cares?? **) 
223 

224 
goal QPair.thy 

225 
"u: A <+> B <> (EX x. x:A & u=QInl(x))  (EX y. y:B & u=QInr(y))"; 

226 
by (fast_tac qsum_cs 1); 

227 
val qsum_iff = result(); 

228 

229 
goal QPair.thy "A <+> B <= C <+> D <> A<=C & B<=D"; 

230 
by (fast_tac qsum_cs 1); 

231 
val qsum_subset_iff = result(); 

232 

233 
goal QPair.thy "A <+> B = C <+> D <> A=C & B=D"; 

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

234 
by (simp_tac (ZF_ss addsimps [extension,qsum_subset_iff]) 1); 
0  235 
by (fast_tac ZF_cs 1); 
236 
val qsum_equal_iff = result(); 

237 

238 
(*** Eliminator  qcase ***) 

239 

240 
goalw QPair.thy qsum_defs "qcase(c, d, QInl(a)) = c(a)"; 

241 
by (rtac (qsplit RS trans) 1); 

242 
by (rtac cond_0 1); 

243 
val qcase_QInl = result(); 

244 

245 
goalw QPair.thy qsum_defs "qcase(c, d, QInr(b)) = d(b)"; 

246 
by (rtac (qsplit RS trans) 1); 

247 
by (rtac cond_1 1); 

248 
val qcase_QInr = result(); 

249 

250 
val major::prems = goal QPair.thy 

251 
"[ u: A <+> B; \ 

252 
\ !!x. x: A ==> c(x): C(QInl(x)); \ 

253 
\ !!y. y: B ==> d(y): C(QInr(y)) \ 

254 
\ ] ==> qcase(c,d,u) : C(u)"; 

255 
by (rtac (major RS qsumE) 1); 

256 
by (ALLGOALS (etac ssubst)); 

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

257 
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps 
0  258 
(prems@[qcase_QInl,qcase_QInr])))); 
259 
val qcase_type = result(); 

260 

261 
(** Rules for the Part primitive **) 

262 

263 
goal QPair.thy "Part(A <+> B,QInl) = {QInl(x). x: A}"; 

264 
by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1); 

265 
val Part_QInl = result(); 

266 

267 
goal QPair.thy "Part(A <+> B,QInr) = {QInr(y). y: B}"; 

268 
by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1); 

269 
val Part_QInr = result(); 

270 

271 
goal QPair.thy "Part(A <+> B, %x.QInr(h(x))) = {QInr(y). y: Part(B,h)}"; 

272 
by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1); 

273 
val Part_QInr2 = result(); 

274 

275 
goal QPair.thy "!!A B C. C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C"; 

276 
by (rtac equalityI 1); 

277 
by (rtac Un_least 1); 

278 
by (rtac Part_subset 1); 

279 
by (rtac Part_subset 1); 

280 
by (fast_tac (ZF_cs addIs [PartI] addSEs [qsumE]) 1); 

281 
val Part_qsum_equality = result(); 