|
1 (* Title: ZF/sum |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 Disjoint sums in Zermelo-Fraenkel Set Theory |
|
7 *) |
|
8 |
|
9 open Sum; |
|
10 |
|
11 val sum_defs = [sum_def,Inl_def,Inr_def,case_def]; |
|
12 |
|
13 (** Introduction rules for the injections **) |
|
14 |
|
15 goalw Sum.thy sum_defs "!!a A B. a : A ==> Inl(a) : A+B"; |
|
16 by (REPEAT (ares_tac [UnI1,SigmaI,singletonI] 1)); |
|
17 val InlI = result(); |
|
18 |
|
19 goalw Sum.thy sum_defs "!!b A B. b : B ==> Inr(b) : A+B"; |
|
20 by (REPEAT (ares_tac [UnI2,SigmaI,singletonI] 1)); |
|
21 val InrI = result(); |
|
22 |
|
23 (** Elimination rules **) |
|
24 |
|
25 val major::prems = goalw Sum.thy sum_defs |
|
26 "[| u: A+B; \ |
|
27 \ !!x. [| x:A; u=Inl(x) |] ==> P; \ |
|
28 \ !!y. [| y:B; u=Inr(y) |] ==> P \ |
|
29 \ |] ==> P"; |
|
30 by (rtac (major RS UnE) 1); |
|
31 by (REPEAT (rtac refl 1 |
|
32 ORELSE eresolve_tac (prems@[SigmaE,singletonE,ssubst]) 1)); |
|
33 val sumE = result(); |
|
34 |
|
35 (** Injection and freeness rules **) |
|
36 |
|
37 val [major] = goalw Sum.thy sum_defs "Inl(a)=Inl(b) ==> a=b"; |
|
38 by (EVERY1 [rtac (major RS Pair_inject), assume_tac]); |
|
39 val Inl_inject = result(); |
|
40 |
|
41 val [major] = goalw Sum.thy sum_defs "Inr(a)=Inr(b) ==> a=b"; |
|
42 by (EVERY1 [rtac (major RS Pair_inject), assume_tac]); |
|
43 val Inr_inject = result(); |
|
44 |
|
45 val [major] = goalw Sum.thy sum_defs "Inl(a)=Inr(b) ==> P"; |
|
46 by (rtac (major RS Pair_inject) 1); |
|
47 by (etac (sym RS one_neq_0) 1); |
|
48 val Inl_neq_Inr = result(); |
|
49 |
|
50 val Inr_neq_Inl = sym RS Inl_neq_Inr; |
|
51 |
|
52 (** Injection and freeness equivalences, for rewriting **) |
|
53 |
|
54 goal Sum.thy "Inl(a)=Inl(b) <-> a=b"; |
|
55 by (rtac iffI 1); |
|
56 by (REPEAT (eresolve_tac [Inl_inject,subst_context] 1)); |
|
57 val Inl_iff = result(); |
|
58 |
|
59 goal Sum.thy "Inr(a)=Inr(b) <-> a=b"; |
|
60 by (rtac iffI 1); |
|
61 by (REPEAT (eresolve_tac [Inr_inject,subst_context] 1)); |
|
62 val Inr_iff = result(); |
|
63 |
|
64 goal Sum.thy "Inl(a)=Inr(b) <-> False"; |
|
65 by (rtac iffI 1); |
|
66 by (REPEAT (eresolve_tac [Inl_neq_Inr,FalseE] 1)); |
|
67 val Inl_Inr_iff = result(); |
|
68 |
|
69 goal Sum.thy "Inr(b)=Inl(a) <-> False"; |
|
70 by (rtac iffI 1); |
|
71 by (REPEAT (eresolve_tac [Inr_neq_Inl,FalseE] 1)); |
|
72 val Inr_Inl_iff = result(); |
|
73 |
|
74 val sum_cs = ZF_cs addIs [InlI,InrI] addSEs [sumE,Inl_neq_Inr,Inr_neq_Inl] |
|
75 addSDs [Inl_inject,Inr_inject]; |
|
76 |
|
77 goal Sum.thy "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))"; |
|
78 by (fast_tac sum_cs 1); |
|
79 val sum_iff = result(); |
|
80 |
|
81 goal Sum.thy "A+B <= C+D <-> A<=C & B<=D"; |
|
82 by (fast_tac sum_cs 1); |
|
83 val sum_subset_iff = result(); |
|
84 |
|
85 goal Sum.thy "A+B = C+D <-> A=C & B=D"; |
|
86 by (SIMP_TAC (ZF_ss addrews [extension,sum_subset_iff]) 1); |
|
87 by (fast_tac ZF_cs 1); |
|
88 val sum_equal_iff = result(); |
|
89 |
|
90 (*** Eliminator -- case ***) |
|
91 |
|
92 goalw Sum.thy sum_defs "case(c, d, Inl(a)) = c(a)"; |
|
93 by (rtac (split RS trans) 1); |
|
94 by (rtac cond_0 1); |
|
95 val case_Inl = result(); |
|
96 |
|
97 goalw Sum.thy sum_defs "case(c, d, Inr(b)) = d(b)"; |
|
98 by (rtac (split RS trans) 1); |
|
99 by (rtac cond_1 1); |
|
100 val case_Inr = result(); |
|
101 |
|
102 val prems = goalw Sum.thy [case_def] |
|
103 "[| u=u'; !!x. c(x)=c'(x); !!y. d(y)=d'(y) |] ==> \ |
|
104 \ case(c,d,u)=case(c',d',u')"; |
|
105 by (REPEAT (resolve_tac ([refl,split_cong,cond_cong] @ prems) 1)); |
|
106 val case_cong = result(); |
|
107 |
|
108 val major::prems = goal Sum.thy |
|
109 "[| u: A+B; \ |
|
110 \ !!x. x: A ==> c(x): C(Inl(x)); \ |
|
111 \ !!y. y: B ==> d(y): C(Inr(y)) \ |
|
112 \ |] ==> case(c,d,u) : C(u)"; |
|
113 by (rtac (major RS sumE) 1); |
|
114 by (ALLGOALS (etac ssubst)); |
|
115 by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews |
|
116 (prems@[case_Inl,case_Inr])))); |
|
117 val case_type = result(); |
|
118 |
|
119 (** Rules for the Part primitive **) |
|
120 |
|
121 goalw Sum.thy [Part_def] |
|
122 "!!a b A h. [| a : A; a=h(b) |] ==> a : Part(A,h)"; |
|
123 by (REPEAT (ares_tac [exI,CollectI] 1)); |
|
124 val Part_eqI = result(); |
|
125 |
|
126 val PartI = refl RSN (2,Part_eqI); |
|
127 |
|
128 val major::prems = goalw Sum.thy [Part_def] |
|
129 "[| a : Part(A,h); !!z. [| a : A; a=h(z) |] ==> P \ |
|
130 \ |] ==> P"; |
|
131 by (rtac (major RS CollectE) 1); |
|
132 by (etac exE 1); |
|
133 by (REPEAT (ares_tac prems 1)); |
|
134 val PartE = result(); |
|
135 |
|
136 goalw Sum.thy [Part_def] "Part(A,h) <= A"; |
|
137 by (rtac Collect_subset 1); |
|
138 val Part_subset = result(); |
|
139 |
|
140 goal Sum.thy "!!A B h. A<=B ==> Part(A,h)<=Part(B,h)"; |
|
141 by (fast_tac (ZF_cs addIs [PartI] addSEs [PartE]) 1); |
|
142 val Part_mono = result(); |
|
143 |
|
144 goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}"; |
|
145 by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1); |
|
146 val Part_Inl = result(); |
|
147 |
|
148 goal Sum.thy "Part(A+B,Inr) = {Inr(y). y: B}"; |
|
149 by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1); |
|
150 val Part_Inr = result(); |
|
151 |
|
152 goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A"; |
|
153 by (etac CollectD1 1); |
|
154 val PartD1 = result(); |
|
155 |
|
156 goal Sum.thy "Part(A,%x.x) = A"; |
|
157 by (fast_tac (ZF_cs addIs [PartI,equalityI] addSEs [PartE]) 1); |
|
158 val Part_id = result(); |
|
159 |
|
160 goal Sum.thy "Part(A+B, %x.Inr(h(x))) = {Inr(y). y: Part(B,h)}"; |
|
161 by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1); |
|
162 val Part_Inr2 = result(); |
|
163 |
|
164 goal Sum.thy "!!A B C. C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C"; |
|
165 by (rtac equalityI 1); |
|
166 by (rtac Un_least 1); |
|
167 by (rtac Part_subset 1); |
|
168 by (rtac Part_subset 1); |
|
169 by (fast_tac (ZF_cs addIs [PartI] addSEs [sumE]) 1); |
|
170 val Part_sum_equality = result(); |