66 qed "sumE"; |
69 qed "sumE"; |
67 |
70 |
68 (** Injection and freeness equivalences, for rewriting **) |
71 (** Injection and freeness equivalences, for rewriting **) |
69 |
72 |
70 goalw Sum.thy sum_defs "Inl(a)=Inl(b) <-> a=b"; |
73 goalw Sum.thy sum_defs "Inl(a)=Inl(b) <-> a=b"; |
71 by (simp_tac ZF_ss 1); |
74 by (Simp_tac 1); |
72 qed "Inl_iff"; |
75 qed "Inl_iff"; |
73 |
76 |
74 goalw Sum.thy sum_defs "Inr(a)=Inr(b) <-> a=b"; |
77 goalw Sum.thy sum_defs "Inr(a)=Inr(b) <-> a=b"; |
75 by (simp_tac ZF_ss 1); |
78 by (Simp_tac 1); |
76 qed "Inr_iff"; |
79 qed "Inr_iff"; |
77 |
80 |
78 goalw Sum.thy sum_defs "Inl(a)=Inr(b) <-> False"; |
81 goalw Sum.thy sum_defs "Inl(a)=Inr(b) <-> False"; |
79 by (simp_tac (ZF_ss addsimps [one_not_0 RS not_sym]) 1); |
82 by (Simp_tac 1); |
80 qed "Inl_Inr_iff"; |
83 qed "Inl_Inr_iff"; |
81 |
84 |
82 goalw Sum.thy sum_defs "Inr(b)=Inl(a) <-> False"; |
85 goalw Sum.thy sum_defs "Inr(b)=Inl(a) <-> False"; |
83 by (simp_tac (ZF_ss addsimps [one_not_0]) 1); |
86 by (Simp_tac 1); |
84 qed "Inr_Inl_iff"; |
87 qed "Inr_Inl_iff"; |
|
88 |
|
89 goalw Sum.thy sum_defs "0+0 = 0"; |
|
90 by (Simp_tac 1); |
|
91 qed "sum_empty"; |
85 |
92 |
86 (*Injection and freeness rules*) |
93 (*Injection and freeness rules*) |
87 |
94 |
88 bind_thm ("Inl_inject", (Inl_iff RS iffD1)); |
95 bind_thm ("Inl_inject", (Inl_iff RS iffD1)); |
89 bind_thm ("Inr_inject", (Inr_iff RS iffD1)); |
96 bind_thm ("Inr_inject", (Inr_iff RS iffD1)); |
90 bind_thm ("Inl_neq_Inr", (Inl_Inr_iff RS iffD1 RS FalseE)); |
97 bind_thm ("Inl_neq_Inr", (Inl_Inr_iff RS iffD1 RS FalseE)); |
91 bind_thm ("Inr_neq_Inl", (Inr_Inl_iff RS iffD1 RS FalseE)); |
98 bind_thm ("Inr_neq_Inl", (Inr_Inl_iff RS iffD1 RS FalseE)); |
92 |
99 |
93 val sum_cs = ZF_cs addSIs [PartI, InlI, InrI] |
100 AddSIs [InlI, InrI]; |
94 addSEs [PartE, sumE, Inl_neq_Inr, Inr_neq_Inl] |
101 AddSEs [sumE, Inl_neq_Inr, Inr_neq_Inl]; |
95 addSDs [Inl_inject, Inr_inject]; |
102 AddSDs [Inl_inject, Inr_inject]; |
|
103 |
|
104 Addsimps [InlI, InrI, Inl_iff, Inr_iff, Inl_Inr_iff, Inr_Inl_iff, sum_empty]; |
|
105 |
|
106 val sum_cs = !claset; |
96 |
107 |
97 goal Sum.thy "!!A B. Inl(a): A+B ==> a: A"; |
108 goal Sum.thy "!!A B. Inl(a): A+B ==> a: A"; |
98 by (fast_tac sum_cs 1); |
109 by (Fast_tac 1); |
99 qed "InlD"; |
110 qed "InlD"; |
100 |
111 |
101 goal Sum.thy "!!A B. Inr(b): A+B ==> b: B"; |
112 goal Sum.thy "!!A B. Inr(b): A+B ==> b: B"; |
102 by (fast_tac sum_cs 1); |
113 by (Fast_tac 1); |
103 qed "InrD"; |
114 qed "InrD"; |
104 |
115 |
105 goal Sum.thy "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))"; |
116 goal Sum.thy "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))"; |
106 by (fast_tac sum_cs 1); |
117 by (Fast_tac 1); |
107 qed "sum_iff"; |
118 qed "sum_iff"; |
108 |
119 |
109 goal Sum.thy "A+B <= C+D <-> A<=C & B<=D"; |
120 goal Sum.thy "A+B <= C+D <-> A<=C & B<=D"; |
110 by (fast_tac sum_cs 1); |
121 by (Fast_tac 1); |
111 qed "sum_subset_iff"; |
122 qed "sum_subset_iff"; |
112 |
123 |
113 goal Sum.thy "A+B = C+D <-> A=C & B=D"; |
124 goal Sum.thy "A+B = C+D <-> A=C & B=D"; |
114 by (simp_tac (ZF_ss addsimps [extension,sum_subset_iff]) 1); |
125 by (simp_tac (!simpset addsimps [extension,sum_subset_iff]) 1); |
115 by (fast_tac ZF_cs 1); |
126 by (Fast_tac 1); |
116 qed "sum_equal_iff"; |
127 qed "sum_equal_iff"; |
117 |
128 |
118 goalw Sum.thy [sum_def] "A+A = 2*A"; |
129 goalw Sum.thy [sum_def] "A+A = 2*A"; |
119 by (fast_tac eq_cs 1); |
130 by (fast_tac eq_cs 1); |
120 qed "sum_eq_2_times"; |
131 qed "sum_eq_2_times"; |
121 |
132 |
122 |
133 |
123 (*** Eliminator -- case ***) |
134 (*** Eliminator -- case ***) |
124 |
135 |
125 goalw Sum.thy sum_defs "case(c, d, Inl(a)) = c(a)"; |
136 goalw Sum.thy sum_defs "case(c, d, Inl(a)) = c(a)"; |
126 by (simp_tac (ZF_ss addsimps [cond_0]) 1); |
137 by (simp_tac (!simpset addsimps [cond_0]) 1); |
127 qed "case_Inl"; |
138 qed "case_Inl"; |
128 |
139 |
129 goalw Sum.thy sum_defs "case(c, d, Inr(b)) = d(b)"; |
140 goalw Sum.thy sum_defs "case(c, d, Inr(b)) = d(b)"; |
130 by (simp_tac (ZF_ss addsimps [cond_1]) 1); |
141 by (simp_tac (!simpset addsimps [cond_1]) 1); |
131 qed "case_Inr"; |
142 qed "case_Inr"; |
|
143 |
|
144 Addsimps [case_Inl, case_Inr]; |
|
145 |
|
146 val sum_ss = !simpset; |
132 |
147 |
133 val major::prems = goal Sum.thy |
148 val major::prems = goal Sum.thy |
134 "[| u: A+B; \ |
149 "[| u: A+B; \ |
135 \ !!x. x: A ==> c(x): C(Inl(x)); \ |
150 \ !!x. x: A ==> c(x): C(Inl(x)); \ |
136 \ !!y. y: B ==> d(y): C(Inr(y)) \ |
151 \ !!y. y: B ==> d(y): C(Inr(y)) \ |
137 \ |] ==> case(c,d,u) : C(u)"; |
152 \ |] ==> case(c,d,u) : C(u)"; |
138 by (rtac (major RS sumE) 1); |
153 by (rtac (major RS sumE) 1); |
139 by (ALLGOALS (etac ssubst)); |
154 by (ALLGOALS (etac ssubst)); |
140 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps |
155 by (ALLGOALS (asm_simp_tac (!simpset addsimps prems))); |
141 (prems@[case_Inl,case_Inr])))); |
|
142 qed "case_type"; |
156 qed "case_type"; |
143 |
157 |
144 goal Sum.thy |
158 goal Sum.thy |
145 "!!u. u: A+B ==> \ |
159 "!!u. u: A+B ==> \ |
146 \ R(case(c,d,u)) <-> \ |
160 \ R(case(c,d,u)) <-> \ |
147 \ ((ALL x:A. u = Inl(x) --> R(c(x))) & \ |
161 \ ((ALL x:A. u = Inl(x) --> R(c(x))) & \ |
148 \ (ALL y:B. u = Inr(y) --> R(d(y))))"; |
162 \ (ALL y:B. u = Inr(y) --> R(d(y))))"; |
149 by (etac sumE 1); |
163 by (Auto_tac()); |
150 by (asm_simp_tac (ZF_ss addsimps [case_Inl]) 1); |
|
151 by (fast_tac sum_cs 1); |
|
152 by (asm_simp_tac (ZF_ss addsimps [case_Inr]) 1); |
|
153 by (fast_tac sum_cs 1); |
|
154 qed "expand_case"; |
164 qed "expand_case"; |
155 |
165 |
156 val major::prems = goal Sum.thy |
166 val major::prems = goal Sum.thy |
157 "[| z: A+B; \ |
167 "[| z: A+B; \ |
158 \ !!x. x:A ==> c(x)=c'(x); \ |
168 \ !!x. x:A ==> c(x)=c'(x); \ |
159 \ !!y. y:B ==> d(y)=d'(y) \ |
169 \ !!y. y:B ==> d(y)=d'(y) \ |
160 \ |] ==> case(c,d,z) = case(c',d',z)"; |
170 \ |] ==> case(c,d,z) = case(c',d',z)"; |
161 by (resolve_tac [major RS sumE] 1); |
171 by (resolve_tac [major RS sumE] 1); |
162 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps ([case_Inl, case_Inr] @ prems)))); |
172 by (ALLGOALS (asm_simp_tac (!simpset addsimps prems))); |
163 qed "case_cong"; |
173 qed "case_cong"; |
164 |
174 |
165 val [major] = goal Sum.thy |
175 goal Sum.thy |
166 "z: A+B ==> \ |
176 "!!z. z: A+B ==> \ |
167 \ case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) = \ |
177 \ case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) = \ |
168 \ case(%x. c(c'(x)), %y. d(d'(y)), z)"; |
178 \ case(%x. c(c'(x)), %y. d(d'(y)), z)"; |
169 by (resolve_tac [major RS sumE] 1); |
179 by (Auto_tac()); |
170 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [case_Inl, case_Inr]))); |
|
171 qed "case_case"; |
180 qed "case_case"; |
172 |
181 |
173 val sum_ss = ZF_ss addsimps [InlI, InrI, Inl_iff, Inr_iff, |
|
174 Inl_Inr_iff, Inr_Inl_iff, |
|
175 case_Inl, case_Inr]; |
|
176 |
182 |
177 (*** More rules for Part(A,h) ***) |
183 (*** More rules for Part(A,h) ***) |
178 |
184 |
179 goal Sum.thy "!!A B h. A<=B ==> Part(A,h)<=Part(B,h)"; |
185 goal Sum.thy "!!A B h. A<=B ==> Part(A,h)<=Part(B,h)"; |
180 by (fast_tac sum_cs 1); |
186 by (Fast_tac 1); |
181 qed "Part_mono"; |
187 qed "Part_mono"; |
182 |
188 |
183 goal Sum.thy "Part(Collect(A,P), h) = Collect(Part(A,h), P)"; |
189 goal Sum.thy "Part(Collect(A,P), h) = Collect(Part(A,h), P)"; |
184 by (fast_tac (sum_cs addSIs [equalityI]) 1); |
190 by (fast_tac (!claset addSIs [equalityI]) 1); |
185 qed "Part_Collect"; |
191 qed "Part_Collect"; |
186 |
192 |
187 bind_thm ("Part_CollectE", Part_Collect RS equalityD1 RS subsetD RS CollectE); |
193 bind_thm ("Part_CollectE", Part_Collect RS equalityD1 RS subsetD RS CollectE); |
188 |
194 |
189 goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}"; |
195 goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}"; |
190 by (fast_tac (sum_cs addIs [equalityI]) 1); |
196 by (fast_tac (!claset addIs [equalityI]) 1); |
191 qed "Part_Inl"; |
197 qed "Part_Inl"; |
192 |
198 |
193 goal Sum.thy "Part(A+B,Inr) = {Inr(y). y: B}"; |
199 goal Sum.thy "Part(A+B,Inr) = {Inr(y). y: B}"; |
194 by (fast_tac (sum_cs addIs [equalityI]) 1); |
200 by (fast_tac (!claset addIs [equalityI]) 1); |
195 qed "Part_Inr"; |
201 qed "Part_Inr"; |
196 |
202 |
197 goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A"; |
203 goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A"; |
198 by (etac CollectD1 1); |
204 by (etac CollectD1 1); |
199 qed "PartD1"; |
205 qed "PartD1"; |
200 |
206 |
201 goal Sum.thy "Part(A,%x.x) = A"; |
207 goal Sum.thy "Part(A,%x.x) = A"; |
202 by (fast_tac (sum_cs addIs [equalityI]) 1); |
208 by (fast_tac (!claset addIs [equalityI]) 1); |
203 qed "Part_id"; |
209 qed "Part_id"; |
204 |
210 |
205 goal Sum.thy "Part(A+B, %x.Inr(h(x))) = {Inr(y). y: Part(B,h)}"; |
211 goal Sum.thy "Part(A+B, %x.Inr(h(x))) = {Inr(y). y: Part(B,h)}"; |
206 by (fast_tac (sum_cs addIs [equalityI]) 1); |
212 by (fast_tac (!claset addIs [equalityI]) 1); |
207 qed "Part_Inr2"; |
213 qed "Part_Inr2"; |
208 |
214 |
209 goal Sum.thy "!!A B C. C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C"; |
215 goal Sum.thy "!!A B C. C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C"; |
210 by (fast_tac (sum_cs addIs [equalityI]) 1); |
216 by (fast_tac (!claset addIs [equalityI]) 1); |
211 qed "Part_sum_equality"; |
217 qed "Part_sum_equality"; |