author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 1609  5324067d993f 
permissions  rwrr 
1461  1 
(* Title: ZF/upair 
0  2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  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 

1461  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 *) 

0  20 

21 

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

23 

760  24 
qed_goalw "pairing" ZF.thy [Upair_def] 
0  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 

760  28 
qed_goal "UpairI1" ZF.thy "a : Upair(a,b)" 
0  29 
(fn _ => [ (rtac (refl RS disjI1 RS (pairing RS iffD2)) 1) ]); 
30 

760  31 
qed_goal "UpairI2" ZF.thy "b : Upair(a,b)" 
0  32 
(fn _ => [ (rtac (refl RS disjI2 RS (pairing RS iffD2)) 1) ]); 
33 

760  34 
qed_goal "UpairE" ZF.thy 
0  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 

760  42 
qed_goalw "UnI1" ZF.thy [Un_def] "c : A ==> c : A Un B" 
0  43 
(fn [prem]=> [ (rtac (prem RS (UpairI1 RS UnionI)) 1) ]); 
44 

760  45 
qed_goalw "UnI2" ZF.thy [Un_def] "c : B ==> c : A Un B" 
0  46 
(fn [prem]=> [ (rtac (prem RS (UpairI2 RS UnionI)) 1) ]); 
47 

760  48 
qed_goalw "UnE" ZF.thy [Un_def] 
0  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*) 
760  56 
qed_goal "UnE'" ZF.thy 
572  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 

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

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

760  70 
qed_goal "UnCI" 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 

760  78 
qed_goalw "IntI" ZF.thy [Int_def] 
0  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 

760  84 
qed_goalw "IntD1" ZF.thy [Int_def] "c : A Int B ==> c : A" 
0  85 
(fn [major]=> 
86 
[ (rtac (UpairI1 RS (major RS InterD)) 1) ]); 

87 

760  88 
qed_goalw "IntD2" ZF.thy [Int_def] "c : A Int B ==> c : B" 
0  89 
(fn [major]=> 
90 
[ (rtac (UpairI2 RS (major RS InterD)) 1) ]); 

91 

760  92 
qed_goal "IntE" ZF.thy 
0  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 

760  98 
qed_goal "Int_iff" ZF.thy "c : A Int B <> (c:A & c:B)" 
0  99 
(fn _ => [ (fast_tac (lemmas_cs addSIs [IntI] addSEs [IntE]) 1) ]); 
100 

101 

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

103 

760  104 
qed_goalw "DiffI" ZF.thy [Diff_def] 
37  105 
"[ c : A; c ~: B ] ==> c : A  B" 
0  106 
(fn prems=> [ (REPEAT (resolve_tac (prems @ [CollectI]) 1)) ]); 
107 

760  108 
qed_goalw "DiffD1" ZF.thy [Diff_def] 
0  109 
"c : A  B ==> c : A" 
110 
(fn [major]=> [ (rtac (major RS CollectD1) 1) ]); 

111 

760  112 
qed_goalw "DiffD2" ZF.thy [Diff_def] 
485  113 
"c : A  B ==> c ~: B" 
114 
(fn [major]=> [ (rtac (major RS CollectD2) 1) ]); 

0  115 

760  116 
qed_goal "DiffE" 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 

760  122 
qed_goal "Diff_iff" 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 

760  127 
qed_goalw "consI1" ZF.thy [cons_def] "a : cons(a,B)" 
0  128 
(fn _ => [ (rtac (UpairI1 RS UnI1) 1) ]); 
129 

760  130 
qed_goalw "consI2" ZF.thy [cons_def] "a : B ==> a : cons(b,B)" 
0  131 
(fn [prem]=> [ (rtac (prem RS UnI2) 1) ]); 
132 

760  133 
qed_goalw "consE" ZF.thy [cons_def] 
0  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*) 
760  140 
qed_goal "consE'" ZF.thy 
572  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 

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

153 
(*Classical introduction rule*) 

760  154 
qed_goal "consCI" 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 

760  161 
qed_goal "singletonI" ZF.thy "a : {a}" 
0  162 
(fn _=> [ (rtac consI1 1) ]); 
163 

760  164 
qed_goal "singletonE" ZF.thy "[ a: {b}; a=b ==> P ] ==> P" 
0  165 
(fn major::prems=> 
166 
[ (rtac (major RS consE) 1), 

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

168 

834  169 
qed_goal "singleton_iff" ZF.thy "a : {b} <> a=b" 
170 
(fn _ => [ (fast_tac (lemmas_cs addIs [consI1] addSEs [consE]) 1) ]); 

171 

0  172 

173 
(*** Rules for Descriptions ***) 

174 

760  175 
qed_goalw "the_equality" ZF.thy [the_def] 
0  176 
"[ P(a); !!x. P(x) ==> x=a ] ==> (THE x. P(x)) = a" 
738  177 
(fn [pa,eq] => 
178 
[ (fast_tac (lemmas_cs addSIs [singletonI,pa] addIs [equalityI] 

1461  179 
addEs [eq RS subst]) 1) ]); 
0  180 

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

760  182 
qed_goal "the_equality2" ZF.thy 
673  183 
"!!P. [ EX! x. P(x); P(a) ] ==> (THE x. P(x)) = a" 
184 
(fn _ => 

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

0  186 

760  187 
qed_goal "theI" ZF.thy "EX! x. P(x) ==> P(THE x. P(x))" 
0  188 
(fn [major]=> 
189 
[ (rtac (major RS ex1E) 1), 

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

191 
(REPEAT (assume_tac 1)) ]); 

192 

686  193 
(*Easier to apply than theI: conclusion has only one occurrence of P*) 
760  194 
qed_goal "theI2" ZF.thy 
686  195 
"[ EX! x. P(x); !!x. P(x) ==> Q(x) ] ==> Q(THE x.P(x))" 
196 
(fn prems => [ resolve_tac prems 1, 

1461  197 
rtac theI 1, 
198 
resolve_tac prems 1 ]); 

686  199 

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

202 

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

760  204 
qed_goalw "the_0" ZF.thy [the_def] 
435  205 
"!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0" 
206 
(fn _ => 

485  207 
[ (fast_tac (lemmas_cs addIs [equalityI] addSEs [ReplaceE]) 1) ]); 
435  208 

0  209 

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

211 

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

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

760  214 
qed "if_true"; 
0  215 

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

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

760  218 
qed "if_false"; 
0  219 

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

220 
(*Never use with case splitting, or if P is known to be true or false*) 
0  221 
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

222 
"[ 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

223 
by (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1); 
760  224 
qed "if_cong"; 
0  225 

226 
(*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

227 
goalw ZF.thy [if_def] "!!P. P ==> if(P,a,b) = a"; 
0  228 
by (fast_tac (lemmas_cs addSIs [the_equality]) 1); 
760  229 
qed "if_P"; 
0  230 

231 
(*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

232 
goalw ZF.thy [if_def] "!!P. ~P ==> if(P,a,b) = b"; 
0  233 
by (fast_tac (lemmas_cs addSIs [the_equality]) 1); 
760  234 
qed "if_not_P"; 
0  235 

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

236 
val if_ss = FOL_ss addsimps [if_true,if_false]; 
0  237 

760  238 
qed_goal "expand_if" ZF.thy 
0  239 
"P(if(Q,x,y)) <> ((Q > P(x)) & (~Q > P(y)))" 
437  240 
(fn _=> [ (excluded_middle_tac "Q" 1), 
1461  241 
(asm_simp_tac if_ss 1), 
242 
(asm_simp_tac if_ss 1) ]); 

0  243 

1017
6a402dc505cf
Proved if_iff and used it to simplify proof of if_type.
lcp
parents:
985
diff
changeset

244 
qed_goal "if_iff" ZF.thy "a: if(P,x,y) <> P & a:x  ~P & a:y" 
6a402dc505cf
Proved if_iff and used it to simplify proof of if_type.
lcp
parents:
985
diff
changeset

245 
(fn _=> [ (simp_tac (if_ss setloop split_tac [expand_if]) 1) ]); 
6a402dc505cf
Proved if_iff and used it to simplify proof of if_type.
lcp
parents:
985
diff
changeset

246 

6a402dc505cf
Proved if_iff and used it to simplify proof of if_type.
lcp
parents:
985
diff
changeset

247 
qed_goal "if_type" ZF.thy 
6a402dc505cf
Proved if_iff and used it to simplify proof of if_type.
lcp
parents:
985
diff
changeset

248 
"[ P ==> a: A; ~P ==> b: A ] ==> if(P,a,b): A" 
6a402dc505cf
Proved if_iff and used it to simplify proof of if_type.
lcp
parents:
985
diff
changeset

249 
(fn prems=> [ (simp_tac 
1461  250 
(if_ss addsimps prems setloop split_tac [expand_if]) 1) ]); 
0  251 

252 

253 
(*** Foundation lemmas ***) 

254 

437  255 
(*was called mem_anti_sym*) 
760  256 
qed_goal "mem_asym" ZF.thy "!!P. [ a:b; b:a ] ==> P" 
673  257 
(fn _=> 
258 
[ (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1), 

0  259 
(etac equals0D 1), 
260 
(rtac consI1 1), 

673  261 
(fast_tac (lemmas_cs addIs [consI1,consI2] 
1461  262 
addSEs [consE,equalityE]) 1) ]); 
0  263 

437  264 
(*was called mem_anti_refl*) 
760  265 
qed_goal "mem_irrefl" ZF.thy "a:a ==> P" 
437  266 
(fn [major]=> [ (rtac (major RS (major RS mem_asym)) 1) ]); 
0  267 

760  268 
qed_goal "mem_not_refl" ZF.thy "a ~: a" 
437  269 
(K [ (rtac notI 1), (etac mem_irrefl 1) ]); 
0  270 

435  271 
(*Good for proving inequalities by rewriting*) 
760  272 
qed_goal "mem_imp_not_eq" ZF.thy "!!a A. a:A ==> a ~= A" 
437  273 
(fn _=> [ fast_tac (lemmas_cs addSEs [mem_irrefl]) 1 ]); 
435  274 

0  275 
(*** Rules for succ ***) 
276 

760  277 
qed_goalw "succI1" ZF.thy [succ_def] "i : succ(i)" 
0  278 
(fn _=> [ (rtac consI1 1) ]); 
279 

760  280 
qed_goalw "succI2" ZF.thy [succ_def] 
0  281 
"i : j ==> i : succ(j)" 
282 
(fn [prem]=> [ (rtac (prem RS consI2) 1) ]); 

283 

760  284 
qed_goalw "succE" ZF.thy [succ_def] 
0  285 
"[ i : succ(j); i=j ==> P; i:j ==> P ] ==> P" 
286 
(fn major::prems=> 

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

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

289 

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

291 
(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

292 

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

293 
(*Classical introduction rule*) 
760  294 
qed_goal "succCI" 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

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

296 
[ (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

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

298 

760  299 
qed_goal "succ_neq_0" ZF.thy "succ(n)=0 ==> P" 
0  300 
(fn [major]=> 
301 
[ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1), 

302 
(rtac succI1 1) ]); 

303 

304 
(*Useful for rewriting*) 

760  305 
qed_goal "succ_not_0" ZF.thy "succ(n) ~= 0" 
0  306 
(fn _=> [ (rtac notI 1), (etac succ_neq_0 1) ]); 
307 

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

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

310 

760  311 
qed_goal "succ_inject" ZF.thy "!!m n. succ(m) = succ(n) ==> m=n" 
673  312 
(fn _ => 
313 
[ (fast_tac (lemmas_cs addSEs [succE, equalityE, make_elim succ_subsetD] 

314 
addEs [mem_asym]) 1) ]); 

0  315 

760  316 
qed_goal "succ_inject_iff" ZF.thy "succ(m) = succ(n) <> m=n" 
0  317 
(fn _=> [ (fast_tac (FOL_cs addSEs [succ_inject]) 1) ]); 
318 

985
2e50c5124ca3
Added comment about why mem_irrefl should not be a safeE.
lcp
parents:
834
diff
changeset

319 
(*UpairI1/2 should become UpairCI? 
2e50c5124ca3
Added comment about why mem_irrefl should not be a safeE.
lcp
parents:
834
diff
changeset

320 
mem_irrefl should NOT be added as an elimrule here; 
2e50c5124ca3
Added comment about why mem_irrefl should not be a safeE.
lcp
parents:
834
diff
changeset

321 
it would be tried on most goals, making proof slower!*) 
0  322 
val upair_cs = lemmas_cs 
323 
addSIs [singletonI, DiffI, IntI, UnCI, consCI, succCI, UpairI1,UpairI2] 

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

325 