21 translations |
26 translations |
22 "(:x, y, z:)" == "(:x, (:y, z:):)" |
27 "(:x, y, z:)" == "(:x, (:y, z:):)" |
23 "(:x, y:)" == "spair$x$y" |
28 "(:x, y:)" == "spair$x$y" |
24 |
29 |
25 defs |
30 defs |
26 spair_def "spair == (LAM x y. Ispair x y)" |
31 spair_def: "spair == (LAM x y. Ispair x y)" |
27 sfst_def "sfst == (LAM p. Isfst p)" |
32 sfst_def: "sfst == (LAM p. Isfst p)" |
28 ssnd_def "ssnd == (LAM p. Issnd p)" |
33 ssnd_def: "ssnd == (LAM p. Issnd p)" |
29 ssplit_def "ssplit == (LAM f. strictify$(LAM p. f$(sfst$p)$(ssnd$p)))" |
34 ssplit_def: "ssplit == (LAM f. strictify$(LAM p. f$(sfst$p)$(ssnd$p)))" |
|
35 |
|
36 (* Title: HOLCF/Sprod3 |
|
37 ID: $Id$ |
|
38 Author: Franz Regensburger |
|
39 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
40 |
|
41 Class instance of ** for class pcpo |
|
42 *) |
|
43 |
|
44 (* for compatibility with old HOLCF-Version *) |
|
45 lemma inst_sprod_pcpo: "UU = Ispair UU UU" |
|
46 apply (simp add: UU_def UU_sprod_def) |
|
47 done |
|
48 |
|
49 declare inst_sprod_pcpo [symmetric, simp] |
|
50 |
|
51 (* ------------------------------------------------------------------------ *) |
|
52 (* continuity of Ispair, Isfst, Issnd *) |
|
53 (* ------------------------------------------------------------------------ *) |
|
54 |
|
55 lemma sprod3_lemma1: |
|
56 "[| chain(Y); x~= UU; lub(range(Y))~= UU |] ==> |
|
57 Ispair (lub(range Y)) x = |
|
58 Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) |
|
59 (lub(range(%i. Issnd(Ispair(Y i) x))))" |
|
60 apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong]) |
|
61 apply (rule lub_equal) |
|
62 apply assumption |
|
63 apply (rule monofun_Isfst [THEN ch2ch_monofun]) |
|
64 apply (rule ch2ch_fun) |
|
65 apply (rule monofun_Ispair1 [THEN ch2ch_monofun]) |
|
66 apply assumption |
|
67 apply (rule allI) |
|
68 apply (simp (no_asm_simp)) |
|
69 apply (rule sym) |
|
70 apply (drule chain_UU_I_inverse2) |
|
71 apply (erule exE) |
|
72 apply (rule lub_chain_maxelem) |
|
73 apply (erule Issnd2) |
|
74 apply (rule allI) |
|
75 apply (rename_tac "j") |
|
76 apply (case_tac "Y (j) =UU") |
|
77 apply auto |
|
78 done |
|
79 |
|
80 lemma sprod3_lemma2: |
|
81 "[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==> |
|
82 Ispair (lub(range Y)) x = |
|
83 Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) |
|
84 (lub(range(%i. Issnd(Ispair(Y i) x))))" |
|
85 apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst) |
|
86 apply assumption |
|
87 apply (rule trans) |
|
88 apply (rule strict_Ispair1) |
|
89 apply (rule strict_Ispair [symmetric]) |
|
90 apply (rule disjI1) |
|
91 apply (rule chain_UU_I_inverse) |
|
92 apply auto |
|
93 apply (erule chain_UU_I [THEN spec]) |
|
94 apply assumption |
|
95 done |
|
96 |
|
97 |
|
98 lemma sprod3_lemma3: |
|
99 "[| chain(Y); x = UU |] ==> |
|
100 Ispair (lub(range Y)) x = |
|
101 Ispair (lub(range(%i. Isfst(Ispair (Y i) x)))) |
|
102 (lub(range(%i. Issnd(Ispair (Y i) x))))" |
|
103 apply (erule ssubst) |
|
104 apply (rule trans) |
|
105 apply (rule strict_Ispair2) |
|
106 apply (rule strict_Ispair [symmetric]) |
|
107 apply (rule disjI1) |
|
108 apply (rule chain_UU_I_inverse) |
|
109 apply (rule allI) |
|
110 apply (simp add: Sprod0_ss) |
|
111 done |
|
112 |
|
113 lemma contlub_Ispair1: "contlub(Ispair)" |
|
114 apply (rule contlubI) |
|
115 apply (intro strip) |
|
116 apply (rule expand_fun_eq [THEN iffD2]) |
|
117 apply (intro strip) |
|
118 apply (subst lub_fun [THEN thelubI]) |
|
119 apply (erule monofun_Ispair1 [THEN ch2ch_monofun]) |
|
120 apply (rule trans) |
|
121 apply (rule_tac [2] thelub_sprod [symmetric]) |
|
122 apply (rule_tac [2] ch2ch_fun) |
|
123 apply (erule_tac [2] monofun_Ispair1 [THEN ch2ch_monofun]) |
|
124 apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE]) |
|
125 apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE]) |
|
126 apply (erule sprod3_lemma1) |
|
127 apply assumption |
|
128 apply assumption |
|
129 apply (erule sprod3_lemma2) |
|
130 apply assumption |
|
131 apply assumption |
|
132 apply (erule sprod3_lemma3) |
|
133 apply assumption |
|
134 done |
|
135 |
|
136 lemma sprod3_lemma4: |
|
137 "[| chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==> |
|
138 Ispair x (lub(range Y)) = |
|
139 Ispair (lub(range(%i. Isfst (Ispair x (Y i))))) |
|
140 (lub(range(%i. Issnd (Ispair x (Y i)))))" |
|
141 apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong]) |
|
142 apply (rule sym) |
|
143 apply (drule chain_UU_I_inverse2) |
|
144 apply (erule exE) |
|
145 apply (rule lub_chain_maxelem) |
|
146 apply (erule Isfst2) |
|
147 apply (rule allI) |
|
148 apply (rename_tac "j") |
|
149 apply (case_tac "Y (j) =UU") |
|
150 apply auto |
|
151 done |
|
152 |
|
153 lemma sprod3_lemma5: |
|
154 "[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==> |
|
155 Ispair x (lub(range Y)) = |
|
156 Ispair (lub(range(%i. Isfst(Ispair x (Y i))))) |
|
157 (lub(range(%i. Issnd(Ispair x (Y i)))))" |
|
158 apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst) |
|
159 apply assumption |
|
160 apply (rule trans) |
|
161 apply (rule strict_Ispair2) |
|
162 apply (rule strict_Ispair [symmetric]) |
|
163 apply (rule disjI2) |
|
164 apply (rule chain_UU_I_inverse) |
|
165 apply (rule allI) |
|
166 apply (simp add: Sprod0_ss) |
|
167 apply (erule chain_UU_I [THEN spec]) |
|
168 apply assumption |
|
169 done |
|
170 |
|
171 lemma sprod3_lemma6: |
|
172 "[| chain(Y); x = UU |] ==> |
|
173 Ispair x (lub(range Y)) = |
|
174 Ispair (lub(range(%i. Isfst (Ispair x (Y i))))) |
|
175 (lub(range(%i. Issnd (Ispair x (Y i)))))" |
|
176 apply (rule_tac s = "UU" and t = "x" in ssubst) |
|
177 apply assumption |
|
178 apply (rule trans) |
|
179 apply (rule strict_Ispair1) |
|
180 apply (rule strict_Ispair [symmetric]) |
|
181 apply (rule disjI1) |
|
182 apply (rule chain_UU_I_inverse) |
|
183 apply (rule allI) |
|
184 apply (simp add: Sprod0_ss) |
|
185 done |
|
186 |
|
187 lemma contlub_Ispair2: "contlub(Ispair(x))" |
|
188 apply (rule contlubI) |
|
189 apply (intro strip) |
|
190 apply (rule trans) |
|
191 apply (rule_tac [2] thelub_sprod [symmetric]) |
|
192 apply (erule_tac [2] monofun_Ispair2 [THEN ch2ch_monofun]) |
|
193 apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE]) |
|
194 apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE]) |
|
195 apply (erule sprod3_lemma4) |
|
196 apply assumption |
|
197 apply assumption |
|
198 apply (erule sprod3_lemma5) |
|
199 apply assumption |
|
200 apply assumption |
|
201 apply (erule sprod3_lemma6) |
|
202 apply assumption |
|
203 done |
|
204 |
|
205 lemma cont_Ispair1: "cont(Ispair)" |
|
206 apply (rule monocontlub2cont) |
|
207 apply (rule monofun_Ispair1) |
|
208 apply (rule contlub_Ispair1) |
|
209 done |
|
210 |
|
211 |
|
212 lemma cont_Ispair2: "cont(Ispair(x))" |
|
213 apply (rule monocontlub2cont) |
|
214 apply (rule monofun_Ispair2) |
|
215 apply (rule contlub_Ispair2) |
|
216 done |
|
217 |
|
218 lemma contlub_Isfst: "contlub(Isfst)" |
|
219 apply (rule contlubI) |
|
220 apply (intro strip) |
|
221 apply (subst lub_sprod [THEN thelubI]) |
|
222 apply assumption |
|
223 apply (rule_tac Q = "lub (range (%i. Issnd (Y (i))))=UU" in excluded_middle [THEN disjE]) |
|
224 apply (simp add: Sprod0_ss) |
|
225 apply (rule_tac s = "UU" and t = "lub (range (%i. Issnd (Y (i))))" in ssubst) |
|
226 apply assumption |
|
227 apply (rule trans) |
|
228 apply (simp add: Sprod0_ss) |
|
229 apply (rule sym) |
|
230 apply (rule chain_UU_I_inverse) |
|
231 apply (rule allI) |
|
232 apply (rule strict_Isfst) |
|
233 apply (rule contrapos_np) |
|
234 apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct2]) |
|
235 apply (fast dest!: monofun_Issnd [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec]) |
|
236 done |
|
237 |
|
238 lemma contlub_Issnd: "contlub(Issnd)" |
|
239 apply (rule contlubI) |
|
240 apply (intro strip) |
|
241 apply (subst lub_sprod [THEN thelubI]) |
|
242 apply assumption |
|
243 apply (rule_tac Q = "lub (range (%i. Isfst (Y (i))))=UU" in excluded_middle [THEN disjE]) |
|
244 apply (simp add: Sprod0_ss) |
|
245 apply (rule_tac s = "UU" and t = "lub (range (%i. Isfst (Y (i))))" in ssubst) |
|
246 apply assumption |
|
247 apply (simp add: Sprod0_ss) |
|
248 apply (rule sym) |
|
249 apply (rule chain_UU_I_inverse) |
|
250 apply (rule allI) |
|
251 apply (rule strict_Issnd) |
|
252 apply (rule contrapos_np) |
|
253 apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct1]) |
|
254 apply (fast dest!: monofun_Isfst [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec]) |
|
255 done |
|
256 |
|
257 lemma cont_Isfst: "cont(Isfst)" |
|
258 apply (rule monocontlub2cont) |
|
259 apply (rule monofun_Isfst) |
|
260 apply (rule contlub_Isfst) |
|
261 done |
|
262 |
|
263 lemma cont_Issnd: "cont(Issnd)" |
|
264 apply (rule monocontlub2cont) |
|
265 apply (rule monofun_Issnd) |
|
266 apply (rule contlub_Issnd) |
|
267 done |
|
268 |
|
269 lemma spair_eq: "[|x1=x2;y1=y2|] ==> (:x1,y1:) = (:x2,y2:)" |
|
270 apply fast |
|
271 done |
|
272 |
|
273 (* ------------------------------------------------------------------------ *) |
|
274 (* convert all lemmas to the continuous versions *) |
|
275 (* ------------------------------------------------------------------------ *) |
|
276 |
|
277 lemma beta_cfun_sprod: |
|
278 "(LAM x y. Ispair x y)$a$b = Ispair a b" |
|
279 apply (subst beta_cfun) |
|
280 apply (simp (no_asm) add: cont_Ispair2 cont_Ispair1 cont2cont_CF1L) |
|
281 apply (subst beta_cfun) |
|
282 apply (rule cont_Ispair2) |
|
283 apply (rule refl) |
|
284 done |
|
285 |
|
286 declare beta_cfun_sprod [simp] |
|
287 |
|
288 lemma inject_spair: |
|
289 "[| aa~=UU ; ba~=UU ; (:a,b:)=(:aa,ba:) |] ==> a=aa & b=ba" |
|
290 apply (unfold spair_def) |
|
291 apply (erule inject_Ispair) |
|
292 apply assumption |
|
293 apply (erule box_equals) |
|
294 apply (rule beta_cfun_sprod) |
|
295 apply (rule beta_cfun_sprod) |
|
296 done |
|
297 |
|
298 lemma inst_sprod_pcpo2: "UU = (:UU,UU:)" |
|
299 apply (unfold spair_def) |
|
300 apply (rule sym) |
|
301 apply (rule trans) |
|
302 apply (rule beta_cfun_sprod) |
|
303 apply (rule sym) |
|
304 apply (rule inst_sprod_pcpo) |
|
305 done |
|
306 |
|
307 lemma strict_spair: |
|
308 "(a=UU | b=UU) ==> (:a,b:)=UU" |
|
309 apply (unfold spair_def) |
|
310 apply (rule trans) |
|
311 apply (rule beta_cfun_sprod) |
|
312 apply (rule trans) |
|
313 apply (rule_tac [2] inst_sprod_pcpo [symmetric]) |
|
314 apply (erule strict_Ispair) |
|
315 done |
|
316 |
|
317 lemma strict_spair1: "(:UU,b:) = UU" |
|
318 apply (unfold spair_def) |
|
319 apply (subst beta_cfun_sprod) |
|
320 apply (rule trans) |
|
321 apply (rule_tac [2] inst_sprod_pcpo [symmetric]) |
|
322 apply (rule strict_Ispair1) |
|
323 done |
|
324 |
|
325 lemma strict_spair2: "(:a,UU:) = UU" |
|
326 apply (unfold spair_def) |
|
327 apply (subst beta_cfun_sprod) |
|
328 apply (rule trans) |
|
329 apply (rule_tac [2] inst_sprod_pcpo [symmetric]) |
|
330 apply (rule strict_Ispair2) |
|
331 done |
|
332 |
|
333 declare strict_spair1 [simp] strict_spair2 [simp] |
|
334 |
|
335 lemma strict_spair_rev: "(:x,y:)~=UU ==> ~x=UU & ~y=UU" |
|
336 apply (unfold spair_def) |
|
337 apply (rule strict_Ispair_rev) |
|
338 apply auto |
|
339 done |
|
340 |
|
341 lemma defined_spair_rev: "(:a,b:) = UU ==> (a = UU | b = UU)" |
|
342 apply (unfold spair_def) |
|
343 apply (rule defined_Ispair_rev) |
|
344 apply auto |
|
345 done |
|
346 |
|
347 lemma defined_spair: |
|
348 "[|a~=UU; b~=UU|] ==> (:a,b:) ~= UU" |
|
349 apply (unfold spair_def) |
|
350 apply (subst beta_cfun_sprod) |
|
351 apply (subst inst_sprod_pcpo) |
|
352 apply (erule defined_Ispair) |
|
353 apply assumption |
|
354 done |
|
355 |
|
356 lemma Exh_Sprod2: |
|
357 "z=UU | (? a b. z=(:a,b:) & a~=UU & b~=UU)" |
|
358 apply (unfold spair_def) |
|
359 apply (rule Exh_Sprod [THEN disjE]) |
|
360 apply (rule disjI1) |
|
361 apply (subst inst_sprod_pcpo) |
|
362 apply assumption |
|
363 apply (rule disjI2) |
|
364 apply (erule exE) |
|
365 apply (erule exE) |
|
366 apply (rule exI) |
|
367 apply (rule exI) |
|
368 apply (rule conjI) |
|
369 apply (subst beta_cfun_sprod) |
|
370 apply fast |
|
371 apply fast |
|
372 done |
|
373 |
|
374 |
|
375 lemma sprodE: |
|
376 assumes prem1: "p=UU ==> Q" |
|
377 assumes prem2: "!!x y. [| p=(:x,y:); x~=UU; y~=UU|] ==> Q" |
|
378 shows "Q" |
|
379 apply (rule IsprodE) |
|
380 apply (rule prem1) |
|
381 apply (subst inst_sprod_pcpo) |
|
382 apply assumption |
|
383 apply (rule prem2) |
|
384 prefer 2 apply (assumption) |
|
385 prefer 2 apply (assumption) |
|
386 apply (unfold spair_def) |
|
387 apply (subst beta_cfun_sprod) |
|
388 apply assumption |
|
389 done |
|
390 |
|
391 |
|
392 lemma strict_sfst: |
|
393 "p=UU==>sfst$p=UU" |
|
394 apply (unfold sfst_def) |
|
395 apply (subst beta_cfun) |
|
396 apply (rule cont_Isfst) |
|
397 apply (rule strict_Isfst) |
|
398 apply (rule inst_sprod_pcpo [THEN subst]) |
|
399 apply assumption |
|
400 done |
|
401 |
|
402 lemma strict_sfst1: |
|
403 "sfst$(:UU,y:) = UU" |
|
404 apply (unfold sfst_def spair_def) |
|
405 apply (subst beta_cfun_sprod) |
|
406 apply (subst beta_cfun) |
|
407 apply (rule cont_Isfst) |
|
408 apply (rule strict_Isfst1) |
|
409 done |
|
410 |
|
411 lemma strict_sfst2: |
|
412 "sfst$(:x,UU:) = UU" |
|
413 apply (unfold sfst_def spair_def) |
|
414 apply (subst beta_cfun_sprod) |
|
415 apply (subst beta_cfun) |
|
416 apply (rule cont_Isfst) |
|
417 apply (rule strict_Isfst2) |
|
418 done |
|
419 |
|
420 lemma strict_ssnd: |
|
421 "p=UU==>ssnd$p=UU" |
|
422 apply (unfold ssnd_def) |
|
423 apply (subst beta_cfun) |
|
424 apply (rule cont_Issnd) |
|
425 apply (rule strict_Issnd) |
|
426 apply (rule inst_sprod_pcpo [THEN subst]) |
|
427 apply assumption |
|
428 done |
|
429 |
|
430 lemma strict_ssnd1: |
|
431 "ssnd$(:UU,y:) = UU" |
|
432 apply (unfold ssnd_def spair_def) |
|
433 apply (subst beta_cfun_sprod) |
|
434 apply (subst beta_cfun) |
|
435 apply (rule cont_Issnd) |
|
436 apply (rule strict_Issnd1) |
|
437 done |
|
438 |
|
439 lemma strict_ssnd2: |
|
440 "ssnd$(:x,UU:) = UU" |
|
441 apply (unfold ssnd_def spair_def) |
|
442 apply (subst beta_cfun_sprod) |
|
443 apply (subst beta_cfun) |
|
444 apply (rule cont_Issnd) |
|
445 apply (rule strict_Issnd2) |
|
446 done |
|
447 |
|
448 lemma sfst2: |
|
449 "y~=UU ==>sfst$(:x,y:)=x" |
|
450 apply (unfold sfst_def spair_def) |
|
451 apply (subst beta_cfun_sprod) |
|
452 apply (subst beta_cfun) |
|
453 apply (rule cont_Isfst) |
|
454 apply (erule Isfst2) |
|
455 done |
|
456 |
|
457 lemma ssnd2: |
|
458 "x~=UU ==>ssnd$(:x,y:)=y" |
|
459 apply (unfold ssnd_def spair_def) |
|
460 apply (subst beta_cfun_sprod) |
|
461 apply (subst beta_cfun) |
|
462 apply (rule cont_Issnd) |
|
463 apply (erule Issnd2) |
|
464 done |
|
465 |
|
466 |
|
467 lemma defined_sfstssnd: |
|
468 "p~=UU ==> sfst$p ~=UU & ssnd$p ~=UU" |
|
469 apply (unfold sfst_def ssnd_def spair_def) |
|
470 apply (simplesubst beta_cfun) |
|
471 apply (rule cont_Issnd) |
|
472 apply (subst beta_cfun) |
|
473 apply (rule cont_Isfst) |
|
474 apply (rule defined_IsfstIssnd) |
|
475 apply (rule inst_sprod_pcpo [THEN subst]) |
|
476 apply assumption |
|
477 done |
|
478 |
|
479 lemma surjective_pairing_Sprod2: "(:sfst$p , ssnd$p:) = p" |
|
480 |
|
481 apply (unfold sfst_def ssnd_def spair_def) |
|
482 apply (subst beta_cfun_sprod) |
|
483 apply (simplesubst beta_cfun) |
|
484 apply (rule cont_Issnd) |
|
485 apply (subst beta_cfun) |
|
486 apply (rule cont_Isfst) |
|
487 apply (rule surjective_pairing_Sprod [symmetric]) |
|
488 done |
|
489 |
|
490 lemma lub_sprod2: |
|
491 "chain(S) ==> range(S) <<| |
|
492 (: lub(range(%i. sfst$(S i))), lub(range(%i. ssnd$(S i))) :)" |
|
493 apply (unfold sfst_def ssnd_def spair_def) |
|
494 apply (subst beta_cfun_sprod) |
|
495 apply (simplesubst beta_cfun [THEN ext]) |
|
496 apply (rule cont_Issnd) |
|
497 apply (subst beta_cfun [THEN ext]) |
|
498 apply (rule cont_Isfst) |
|
499 apply (erule lub_sprod) |
|
500 done |
|
501 |
|
502 |
|
503 lemmas thelub_sprod2 = lub_sprod2 [THEN thelubI, standard] |
|
504 (* |
|
505 "chain ?S1 ==> |
|
506 lub (range ?S1) = |
|
507 (:lub (range (%i. sfst$(?S1 i))), lub (range (%i. ssnd$(?S1 i))):)" : thm |
|
508 *) |
|
509 |
|
510 lemma ssplit1: |
|
511 "ssplit$f$UU=UU" |
|
512 |
|
513 apply (unfold ssplit_def) |
|
514 apply (subst beta_cfun) |
|
515 apply (simp (no_asm)) |
|
516 apply (subst strictify1) |
|
517 apply (rule refl) |
|
518 done |
|
519 |
|
520 lemma ssplit2: |
|
521 "[|x~=UU;y~=UU|] ==> ssplit$f$(:x,y:)= f$x$y" |
|
522 apply (unfold ssplit_def) |
|
523 apply (subst beta_cfun) |
|
524 apply (simp (no_asm)) |
|
525 apply (subst strictify2) |
|
526 apply (rule defined_spair) |
|
527 apply assumption |
|
528 apply assumption |
|
529 apply (subst beta_cfun) |
|
530 apply (simp (no_asm)) |
|
531 apply (subst sfst2) |
|
532 apply assumption |
|
533 apply (subst ssnd2) |
|
534 apply assumption |
|
535 apply (rule refl) |
|
536 done |
|
537 |
|
538 |
|
539 lemma ssplit3: |
|
540 "ssplit$spair$z=z" |
|
541 |
|
542 apply (unfold ssplit_def) |
|
543 apply (subst beta_cfun) |
|
544 apply (simp (no_asm)) |
|
545 apply (case_tac "z=UU") |
|
546 apply (erule ssubst) |
|
547 apply (rule strictify1) |
|
548 apply (rule trans) |
|
549 apply (rule strictify2) |
|
550 apply assumption |
|
551 apply (subst beta_cfun) |
|
552 apply (simp (no_asm)) |
|
553 apply (rule surjective_pairing_Sprod2) |
|
554 done |
|
555 |
|
556 (* ------------------------------------------------------------------------ *) |
|
557 (* install simplifier for Sprod *) |
|
558 (* ------------------------------------------------------------------------ *) |
|
559 |
|
560 lemmas Sprod_rews = strict_sfst1 strict_sfst2 |
|
561 strict_ssnd1 strict_ssnd2 sfst2 ssnd2 defined_spair |
|
562 ssplit1 ssplit2 |
|
563 declare Sprod_rews [simp] |
30 |
564 |
31 end |
565 end |