isabelle-cookbook: comparison ProgTutorial/Tactical.thy

equal deleted inserted replaced

-:2565c87f8db7
+:8057d65607eb
 text {*
 Similarly, @{ML [index] rtac}, @{ML [index] dtac}, @{ML [index] etac} and
 @{ML [index] ftac} correspond (roughly)
 to @{text rule}, @{text drule}, @{text erule} and @{text frule},
-respectively. Each of them take a theorem as argument and attempt to
+respectively. Each of them takes a theorem as argument and attempts to
 apply it to a goal. Below are three self-explanatory examples.
 *}
 lemma shows "P \<and> Q"
 apply(tactic {* rtac @{thm conjI} 1 *})
 procedure might become too fragile, if it just applies inference rules as
 shown above. The reason is that a number of rules introduce meta-variables
 into the goal state. Consider for example the proof
 *}
-lemma shows "\<forall>x\<in>A. P x \<Longrightarrow> Q x"
+lemma shows "\<forall>x \<in> A. P x \<Longrightarrow> Q x"
 apply(tactic {* dtac @{thm bspec} 1 *})
 txt{*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 \end{readmore}
 Often proofs on the ML-level involve elaborate operations on assumptions and
 @{text "\<And>"}-quantified variables. To do such operations using the basic tactics
 shown so far is very unwieldy and brittle. Some convenience and
-safety is provided by @{ML [index] SUBPROOF}. This tactic fixes the parameters
+safety is provided by the functions @{ML [index] FOCUS} and @{ML [index] SUBPROOF}.
-and binds the various components of a goal state to a record.
+These tactics fix the parameters
+and bind the various components of a goal state to a record.
 To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
 takes a record and just prints out the content of this record (using the
 string transformation functions from in Section~\ref{sec:printing}). Consider
 now the proof:
 *}
 \begin{minipage}{\textwidth}
 \begin{isabelle}
 *}
-ML{*fun sp_tac {prems, params, asms, concl, context, schematics} =
+ML{*fun foc_tac {prems, params, asms, concl, context, schematics} =
 let
 val string_of_params = string_of_cterms context (map snd params)
-val test = commas (map fst params)
 val string_of_asms = string_of_cterms context asms
 val string_of_concl = string_of_cterm context concl
 val string_of_prems = string_of_thms_no_vars context prems
 val string_of_schms = string_of_cterms context (snd schematics)
 val _ = (writeln ("params: " ^ string_of_params);
-writeln ("param names: " ^ test);
 writeln ("schematics: " ^ string_of_schms);
 writeln ("assumptions: " ^ string_of_asms);
 writeln ("conclusion: " ^ string_of_concl);
 writeln ("premises: " ^ string_of_prems))
 in
-no_tac
+all_tac
 end*}
 text_raw{*
 \end{isabelle}
 \end{minipage}
-\caption{A function that prints out the various parameters provided by the tactic
+\caption{A function that prints out the various parameters provided by
-@{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for
+@{ML FOCUS} and @{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for
 extracting strings from @{ML_type cterm}s and @{ML_type thm}s.\label{fig:sptac}}
 \end{figure}
 *}
 lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
-apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
+apply(tactic {* FOCUS foc_tac @{context} 1 *})
 txt {*
 The tactic produces the following printout:
 \begin{quote}\small
 the subproof. By convention these fixed variables are printed in brown colour.
 Similarly the schematic variable @{term z}. The assumption, or premise,
 @{prop "A x y"} is bound as @{ML_type cterm} to the record-variable
 @{text asms}, but also as @{ML_type thm} to @{text prems}.
-Notice also that we had to append @{text [quotes] "?"} to the
-\isacommand{apply}-command. The reason is that @{ML [index] SUBPROOF} normally
-expects that the subgoal is solved completely.  Since in the function @{ML
-sp_tac} we returned the tactic @{ML no_tac}, the subproof obviously
-fails. The question-mark allows us to recover from this failure in a
-graceful manner so that the output messages are not overwritten by an
-``empty sequence'' error message.
 If we continue the proof script by applying the @{text impI}-rule
 *}
 apply(rule impI)
-apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
+apply(tactic {* FOCUS foc_tac @{context} 1 *})
 txt {*
 then the tactic prints out:
 \begin{quote}\small
 (*<*)oops(*>*)
 text {*
 Now also @{term "B y x"} is an assumption bound to @{text asms} and @{text prems}.
-One convenience of @{ML SUBPROOF} is that we can apply the assumptions
+The difference between @{ML SUBPROOF} and @{ML FOCUS} is that the former
-using the usual tactics, because the parameter @{text prems}
+expects that the goal is solved completely, which the latter does not.  One
-contains them as theorems. With this you can easily
+convenience of both @{ML FOCUS} and @{ML SUBPROOF} is that we can apply the
-implement a tactic that behaves almost like @{ML atac}:
+assumptions using the usual tactics, because the parameter @{text prems}
+contains them as theorems. With this you can easily implement a tactic that
+behaves almost like @{ML atac}:
 *}
 ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*}
 text {*
 done
 text {*
 \begin{readmore}
-The function @{ML SUBPROOF} is defined in @{ML_file "Pure/subgoal.ML"} and
+The functions @{ML FOCUS} and @{ML SUBPROOF} are defined in
-also described in \isccite{sec:results}.
+@{ML_file "Pure/subgoal.ML"} and also described in
+\isccite{sec:results}.
 \end{readmore}
-Similar but less powerful functions than @{ML SUBPROOF} are @{ML [index] SUBGOAL}
+Similar but less powerful functions than @{ML FOCUS} are @{ML [index] SUBGOAL}
 and @{ML [index] CSUBGOAL}. They allow you to inspect a given subgoal (the former
 presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type
 cterm}). With this you can implement a tactic that applies a rule according
 to the topmost logic connective in the subgoal (to illustrate this we only
 analyse a few connectives). The code of the tactic is as
 construct the patterns, the pattern in Line 8 cannot be constructed in this
 way. The reason is that an antiquotation would fix the type of the
 quantified variable. So you really have to construct the pattern using the
 basic term-constructors. This is not necessary in other cases, because their
 type is always fixed to function types involving only the type @{typ
-bool}. (See Section \ref{sec:terms_manually} about constructing terms
+bool}. (See Section \ref{sec:terms_types_manually} about constructing terms
 manually.) For the catch-all pattern, we chose to just return @{ML all_tac}.
 Consequently, @{ML select_tac} never fails.
 Let us now see how to apply this tactic. Consider the four goals:
 list. The same can be achieved with the tactic combinator @{ML [index] TRY}.
 For example:
 *}
 ML{*val select_tac'' = TRY o FIRST' [rtac @{thm conjI}, rtac @{thm impI},
 rtac @{thm notI}, rtac @{thm allI}]*}
 text_raw{*\label{tac:selectprimeprime}*}
 text {*
 This tactic behaves in the same way as @{ML select_tac'}: it tries out
 one of the given tactics and if none applies leaves the goal state

changeset 298	8057d65607eb
parent 294	ee9d53fbb56b
child 299	d0b81d6e1b28