author  lcp 
Thu, 30 Mar 1995 14:01:35 +0200  
changeset 985  2e50c5124ca3 
parent 834  ad1d0eb0ee82 
child 1017  6a402dc505cf 
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 

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] 

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, 

197 
rtac theI 1, 

198 
resolve_tac prems 1 ]); 

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), 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

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

242 
(asm_simp_tac if_ss 1) ]); 
0  243 

244 
val prems = goal ZF.thy 

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

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

247 
by (ALLGOALS (asm_simp_tac (if_ss addsimps prems))); 
760  248 
qed "if_type"; 
0  249 

250 

251 
(*** Foundation lemmas ***) 

252 

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

0  257 
(etac equals0D 1), 
258 
(rtac consI1 1), 

673  259 
(fast_tac (lemmas_cs addIs [consI1,consI2] 
0  260 
addSEs [consE,equalityE]) 1) ]); 
261 

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

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

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

0  273 
(*** Rules for succ ***) 
274 

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

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

281 

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

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

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

287 

760  288 
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

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

290 

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

291 
(*Classical introduction rule*) 
760  292 
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

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

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

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

296 

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

300 
(rtac succI1 1) ]); 

301 

302 
(*Useful for rewriting*) 

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

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

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

308 

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

312 
addEs [mem_asym]) 1) ]); 

0  313 

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

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

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

318 
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

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

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

323 