|
1 (* Title: HOLCF/sprod3.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for Sprod3.thy |
|
7 *) |
|
8 |
|
9 open Sprod3; |
|
10 |
|
11 (* ------------------------------------------------------------------------ *) |
|
12 (* continuity of Ispair, Isfst, Issnd *) |
|
13 (* ------------------------------------------------------------------------ *) |
|
14 |
|
15 val sprod3_lemma1 = prove_goal Sprod3.thy |
|
16 "[| is_chain(Y); x~= UU; lub(range(Y))~= UU |] ==>\ |
|
17 \ Ispair(lub(range(Y)),x) =\ |
|
18 \ Ispair(lub(range(%i. Isfst(Ispair(Y(i),x)))),\ |
|
19 \ lub(range(%i. Issnd(Ispair(Y(i),x)))))" |
|
20 (fn prems => |
|
21 [ |
|
22 (cut_facts_tac prems 1), |
|
23 (res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1), |
|
24 (rtac lub_equal 1), |
|
25 (atac 1), |
|
26 (rtac (monofun_Isfst RS ch2ch_monofun) 1), |
|
27 (rtac ch2ch_fun 1), |
|
28 (rtac (monofun_Ispair1 RS ch2ch_monofun) 1), |
|
29 (atac 1), |
|
30 (rtac allI 1), |
|
31 (asm_simp_tac Sprod_ss 1), |
|
32 (rtac sym 1), |
|
33 (rtac lub_chain_maxelem 1), |
|
34 (rtac (monofun_Issnd RS ch2ch_monofun) 1), |
|
35 (rtac ch2ch_fun 1), |
|
36 (rtac (monofun_Ispair1 RS ch2ch_monofun) 1), |
|
37 (atac 1), |
|
38 (res_inst_tac [("P","%j.~Y(j)=UU")] exE 1), |
|
39 (rtac (notall2ex RS iffD1) 1), |
|
40 (res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1), |
|
41 (atac 1), |
|
42 (rtac chain_UU_I_inverse 1), |
|
43 (atac 1), |
|
44 (rtac exI 1), |
|
45 (etac Issnd2 1), |
|
46 (rtac allI 1), |
|
47 (res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1), |
|
48 (asm_simp_tac Sprod_ss 1), |
|
49 (rtac refl_less 1), |
|
50 (res_inst_tac [("s","UU"),("t","Y(i)")] subst 1), |
|
51 (etac sym 1), |
|
52 (asm_simp_tac Sprod_ss 1), |
|
53 (rtac minimal 1) |
|
54 ]); |
|
55 |
|
56 |
|
57 val sprod3_lemma2 = prove_goal Sprod3.thy |
|
58 "[| is_chain(Y); ~ x = UU; lub(range(Y)) = UU |] ==>\ |
|
59 \ Ispair(lub(range(Y)),x) =\ |
|
60 \ Ispair(lub(range(%i. Isfst(Ispair(Y(i),x)))),\ |
|
61 \ lub(range(%i. Issnd(Ispair(Y(i),x)))))" |
|
62 (fn prems => |
|
63 [ |
|
64 (cut_facts_tac prems 1), |
|
65 (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1), |
|
66 (atac 1), |
|
67 (rtac trans 1), |
|
68 (rtac strict_Ispair1 1), |
|
69 (rtac (strict_Ispair RS sym) 1), |
|
70 (rtac disjI1 1), |
|
71 (rtac chain_UU_I_inverse 1), |
|
72 (rtac allI 1), |
|
73 (asm_simp_tac Sprod_ss 1), |
|
74 (etac (chain_UU_I RS spec) 1), |
|
75 (atac 1) |
|
76 ]); |
|
77 |
|
78 |
|
79 val sprod3_lemma3 = prove_goal Sprod3.thy |
|
80 "[| is_chain(Y); x = UU |] ==>\ |
|
81 \ Ispair(lub(range(Y)),x) =\ |
|
82 \ Ispair(lub(range(%i. Isfst(Ispair(Y(i),x)))),\ |
|
83 \ lub(range(%i. Issnd(Ispair(Y(i),x)))))" |
|
84 (fn prems => |
|
85 [ |
|
86 (cut_facts_tac prems 1), |
|
87 (res_inst_tac [("s","UU"),("t","x")] ssubst 1), |
|
88 (atac 1), |
|
89 (rtac trans 1), |
|
90 (rtac strict_Ispair2 1), |
|
91 (rtac (strict_Ispair RS sym) 1), |
|
92 (rtac disjI1 1), |
|
93 (rtac chain_UU_I_inverse 1), |
|
94 (rtac allI 1), |
|
95 (simp_tac Sprod_ss 1) |
|
96 ]); |
|
97 |
|
98 |
|
99 val contlub_Ispair1 = prove_goal Sprod3.thy "contlub(Ispair)" |
|
100 (fn prems => |
|
101 [ |
|
102 (rtac contlubI 1), |
|
103 (strip_tac 1), |
|
104 (rtac (expand_fun_eq RS iffD2) 1), |
|
105 (strip_tac 1), |
|
106 (rtac (lub_fun RS thelubI RS ssubst) 1), |
|
107 (etac (monofun_Ispair1 RS ch2ch_monofun) 1), |
|
108 (rtac trans 1), |
|
109 (rtac (thelub_sprod RS sym) 2), |
|
110 (rtac ch2ch_fun 2), |
|
111 (etac (monofun_Ispair1 RS ch2ch_monofun) 2), |
|
112 (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1), |
|
113 (res_inst_tac |
|
114 [("Q","lub(range(Y))=UU")] (excluded_middle RS disjE) 1), |
|
115 (etac sprod3_lemma1 1), |
|
116 (atac 1), |
|
117 (atac 1), |
|
118 (etac sprod3_lemma2 1), |
|
119 (atac 1), |
|
120 (atac 1), |
|
121 (etac sprod3_lemma3 1), |
|
122 (atac 1) |
|
123 ]); |
|
124 |
|
125 val sprod3_lemma4 = prove_goal Sprod3.thy |
|
126 "[| is_chain(Y); ~ x = UU; ~ lub(range(Y)) = UU |] ==>\ |
|
127 \ Ispair(x,lub(range(Y))) =\ |
|
128 \ Ispair(lub(range(%i. Isfst(Ispair(x,Y(i))))),\ |
|
129 \ lub(range(%i. Issnd(Ispair(x,Y(i))))))" |
|
130 (fn prems => |
|
131 [ |
|
132 (cut_facts_tac prems 1), |
|
133 (res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1), |
|
134 (rtac sym 1), |
|
135 (rtac lub_chain_maxelem 1), |
|
136 (rtac (monofun_Isfst RS ch2ch_monofun) 1), |
|
137 (rtac (monofun_Ispair2 RS ch2ch_monofun) 1), |
|
138 (atac 1), |
|
139 (res_inst_tac [("P","%j.~Y(j)=UU")] exE 1), |
|
140 (rtac (notall2ex RS iffD1) 1), |
|
141 (res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1), |
|
142 (atac 1), |
|
143 (rtac chain_UU_I_inverse 1), |
|
144 (atac 1), |
|
145 (rtac exI 1), |
|
146 (etac Isfst2 1), |
|
147 (rtac allI 1), |
|
148 (res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1), |
|
149 (asm_simp_tac Sprod_ss 1), |
|
150 (rtac refl_less 1), |
|
151 (res_inst_tac [("s","UU"),("t","Y(i)")] subst 1), |
|
152 (etac sym 1), |
|
153 (asm_simp_tac Sprod_ss 1), |
|
154 (rtac minimal 1), |
|
155 (rtac lub_equal 1), |
|
156 (atac 1), |
|
157 (rtac (monofun_Issnd RS ch2ch_monofun) 1), |
|
158 (rtac (monofun_Ispair2 RS ch2ch_monofun) 1), |
|
159 (atac 1), |
|
160 (rtac allI 1), |
|
161 (asm_simp_tac Sprod_ss 1) |
|
162 ]); |
|
163 |
|
164 val sprod3_lemma5 = prove_goal Sprod3.thy |
|
165 "[| is_chain(Y); ~ x = UU; lub(range(Y)) = UU |] ==>\ |
|
166 \ Ispair(x,lub(range(Y))) =\ |
|
167 \ Ispair(lub(range(%i. Isfst(Ispair(x,Y(i))))),\ |
|
168 \ lub(range(%i. Issnd(Ispair(x,Y(i))))))" |
|
169 (fn prems => |
|
170 [ |
|
171 (cut_facts_tac prems 1), |
|
172 (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1), |
|
173 (atac 1), |
|
174 (rtac trans 1), |
|
175 (rtac strict_Ispair2 1), |
|
176 (rtac (strict_Ispair RS sym) 1), |
|
177 (rtac disjI2 1), |
|
178 (rtac chain_UU_I_inverse 1), |
|
179 (rtac allI 1), |
|
180 (asm_simp_tac Sprod_ss 1), |
|
181 (etac (chain_UU_I RS spec) 1), |
|
182 (atac 1) |
|
183 ]); |
|
184 |
|
185 val sprod3_lemma6 = prove_goal Sprod3.thy |
|
186 "[| is_chain(Y); x = UU |] ==>\ |
|
187 \ Ispair(x,lub(range(Y))) =\ |
|
188 \ Ispair(lub(range(%i. Isfst(Ispair(x,Y(i))))),\ |
|
189 \ lub(range(%i. Issnd(Ispair(x,Y(i))))))" |
|
190 (fn prems => |
|
191 [ |
|
192 (cut_facts_tac prems 1), |
|
193 (res_inst_tac [("s","UU"),("t","x")] ssubst 1), |
|
194 (atac 1), |
|
195 (rtac trans 1), |
|
196 (rtac strict_Ispair1 1), |
|
197 (rtac (strict_Ispair RS sym) 1), |
|
198 (rtac disjI1 1), |
|
199 (rtac chain_UU_I_inverse 1), |
|
200 (rtac allI 1), |
|
201 (simp_tac Sprod_ss 1) |
|
202 ]); |
|
203 |
|
204 val contlub_Ispair2 = prove_goal Sprod3.thy "contlub(Ispair(x))" |
|
205 (fn prems => |
|
206 [ |
|
207 (rtac contlubI 1), |
|
208 (strip_tac 1), |
|
209 (rtac trans 1), |
|
210 (rtac (thelub_sprod RS sym) 2), |
|
211 (etac (monofun_Ispair2 RS ch2ch_monofun) 2), |
|
212 (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1), |
|
213 (res_inst_tac [("Q","lub(range(Y))=UU")] |
|
214 (excluded_middle RS disjE) 1), |
|
215 (etac sprod3_lemma4 1), |
|
216 (atac 1), |
|
217 (atac 1), |
|
218 (etac sprod3_lemma5 1), |
|
219 (atac 1), |
|
220 (atac 1), |
|
221 (etac sprod3_lemma6 1), |
|
222 (atac 1) |
|
223 ]); |
|
224 |
|
225 |
|
226 val contX_Ispair1 = prove_goal Sprod3.thy "contX(Ispair)" |
|
227 (fn prems => |
|
228 [ |
|
229 (rtac monocontlub2contX 1), |
|
230 (rtac monofun_Ispair1 1), |
|
231 (rtac contlub_Ispair1 1) |
|
232 ]); |
|
233 |
|
234 |
|
235 val contX_Ispair2 = prove_goal Sprod3.thy "contX(Ispair(x))" |
|
236 (fn prems => |
|
237 [ |
|
238 (rtac monocontlub2contX 1), |
|
239 (rtac monofun_Ispair2 1), |
|
240 (rtac contlub_Ispair2 1) |
|
241 ]); |
|
242 |
|
243 val contlub_Isfst = prove_goal Sprod3.thy "contlub(Isfst)" |
|
244 (fn prems => |
|
245 [ |
|
246 (rtac contlubI 1), |
|
247 (strip_tac 1), |
|
248 (rtac (lub_sprod RS thelubI RS ssubst) 1), |
|
249 (atac 1), |
|
250 (res_inst_tac [("Q","lub(range(%i. Issnd(Y(i))))=UU")] |
|
251 (excluded_middle RS disjE) 1), |
|
252 (asm_simp_tac Sprod_ss 1), |
|
253 (res_inst_tac [("s","UU"),("t","lub(range(%i. Issnd(Y(i))))")] |
|
254 ssubst 1), |
|
255 (atac 1), |
|
256 (rtac trans 1), |
|
257 (asm_simp_tac Sprod_ss 1), |
|
258 (rtac sym 1), |
|
259 (rtac chain_UU_I_inverse 1), |
|
260 (rtac allI 1), |
|
261 (rtac strict_Isfst 1), |
|
262 (rtac swap 1), |
|
263 (etac (defined_IsfstIssnd RS conjunct2) 2), |
|
264 (rtac notnotI 1), |
|
265 (rtac (chain_UU_I RS spec) 1), |
|
266 (rtac (monofun_Issnd RS ch2ch_monofun) 1), |
|
267 (atac 1), |
|
268 (atac 1) |
|
269 ]); |
|
270 |
|
271 |
|
272 val contlub_Issnd = prove_goal Sprod3.thy "contlub(Issnd)" |
|
273 (fn prems => |
|
274 [ |
|
275 (rtac contlubI 1), |
|
276 (strip_tac 1), |
|
277 (rtac (lub_sprod RS thelubI RS ssubst) 1), |
|
278 (atac 1), |
|
279 (res_inst_tac [("Q","lub(range(%i. Isfst(Y(i))))=UU")] |
|
280 (excluded_middle RS disjE) 1), |
|
281 (asm_simp_tac Sprod_ss 1), |
|
282 (res_inst_tac [("s","UU"),("t","lub(range(%i. Isfst(Y(i))))")] |
|
283 ssubst 1), |
|
284 (atac 1), |
|
285 (asm_simp_tac Sprod_ss 1), |
|
286 (rtac sym 1), |
|
287 (rtac chain_UU_I_inverse 1), |
|
288 (rtac allI 1), |
|
289 (rtac strict_Issnd 1), |
|
290 (rtac swap 1), |
|
291 (etac (defined_IsfstIssnd RS conjunct1) 2), |
|
292 (rtac notnotI 1), |
|
293 (rtac (chain_UU_I RS spec) 1), |
|
294 (rtac (monofun_Isfst RS ch2ch_monofun) 1), |
|
295 (atac 1), |
|
296 (atac 1) |
|
297 ]); |
|
298 |
|
299 |
|
300 val contX_Isfst = prove_goal Sprod3.thy "contX(Isfst)" |
|
301 (fn prems => |
|
302 [ |
|
303 (rtac monocontlub2contX 1), |
|
304 (rtac monofun_Isfst 1), |
|
305 (rtac contlub_Isfst 1) |
|
306 ]); |
|
307 |
|
308 val contX_Issnd = prove_goal Sprod3.thy "contX(Issnd)" |
|
309 (fn prems => |
|
310 [ |
|
311 (rtac monocontlub2contX 1), |
|
312 (rtac monofun_Issnd 1), |
|
313 (rtac contlub_Issnd 1) |
|
314 ]); |
|
315 |
|
316 (* |
|
317 -------------------------------------------------------------------------- |
|
318 more lemmas for Sprod3.thy |
|
319 |
|
320 -------------------------------------------------------------------------- |
|
321 *) |
|
322 |
|
323 val spair_eq = prove_goal Sprod3.thy "[|x1=x2;y1=y2|] ==> x1##y1 = x2##y2" |
|
324 (fn prems => |
|
325 [ |
|
326 (cut_facts_tac prems 1), |
|
327 (fast_tac HOL_cs 1) |
|
328 ]); |
|
329 |
|
330 (* ------------------------------------------------------------------------ *) |
|
331 (* convert all lemmas to the continuous versions *) |
|
332 (* ------------------------------------------------------------------------ *) |
|
333 |
|
334 val beta_cfun_sprod = prove_goalw Sprod3.thy [spair_def] |
|
335 "(LAM x y.Ispair(x,y))[a][b] = Ispair(a,b)" |
|
336 (fn prems => |
|
337 [ |
|
338 (rtac (beta_cfun RS ssubst) 1), |
|
339 (contX_tac 1), |
|
340 (rtac contX_Ispair2 1), |
|
341 (rtac contX2contX_CF1L 1), |
|
342 (rtac contX_Ispair1 1), |
|
343 (rtac (beta_cfun RS ssubst) 1), |
|
344 (rtac contX_Ispair2 1), |
|
345 (rtac refl 1) |
|
346 ]); |
|
347 |
|
348 val inject_spair = prove_goalw Sprod3.thy [spair_def] |
|
349 "[|~aa=UU ; ~ba=UU ; (a##b)=(aa##ba) |] ==> a=aa & b=ba" |
|
350 (fn prems => |
|
351 [ |
|
352 (cut_facts_tac prems 1), |
|
353 (etac inject_Ispair 1), |
|
354 (atac 1), |
|
355 (etac box_equals 1), |
|
356 (rtac beta_cfun_sprod 1), |
|
357 (rtac beta_cfun_sprod 1) |
|
358 ]); |
|
359 |
|
360 val inst_sprod_pcpo2 = prove_goalw Sprod3.thy [spair_def] "UU = (UU##UU)" |
|
361 (fn prems => |
|
362 [ |
|
363 (rtac sym 1), |
|
364 (rtac trans 1), |
|
365 (rtac beta_cfun_sprod 1), |
|
366 (rtac sym 1), |
|
367 (rtac inst_sprod_pcpo 1) |
|
368 ]); |
|
369 |
|
370 val strict_spair = prove_goalw Sprod3.thy [spair_def] |
|
371 "(a=UU | b=UU) ==> (a##b)=UU" |
|
372 (fn prems => |
|
373 [ |
|
374 (cut_facts_tac prems 1), |
|
375 (rtac trans 1), |
|
376 (rtac beta_cfun_sprod 1), |
|
377 (rtac trans 1), |
|
378 (rtac (inst_sprod_pcpo RS sym) 2), |
|
379 (etac strict_Ispair 1) |
|
380 ]); |
|
381 |
|
382 val strict_spair1 = prove_goalw Sprod3.thy [spair_def] "(UU##b) = UU" |
|
383 (fn prems => |
|
384 [ |
|
385 (rtac (beta_cfun_sprod RS ssubst) 1), |
|
386 (rtac trans 1), |
|
387 (rtac (inst_sprod_pcpo RS sym) 2), |
|
388 (rtac strict_Ispair1 1) |
|
389 ]); |
|
390 |
|
391 val strict_spair2 = prove_goalw Sprod3.thy [spair_def] "(a##UU) = UU" |
|
392 (fn prems => |
|
393 [ |
|
394 (rtac (beta_cfun_sprod RS ssubst) 1), |
|
395 (rtac trans 1), |
|
396 (rtac (inst_sprod_pcpo RS sym) 2), |
|
397 (rtac strict_Ispair2 1) |
|
398 ]); |
|
399 |
|
400 val strict_spair_rev = prove_goalw Sprod3.thy [spair_def] |
|
401 "~(x##y)=UU ==> ~x=UU & ~y=UU" |
|
402 (fn prems => |
|
403 [ |
|
404 (cut_facts_tac prems 1), |
|
405 (rtac strict_Ispair_rev 1), |
|
406 (rtac (beta_cfun_sprod RS subst) 1), |
|
407 (rtac (inst_sprod_pcpo RS subst) 1), |
|
408 (atac 1) |
|
409 ]); |
|
410 |
|
411 val defined_spair_rev = prove_goalw Sprod3.thy [spair_def] |
|
412 "(a##b) = UU ==> (a = UU | b = UU)" |
|
413 (fn prems => |
|
414 [ |
|
415 (cut_facts_tac prems 1), |
|
416 (rtac defined_Ispair_rev 1), |
|
417 (rtac (beta_cfun_sprod RS subst) 1), |
|
418 (rtac (inst_sprod_pcpo RS subst) 1), |
|
419 (atac 1) |
|
420 ]); |
|
421 |
|
422 val defined_spair = prove_goalw Sprod3.thy [spair_def] |
|
423 "[|~a=UU; ~b=UU|] ==> ~(a##b) = UU" |
|
424 (fn prems => |
|
425 [ |
|
426 (cut_facts_tac prems 1), |
|
427 (rtac (beta_cfun_sprod RS ssubst) 1), |
|
428 (rtac (inst_sprod_pcpo RS ssubst) 1), |
|
429 (etac defined_Ispair 1), |
|
430 (atac 1) |
|
431 ]); |
|
432 |
|
433 val Exh_Sprod2 = prove_goalw Sprod3.thy [spair_def] |
|
434 "z=UU | (? a b. z=(a##b) & ~a=UU & ~b=UU)" |
|
435 (fn prems => |
|
436 [ |
|
437 (rtac (Exh_Sprod RS disjE) 1), |
|
438 (rtac disjI1 1), |
|
439 (rtac (inst_sprod_pcpo RS ssubst) 1), |
|
440 (atac 1), |
|
441 (rtac disjI2 1), |
|
442 (etac exE 1), |
|
443 (etac exE 1), |
|
444 (rtac exI 1), |
|
445 (rtac exI 1), |
|
446 (rtac conjI 1), |
|
447 (rtac (beta_cfun_sprod RS ssubst) 1), |
|
448 (fast_tac HOL_cs 1), |
|
449 (fast_tac HOL_cs 1) |
|
450 ]); |
|
451 |
|
452 |
|
453 val sprodE = prove_goalw Sprod3.thy [spair_def] |
|
454 "[|p=UU ==> Q;!!x y. [|p=(x##y);~x=UU ; ~y=UU|] ==> Q|] ==> Q" |
|
455 (fn prems => |
|
456 [ |
|
457 (rtac IsprodE 1), |
|
458 (resolve_tac prems 1), |
|
459 (rtac (inst_sprod_pcpo RS ssubst) 1), |
|
460 (atac 1), |
|
461 (resolve_tac prems 1), |
|
462 (atac 2), |
|
463 (atac 2), |
|
464 (rtac (beta_cfun_sprod RS ssubst) 1), |
|
465 (atac 1) |
|
466 ]); |
|
467 |
|
468 |
|
469 val strict_sfst = prove_goalw Sprod3.thy [sfst_def] |
|
470 "p=UU==>sfst[p]=UU" |
|
471 (fn prems => |
|
472 [ |
|
473 (cut_facts_tac prems 1), |
|
474 (rtac (beta_cfun RS ssubst) 1), |
|
475 (rtac contX_Isfst 1), |
|
476 (rtac strict_Isfst 1), |
|
477 (rtac (inst_sprod_pcpo RS subst) 1), |
|
478 (atac 1) |
|
479 ]); |
|
480 |
|
481 val strict_sfst1 = prove_goalw Sprod3.thy [sfst_def,spair_def] |
|
482 "sfst[UU##y] = UU" |
|
483 (fn prems => |
|
484 [ |
|
485 (rtac (beta_cfun_sprod RS ssubst) 1), |
|
486 (rtac (beta_cfun RS ssubst) 1), |
|
487 (rtac contX_Isfst 1), |
|
488 (rtac strict_Isfst1 1) |
|
489 ]); |
|
490 |
|
491 val strict_sfst2 = prove_goalw Sprod3.thy [sfst_def,spair_def] |
|
492 "sfst[x##UU] = UU" |
|
493 (fn prems => |
|
494 [ |
|
495 (rtac (beta_cfun_sprod RS ssubst) 1), |
|
496 (rtac (beta_cfun RS ssubst) 1), |
|
497 (rtac contX_Isfst 1), |
|
498 (rtac strict_Isfst2 1) |
|
499 ]); |
|
500 |
|
501 val strict_ssnd = prove_goalw Sprod3.thy [ssnd_def] |
|
502 "p=UU==>ssnd[p]=UU" |
|
503 (fn prems => |
|
504 [ |
|
505 (cut_facts_tac prems 1), |
|
506 (rtac (beta_cfun RS ssubst) 1), |
|
507 (rtac contX_Issnd 1), |
|
508 (rtac strict_Issnd 1), |
|
509 (rtac (inst_sprod_pcpo RS subst) 1), |
|
510 (atac 1) |
|
511 ]); |
|
512 |
|
513 val strict_ssnd1 = prove_goalw Sprod3.thy [ssnd_def,spair_def] |
|
514 "ssnd[UU##y] = UU" |
|
515 (fn prems => |
|
516 [ |
|
517 (rtac (beta_cfun_sprod RS ssubst) 1), |
|
518 (rtac (beta_cfun RS ssubst) 1), |
|
519 (rtac contX_Issnd 1), |
|
520 (rtac strict_Issnd1 1) |
|
521 ]); |
|
522 |
|
523 val strict_ssnd2 = prove_goalw Sprod3.thy [ssnd_def,spair_def] |
|
524 "ssnd[x##UU] = UU" |
|
525 (fn prems => |
|
526 [ |
|
527 (rtac (beta_cfun_sprod RS ssubst) 1), |
|
528 (rtac (beta_cfun RS ssubst) 1), |
|
529 (rtac contX_Issnd 1), |
|
530 (rtac strict_Issnd2 1) |
|
531 ]); |
|
532 |
|
533 val sfst2 = prove_goalw Sprod3.thy [sfst_def,spair_def] |
|
534 "~y=UU ==>sfst[x##y]=x" |
|
535 (fn prems => |
|
536 [ |
|
537 (cut_facts_tac prems 1), |
|
538 (rtac (beta_cfun_sprod RS ssubst) 1), |
|
539 (rtac (beta_cfun RS ssubst) 1), |
|
540 (rtac contX_Isfst 1), |
|
541 (etac Isfst2 1) |
|
542 ]); |
|
543 |
|
544 val ssnd2 = prove_goalw Sprod3.thy [ssnd_def,spair_def] |
|
545 "~x=UU ==>ssnd[x##y]=y" |
|
546 (fn prems => |
|
547 [ |
|
548 (cut_facts_tac prems 1), |
|
549 (rtac (beta_cfun_sprod RS ssubst) 1), |
|
550 (rtac (beta_cfun RS ssubst) 1), |
|
551 (rtac contX_Issnd 1), |
|
552 (etac Issnd2 1) |
|
553 ]); |
|
554 |
|
555 |
|
556 val defined_sfstssnd = prove_goalw Sprod3.thy [sfst_def,ssnd_def,spair_def] |
|
557 "~p=UU ==> ~sfst[p]=UU & ~ssnd[p]=UU" |
|
558 (fn prems => |
|
559 [ |
|
560 (cut_facts_tac prems 1), |
|
561 (rtac (beta_cfun RS ssubst) 1), |
|
562 (rtac contX_Issnd 1), |
|
563 (rtac (beta_cfun RS ssubst) 1), |
|
564 (rtac contX_Isfst 1), |
|
565 (rtac defined_IsfstIssnd 1), |
|
566 (rtac (inst_sprod_pcpo RS subst) 1), |
|
567 (atac 1) |
|
568 ]); |
|
569 |
|
570 |
|
571 val surjective_pairing_Sprod2 = prove_goalw Sprod3.thy |
|
572 [sfst_def,ssnd_def,spair_def] "(sfst[p] ## ssnd[p]) = p" |
|
573 (fn prems => |
|
574 [ |
|
575 (rtac (beta_cfun_sprod RS ssubst) 1), |
|
576 (rtac (beta_cfun RS ssubst) 1), |
|
577 (rtac contX_Issnd 1), |
|
578 (rtac (beta_cfun RS ssubst) 1), |
|
579 (rtac contX_Isfst 1), |
|
580 (rtac (surjective_pairing_Sprod RS sym) 1) |
|
581 ]); |
|
582 |
|
583 |
|
584 val less_sprod5b = prove_goalw Sprod3.thy [sfst_def,ssnd_def,spair_def] |
|
585 "~p1=UU ==> (p1<<p2) = (sfst[p1]<<sfst[p2] & ssnd[p1]<<ssnd[p2])" |
|
586 (fn prems => |
|
587 [ |
|
588 (cut_facts_tac prems 1), |
|
589 (rtac (beta_cfun RS ssubst) 1), |
|
590 (rtac contX_Issnd 1), |
|
591 (rtac (beta_cfun RS ssubst) 1), |
|
592 (rtac contX_Issnd 1), |
|
593 (rtac (beta_cfun RS ssubst) 1), |
|
594 (rtac contX_Isfst 1), |
|
595 (rtac (beta_cfun RS ssubst) 1), |
|
596 (rtac contX_Isfst 1), |
|
597 (rtac less_sprod3b 1), |
|
598 (rtac (inst_sprod_pcpo RS subst) 1), |
|
599 (atac 1) |
|
600 ]); |
|
601 |
|
602 |
|
603 val less_sprod5c = prove_goalw Sprod3.thy [sfst_def,ssnd_def,spair_def] |
|
604 "[|xa##ya<<x##y;~xa=UU;~ya=UU;~x=UU;~y=UU|] ==>xa<<x & ya << y" |
|
605 (fn prems => |
|
606 [ |
|
607 (cut_facts_tac prems 1), |
|
608 (rtac less_sprod4c 1), |
|
609 (REPEAT (atac 2)), |
|
610 (rtac (beta_cfun_sprod RS subst) 1), |
|
611 (rtac (beta_cfun_sprod RS subst) 1), |
|
612 (atac 1) |
|
613 ]); |
|
614 |
|
615 val lub_sprod2 = prove_goalw Sprod3.thy [sfst_def,ssnd_def,spair_def] |
|
616 "[|is_chain(S)|] ==> range(S) <<| \ |
|
617 \ (lub(range(%i.sfst[S(i)])) ## lub(range(%i.ssnd[S(i)])))" |
|
618 (fn prems => |
|
619 [ |
|
620 (cut_facts_tac prems 1), |
|
621 (rtac (beta_cfun_sprod RS ssubst) 1), |
|
622 (rtac (beta_cfun RS ext RS ssubst) 1), |
|
623 (rtac contX_Issnd 1), |
|
624 (rtac (beta_cfun RS ext RS ssubst) 1), |
|
625 (rtac contX_Isfst 1), |
|
626 (rtac lub_sprod 1), |
|
627 (resolve_tac prems 1) |
|
628 ]); |
|
629 |
|
630 |
|
631 val thelub_sprod2 = (lub_sprod2 RS thelubI); |
|
632 (* is_chain(?S1) ==> lub(range(?S1)) = *) |
|
633 (* (lub(range(%i. sfst[?S1(i)]))## lub(range(%i. ssnd[?S1(i)]))) *) |
|
634 |
|
635 |
|
636 |
|
637 val ssplit1 = prove_goalw Sprod3.thy [ssplit_def] |
|
638 "ssplit[f][UU]=UU" |
|
639 (fn prems => |
|
640 [ |
|
641 (rtac (beta_cfun RS ssubst) 1), |
|
642 (contX_tacR 1), |
|
643 (rtac (strictify1 RS ssubst) 1), |
|
644 (rtac refl 1) |
|
645 ]); |
|
646 |
|
647 val ssplit2 = prove_goalw Sprod3.thy [ssplit_def] |
|
648 "[|~x=UU;~y=UU|] ==> ssplit[f][x##y]=f[x][y]" |
|
649 (fn prems => |
|
650 [ |
|
651 (rtac (beta_cfun RS ssubst) 1), |
|
652 (contX_tacR 1), |
|
653 (rtac (strictify2 RS ssubst) 1), |
|
654 (rtac defined_spair 1), |
|
655 (resolve_tac prems 1), |
|
656 (resolve_tac prems 1), |
|
657 (rtac (beta_cfun RS ssubst) 1), |
|
658 (contX_tacR 1), |
|
659 (rtac (sfst2 RS ssubst) 1), |
|
660 (resolve_tac prems 1), |
|
661 (rtac (ssnd2 RS ssubst) 1), |
|
662 (resolve_tac prems 1), |
|
663 (rtac refl 1) |
|
664 ]); |
|
665 |
|
666 |
|
667 val ssplit3 = prove_goalw Sprod3.thy [ssplit_def] |
|
668 "ssplit[spair][z]=z" |
|
669 (fn prems => |
|
670 [ |
|
671 (rtac (beta_cfun RS ssubst) 1), |
|
672 (contX_tacR 1), |
|
673 (res_inst_tac [("Q","z=UU")] classical2 1), |
|
674 (hyp_subst_tac 1), |
|
675 (rtac strictify1 1), |
|
676 (rtac trans 1), |
|
677 (rtac strictify2 1), |
|
678 (atac 1), |
|
679 (rtac (beta_cfun RS ssubst) 1), |
|
680 (contX_tacR 1), |
|
681 (rtac surjective_pairing_Sprod2 1) |
|
682 ]); |
|
683 |
|
684 |
|
685 (* ------------------------------------------------------------------------ *) |
|
686 (* install simplifier for Sprod *) |
|
687 (* ------------------------------------------------------------------------ *) |
|
688 |
|
689 val Sprod_rews = [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2, |
|
690 strict_ssnd1,strict_ssnd2,sfst2,ssnd2, |
|
691 ssplit1,ssplit2]; |
|
692 |
|
693 val Sprod_ss = Cfun_ss addsimps Sprod_rews; |
|
694 |
|
695 |