author  lcp 
Thu, 15 Dec 1994 11:08:22 +0100  
changeset 790  4c10e8532d43 
parent 782  200a16083201 
child 1096  6c177c4c2127 
permissions  rwrr 
744  1 
(* Title: ZF/QPair.ML 
0  2 
ID: $Id$ 
3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

744  6 
For QPair.thy. 
0  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 

760  28 
qed_goalw "QPair_iff" QPair.thy [QPair_def] 
0  29 
"<a;b> = <c;d> <> a=c & b=d" 
30 
(fn _=> [rtac sum_equal_iff 1]); 

31 

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

32 
bind_thm ("QPair_inject", (QPair_iff RS iffD1 RS conjE)); 
0  33 

760  34 
qed_goal "QPair_inject1" QPair.thy "<a;b> = <c;d> ==> a=c" 
0  35 
(fn [major]=> 
36 
[ (rtac (major RS QPair_inject) 1), (assume_tac 1) ]); 

37 

760  38 
qed_goal "QPair_inject2" QPair.thy "<a;b> = <c;d> ==> b=d" 
0  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 

760  46 
qed_goalw "QSigmaI" QPair.thy [QSigma_def] 
0  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*) 

760  51 
qed_goalw "QSigmaE" QPair.thy [QSigma_def] 
0  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 

760  66 
qed_goal "QSigmaD1" QPair.thy "<a;b> : QSigma(A,B) ==> a : A" 
0  67 
(fn [major]=> 
68 
[ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]); 

69 

760  70 
qed_goal "QSigmaD2" QPair.thy "<a;b> : QSigma(A,B) ==> b : B(a)" 
0  71 
(fn [major]=> 
72 
[ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]); 

73 

744  74 
val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject]; 
75 

76 

760  77 
qed_goalw "QSigma_cong" QPair.thy [QSigma_def] 
0  78 
"[ A=A'; !!x. x:A' ==> B(x)=B'(x) ] ==> \ 
79 
\ QSigma(A,B) = QSigma(A',B')" 

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

80 
(fn prems=> [ (simp_tac (ZF_ss addsimps prems) 1) ]); 
0  81 

760  82 
qed_goal "QSigma_empty1" QPair.thy "QSigma(0,B) = 0" 
744  83 
(fn _ => [ (fast_tac (qpair_cs addIs [equalityI]) 1) ]); 
0  84 

760  85 
qed_goal "QSigma_empty2" QPair.thy "A <*> 0 = 0" 
744  86 
(fn _ => [ (fast_tac (qpair_cs addIs [equalityI]) 1) ]); 
0  87 

88 

89 
(*** Eliminator  qsplit ***) 

90 

760  91 
qed_goalw "qsplit" QPair.thy [qsplit_def] 
0  92 
"qsplit(%x y.c(x,y), <a;b>) = c(a,b)" 
744  93 
(fn _ => [ (fast_tac (qpair_cs addIs [the_equality]) 1) ]); 
0  94 

760  95 
qed_goal "qsplit_type" QPair.thy 
0  96 
"[ p:QSigma(A,B); \ 
97 
\ !!x y.[ x:A; y:B(x) ] ==> c(x,y):C(<x;y>) \ 

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

99 
(fn major::prems=> 

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

101 
(etac ssubst 1), 

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

103 

104 

105 
(*** qconverse ***) 

106 

760  107 
qed_goalw "qconverseI" QPair.thy [qconverse_def] 
0  108 
"!!a b r. <a;b>:r ==> <b;a>:qconverse(r)" 
109 
(fn _ => [ (fast_tac qpair_cs 1) ]); 

110 

760  111 
qed_goalw "qconverseD" QPair.thy [qconverse_def] 
0  112 
"!!a b r. <a;b> : qconverse(r) ==> <b;a> : r" 
113 
(fn _ => [ (fast_tac qpair_cs 1) ]); 

114 

760  115 
qed_goalw "qconverseE" QPair.thy [qconverse_def] 
0  116 
"[ yx : qconverse(r); \ 
117 
\ !!x y. [ yx=<y;x>; <x;y>:r ] ==> P \ 

118 
\ ] ==> P" 

119 
(fn [major,minor]=> 

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

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

122 
(hyp_subst_tac 1), 

123 
(assume_tac 1) ]); 

124 

125 
val qconverse_cs = qpair_cs addSIs [qconverseI] 

126 
addSEs [qconverseD,qconverseE]; 

127 

790  128 
qed_goal "qconverse_qconverse" QPair.thy 
0  129 
"!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r" 
130 
(fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]); 

131 

760  132 
qed_goal "qconverse_type" QPair.thy 
0  133 
"!!A B r. r <= A <*> B ==> qconverse(r) <= B <*> A" 
134 
(fn _ => [ (fast_tac qconverse_cs 1) ]); 

135 

790  136 
qed_goal "qconverse_prod" QPair.thy "qconverse(A <*> B) = B <*> A" 
0  137 
(fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]); 
138 

760  139 
qed_goal "qconverse_empty" QPair.thy "qconverse(0) = 0" 
0  140 
(fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]); 
141 

142 

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

144 

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

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

760  147 
qed "qfsplitI"; 
0  148 

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

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

151 
by (cut_facts_tac [major] 1); 

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

760  153 
qed "qfsplitE"; 
0  154 

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

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

760  157 
qed "qfsplitD"; 
0  158 

159 

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

161 

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

163 

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

165 

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

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

760  168 
qed "QInlI"; 
0  169 

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

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

760  172 
qed "QInrI"; 
0  173 

174 
(** Elimination rules **) 

175 

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

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

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

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

180 
\ ] ==> P"; 

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

182 
by (REPEAT (rtac refl 1 

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

760  184 
qed "qsumE"; 
0  185 

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

187 

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

760  190 
qed "QInl_iff"; 
0  191 

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

760  194 
qed "QInr_iff"; 
0  195 

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

760  198 
qed "QInl_QInr_iff"; 
0  199 

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

760  202 
qed "QInr_QInl_iff"; 
0  203 

55  204 
(*Injection and freeness rules*) 
205 

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

206 
bind_thm ("QInl_inject", (QInl_iff RS iffD1)); 
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset

207 
bind_thm ("QInr_inject", (QInr_iff RS iffD1)); 
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset

208 
bind_thm ("QInl_neq_QInr", (QInl_QInr_iff RS iffD1 RS FalseE)); 
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset

209 
bind_thm ("QInr_neq_QInl", (QInr_QInl_iff RS iffD1 RS FalseE)); 
55  210 

0  211 
val qsum_cs = 
744  212 
qpair_cs addSIs [PartI, QInlI, QInrI] 
213 
addSEs [PartE, qsumE, QInl_neq_QInr, QInr_neq_QInl] 

214 
addSDs [QInl_inject, QInr_inject]; 

0  215 

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

760  218 
qed "QInlD"; 
55  219 

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

221 
by (fast_tac qsum_cs 1); 

760  222 
qed "QInrD"; 
55  223 

0  224 
(** <+> is itself injective... who cares?? **) 
225 

226 
goal QPair.thy 

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

228 
by (fast_tac qsum_cs 1); 

760  229 
qed "qsum_iff"; 
0  230 

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

232 
by (fast_tac qsum_cs 1); 

760  233 
qed "qsum_subset_iff"; 
0  234 

235 
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

236 
by (simp_tac (ZF_ss addsimps [extension,qsum_subset_iff]) 1); 
0  237 
by (fast_tac ZF_cs 1); 
760  238 
qed "qsum_equal_iff"; 
0  239 

240 
(*** Eliminator  qcase ***) 

241 

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

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

244 
by (rtac cond_0 1); 

760  245 
qed "qcase_QInl"; 
0  246 

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

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

249 
by (rtac cond_1 1); 

760  250 
qed "qcase_QInr"; 
0  251 

252 
val major::prems = goal QPair.thy 

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

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

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

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

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

258 
by (ALLGOALS (etac ssubst)); 

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

259 
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps 
0  260 
(prems@[qcase_QInl,qcase_QInr])))); 
760  261 
qed "qcase_type"; 
0  262 

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

264 

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

744  266 
by (fast_tac (qsum_cs addIs [equalityI]) 1); 
760  267 
qed "Part_QInl"; 
0  268 

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

744  270 
by (fast_tac (qsum_cs addIs [equalityI]) 1); 
760  271 
qed "Part_QInr"; 
0  272 

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

744  274 
by (fast_tac (qsum_cs addIs [equalityI]) 1); 
760  275 
qed "Part_QInr2"; 
0  276 

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

744  278 
by (fast_tac (qsum_cs addIs [equalityI]) 1); 
760  279 
qed "Part_qsum_equality"; 