|
1 (* Title: HOLCF/sprod0.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for theory sprod0.thy |
|
7 *) |
|
8 |
|
9 open Sprod0; |
|
10 |
|
11 (* ------------------------------------------------------------------------ *) |
|
12 (* A non-emptyness result for Sprod *) |
|
13 (* ------------------------------------------------------------------------ *) |
|
14 |
|
15 val SprodI = prove_goalw Sprod0.thy [Sprod_def] |
|
16 "Spair_Rep(a,b):Sprod" |
|
17 (fn prems => |
|
18 [ |
|
19 (EVERY1 [rtac CollectI, rtac exI,rtac exI, rtac refl]) |
|
20 ]); |
|
21 |
|
22 |
|
23 val inj_onto_Abs_Sprod = prove_goal Sprod0.thy |
|
24 "inj_onto(Abs_Sprod,Sprod)" |
|
25 (fn prems => |
|
26 [ |
|
27 (rtac inj_onto_inverseI 1), |
|
28 (etac Abs_Sprod_inverse 1) |
|
29 ]); |
|
30 |
|
31 |
|
32 (* ------------------------------------------------------------------------ *) |
|
33 (* Strictness and definedness of Spair_Rep *) |
|
34 (* ------------------------------------------------------------------------ *) |
|
35 |
|
36 |
|
37 val strict_Spair_Rep = prove_goalw Sprod0.thy [Spair_Rep_def] |
|
38 "(a=UU | b=UU) ==> (Spair_Rep(a,b) = Spair_Rep(UU,UU))" |
|
39 (fn prems => |
|
40 [ |
|
41 (cut_facts_tac prems 1), |
|
42 (rtac ext 1), |
|
43 (rtac ext 1), |
|
44 (rtac iffI 1), |
|
45 (fast_tac HOL_cs 1), |
|
46 (fast_tac HOL_cs 1) |
|
47 ]); |
|
48 |
|
49 val defined_Spair_Rep_rev = prove_goalw Sprod0.thy [Spair_Rep_def] |
|
50 "(Spair_Rep(a,b) = Spair_Rep(UU,UU)) ==> (a=UU | b=UU)" |
|
51 (fn prems => |
|
52 [ |
|
53 (res_inst_tac [("Q","a=UU|b=UU")] classical2 1), |
|
54 (atac 1), |
|
55 (rtac disjI1 1), |
|
56 (rtac ((hd prems) RS fun_cong RS fun_cong RS iffD2 RS mp RS |
|
57 conjunct1 RS sym) 1), |
|
58 (fast_tac HOL_cs 1), |
|
59 (fast_tac HOL_cs 1) |
|
60 ]); |
|
61 |
|
62 |
|
63 (* ------------------------------------------------------------------------ *) |
|
64 (* injectivity of Spair_Rep and Ispair *) |
|
65 (* ------------------------------------------------------------------------ *) |
|
66 |
|
67 val inject_Spair_Rep = prove_goalw Sprod0.thy [Spair_Rep_def] |
|
68 "[|~aa=UU ; ~ba=UU ; Spair_Rep(a,b)=Spair_Rep(aa,ba) |] ==> a=aa & b=ba" |
|
69 (fn prems => |
|
70 [ |
|
71 (cut_facts_tac prems 1), |
|
72 (rtac ((nth_elem (2,prems)) RS fun_cong RS fun_cong |
|
73 RS iffD1 RS mp) 1), |
|
74 (fast_tac HOL_cs 1), |
|
75 (fast_tac HOL_cs 1) |
|
76 ]); |
|
77 |
|
78 |
|
79 val inject_Ispair = prove_goalw Sprod0.thy [Ispair_def] |
|
80 "[|~aa=UU ; ~ba=UU ; Ispair(a,b)=Ispair(aa,ba) |] ==> a=aa & b=ba" |
|
81 (fn prems => |
|
82 [ |
|
83 (cut_facts_tac prems 1), |
|
84 (etac inject_Spair_Rep 1), |
|
85 (atac 1), |
|
86 (etac (inj_onto_Abs_Sprod RS inj_ontoD) 1), |
|
87 (rtac SprodI 1), |
|
88 (rtac SprodI 1) |
|
89 ]); |
|
90 |
|
91 |
|
92 (* ------------------------------------------------------------------------ *) |
|
93 (* strictness and definedness of Ispair *) |
|
94 (* ------------------------------------------------------------------------ *) |
|
95 |
|
96 val strict_Ispair = prove_goalw Sprod0.thy [Ispair_def] |
|
97 "(a=UU | b=UU) ==> Ispair(a,b)=Ispair(UU,UU)" |
|
98 (fn prems => |
|
99 [ |
|
100 (cut_facts_tac prems 1), |
|
101 (etac (strict_Spair_Rep RS arg_cong) 1) |
|
102 ]); |
|
103 |
|
104 val strict_Ispair1 = prove_goalw Sprod0.thy [Ispair_def] |
|
105 "Ispair(UU,b) = Ispair(UU,UU)" |
|
106 (fn prems => |
|
107 [ |
|
108 (rtac (strict_Spair_Rep RS arg_cong) 1), |
|
109 (rtac disjI1 1), |
|
110 (rtac refl 1) |
|
111 ]); |
|
112 |
|
113 val strict_Ispair2 = prove_goalw Sprod0.thy [Ispair_def] |
|
114 "Ispair(a,UU) = Ispair(UU,UU)" |
|
115 (fn prems => |
|
116 [ |
|
117 (rtac (strict_Spair_Rep RS arg_cong) 1), |
|
118 (rtac disjI2 1), |
|
119 (rtac refl 1) |
|
120 ]); |
|
121 |
|
122 val strict_Ispair_rev = prove_goal Sprod0.thy |
|
123 "~Ispair(x,y)=Ispair(UU,UU) ==> ~x=UU & ~y=UU" |
|
124 (fn prems => |
|
125 [ |
|
126 (cut_facts_tac prems 1), |
|
127 (rtac (de_morgan1 RS ssubst) 1), |
|
128 (etac contrapos 1), |
|
129 (etac strict_Ispair 1) |
|
130 ]); |
|
131 |
|
132 val defined_Ispair_rev = prove_goalw Sprod0.thy [Ispair_def] |
|
133 "Ispair(a,b) = Ispair(UU,UU) ==> (a = UU | b = UU)" |
|
134 (fn prems => |
|
135 [ |
|
136 (cut_facts_tac prems 1), |
|
137 (rtac defined_Spair_Rep_rev 1), |
|
138 (rtac (inj_onto_Abs_Sprod RS inj_ontoD) 1), |
|
139 (atac 1), |
|
140 (rtac SprodI 1), |
|
141 (rtac SprodI 1) |
|
142 ]); |
|
143 |
|
144 val defined_Ispair = prove_goal Sprod0.thy |
|
145 "[|~a=UU; ~b=UU|] ==> ~(Ispair(a,b) = Ispair(UU,UU))" |
|
146 (fn prems => |
|
147 [ |
|
148 (cut_facts_tac prems 1), |
|
149 (rtac contrapos 1), |
|
150 (etac defined_Ispair_rev 2), |
|
151 (rtac (de_morgan1 RS iffD1) 1), |
|
152 (etac conjI 1), |
|
153 (atac 1) |
|
154 ]); |
|
155 |
|
156 |
|
157 (* ------------------------------------------------------------------------ *) |
|
158 (* Exhaustion of the strict product ** *) |
|
159 (* ------------------------------------------------------------------------ *) |
|
160 |
|
161 val Exh_Sprod = prove_goalw Sprod0.thy [Ispair_def] |
|
162 "z=Ispair(UU,UU) | (? a b. z=Ispair(a,b) & ~a=UU & ~b=UU)" |
|
163 (fn prems => |
|
164 [ |
|
165 (rtac (rewrite_rule [Sprod_def] Rep_Sprod RS CollectE) 1), |
|
166 (etac exE 1), |
|
167 (etac exE 1), |
|
168 (rtac (excluded_middle RS disjE) 1), |
|
169 (rtac disjI2 1), |
|
170 (rtac exI 1), |
|
171 (rtac exI 1), |
|
172 (rtac conjI 1), |
|
173 (rtac (Rep_Sprod_inverse RS sym RS trans) 1), |
|
174 (etac arg_cong 1), |
|
175 (rtac (de_morgan1 RS ssubst) 1), |
|
176 (atac 1), |
|
177 (rtac disjI1 1), |
|
178 (rtac (Rep_Sprod_inverse RS sym RS trans) 1), |
|
179 (res_inst_tac [("f","Abs_Sprod")] arg_cong 1), |
|
180 (etac trans 1), |
|
181 (etac strict_Spair_Rep 1) |
|
182 ]); |
|
183 |
|
184 (* ------------------------------------------------------------------------ *) |
|
185 (* general elimination rule for strict product *) |
|
186 (* ------------------------------------------------------------------------ *) |
|
187 |
|
188 val IsprodE = prove_goal Sprod0.thy |
|
189 "[|p=Ispair(UU,UU) ==> Q ;!!x y. [|p=Ispair(x,y); ~x=UU ; ~y=UU|] ==> Q|] ==> Q" |
|
190 (fn prems => |
|
191 [ |
|
192 (rtac (Exh_Sprod RS disjE) 1), |
|
193 (etac (hd prems) 1), |
|
194 (etac exE 1), |
|
195 (etac exE 1), |
|
196 (etac conjE 1), |
|
197 (etac conjE 1), |
|
198 (etac (hd (tl prems)) 1), |
|
199 (atac 1), |
|
200 (atac 1) |
|
201 ]); |
|
202 |
|
203 |
|
204 (* ------------------------------------------------------------------------ *) |
|
205 (* some results about the selectors Isfst, Issnd *) |
|
206 (* ------------------------------------------------------------------------ *) |
|
207 |
|
208 val strict_Isfst = prove_goalw Sprod0.thy [Isfst_def] |
|
209 "p=Ispair(UU,UU)==>Isfst(p)=UU" |
|
210 (fn prems => |
|
211 [ |
|
212 (cut_facts_tac prems 1), |
|
213 (rtac select_equality 1), |
|
214 (rtac conjI 1), |
|
215 (fast_tac HOL_cs 1), |
|
216 (strip_tac 1), |
|
217 (res_inst_tac [("P","Ispair(UU,UU) = Ispair(a,b)")] notE 1), |
|
218 (rtac not_sym 1), |
|
219 (rtac defined_Ispair 1), |
|
220 (REPEAT (fast_tac HOL_cs 1)) |
|
221 ]); |
|
222 |
|
223 |
|
224 val strict_Isfst1 = prove_goal Sprod0.thy |
|
225 "Isfst(Ispair(UU,y)) = UU" |
|
226 (fn prems => |
|
227 [ |
|
228 (rtac (strict_Ispair1 RS ssubst) 1), |
|
229 (rtac strict_Isfst 1), |
|
230 (rtac refl 1) |
|
231 ]); |
|
232 |
|
233 val strict_Isfst2 = prove_goal Sprod0.thy |
|
234 "Isfst(Ispair(x,UU)) = UU" |
|
235 (fn prems => |
|
236 [ |
|
237 (rtac (strict_Ispair2 RS ssubst) 1), |
|
238 (rtac strict_Isfst 1), |
|
239 (rtac refl 1) |
|
240 ]); |
|
241 |
|
242 |
|
243 val strict_Issnd = prove_goalw Sprod0.thy [Issnd_def] |
|
244 "p=Ispair(UU,UU)==>Issnd(p)=UU" |
|
245 (fn prems => |
|
246 [ |
|
247 (cut_facts_tac prems 1), |
|
248 (rtac select_equality 1), |
|
249 (rtac conjI 1), |
|
250 (fast_tac HOL_cs 1), |
|
251 (strip_tac 1), |
|
252 (res_inst_tac [("P","Ispair(UU,UU) = Ispair(a,b)")] notE 1), |
|
253 (rtac not_sym 1), |
|
254 (rtac defined_Ispair 1), |
|
255 (REPEAT (fast_tac HOL_cs 1)) |
|
256 ]); |
|
257 |
|
258 val strict_Issnd1 = prove_goal Sprod0.thy |
|
259 "Issnd(Ispair(UU,y)) = UU" |
|
260 (fn prems => |
|
261 [ |
|
262 (rtac (strict_Ispair1 RS ssubst) 1), |
|
263 (rtac strict_Issnd 1), |
|
264 (rtac refl 1) |
|
265 ]); |
|
266 |
|
267 val strict_Issnd2 = prove_goal Sprod0.thy |
|
268 "Issnd(Ispair(x,UU)) = UU" |
|
269 (fn prems => |
|
270 [ |
|
271 (rtac (strict_Ispair2 RS ssubst) 1), |
|
272 (rtac strict_Issnd 1), |
|
273 (rtac refl 1) |
|
274 ]); |
|
275 |
|
276 val Isfst = prove_goalw Sprod0.thy [Isfst_def] |
|
277 "[|~x=UU ;~y=UU |] ==> Isfst(Ispair(x,y)) = x" |
|
278 (fn prems => |
|
279 [ |
|
280 (cut_facts_tac prems 1), |
|
281 (rtac select_equality 1), |
|
282 (rtac conjI 1), |
|
283 (strip_tac 1), |
|
284 (res_inst_tac [("P","Ispair(x,y) = Ispair(UU,UU)")] notE 1), |
|
285 (etac defined_Ispair 1), |
|
286 (atac 1), |
|
287 (atac 1), |
|
288 (strip_tac 1), |
|
289 (rtac (inject_Ispair RS conjunct1) 1), |
|
290 (fast_tac HOL_cs 3), |
|
291 (fast_tac HOL_cs 1), |
|
292 (fast_tac HOL_cs 1), |
|
293 (fast_tac HOL_cs 1) |
|
294 ]); |
|
295 |
|
296 val Issnd = prove_goalw Sprod0.thy [Issnd_def] |
|
297 "[|~x=UU ;~y=UU |] ==> Issnd(Ispair(x,y)) = y" |
|
298 (fn prems => |
|
299 [ |
|
300 (cut_facts_tac prems 1), |
|
301 (rtac select_equality 1), |
|
302 (rtac conjI 1), |
|
303 (strip_tac 1), |
|
304 (res_inst_tac [("P","Ispair(x,y) = Ispair(UU,UU)")] notE 1), |
|
305 (etac defined_Ispair 1), |
|
306 (atac 1), |
|
307 (atac 1), |
|
308 (strip_tac 1), |
|
309 (rtac (inject_Ispair RS conjunct2) 1), |
|
310 (fast_tac HOL_cs 3), |
|
311 (fast_tac HOL_cs 1), |
|
312 (fast_tac HOL_cs 1), |
|
313 (fast_tac HOL_cs 1) |
|
314 ]); |
|
315 |
|
316 val Isfst2 = prove_goal Sprod0.thy "~y=UU ==>Isfst(Ispair(x,y))=x" |
|
317 (fn prems => |
|
318 [ |
|
319 (cut_facts_tac prems 1), |
|
320 (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1), |
|
321 (etac Isfst 1), |
|
322 (atac 1), |
|
323 (hyp_subst_tac 1), |
|
324 (rtac strict_Isfst1 1) |
|
325 ]); |
|
326 |
|
327 val Issnd2 = prove_goal Sprod0.thy "~x=UU ==>Issnd(Ispair(x,y))=y" |
|
328 (fn prems => |
|
329 [ |
|
330 (cut_facts_tac prems 1), |
|
331 (res_inst_tac [("Q","y=UU")] (excluded_middle RS disjE) 1), |
|
332 (etac Issnd 1), |
|
333 (atac 1), |
|
334 (hyp_subst_tac 1), |
|
335 (rtac strict_Issnd2 1) |
|
336 ]); |
|
337 |
|
338 |
|
339 (* ------------------------------------------------------------------------ *) |
|
340 (* instantiate the simplifier *) |
|
341 (* ------------------------------------------------------------------------ *) |
|
342 |
|
343 val Sprod_ss = |
|
344 HOL_ss |
|
345 addsimps [strict_Isfst1,strict_Isfst2,strict_Issnd1,strict_Issnd2, |
|
346 Isfst2,Issnd2]; |
|
347 |
|
348 |
|
349 val defined_IsfstIssnd = prove_goal Sprod0.thy |
|
350 "~p=Ispair(UU,UU) ==> ~Isfst(p)=UU & ~Issnd(p)=UU" |
|
351 (fn prems => |
|
352 [ |
|
353 (cut_facts_tac prems 1), |
|
354 (res_inst_tac [("p","p")] IsprodE 1), |
|
355 (contr_tac 1), |
|
356 (hyp_subst_tac 1), |
|
357 (rtac conjI 1), |
|
358 (asm_simp_tac Sprod_ss 1), |
|
359 (asm_simp_tac Sprod_ss 1) |
|
360 ]); |
|
361 |
|
362 |
|
363 (* ------------------------------------------------------------------------ *) |
|
364 (* Surjective pairing: equivalent to Exh_Sprod *) |
|
365 (* ------------------------------------------------------------------------ *) |
|
366 |
|
367 val surjective_pairing_Sprod = prove_goal Sprod0.thy |
|
368 "z = Ispair(Isfst(z))(Issnd(z))" |
|
369 (fn prems => |
|
370 [ |
|
371 (res_inst_tac [("z1","z")] (Exh_Sprod RS disjE) 1), |
|
372 (asm_simp_tac Sprod_ss 1), |
|
373 (etac exE 1), |
|
374 (etac exE 1), |
|
375 (asm_simp_tac Sprod_ss 1) |
|
376 ]); |
|
377 |
|
378 |
|
379 |
|
380 |
|
381 |
|
382 |
|
383 |
|
384 |
|
385 |
|
386 |
|
387 |
|
388 |
|
389 |