621 One difference between the tactics @{ML SUBPROOF} and @{ML FOCUS in Subgoal} |
621 One difference between the tactics @{ML SUBPROOF} and @{ML FOCUS in Subgoal} |
622 is that the former expects that the goal is solved completely, which the |
622 is that the former expects that the goal is solved completely, which the |
623 latter does not. Another is that @{ML SUBPROOF} cannot instantiate any schematic |
623 latter does not. Another is that @{ML SUBPROOF} cannot instantiate any schematic |
624 variables. |
624 variables. |
625 |
625 |
626 One convenience of both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} is that we |
626 Observe that inside @{ML FOCUS in Subgoal} and @{ML SUBPROOF}, we are in a goal |
627 can apply the assumptions using the usual tactics, because the parameter |
627 state where there is only a conclusion. This means the tactics @{ML dtac} and |
628 @{text prems} contains them as theorems. With this you can easily implement |
628 the like are of no use for manipulating the goal state. The assumptions inside |
629 a tactic that behaves almost like @{ML atac}: |
629 @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are given as cterms and theorems in |
|
630 the arguments @{text "asms"} and @{text "prems"}, respectively. This |
|
631 means we can apply them using the usual assumption tactics. With this you can |
|
632 for example easily implement a tactic that behaves almost like @{ML atac}: |
630 *} |
633 *} |
631 |
634 |
632 ML{*val atac' = Subgoal.FOCUS (fn {prems, ...} => resolve_tac prems 1)*} |
635 ML{*val atac' = Subgoal.FOCUS (fn {prems, ...} => resolve_tac prems 1)*} |
633 |
636 |
634 text {* |
637 text {* |
660 apply(rule TrueI) |
663 apply(rule TrueI) |
661 done |
664 done |
662 |
665 |
663 |
666 |
664 text {* |
667 text {* |
|
668 There is one peculiarity about @{ML FOCUS in Subgoal} and @{ML SUBPROOF}. |
|
669 If we apply @{text "rtac @{thm allI}"} in the proof below |
|
670 *} |
|
671 |
|
672 lemma |
|
673 shows "B \<Longrightarrow> \<forall>x. A x" |
|
674 apply(tactic {* rtac @{thm allI} 1 *}) |
|
675 txt{* it will produce the expected goal state |
|
676 @{subgoals [display]} *} |
|
677 (*<*)oops(*>*) |
|
678 |
|
679 text {* But if we apply the same tactic inside @{ML FOCUS in Subgoal} |
|
680 we obtain |
|
681 *} |
|
682 |
|
683 lemma |
|
684 shows "B \<Longrightarrow> \<forall>x. A x" |
|
685 apply(tactic {* Subgoal.FOCUS (fn _ => rtac @{thm allI} 1) @{context} 1 *}) |
|
686 txt{* it will produce the goal state |
|
687 @{subgoals [display]} |
|
688 |
|
689 If we want to imitate the behaviour of the ``plain'' tactic, then we |
|
690 can apply the tactic @{ML norm_hhf_tac in Goal}. This gives |
|
691 *} |
|
692 apply(tactic {* Goal.norm_hhf_tac 1 *}) |
|
693 txt{*@{subgoals [display]}*} |
|
694 (*<*)oops(*>*) |
|
695 |
|
696 text {* |
|
697 This tactic transforms the goal state into a \emph{hereditary Harrop normal |
|
698 form}. To sum up, both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are rather |
|
699 convenient, but can impose a considerable run-time penalty in automatic |
|
700 proofs. If speed is of the essence, then maybe the two lower level combinators |
|
701 described next are more appropriate. |
|
702 |
|
703 |
665 \begin{readmore} |
704 \begin{readmore} |
666 The functions @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are defined in |
705 The functions @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are defined in |
667 @{ML_file "Pure/subgoal.ML"} and also described in |
706 @{ML_file "Pure/subgoal.ML"} and also described in |
668 \isccite{sec:results}. |
707 \isccite{sec:results}. |
669 \end{readmore} |
708 \end{readmore} |
670 |
709 |
671 Similar but less powerful functions than @{ML FOCUS in Subgoal}, respectively |
710 Similar but less powerful functions than @{ML FOCUS in Subgoal}, |
672 @{ML SUBPROOF}, are |
711 respectively @{ML SUBPROOF}, are @{ML_ind SUBGOAL in Tactical} and @{ML_ind |
673 @{ML_ind SUBGOAL in Tactical} and @{ML_ind CSUBGOAL in Tactical}. They allow you to |
712 CSUBGOAL in Tactical}. They allow you to inspect a given subgoal (the former |
674 inspect a given subgoal (the former |
|
675 presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type |
713 presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type |
676 cterm}). With them you can implement a tactic that applies a rule according |
714 cterm}). With them you can implement a tactic that applies a rule according |
677 to the topmost logic connective in the subgoal (to illustrate this we only |
715 to the topmost logic connective in the subgoal (to illustrate this we only |
678 analyse a few connectives). The code of the tactic is as |
716 analyse a few connectives). The code of the tactic is as follows. |
679 follows. |
|
680 *} |
717 *} |
681 |
718 |
682 ML %linenosgray{*fun select_tac (t, i) = |
719 ML %linenosgray{*fun select_tac (t, i) = |
683 case t of |
720 case t of |
684 @{term "Trueprop"} $ t' => select_tac (t', i) |
721 @{term "Trueprop"} $ t' => select_tac (t', i) |