isabelle-cookbook: comparison ProgTutorial/Tactical.thy

equal deleted inserted replaced

-:f286dfa9f173
+:2728e8daebc0
 \begin{isabelle}
 @{text "*** empty result sequence -- proof command failed"}\\
 @{text "*** At command \"apply\"."}
 \end{isabelle}
-This means they failed.\footnote{To be precise tactics do not produce this error
+This means they failed.\footnote{To be precise, tactics do not produce this error
 message, it originates from the \isacommand{apply} wrapper.} The reason for this
 error message is that tactics
 are functions mapping a goal state to a (lazy) sequence of successor states.
 Hence the type of a tactic is:
 *}
 tactic
 *}
 ML{*fun my_print_tac ctxt thm =
 let
-val _ = writeln (string_of_thm_no_vars ctxt thm)
+val _ = tracing (string_of_thm_no_vars ctxt thm)
 in
 Seq.single thm
 end*}
 text_raw {*
 @{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 in Subgoal} 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
+To see what happens, use the function defined in Figure~\ref{fig:sptac}, which
-takes a record and just prints out the content of this record (using the
+takes a record and just prints out the contents of this record. Consider
-string transformation functions from in Section~\ref{sec:printing}). Consider
 now the proof:
 *}
 text_raw{*
 \begin{figure}[t]
 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 (map fst (snd schematics))
-val _ = (writeln ("params: " ^ string_of_params);
+val _ = (tracing ("params: " ^ string_of_params);
-writeln ("schematics: " ^ string_of_schms);
+tracing ("schematics: " ^ string_of_schms);
-writeln ("assumptions: " ^ string_of_asms);
+tracing ("assumptions: " ^ string_of_asms);
-writeln ("conclusion: " ^ string_of_concl);
+tracing ("conclusion: " ^ string_of_concl);
-writeln ("premises: " ^ string_of_prems))
+tracing ("premises: " ^ string_of_prems))
 in
 all_tac
 end*}
 text_raw{*
 The tactic produces the following printout:
 \begin{quote}\small
 \begin{tabular}{ll}
 params:      & @{term x}, @{term y}\\
-schematics:  & @{term z}\\
+schematics:  & @{text ?z}\\
 assumptions: & @{term "A x y"}\\
 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)
+(FIXME: Find out how nowadays the schematics are handled)
-Notice in the actual output the brown colour of the variables @{term x} and
+Notice in the actual output the brown colour of the variables @{term x},
-@{term y}. Although they are parameters in the original goal, they are fixed inside
+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.
+the tactic. By convention these fixed variables are printed in brown colour.
-Similarly the schematic variable @{term z}. The assumption, or premise,
+Similarly the schematic variable @{text ?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}.
 If we continue the proof script by applying the @{text impI}-rule
 *}
 then the tactic prints out:
 \begin{quote}\small
 \begin{tabular}{ll}
 params:      & @{term x}, @{term y}\\
-schematics:  & @{term z}\\
+schematics:  & @{text ?z}\\
 assumptions: & @{term "A x y"}, @{term "B y x"}\\
 conclusion:  & @{term "C (z y) x"}\\
 premises:    & @{term "A x y"}, @{term "B y x"}
 \end{tabular}
 \end{quote}
 (*<*)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 in Subgoal} is that the former
+The difference between the tactics @{ML SUBPROOF} and @{ML FOCUS in Subgoal}
-expects that the goal is solved completely, which the latter does not.  One
+is that the former expects that the goal is solved completely, which the
-convenience of both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} is that we can apply the
+latter does not. @{ML SUBPROOF} can also not instantiate an schematic
-assumptions using the usual tactics, because the parameter @{text prems}
+variables.
-contains them as theorems. With this you can easily implement a tactic that
-behaves almost like @{ML atac}:
+One 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
-ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*}
+a tactic that behaves almost like @{ML atac}:
+*}
+ML{*val atac' = Subgoal.FOCUS (fn {prems, ...} => resolve_tac prems 1)*}
 text {*
 If you apply @{ML atac'} to the next lemma
 *}
 txt{* it will produce
 @{subgoals [display]} *}
 (*<*)oops(*>*)
 text {*
-The restriction in this tactic which is not present in @{ML atac} is that it
+Notice that @{ML atac'} inside @{ML FOCUS in Subgoal} calls @{ML
-cannot instantiate any schematic variables. This might be seen as a defect,
+resolve_tac} with the subgoal number @{text "1"} and also the outer call to
-but it is actually an advantage in the situations for which @{ML SUBPROOF}
+@{ML FOCUS in Subgoal} in the \isacommand{apply}-step uses @{text "1"}. This
-was designed: the reason is that, as mentioned before, instantiation of
+is another advantage of @{ML FOCUS in Subgoal} and @{ML SUBPROOF}: the
-schematic variables can affect several goals and can render them
+addressing inside it is completely local to the tactic inside the
-unprovable. @{ML SUBPROOF} is meant to avoid this.
+subproof. It is therefore possible to also apply @{ML atac'} to the second
+goal by just writing:
-Notice that @{ML atac'} inside @{ML SUBPROOF} calls @{ML resolve_tac} with
-the subgoal number @{text "1"} and also the outer call to @{ML SUBPROOF} in
-the \isacommand{apply}-step uses @{text "1"}. This is another advantage of
-@{ML SUBPROOF}: the addressing inside it is completely local to the tactic
-inside the subproof. It is therefore possible to also apply @{ML atac'} to
-the second goal by just writing:
 *}
 lemma shows "True" and "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
 apply(tactic {* atac' @{context} 2 *})
 apply(rule TrueI)
 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 in Subgoal} are
+Similar but less powerful functions than @{ML FOCUS in Subgoal}, respectively
+@{ML SUBPROOF}, 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
 val s = ["Simplification rules:"] @ map name_thm simps @
 ["Congruences rules:"] @ map name_thm congs @
 ["Simproc patterns:"] @ map name_ctrm procs
 in
 s |> cat_lines
-|> writeln
+|> tracing
 end*}
 text_raw {*
 \end{isabelle}
 \end{minipage}
 \caption{The function @{ML [index] dest_ss in Simplifier} returns a record containing
 *}
 ML %linenosgray{*fun fail_simproc simpset redex =
 let
 val ctxt = Simplifier.the_context simpset
-val _ = writeln ("The redex: " ^ (string_of_cterm ctxt redex))
+val _ = tracing ("The redex: " ^ (string_of_cterm ctxt redex))
 in
 NONE
 end*}
 text {*
 *}
 ML{*fun fail_simproc' simpset redex =
 let
 val ctxt = Simplifier.the_context simpset
-val _ = writeln ("The redex: " ^ (Syntax.string_of_term ctxt redex))
+val _ = tracing ("The redex: " ^ (Syntax.string_of_term ctxt redex))
 in
 NONE
 end*}
 text {*

changeset 301	2728e8daebc0
parent 299	d0b81d6e1b28
child 302	0cbd34857b9e