isabelle-cookbook: comparison ProgTutorial/Tactical.thy

equal deleted inserted replaced

-:8057d65607eb
+:d0b81d6e1b28
 \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 the functions @{ML [index] FOCUS} and @{ML [index] SUBPROOF}.
+safety is provided by the functions @{ML [index] FOCUS in Subgoal} and
-These tactics fix the parameters
+@{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
 now the proof:
 let
 val string_of_params = string_of_cterms context (map snd 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 string_of_schms = string_of_cterms context (map fst (snd schematics))
 val _ = (writeln ("params: " ^ string_of_params);
 writeln ("schematics: " ^ string_of_schms);
 writeln ("assumptions: " ^ string_of_asms);
 writeln ("conclusion: " ^ string_of_concl);
 writeln ("premises: " ^ string_of_prems))
 in
 all_tac
 end*}
 text_raw{*
 \end{isabelle}
 \end{minipage}
 \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
+@{ML FOCUS in Subgoal} and @{ML SUBPROOF}. It uses the functions defined
-extracting strings from @{ML_type cterm}s and @{ML_type thm}s.\label{fig:sptac}}
+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 {* FOCUS foc_tac @{context} 1 *})
+apply(tactic {* Subgoal.FOCUS foc_tac @{context} 1 *})
 txt {*
 The tactic produces the following printout:
 \begin{quote}\small
 conclusion:  & @{term "B y x \<longrightarrow> C (z y) x"}\\
 premises:    & @{term "A x y"}
 \end{tabular}
 \end{quote}
+(FIXME: find out how nowadays the schmetics are handled)
 Notice in the actual output the brown colour of the variables @{term x} and
 @{term y}. Although they are parameters in the original goal, they are fixed inside
 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
 If we continue the proof script by applying the @{text impI}-rule
 *}
 apply(rule impI)
-apply(tactic {* FOCUS foc_tac @{context} 1 *})
+apply(tactic {* Subgoal.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}.
-The difference between @{ML SUBPROOF} and @{ML FOCUS} is that the former
+The difference between @{ML SUBPROOF} and @{ML FOCUS in Subgoal} 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
+convenience of both @{ML FOCUS in Subgoal} 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}:
 *}
 done
 text {*
 \begin{readmore}
-The functions @{ML FOCUS} and @{ML SUBPROOF} are defined in
+The functions @{ML FOCUS in Subgoal} 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 FOCUS} are @{ML [index] SUBGOAL}
+Similar but less powerful functions than @{ML FOCUS in Subgoal} are
-and @{ML [index] CSUBGOAL}. They allow you to inspect a given subgoal (the former
+@{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
 follows.
 text {*
 will solve all trivial subgoals involving @{term True} or @{term "False"}.
 (FIXME: say something about @{ML [index] COND} and COND')
-(FIXME: say something about @{ML [index] FOCUS})
 \begin{readmore}
 Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}.
 Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}.
+The function @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are defined in @{ML_file "Pure/subgoal.ML"}
 \end{readmore}
 *}
 section {* Simplifier Tactics *}

changeset 299	d0b81d6e1b28
parent 298	8057d65607eb
child 301	2728e8daebc0