author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 2469  b50b8c0eec01 
permissions  rwrr 
1461  1 
(* Title: ZF/pair 
0  2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
5 

6 
Ordered pairs in ZermeloFraenkel Set Theory 

7 
*) 

8 

9 
(** Lemmas for showing that <a,b> uniquely determines a and b **) 

10 

822
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset

11 
qed_goal "singleton_eq_iff" ZF.thy 
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset

12 
"{a} = {b} <> a=b" 
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset

13 
(fn _=> [ (resolve_tac [extension RS iff_trans] 1), 
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset

14 
(fast_tac upair_cs 1) ]); 
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset

15 

8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset

16 
qed_goal "doubleton_eq_iff" ZF.thy 
0  17 
"{a,b} = {c,d} <> (a=c & b=d)  (a=d & b=c)" 
18 
(fn _=> [ (resolve_tac [extension RS iff_trans] 1), 

19 
(fast_tac upair_cs 1) ]); 

20 

760  21 
qed_goalw "Pair_iff" ZF.thy [Pair_def] 
0  22 
"<a,b> = <c,d> <> a=c & b=d" 
822
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset

23 
(fn _=> [ (simp_tac (FOL_ss addsimps [doubleton_eq_iff]) 1), 
0  24 
(fast_tac FOL_cs 1) ]); 
25 

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

26 
bind_thm ("Pair_inject", (Pair_iff RS iffD1 RS conjE)); 
0  27 

760  28 
qed_goal "Pair_inject1" ZF.thy "<a,b> = <c,d> ==> a=c" 
0  29 
(fn [major]=> 
30 
[ (rtac (major RS Pair_inject) 1), (assume_tac 1) ]); 

31 

760  32 
qed_goal "Pair_inject2" ZF.thy "<a,b> = <c,d> ==> b=d" 
0  33 
(fn [major]=> 
34 
[ (rtac (major RS Pair_inject) 1), (assume_tac 1) ]); 

35 

760  36 
qed_goalw "Pair_neq_0" ZF.thy [Pair_def] "<a,b>=0 ==> P" 
0  37 
(fn [major]=> 
38 
[ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1), 

39 
(rtac consI1 1) ]); 

40 

760  41 
qed_goalw "Pair_neq_fst" ZF.thy [Pair_def] "<a,b>=a ==> P" 
0  42 
(fn [major]=> 
437  43 
[ (rtac (consI1 RS mem_asym RS FalseE) 1), 
0  44 
(rtac (major RS subst) 1), 
45 
(rtac consI1 1) ]); 

46 

760  47 
qed_goalw "Pair_neq_snd" ZF.thy [Pair_def] "<a,b>=b ==> P" 
0  48 
(fn [major]=> 
437  49 
[ (rtac (consI1 RS consI2 RS mem_asym RS FalseE) 1), 
0  50 
(rtac (major RS subst) 1), 
51 
(rtac (consI1 RS consI2) 1) ]); 

52 

53 

54 
(*** Sigma: Disjoint union of a family of sets 

55 
Generalizes Cartesian product ***) 

56 

760  57 
qed_goalw "SigmaI" ZF.thy [Sigma_def] 
0  58 
"[ a:A; b:B(a) ] ==> <a,b> : Sigma(A,B)" 
59 
(fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]); 

60 

61 
(*The general elimination rule*) 

760  62 
qed_goalw "SigmaE" ZF.thy [Sigma_def] 
0  63 
"[ c: Sigma(A,B); \ 
64 
\ !!x y.[ x:A; y:B(x); c=<x,y> ] ==> P \ 

65 
\ ] ==> P" 

66 
(fn major::prems=> 

67 
[ (cut_facts_tac [major] 1), 

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

69 

70 
(** Elimination of <a,b>:A*B  introduces no eigenvariables **) 

760  71 
qed_goal "SigmaD1" ZF.thy "<a,b> : Sigma(A,B) ==> a : A" 
0  72 
(fn [major]=> 
73 
[ (rtac (major RS SigmaE) 1), 

74 
(REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]); 

75 

760  76 
qed_goal "SigmaD2" ZF.thy "<a,b> : Sigma(A,B) ==> b : B(a)" 
0  77 
(fn [major]=> 
78 
[ (rtac (major RS SigmaE) 1), 

79 
(REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]); 

80 

81 
(*Also provable via 

82 
rule_by_tactic (REPEAT_FIRST (etac Pair_inject ORELSE' bound_hyp_subst_tac) 

1461  83 
THEN prune_params_tac) 
0  84 
(read_instantiate [("c","<a,b>")] SigmaE); *) 
760  85 
qed_goal "SigmaE2" ZF.thy 
0  86 
"[ <a,b> : Sigma(A,B); \ 
87 
\ [ a:A; b:B(a) ] ==> P \ 

88 
\ ] ==> P" 

89 
(fn [major,minor]=> 

90 
[ (rtac minor 1), 

91 
(rtac (major RS SigmaD1) 1), 

92 
(rtac (major RS SigmaD2) 1) ]); 

93 

760  94 
qed_goalw "Sigma_cong" ZF.thy [Sigma_def] 
0  95 
"[ A=A'; !!x. x:A' ==> B(x)=B'(x) ] ==> \ 
96 
\ Sigma(A,B) = Sigma(A',B')" 

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

97 
(fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1) ]); 
0  98 

760  99 
qed_goal "Sigma_empty1" ZF.thy "Sigma(0,B) = 0" 
0  100 
(fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]); 
101 

760  102 
qed_goal "Sigma_empty2" ZF.thy "A*0 = 0" 
0  103 
(fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]); 
104 

1105  105 
val pair_cs = upair_cs 
106 
addSIs [SigmaI] 

107 
addSEs [SigmaE2, SigmaE, Pair_inject, make_elim succ_inject, 

1461  108 
Pair_neq_0, sym RS Pair_neq_0, succ_neq_0, sym RS succ_neq_0]; 
1105  109 

110 

111 
(*** Projections: fst, snd ***) 

112 

113 
qed_goalw "fst_conv" ZF.thy [fst_def] "fst(<a,b>) = a" 

114 
(fn _=> 

115 
[ (fast_tac (pair_cs addIs [the_equality]) 1) ]); 

116 

117 
qed_goalw "snd_conv" ZF.thy [snd_def] "snd(<a,b>) = b" 

118 
(fn _=> 

119 
[ (fast_tac (pair_cs addIs [the_equality]) 1) ]); 

120 

121 
val pair_ss = FOL_ss addsimps [fst_conv,snd_conv]; 

122 

123 
qed_goal "fst_type" ZF.thy 

124 
"!!p. p:Sigma(A,B) ==> fst(p) : A" 

125 
(fn _=> [ (fast_tac (pair_cs addss pair_ss) 1) ]); 

126 

127 
qed_goal "snd_type" ZF.thy 

128 
"!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))" 

129 
(fn _=> [ (fast_tac (pair_cs addss pair_ss) 1) ]); 

130 

131 
goal ZF.thy "!!a A B. a: Sigma(A,B) ==> <fst(a),snd(a)> = a"; 

132 
by (etac SigmaE 1); 

133 
by (asm_simp_tac pair_ss 1); 

134 
qed "Pair_fst_snd_eq"; 

135 

0  136 

137 
(*** Eliminator  split ***) 

138 

1105  139 
(*A METAequality, so that it applies to higher types as well...*) 
760  140 
qed_goalw "split" ZF.thy [split_def] 
1105  141 
"split(%x y.c(x,y), <a,b>) == c(a,b)" 
142 
(fn _ => [ (simp_tac pair_ss 1), 

143 
(rtac reflexive_thm 1) ]); 

0  144 

760  145 
qed_goal "split_type" ZF.thy 
0  146 
"[ p:Sigma(A,B); \ 
147 
\ !!x y.[ x:A; y:B(x) ] ==> c(x,y):C(<x,y>) \ 

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

149 
(fn major::prems=> 

150 
[ (rtac (major RS SigmaE) 1), 

1105  151 
(asm_simp_tac (pair_ss addsimps (split::prems)) 1) ]); 
0  152 

1105  153 
goalw ZF.thy [split_def] 
435  154 
"!!u. u: A*B ==> \ 
155 
\ R(split(c,u)) <> (ALL x:A. ALL y:B. u = <x,y> > R(c(x,y)))"; 

156 
by (etac SigmaE 1); 

1105  157 
by (asm_simp_tac pair_ss 1); 
158 
by (fast_tac pair_cs 1); 

760  159 
qed "expand_split"; 
435  160 

161 

0  162 
(*** split for predicates: result type o ***) 
163 

1105  164 
goalw ZF.thy [split_def] "!!R a b. R(a,b) ==> split(R, <a,b>)"; 
165 
by (asm_simp_tac pair_ss 1); 

166 
qed "splitI"; 

0  167 

1105  168 
val major::sigma::prems = goalw ZF.thy [split_def] 
1461  169 
"[ split(R,z); z:Sigma(A,B); \ 
170 
\ !!x y. [ z = <x,y>; R(x,y) ] ==> P \ 

1105  171 
\ ] ==> P"; 
172 
by (rtac (sigma RS SigmaE) 1); 

0  173 
by (cut_facts_tac [major] 1); 
1105  174 
by (asm_full_simp_tac (pair_ss addsimps prems) 1); 
175 
qed "splitE"; 

0  176 

1105  177 
goalw ZF.thy [split_def] "!!R a b. split(R,<a,b>) ==> R(a,b)"; 
178 
by (asm_full_simp_tac pair_ss 1); 

179 
qed "splitD"; 

0  180 

533
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

181 

7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

182 
(*** Basic simplification for ZF; see simpdata.ML for full version ***) 
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

183 

7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

184 
fun prove_fun s = 
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

185 
(writeln s; prove_goal ZF.thy s 
860
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

186 
(fn prems => [ (cut_facts_tac prems 1), 
1461  187 
(fast_tac (pair_cs addSIs [equalityI]) 1) ])); 
533
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

188 

7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

189 
(*INCLUDED IN ZF_ss*) 
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

190 
val mem_simps = map prove_fun 
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

191 
[ "a : 0 <> False", 
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

192 
"a : A Un B <> a:A  a:B", 
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

193 
"a : A Int B <> a:A & a:B", 
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

194 
"a : AB <> a:A & ~a:B", 
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

195 
"<a,b>: Sigma(A,B) <> a:A & b:B(a)", 
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

196 
"a : Collect(A,P) <> a:A & P(a)" ]; 
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

197 

7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

198 
goal ZF.thy "{x.x:A} = A"; 
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

199 
by (fast_tac (pair_cs addSIs [equalityI]) 1); 
760  200 
qed "triv_RepFun"; 
533
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

201 

860
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

202 
(*INCLUDED: should be? And what about cons(a,b)?*) 
533
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

203 
val bquant_simps = map prove_fun 
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

204 
[ "(ALL x:0.P(x)) <> True", 
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

205 
"(EX x:0.P(x)) <> False", 
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

206 
"(ALL x:succ(i).P(x)) <> P(i) & (ALL x:i.P(x))", 
860
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

207 
"(EX x:succ(i).P(x)) <> P(i)  (EX x:i.P(x))", 
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

208 
"(ALL x:cons(a,B).P(x)) <> P(a) & (ALL x:B.P(x))", 
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

209 
"(EX x:cons(a,B).P(x)) <> P(a)  (EX x:B.P(x))" ]; 
533
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset

210 

860
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

211 
val Collect_simps = map prove_fun 
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

212 
[ "{x:0. P(x)} = 0", 
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

213 
"{x:A. False} = 0", 
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

214 
"{x:A. True} = A", 
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

215 
"RepFun(0,f) = 0", 
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

216 
"RepFun(succ(i),f) = cons(f(i), RepFun(i,f))", 
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

217 
"RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))" ]; 
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

218 

c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

219 
val UnInt_simps = map prove_fun 
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

220 
[ "0 Un A = A", "A Un 0 = A", 
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

221 
"0 Int A = 0", "A Int 0 = 0", 
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

222 
"0A = 0", "A0 = A", 
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

223 
"Union(0) = 0", 
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

224 
"Union(cons(b,A)) = b Un Union(A)", 
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

225 
"Inter({b}) = b"]; 
c8e93e8b3f55
prove_fun now includes equalityI. Added the rewrite rules
lcp
parents:
822
diff
changeset

226 