equal
deleted
inserted
replaced
645 val take_stricts = |
645 val take_stricts = |
646 let |
646 let |
647 fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n"); |
647 fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n"); |
648 val goal = mk_trp (foldr1 mk_conj (map one_eq eqs)); |
648 val goal = mk_trp (foldr1 mk_conj (map one_eq eqs)); |
649 val tacs = [ |
649 val tacs = [ |
650 DatatypePackage.induct_tac "n" 1, |
650 DatatypePackage.induct_tac @{context} "n" 1, |
651 simp_tac iterate_Cprod_ss 1, |
651 simp_tac iterate_Cprod_ss 1, |
652 asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1]; |
652 asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1]; |
653 in pg copy_take_defs goal tacs end; |
653 in pg copy_take_defs goal tacs end; |
654 |
654 |
655 val take_stricts' = rewrite_rule copy_take_defs take_stricts; |
655 val take_stricts' = rewrite_rule copy_take_defs take_stricts; |
676 else EVERY (map c_UU_tac (nonlazy_rec args)) THEN |
676 else EVERY (map c_UU_tac (nonlazy_rec args)) THEN |
677 asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1; |
677 asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1; |
678 fun eq_tacs ((dn, _), cons) = map con_tac cons; |
678 fun eq_tacs ((dn, _), cons) = map con_tac cons; |
679 val tacs = |
679 val tacs = |
680 simp_tac iterate_Cprod_ss 1 :: |
680 simp_tac iterate_Cprod_ss 1 :: |
681 DatatypePackage.induct_tac "n" 1 :: |
681 DatatypePackage.induct_tac @{context} "n" 1 :: |
682 simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 :: |
682 simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 :: |
683 asm_full_simp_tac (HOLCF_ss addsimps simps) 1 :: |
683 asm_full_simp_tac (HOLCF_ss addsimps simps) 1 :: |
684 TRY (safe_tac HOL_cs) :: |
684 TRY (safe_tac HOL_cs) :: |
685 maps eq_tacs eqs; |
685 maps eq_tacs eqs; |
686 in pg copy_take_defs goal tacs end; |
686 in pg copy_take_defs goal tacs end; |
748 fun tacf prems = |
748 fun tacf prems = |
749 let |
749 let |
750 val tacs1 = [ |
750 val tacs1 = [ |
751 quant_tac 1, |
751 quant_tac 1, |
752 simp_tac HOL_ss 1, |
752 simp_tac HOL_ss 1, |
753 DatatypePackage.induct_tac "n" 1, |
753 DatatypePackage.induct_tac @{context} "n" 1, |
754 simp_tac (take_ss addsimps prems) 1, |
754 simp_tac (take_ss addsimps prems) 1, |
755 TRY (safe_tac HOL_cs)]; |
755 TRY (safe_tac HOL_cs)]; |
756 fun arg_tac arg = |
756 fun arg_tac arg = |
757 case_UU_tac (prems @ con_rews) 1 |
757 case_UU_tac (prems @ con_rews) 1 |
758 (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg); |
758 (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg); |
843 res_inst_tac [("x",x_name n)] cases 1 :: |
843 res_inst_tac [("x",x_name n)] cases 1 :: |
844 asm_simp_tac take_ss 1 :: |
844 asm_simp_tac take_ss 1 :: |
845 maps con_tacs cons; |
845 maps con_tacs cons; |
846 val tacs = |
846 val tacs = |
847 rtac allI 1 :: |
847 rtac allI 1 :: |
848 DatatypePackage.induct_tac "n" 1 :: |
848 DatatypePackage.induct_tac @{context} "n" 1 :: |
849 simp_tac take_ss 1 :: |
849 simp_tac take_ss 1 :: |
850 TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) :: |
850 TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) :: |
851 flat (mapn foo_tacs 1 (conss ~~ cases)); |
851 flat (mapn foo_tacs 1 (conss ~~ cases)); |
852 in pg [] goal tacs end; |
852 in pg [] goal tacs end; |
853 |
853 |
936 eres_inst_tac [("P1", sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1, |
936 eres_inst_tac [("P1", sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1, |
937 TRY (safe_tac HOL_cs), |
937 TRY (safe_tac HOL_cs), |
938 REPEAT (CHANGED (asm_simp_tac take_ss 1))]; |
938 REPEAT (CHANGED (asm_simp_tac take_ss 1))]; |
939 val tacs = [ |
939 val tacs = [ |
940 rtac impI 1, |
940 rtac impI 1, |
941 DatatypePackage.induct_tac "n" 1, |
941 DatatypePackage.induct_tac @{context} "n" 1, |
942 simp_tac take_ss 1, |
942 simp_tac take_ss 1, |
943 safe_tac HOL_cs] @ |
943 safe_tac HOL_cs] @ |
944 flat (mapn x_tacs 0 xs); |
944 flat (mapn x_tacs 0 xs); |
945 in pg [ax_bisim_def] goal tacs end; |
945 in pg [ax_bisim_def] goal tacs end; |
946 in |
946 in |