equal
deleted
inserted
replaced
631 *} |
631 *} |
632 |
632 |
633 ML{*fun chop_test_tac preds rules = |
633 ML{*fun chop_test_tac preds rules = |
634 SUBPROOF_test (fn {params, prems, context, ...} => |
634 SUBPROOF_test (fn {params, prems, context, ...} => |
635 let |
635 let |
636 val (params1, params2) = chop (length params - length preds) params |
636 val (params1, params2) = chop (length params - length preds) (map snd params) |
637 val (prems1, prems2) = chop (length prems - length rules) prems |
637 val (prems1, prems2) = chop (length prems - length rules) prems |
638 in |
638 in |
639 chop_print params1 params2 prems1 prems2 context; no_tac |
639 chop_print params1 params2 prems1 prems2 context; no_tac |
640 end) *} |
640 end) *} |
641 |
641 |
696 *} |
696 *} |
697 |
697 |
698 ML %linenosgray{*fun apply_prem_tac i preds rules = |
698 ML %linenosgray{*fun apply_prem_tac i preds rules = |
699 SUBPROOF_test (fn {params, prems, context, ...} => |
699 SUBPROOF_test (fn {params, prems, context, ...} => |
700 let |
700 let |
701 val (params1, params2) = chop (length params - length preds) params |
701 val (params1, params2) = chop (length params - length preds) (map snd params) |
702 val (prems1, prems2) = chop (length prems - length rules) prems |
702 val (prems1, prems2) = chop (length prems - length rules) prems |
703 in |
703 in |
704 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
704 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
705 THEN print_tac "" |
705 THEN print_tac "" |
706 THEN no_tac |
706 THEN no_tac |
771 *} |
771 *} |
772 |
772 |
773 ML{*fun prove_intro_tac i preds rules = |
773 ML{*fun prove_intro_tac i preds rules = |
774 SUBPROOF (fn {params, prems, ...} => |
774 SUBPROOF (fn {params, prems, ...} => |
775 let |
775 let |
776 val (params1, params2) = chop (length params - length preds) params |
776 val (params1, params2) = chop (length params - length preds) (map snd params) |
777 val (prems1, prems2) = chop (length prems - length rules) prems |
777 val (prems1, prems2) = chop (length prems - length rules) prems |
778 in |
778 in |
779 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
779 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
780 THEN EVERY1 (map (prepare_prem params2 prems2) prems1) |
780 THEN EVERY1 (map (prepare_prem params2 prems2) prems1) |
781 end) *} |
781 end) *} |
866 *} |
866 *} |
867 |
867 |
868 ML %linenosgray{*fun prove_intro_tac i preds rules = |
868 ML %linenosgray{*fun prove_intro_tac i preds rules = |
869 SUBPROOF (fn {params, prems, context, ...} => |
869 SUBPROOF (fn {params, prems, context, ...} => |
870 let |
870 let |
871 val (params1, params2) = chop (length params - length preds) params |
871 val (params1, params2) = chop (length params - length preds) (map snd params) |
872 val (prems1, prems2) = chop (length prems - length rules) prems |
872 val (prems1, prems2) = chop (length prems - length rules) prems |
873 in |
873 in |
874 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
874 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
875 THEN EVERY1 (map (prepare_prem params2 prems2 context) prems1) |
875 THEN EVERY1 (map (prepare_prem params2 prems2 context) prems1) |
876 end) *} |
876 end) *} |