equal
deleted
inserted
replaced
318 qed_goalw "beta_cfun_sprod" Sprod3.thy [spair_def] |
318 qed_goalw "beta_cfun_sprod" Sprod3.thy [spair_def] |
319 "(LAM x y.Ispair x y)`a`b = Ispair a b" |
319 "(LAM x y.Ispair x y)`a`b = Ispair a b" |
320 (fn prems => |
320 (fn prems => |
321 [ |
321 [ |
322 (stac beta_cfun 1), |
322 (stac beta_cfun 1), |
323 (cont_tac 1), |
323 (simp_tac (!simpset addsimps [cont_Ispair2, cont_Ispair1, |
324 (rtac cont_Ispair2 1), |
324 cont2cont_CF1L]) 1), |
325 (rtac cont2cont_CF1L 1), |
|
326 (rtac cont_Ispair1 1), |
|
327 (stac beta_cfun 1), |
325 (stac beta_cfun 1), |
328 (rtac cont_Ispair2 1), |
326 (rtac cont_Ispair2 1), |
329 (rtac refl 1) |
327 (rtac refl 1) |
330 ]); |
328 ]); |
331 |
329 |
622 qed_goalw "ssplit1" Sprod3.thy [ssplit_def] |
620 qed_goalw "ssplit1" Sprod3.thy [ssplit_def] |
623 "ssplit`f`UU=UU" |
621 "ssplit`f`UU=UU" |
624 (fn prems => |
622 (fn prems => |
625 [ |
623 [ |
626 (stac beta_cfun 1), |
624 (stac beta_cfun 1), |
627 (cont_tacR 1), |
625 (Simp_tac 1), |
628 (stac strictify1 1), |
626 (stac strictify1 1), |
629 (rtac refl 1) |
627 (rtac refl 1) |
630 ]); |
628 ]); |
631 |
629 |
632 qed_goalw "ssplit2" Sprod3.thy [ssplit_def] |
630 qed_goalw "ssplit2" Sprod3.thy [ssplit_def] |
633 "[|x~=UU;y~=UU|] ==> ssplit`f`(|x,y|)= f`x`y" |
631 "[|x~=UU;y~=UU|] ==> ssplit`f`(|x,y|)= f`x`y" |
634 (fn prems => |
632 (fn prems => |
635 [ |
633 [ |
636 (stac beta_cfun 1), |
634 (stac beta_cfun 1), |
637 (cont_tacR 1), |
635 (Simp_tac 1), |
638 (stac strictify2 1), |
636 (stac strictify2 1), |
639 (rtac defined_spair 1), |
637 (rtac defined_spair 1), |
640 (resolve_tac prems 1), |
638 (resolve_tac prems 1), |
641 (resolve_tac prems 1), |
639 (resolve_tac prems 1), |
642 (stac beta_cfun 1), |
640 (stac beta_cfun 1), |
643 (cont_tacR 1), |
641 (Simp_tac 1), |
644 (stac sfst2 1), |
642 (stac sfst2 1), |
645 (resolve_tac prems 1), |
643 (resolve_tac prems 1), |
646 (stac ssnd2 1), |
644 (stac ssnd2 1), |
647 (resolve_tac prems 1), |
645 (resolve_tac prems 1), |
648 (rtac refl 1) |
646 (rtac refl 1) |
652 qed_goalw "ssplit3" Sprod3.thy [ssplit_def] |
650 qed_goalw "ssplit3" Sprod3.thy [ssplit_def] |
653 "ssplit`spair`z=z" |
651 "ssplit`spair`z=z" |
654 (fn prems => |
652 (fn prems => |
655 [ |
653 [ |
656 (stac beta_cfun 1), |
654 (stac beta_cfun 1), |
657 (cont_tacR 1), |
655 (Simp_tac 1), |
658 (case_tac "z=UU" 1), |
656 (case_tac "z=UU" 1), |
659 (hyp_subst_tac 1), |
657 (hyp_subst_tac 1), |
660 (rtac strictify1 1), |
658 (rtac strictify1 1), |
661 (rtac trans 1), |
659 (rtac trans 1), |
662 (rtac strictify2 1), |
660 (rtac strictify2 1), |
663 (atac 1), |
661 (atac 1), |
664 (stac beta_cfun 1), |
662 (stac beta_cfun 1), |
665 (cont_tacR 1), |
663 (Simp_tac 1), |
666 (rtac surjective_pairing_Sprod2 1) |
664 (rtac surjective_pairing_Sprod2 1) |
667 ]); |
665 ]); |
668 |
666 |
669 |
667 |
670 (* ------------------------------------------------------------------------ *) |
668 (* ------------------------------------------------------------------------ *) |