596 tactic @{ML [index] SUBPROOF}, since this tactic provides us with the parameters (as |
596 tactic @{ML [index] SUBPROOF}, since this tactic provides us with the parameters (as |
597 list of @{ML_type cterm}s) and the assumptions (as list of @{ML_type thm}s). |
597 list of @{ML_type cterm}s) and the assumptions (as list of @{ML_type thm}s). |
598 The problem with @{ML SUBPROOF}, however, is that it always expects us to |
598 The problem with @{ML SUBPROOF}, however, is that it always expects us to |
599 completely discharge the goal (see Section~\ref{sec:simpletacs}). This is |
599 completely discharge the goal (see Section~\ref{sec:simpletacs}). This is |
600 a bit inconvenient for our gradual explanation of the proof here. Therefore |
600 a bit inconvenient for our gradual explanation of the proof here. Therefore |
601 we use first the function @{ML [index] FOCUS}, which does same as @{ML SUBPROOF} |
601 we use first the function @{ML [index] FOCUS in Subgoal}, which does s |
|
602 ame as @{ML SUBPROOF} |
602 but does not require us to completely discharge the goal. |
603 but does not require us to completely discharge the goal. |
603 *} |
604 *} |
604 (*<*)oops(*>*) |
605 (*<*)oops(*>*) |
605 text_raw {* |
606 text_raw {* |
606 \begin{figure}[t] |
607 \begin{figure}[t] |
628 |
629 |
629 text {* |
630 text {* |
630 First we calculate the values for @{text "params1/2"} and @{text "prems1/2"} |
631 First we calculate the values for @{text "params1/2"} and @{text "prems1/2"} |
631 from @{text "params"} and @{text "prems"}, respectively. To better see what is |
632 from @{text "params"} and @{text "prems"}, respectively. To better see what is |
632 going in our example, we will print out these values using the printing |
633 going in our example, we will print out these values using the printing |
633 function in Figure~\ref{fig:chopprint}. Since @{ML FOCUS} will |
634 function in Figure~\ref{fig:chopprint}. Since @{ML FOCUS in Subgoal} will |
634 supply us the @{text "params"} and @{text "prems"} as lists, we can |
635 supply us the @{text "params"} and @{text "prems"} as lists, we can |
635 separate them using the function @{ML [index] chop}. |
636 separate them using the function @{ML [index] chop}. |
636 *} |
637 *} |
637 |
638 |
638 ML %linenosgray{*fun chop_test_tac preds rules = |
639 ML %linenosgray{*fun chop_test_tac preds rules = |
639 FOCUS (fn {params, prems, context, ...} => |
640 Subgoal.FOCUS (fn {params, prems, context, ...} => |
640 let |
641 let |
641 val cparams = map snd params |
642 val cparams = map snd params |
642 val (params1, params2) = chop (length cparams - length preds) cparams |
643 val (params1, params2) = chop (length cparams - length preds) cparams |
643 val (prems1, prems2) = chop (length prems - length rules) prems |
644 val (prems1, prems2) = chop (length prems - length rules) prems |
644 in |
645 in |
702 format (using @{ML [index] rulify in ObjectLogic}). So we can modify the |
703 format (using @{ML [index] rulify in ObjectLogic}). So we can modify the |
703 code as follows: |
704 code as follows: |
704 *} |
705 *} |
705 |
706 |
706 ML %linenosgray{*fun apply_prem_tac i preds rules = |
707 ML %linenosgray{*fun apply_prem_tac i preds rules = |
707 FOCUS (fn {params, prems, context, ...} => |
708 Subgoal.FOCUS (fn {params, prems, context, ...} => |
708 let |
709 let |
709 val cparams = map snd params |
710 val cparams = map snd params |
710 val (params1, params2) = chop (length cparams - length preds) cparams |
711 val (params1, params2) = chop (length cparams - length preds) cparams |
711 val (prems1, prems2) = chop (length prems - length rules) prems |
712 val (prems1, prems2) = chop (length prems - length rules) prems |
712 in |
713 in |
786 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
787 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
787 THEN EVERY1 (map (prepare_prem params2 prems2) prems1) |
788 THEN EVERY1 (map (prepare_prem params2 prems2) prems1) |
788 end) *} |
789 end) *} |
789 |
790 |
790 text {* |
791 text {* |
791 Note that the tactic is now @{ML SUBPROOF}, not @{ML FOCUS} anymore. |
792 Note that the tactic is now @{ML SUBPROOF}, not @{ML FOCUS in Subgoal} anymore. |
792 The full proof of the introduction rule is as follows: |
793 The full proof of the introduction rule is as follows: |
793 *} |
794 *} |
794 |
795 |
795 lemma fresh_Lam: |
796 lemma fresh_Lam: |
796 shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)" |
797 shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)" |