diff -r 2565c87f8db7 -r 8057d65607eb ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Fri Jul 31 19:10:39 2009 +0200 +++ b/ProgTutorial/Tactical.thy Sat Aug 01 08:59:41 2009 +0200 @@ -384,7 +384,7 @@ 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. *} @@ -457,7 +457,7 @@ into the goal state. Consider for example the proof *} -lemma shows "\x\A. P x \ Q x" +lemma shows "\x \ A. P x \ Q x" apply(tactic {* dtac @{thm bspec} 1 *}) txt{*\begin{minipage}{\textwidth} @{subgoals [display]} @@ -525,8 +525,9 @@ Often proofs on the ML-level involve elaborate operations on assumptions and @{text "\"}-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 - and binds the various components of a goal state to a record. + safety is provided by the functions @{ML [index] FOCUS} and @{ML [index] SUBPROOF}. + 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 @@ -540,35 +541,33 @@ *} -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 - @{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for +\caption{A function that prints out the various parameters provided by + @{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 "\x y. A x y \ B y x \ 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: @@ -590,19 +589,11 @@ @{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: @@ -622,10 +613,12 @@ 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 - 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}: + The difference between @{ML SUBPROOF} and @{ML FOCUS} is that the former + expects that the goal is solved completely, which the latter does not. One + convenience of both @{ML FOCUS} and @{ML SUBPROOF} is that we can apply the + 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)*} @@ -664,11 +657,12 @@ text {* \begin{readmore} - The function @{ML SUBPROOF} is defined in @{ML_file "Pure/subgoal.ML"} and - also described in \isccite{sec:results}. + The functions @{ML FOCUS} and @{ML SUBPROOF} are defined in + @{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 @@ -699,7 +693,7 @@ 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. @@ -876,7 +870,7 @@ *} ML{*val select_tac'' = TRY o FIRST' [rtac @{thm conjI}, rtac @{thm impI}, - rtac @{thm notI}, rtac @{thm allI}]*} + rtac @{thm notI}, rtac @{thm allI}]*} text_raw{*\label{tac:selectprimeprime}*} text {*