isabelle-cookbook: comparison ProgTutorial/Tactical.thy

equal deleted inserted replaced

-:b1a458a03a8e
+:74ba778b09c9
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-The function @{ML_ind  resolve_tac} is similar to @{ML rtac}, except that it
+The function @{ML_ind resolve_tac in Tactic} is similar to @{ML rtac}, except that it
 expects a list of theorems as argument. From this list it will apply the
 first applicable theorem (later theorems that are also applicable can be
 explored via the lazy sequences mechanism). Given the code
 *}
 \isccite{sec:results}.
 \end{readmore}
 Similar but less powerful functions than @{ML FOCUS in Subgoal}, respectively
 @{ML SUBPROOF}, are
-@{ML_ind  SUBGOAL} and @{ML_ind  CSUBGOAL}. They allow you to
+@{ML_ind SUBGOAL in Tactical} and @{ML_ind CSUBGOAL in Tactical}. 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 them 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
 @{text "*** back: no alternatives"}\\
 @{text "*** At command \"back\"."}
 \end{isabelle}
-\footnote{\bf FIXME: say something about @{ML_ind  COND} and COND'}
+\footnote{\bf FIXME: say something about @{ML_ind COND in Tactical} and COND'}
 \footnote{\bf FIXME: PARALLEL-CHOICE PARALLEL-GOALS}
 \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"}.
 apply(tactic {* ALLGOALS (simp_tac HOL_basic_ss) *})
 done
 text {*
 This behaviour is not because of simplification rules, but how the subgoaler, solver
-and looper are set up in @{ML_ind HOL_basic_ss}.
+and looper are set up in @{ML HOL_basic_ss}.
 The simpset @{ML_ind HOL_ss} is an extension of @{ML HOL_basic_ss} containing
 already many useful simplification and congruence rules for the logical
 connectives in HOL.
 text {*
 Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
 The function also takes a list of patterns that can trigger the simproc.
 Now the simproc is set up and can be explicitly added using
-@{ML_ind  addsimprocs} to a simpset whenever
+@{ML_ind addsimprocs in MetaSimplifier} to a simpset whenever
 needed.
 Simprocs are applied from inside to outside and from left to right. You can
 see this in the proof
 *}
 left-hand side of the theorem, then  @{ML_ind  rewr_conv in Conv} fails, raising
 the exception @{ML CTERM}.
 This very primitive way of rewriting can be made more powerful by
 combining several conversions into one. For this you can use conversion
-combinators. The simplest conversion combinator is @{ML_ind  then_conv},
+combinators. The simplest conversion combinator is @{ML_ind then_conv in Conv},
 which applies one conversion after another. For example
 @{ML_response_fake [display,gray]
 "let
 val conv1 = Thm.beta_conversion false
 where we first beta-reduce the term and then rewrite according to
 @{thm [source] true_conj1}. (When running this example recall the
 problem with the pretty-printer normalising all terms.)
-The conversion combinator @{ML_ind  else_conv} tries out the
+The conversion combinator @{ML_ind else_conv in Conv} tries out the
 first one, and if it does not apply, tries the second. For example
 @{ML_response_fake [display,gray]
 "let
 val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv
 Here the conversion of @{thm [source] true_conj1} only applies
 in the first case, but fails in the second. The whole conversion
 does not fail, however, because the combinator @{ML else_conv in Conv} will then
 try out @{ML all_conv in Conv}, which always succeeds.
-The conversion combinator @{ML_ind  try_conv in Conv} constructs a conversion
+The conversion combinator @{ML_ind try_conv in Conv} constructs a conversion
 which is tried out on a term, but in case of failure just does nothing.
 For example
 @{ML_response_fake [display,gray]
 "let
 "True \<or> P \<equiv> True \<or> P"}
 Apart from the function @{ML beta_conversion in Thm}, which is able to fully
 beta-normalise a term, the conversions so far are restricted in that they
 only apply to the outer-most level of a @{ML_type cterm}. In what follows we
-will lift this restriction. The combinators @{ML_ind  fun_conv in Conv}
+will lift this restriction. The combinators @{ML_ind fun_conv in Conv}
-and @{ML_ind  arg_conv in Conv} will apply
+and @{ML_ind arg_conv in Conv} will apply
 a conversion to the first, respectively second, argument of an application.
 For example
 @{ML_response_fake [display,gray]
 "let
 conv thm
 end"
 "?P \<or> \<not> ?P"}
 Finally, conversions can also be turned into tactics and then applied to
-goal states. This can be done with the help of the function @{ML_ind  CONVERSION},
+goal states. This can be done with the help of the function
+@{ML_ind CONVERSION in Tactical},
 and also some predefined conversion combinators that traverse a goal
 state. The combinators for the goal state are:
 \begin{itemize}
-\item @{ML_ind  params_conv in Conv} for converting under parameters
+\item @{ML_ind params_conv in Conv} for converting under parameters
 (i.e.~where goals are of the form @{text "\<And>x. P x \<Longrightarrow> Q x"})
-\item @{ML_ind  prems_conv in Conv} for applying a conversion to all
+\item @{ML_ind prems_conv in Conv} for applying a conversion to all
 premises of a goal, and
-\item @{ML_ind  concl_conv in Conv} for applying a conversion to the
+\item @{ML_ind concl_conv in Conv} for applying a conversion to the
 conclusion of a goal.
 \end{itemize}
 Assume we want to apply @{ML all_true1_conv} only in the conclusion
 of the goal, and @{ML if_true1_conv} should only apply to the premises.
 text {*
 In Line 3 we destruct the meta-equality into the @{ML_type cterm}s
 corresponding to the left-hand and right-hand side of the meta-equality. The
 assumption in @{ML unabs_def} is that the right-hand side is an
 abstraction. We compute the possibly empty list of abstracted variables in
-Line 4 using the function @{ML_ind strip_abs_vars}. For this we have to
+Line 4 using the function @{ML_ind strip_abs_vars in Term}. For this we have to
 transform the @{ML_type cterm} into a @{ML_type term}. In Line 5 we
 importing these variables into the context @{ML_text ctxt'}, in order to
 export them again in Line 15.  In Line 8 we certify the list of variables,
 which in turn we apply to the @{ML_text lhs} of the definition using the
 function @{ML_ind list_comb in Drule}. In Line 11 and 12 we generate the

changeset 369	74ba778b09c9
parent 368	b1a458a03a8e
child 370	2494b5b7a85d