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 (*** Rules for the Part primitive ***) |
|
10 |
|
11 Goalw [Part_def] |
|
12 "a : Part(A,h) <-> a:A & (EX y. a=h(y))"; |
|
13 by (rtac separation 1); |
|
14 qed "Part_iff"; |
|
15 |
|
16 Goalw [Part_def] |
|
17 "[| a : A; a=h(b) |] ==> a : Part(A,h)"; |
|
18 by (Blast_tac 1); |
|
19 qed "Part_eqI"; |
|
20 |
|
21 bind_thm ("PartI", refl RSN (2,Part_eqI)); |
|
22 |
|
23 val major::prems = Goalw [Part_def] |
|
24 "[| a : Part(A,h); !!z. [| a : A; a=h(z) |] ==> P \ |
|
25 \ |] ==> P"; |
|
26 by (rtac (major RS CollectE) 1); |
|
27 by (etac exE 1); |
|
28 by (REPEAT (ares_tac prems 1)); |
|
29 qed "PartE"; |
|
30 |
|
31 AddIs [Part_eqI]; |
|
32 AddSEs [PartE]; |
|
33 |
|
34 Goalw [Part_def] "Part(A,h) <= A"; |
|
35 by (rtac Collect_subset 1); |
|
36 qed "Part_subset"; |
|
37 |
|
38 |
|
39 (*** Rules for Disjoint Sums ***) |
|
40 |
|
41 bind_thms ("sum_defs", [sum_def,Inl_def,Inr_def,case_def]); |
|
42 |
|
43 Goalw (bool_def::sum_defs) "Sigma(bool,C) = C(0) + C(1)"; |
|
44 by (Blast_tac 1); |
|
45 qed "Sigma_bool"; |
|
46 |
|
47 (** Introduction rules for the injections **) |
|
48 |
|
49 Goalw sum_defs "a : A ==> Inl(a) : A+B"; |
|
50 by (Blast_tac 1); |
|
51 qed "InlI"; |
|
52 |
|
53 Goalw sum_defs "b : B ==> Inr(b) : A+B"; |
|
54 by (Blast_tac 1); |
|
55 qed "InrI"; |
|
56 |
|
57 (** Elimination rules **) |
|
58 |
|
59 val major::prems = Goalw sum_defs |
|
60 "[| u: A+B; \ |
|
61 \ !!x. [| x:A; u=Inl(x) |] ==> P; \ |
|
62 \ !!y. [| y:B; u=Inr(y) |] ==> P \ |
|
63 \ |] ==> P"; |
|
64 by (rtac (major RS UnE) 1); |
|
65 by (REPEAT (rtac refl 1 |
|
66 ORELSE eresolve_tac (prems@[SigmaE,singletonE,ssubst]) 1)); |
|
67 qed "sumE"; |
|
68 |
|
69 (** Injection and freeness equivalences, for rewriting **) |
|
70 |
|
71 Goalw sum_defs "Inl(a)=Inl(b) <-> a=b"; |
|
72 by (Simp_tac 1); |
|
73 qed "Inl_iff"; |
|
74 |
|
75 Goalw sum_defs "Inr(a)=Inr(b) <-> a=b"; |
|
76 by (Simp_tac 1); |
|
77 qed "Inr_iff"; |
|
78 |
|
79 Goalw sum_defs "Inl(a)=Inr(b) <-> False"; |
|
80 by (Simp_tac 1); |
|
81 qed "Inl_Inr_iff"; |
|
82 |
|
83 Goalw sum_defs "Inr(b)=Inl(a) <-> False"; |
|
84 by (Simp_tac 1); |
|
85 qed "Inr_Inl_iff"; |
|
86 |
|
87 Goalw sum_defs "0+0 = 0"; |
|
88 by (Simp_tac 1); |
|
89 qed "sum_empty"; |
|
90 |
|
91 (*Injection and freeness rules*) |
|
92 |
|
93 bind_thm ("Inl_inject", (Inl_iff RS iffD1)); |
|
94 bind_thm ("Inr_inject", (Inr_iff RS iffD1)); |
|
95 bind_thm ("Inl_neq_Inr", (Inl_Inr_iff RS iffD1 RS FalseE)); |
|
96 bind_thm ("Inr_neq_Inl", (Inr_Inl_iff RS iffD1 RS FalseE)); |
|
97 |
|
98 AddSIs [InlI, InrI]; |
|
99 AddSEs [sumE, Inl_neq_Inr, Inr_neq_Inl]; |
|
100 AddSDs [Inl_inject, Inr_inject]; |
|
101 |
|
102 Addsimps [InlI, InrI, Inl_iff, Inr_iff, Inl_Inr_iff, Inr_Inl_iff, sum_empty]; |
|
103 AddTCs [InlI, InrI]; |
|
104 |
|
105 Goal "Inl(a): A+B ==> a: A"; |
|
106 by (Blast_tac 1); |
|
107 qed "InlD"; |
|
108 |
|
109 Goal "Inr(b): A+B ==> b: B"; |
|
110 by (Blast_tac 1); |
|
111 qed "InrD"; |
|
112 |
|
113 Goal "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))"; |
|
114 by (Blast_tac 1); |
|
115 qed "sum_iff"; |
|
116 |
|
117 Goal "A+B <= C+D <-> A<=C & B<=D"; |
|
118 by (Blast_tac 1); |
|
119 qed "sum_subset_iff"; |
|
120 |
|
121 Goal "A+B = C+D <-> A=C & B=D"; |
|
122 by (simp_tac (simpset() addsimps [extension,sum_subset_iff]) 1); |
|
123 by (Blast_tac 1); |
|
124 qed "sum_equal_iff"; |
|
125 |
|
126 Goalw [sum_def] "A+A = 2*A"; |
|
127 by (Blast_tac 1); |
|
128 qed "sum_eq_2_times"; |
|
129 |
|
130 |
|
131 (*** Eliminator -- case ***) |
|
132 |
|
133 Goalw sum_defs "case(c, d, Inl(a)) = c(a)"; |
|
134 by (Simp_tac 1); |
|
135 qed "case_Inl"; |
|
136 |
|
137 Goalw sum_defs "case(c, d, Inr(b)) = d(b)"; |
|
138 by (Simp_tac 1); |
|
139 qed "case_Inr"; |
|
140 |
|
141 Addsimps [case_Inl, case_Inr]; |
|
142 |
|
143 val major::prems = Goal |
|
144 "[| u: A+B; \ |
|
145 \ !!x. x: A ==> c(x): C(Inl(x)); \ |
|
146 \ !!y. y: B ==> d(y): C(Inr(y)) \ |
|
147 \ |] ==> case(c,d,u) : C(u)"; |
|
148 by (rtac (major RS sumE) 1); |
|
149 by (ALLGOALS (etac ssubst)); |
|
150 by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); |
|
151 qed "case_type"; |
|
152 AddTCs [case_type]; |
|
153 |
|
154 Goal "u: A+B ==> \ |
|
155 \ R(case(c,d,u)) <-> \ |
|
156 \ ((ALL x:A. u = Inl(x) --> R(c(x))) & \ |
|
157 \ (ALL y:B. u = Inr(y) --> R(d(y))))"; |
|
158 by Auto_tac; |
|
159 qed "expand_case"; |
|
160 |
|
161 val major::prems = Goal |
|
162 "[| z: A+B; \ |
|
163 \ !!x. x:A ==> c(x)=c'(x); \ |
|
164 \ !!y. y:B ==> d(y)=d'(y) \ |
|
165 \ |] ==> case(c,d,z) = case(c',d',z)"; |
|
166 by (resolve_tac [major RS sumE] 1); |
|
167 by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); |
|
168 qed "case_cong"; |
|
169 |
|
170 Goal "z: A+B ==> \ |
|
171 \ case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) = \ |
|
172 \ case(%x. c(c'(x)), %y. d(d'(y)), z)"; |
|
173 by Auto_tac; |
|
174 qed "case_case"; |
|
175 |
|
176 |
|
177 (*** More rules for Part(A,h) ***) |
|
178 |
|
179 Goal "A<=B ==> Part(A,h)<=Part(B,h)"; |
|
180 by (Blast_tac 1); |
|
181 qed "Part_mono"; |
|
182 |
|
183 Goal "Part(Collect(A,P), h) = Collect(Part(A,h), P)"; |
|
184 by (Blast_tac 1); |
|
185 qed "Part_Collect"; |
|
186 |
|
187 bind_thm ("Part_CollectE", Part_Collect RS equalityD1 RS subsetD RS CollectE); |
|
188 |
|
189 Goal "Part(A+B,Inl) = {Inl(x). x: A}"; |
|
190 by (Blast_tac 1); |
|
191 qed "Part_Inl"; |
|
192 |
|
193 Goal "Part(A+B,Inr) = {Inr(y). y: B}"; |
|
194 by (Blast_tac 1); |
|
195 qed "Part_Inr"; |
|
196 |
|
197 Goalw [Part_def] "a : Part(A,h) ==> a : A"; |
|
198 by (etac CollectD1 1); |
|
199 qed "PartD1"; |
|
200 |
|
201 Goal "Part(A,%x. x) = A"; |
|
202 by (Blast_tac 1); |
|
203 qed "Part_id"; |
|
204 |
|
205 Goal "Part(A+B, %x. Inr(h(x))) = {Inr(y). y: Part(B,h)}"; |
|
206 by (Blast_tac 1); |
|
207 qed "Part_Inr2"; |
|
208 |
|
209 Goal "C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C"; |
|
210 by (Blast_tac 1); |
|
211 qed "Part_sum_equality"; |
|