author | paulson |
Tue, 18 Jun 2002 10:52:08 +0200 | |
changeset 13218 | 3732064ccbd1 |
parent 12836 | 5ef96e63fba6 |
permissions | -rw-r--r-- |
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 Zermelo-Fraenkel Set Theory |
|
7 |
*) |
|
8 |
||
9 |
(** Lemmas for showing that <a,b> uniquely determines a and b **) |
|
10 |
||
9180 | 11 |
Goal "{a} = {b} <-> a=b"; |
12 |
by (resolve_tac [extension RS iff_trans] 1); |
|
13 |
by (Blast_tac 1) ; |
|
14 |
qed "singleton_eq_iff"; |
|
12814 | 15 |
AddIffs [singleton_eq_iff]; |
822
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset
|
16 |
|
9180 | 17 |
Goal "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"; |
18 |
by (resolve_tac [extension RS iff_trans] 1); |
|
19 |
by (Blast_tac 1) ; |
|
20 |
qed "doubleton_eq_iff"; |
|
0 | 21 |
|
9211 | 22 |
Goalw [Pair_def] "<a,b> = <c,d> <-> a=c & b=d"; |
23 |
by (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1); |
|
24 |
by (Blast_tac 1) ; |
|
25 |
qed "Pair_iff"; |
|
0 | 26 |
|
2469 | 27 |
Addsimps [Pair_iff]; |
28 |
||
29 |
bind_thm ("Pair_inject", Pair_iff RS iffD1 RS conjE); |
|
0 | 30 |
|
2469 | 31 |
AddSEs [Pair_inject]; |
32 |
||
33 |
bind_thm ("Pair_inject1", Pair_iff RS iffD1 RS conjunct1); |
|
34 |
bind_thm ("Pair_inject2", Pair_iff RS iffD1 RS conjunct2); |
|
0 | 35 |
|
9211 | 36 |
Goalw [Pair_def] "<a,b> ~= 0"; |
37 |
by (blast_tac (claset() addEs [equalityE]) 1) ; |
|
38 |
qed "Pair_not_0"; |
|
0 | 39 |
|
2469 | 40 |
bind_thm ("Pair_neq_0", Pair_not_0 RS notE); |
0 | 41 |
|
2469 | 42 |
AddSEs [Pair_neq_0, sym RS Pair_neq_0]; |
43 |
||
9211 | 44 |
Goalw [Pair_def] "<a,b>=a ==> P"; |
45 |
by (rtac (consI1 RS mem_asym RS FalseE) 1); |
|
46 |
by (etac subst 1); |
|
47 |
by (rtac consI1 1) ; |
|
48 |
qed "Pair_neq_fst"; |
|
0 | 49 |
|
9211 | 50 |
Goalw [Pair_def] "<a,b>=b ==> P"; |
51 |
by (rtac (consI1 RS consI2 RS mem_asym RS FalseE) 1); |
|
52 |
by (etac subst 1); |
|
53 |
by (rtac (consI1 RS consI2) 1) ; |
|
54 |
qed "Pair_neq_snd"; |
|
0 | 55 |
|
56 |
||
57 |
(*** Sigma: Disjoint union of a family of sets |
|
58 |
Generalizes Cartesian product ***) |
|
59 |
||
9211 | 60 |
Goalw [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"; |
61 |
by (Blast_tac 1) ; |
|
62 |
qed "Sigma_iff"; |
|
2469 | 63 |
|
64 |
Addsimps [Sigma_iff]; |
|
65 |
||
9180 | 66 |
Goal "[| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)"; |
67 |
by (Asm_simp_tac 1); |
|
68 |
qed "SigmaI"; |
|
69 |
||
6153 | 70 |
AddTCs [SigmaI]; |
2469 | 71 |
|
72 |
bind_thm ("SigmaD1", Sigma_iff RS iffD1 RS conjunct1); |
|
73 |
bind_thm ("SigmaD2", Sigma_iff RS iffD1 RS conjunct2); |
|
0 | 74 |
|
75 |
(*The general elimination rule*) |
|
9211 | 76 |
val major::prems= Goalw [Sigma_def] |
0 | 77 |
"[| c: Sigma(A,B); \ |
78 |
\ !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P \ |
|
9211 | 79 |
\ |] ==> P"; |
80 |
by (cut_facts_tac [major] 1); |
|
81 |
by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ; |
|
82 |
qed "SigmaE"; |
|
0 | 83 |
|
9180 | 84 |
val [major,minor]= Goal |
0 | 85 |
"[| <a,b> : Sigma(A,B); \ |
86 |
\ [| a:A; b:B(a) |] ==> P \ |
|
9180 | 87 |
\ |] ==> P"; |
88 |
by (rtac minor 1); |
|
89 |
by (rtac (major RS SigmaD1) 1); |
|
90 |
by (rtac (major RS SigmaD2) 1) ; |
|
91 |
qed "SigmaE2"; |
|
0 | 92 |
|
9211 | 93 |
val prems= Goalw [Sigma_def] |
0 | 94 |
"[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \ |
9211 | 95 |
\ Sigma(A,B) = Sigma(A',B')"; |
96 |
by (simp_tac (simpset() addsimps prems) 1) ; |
|
97 |
qed "Sigma_cong"; |
|
2469 | 98 |
|
0 | 99 |
|
2469 | 100 |
(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause |
101 |
flex-flex pairs and the "Check your prover" error. Most |
|
102 |
Sigmas and Pis are abbreviated as * or -> *) |
|
0 | 103 |
|
2469 | 104 |
AddSIs [SigmaI]; |
105 |
AddSEs [SigmaE2, SigmaE]; |
|
0 | 106 |
|
9180 | 107 |
Goal "Sigma(0,B) = 0"; |
108 |
by (Blast_tac 1) ; |
|
109 |
qed "Sigma_empty1"; |
|
2469 | 110 |
|
9180 | 111 |
Goal "A*0 = 0"; |
112 |
by (Blast_tac 1) ; |
|
113 |
qed "Sigma_empty2"; |
|
2469 | 114 |
|
115 |
Addsimps [Sigma_empty1, Sigma_empty2]; |
|
1105 | 116 |
|
5264 | 117 |
Goal "A*B=0 <-> A=0 | B=0"; |
118 |
by (Blast_tac 1); |
|
119 |
qed "Sigma_empty_iff"; |
|
120 |
||
1105 | 121 |
|
122 |
(*** Projections: fst, snd ***) |
|
123 |
||
9211 | 124 |
Goalw [fst_def] "fst(<a,b>) = a"; |
125 |
by (Blast_tac 1) ; |
|
126 |
qed "fst_conv"; |
|
1105 | 127 |
|
9211 | 128 |
Goalw [snd_def] "snd(<a,b>) = b"; |
129 |
by (Blast_tac 1) ; |
|
130 |
qed "snd_conv"; |
|
1105 | 131 |
|
2469 | 132 |
Addsimps [fst_conv,snd_conv]; |
1105 | 133 |
|
9180 | 134 |
Goal "p:Sigma(A,B) ==> fst(p) : A"; |
135 |
by (Auto_tac) ; |
|
136 |
qed "fst_type"; |
|
12836 | 137 |
AddTCs [fst_type]; |
1105 | 138 |
|
9180 | 139 |
Goal "p:Sigma(A,B) ==> snd(p) : B(fst(p))"; |
140 |
by (Auto_tac) ; |
|
141 |
qed "snd_type"; |
|
12836 | 142 |
AddTCs [snd_type]; |
1105 | 143 |
|
9180 | 144 |
Goal "a: Sigma(A,B) ==> <fst(a),snd(a)> = a"; |
145 |
by (Auto_tac) ; |
|
146 |
qed "Pair_fst_snd_eq"; |
|
1105 | 147 |
|
0 | 148 |
|
149 |
(*** Eliminator - split ***) |
|
150 |
||
1105 | 151 |
(*A META-equality, so that it applies to higher types as well...*) |
6112 | 152 |
Goalw [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)"; |
153 |
by (Simp_tac 1); |
|
154 |
qed "split"; |
|
2469 | 155 |
Addsimps [split]; |
156 |
||
9180 | 157 |
val major::prems= Goal |
0 | 158 |
"[| p:Sigma(A,B); \ |
159 |
\ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \ |
|
9180 | 160 |
\ |] ==> split(%x y. c(x,y), p) : C(p)"; |
161 |
by (rtac (major RS SigmaE) 1); |
|
162 |
by (asm_simp_tac (simpset() addsimps prems) 1); |
|
163 |
qed "split_type"; |
|
6153 | 164 |
AddTCs [split_type]; |
0 | 165 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5264
diff
changeset
|
166 |
Goalw [split_def] |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5264
diff
changeset
|
167 |
"u: A*B ==> \ |
435 | 168 |
\ R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))"; |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4091
diff
changeset
|
169 |
by Auto_tac; |
760 | 170 |
qed "expand_split"; |
435 | 171 |
|
172 |
||
0 | 173 |
(*** split for predicates: result type o ***) |
174 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5264
diff
changeset
|
175 |
Goalw [split_def] "R(a,b) ==> split(R, <a,b>)"; |
2469 | 176 |
by (Asm_simp_tac 1); |
1105 | 177 |
qed "splitI"; |
0 | 178 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5264
diff
changeset
|
179 |
val major::sigma::prems = Goalw [split_def] |
1461 | 180 |
"[| split(R,z); z:Sigma(A,B); \ |
181 |
\ !!x y. [| z = <x,y>; R(x,y) |] ==> P \ |
|
1105 | 182 |
\ |] ==> P"; |
183 |
by (rtac (sigma RS SigmaE) 1); |
|
0 | 184 |
by (cut_facts_tac [major] 1); |
2469 | 185 |
by (REPEAT (ares_tac prems 1)); |
186 |
by (Asm_full_simp_tac 1); |
|
1105 | 187 |
qed "splitE"; |
0 | 188 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5264
diff
changeset
|
189 |
Goalw [split_def] "split(R,<a,b>) ==> R(a,b)"; |
2469 | 190 |
by (Full_simp_tac 1); |
1105 | 191 |
qed "splitD"; |