author | lcp |
Fri, 23 Dec 1994 16:25:45 +0100 | |
changeset 822 | 8d5748202c53 |
parent 782 | 200a16083201 |
child 860 | c8e93e8b3f55 |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: ZF/pair |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
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 |
||
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) |
|
83 |
THEN prune_params_tac) |
|
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 |
||
105 |
||
106 |
(*** Eliminator - split ***) |
|
107 |
||
760 | 108 |
qed_goalw "split" ZF.thy [split_def] |
0 | 109 |
"split(%x y.c(x,y), <a,b>) = c(a,b)" |
110 |
(fn _ => |
|
435 | 111 |
[ (fast_tac (upair_cs addIs [the_equality] addSEs [Pair_inject]) 1) ]); |
0 | 112 |
|
760 | 113 |
qed_goal "split_type" ZF.thy |
0 | 114 |
"[| p:Sigma(A,B); \ |
115 |
\ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \ |
|
116 |
\ |] ==> split(%x y.c(x,y), p) : C(p)" |
|
117 |
(fn major::prems=> |
|
118 |
[ (rtac (major RS SigmaE) 1), |
|
119 |
(etac ssubst 1), |
|
120 |
(REPEAT (ares_tac (prems @ [split RS ssubst]) 1)) ]); |
|
121 |
||
435 | 122 |
|
123 |
goal ZF.thy |
|
124 |
"!!u. u: A*B ==> \ |
|
125 |
\ R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))"; |
|
126 |
by (etac SigmaE 1); |
|
127 |
by (asm_simp_tac (FOL_ss addsimps [split]) 1); |
|
128 |
by (fast_tac (upair_cs addSEs [Pair_inject]) 1); |
|
760 | 129 |
qed "expand_split"; |
435 | 130 |
|
131 |
||
0 | 132 |
(*** conversions for fst and snd ***) |
133 |
||
760 | 134 |
qed_goalw "fst_conv" ZF.thy [fst_def] "fst(<a,b>) = a" |
0 | 135 |
(fn _=> [ (rtac split 1) ]); |
136 |
||
760 | 137 |
qed_goalw "snd_conv" ZF.thy [snd_def] "snd(<a,b>) = b" |
0 | 138 |
(fn _=> [ (rtac split 1) ]); |
139 |
||
822
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset
|
140 |
qed_goalw "fst_type" ZF.thy [fst_def] |
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset
|
141 |
"!!p. p:Sigma(A,B) ==> fst(p) : A" |
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset
|
142 |
(fn _=> [ (etac split_type 1), (assume_tac 1) ]); |
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset
|
143 |
|
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset
|
144 |
qed_goalw "snd_type" ZF.thy [snd_def] |
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset
|
145 |
"!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))" |
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset
|
146 |
(fn _=> [ (etac split_type 1), |
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset
|
147 |
(asm_simp_tac (FOL_ss addsimps [fst_conv]) 1) ]); |
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset
|
148 |
|
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset
|
149 |
|
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset
|
150 |
goal ZF.thy "!!a A B. a: Sigma(A,B) ==> <fst(a),snd(a)> = a"; |
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset
|
151 |
by (etac SigmaE 1); |
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset
|
152 |
by (asm_simp_tac (FOL_ss addsimps [fst_conv,snd_conv]) 1); |
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset
|
153 |
qed "Pair_fst_snd_eq"; |
8d5748202c53
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents:
782
diff
changeset
|
154 |
|
0 | 155 |
|
156 |
(*** split for predicates: result type o ***) |
|
157 |
||
158 |
goalw ZF.thy [fsplit_def] "!!R a b. R(a,b) ==> fsplit(R, <a,b>)"; |
|
159 |
by (REPEAT (ares_tac [refl,exI,conjI] 1)); |
|
760 | 160 |
qed "fsplitI"; |
0 | 161 |
|
162 |
val major::prems = goalw ZF.thy [fsplit_def] |
|
163 |
"[| fsplit(R,z); !!x y. [| z = <x,y>; R(x,y) |] ==> P |] ==> P"; |
|
164 |
by (cut_facts_tac [major] 1); |
|
165 |
by (REPEAT (eresolve_tac (prems@[asm_rl,exE,conjE]) 1)); |
|
760 | 166 |
qed "fsplitE"; |
0 | 167 |
|
168 |
goal ZF.thy "!!R a b. fsplit(R,<a,b>) ==> R(a,b)"; |
|
169 |
by (REPEAT (eresolve_tac [asm_rl,fsplitE,Pair_inject,ssubst] 1)); |
|
760 | 170 |
qed "fsplitD"; |
0 | 171 |
|
172 |
val pair_cs = upair_cs |
|
173 |
addSIs [SigmaI] |
|
174 |
addSEs [SigmaE2, SigmaE, Pair_inject, make_elim succ_inject, |
|
175 |
Pair_neq_0, sym RS Pair_neq_0, succ_neq_0, sym RS succ_neq_0]; |
|
176 |
||
533
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
177 |
|
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
178 |
(*** 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
|
179 |
|
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
180 |
fun prove_fun s = |
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
181 |
(writeln s; prove_goal ZF.thy s |
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
182 |
(fn prems => [ (cut_facts_tac prems 1), (fast_tac pair_cs 1) ])); |
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 |
(*INCLUDED IN ZF_ss*) |
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
185 |
val mem_simps = map prove_fun |
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
186 |
[ "a : 0 <-> False", |
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
187 |
"a : A Un B <-> a:A | a:B", |
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
188 |
"a : A Int B <-> a:A & a:B", |
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
189 |
"a : A-B <-> a:A & ~a:B", |
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
190 |
"<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
|
191 |
"a : Collect(A,P) <-> a:A & P(a)" ]; |
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
192 |
|
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
193 |
goal ZF.thy "{x.x:A} = A"; |
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
194 |
by (fast_tac (pair_cs addSIs [equalityI]) 1); |
760 | 195 |
qed "triv_RepFun"; |
533
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
196 |
|
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
197 |
(*INCLUDED: should be??*) |
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
198 |
val bquant_simps = map prove_fun |
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
199 |
[ "(ALL x:0.P(x)) <-> True", |
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
200 |
"(EX x:0.P(x)) <-> False", |
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
201 |
"(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))", |
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
202 |
"(EX x:succ(i).P(x)) <-> P(i) | (EX x:i.P(x))" ]; |
7357160bc56a
ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents:
437
diff
changeset
|
203 |