isabelle-cookbook: comparison ProgTutorial/Tactical.thy

equal deleted inserted replaced

-:79202e2eab6a
+:de49d5780f57
 (that is @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the
 assumptions @{text As} (happens to be empty) with the variables
 @{text xs} that will be generalised once the goal is proved (in our case
 @{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal;
 it can make use of the local assumptions (there are none in this example).
-The tactics @{ML [index] etac}, @{ML [index] rtac} and @{ML [index] atac} in the code above correspond
+The tactics @{ML_ind [index] etac}, @{ML_ind [index] rtac} and @{ML_ind [index] atac}
+in the code above correspond
 roughly to @{text erule}, @{text rule} and @{text assumption}, respectively.
-The operator @{ML [index] THEN} strings the tactics together.
+The operator @{ML_ind [index] THEN} strings the tactics together.
 \begin{readmore}
-To learn more about the function @{ML [index] prove in Goal} see \isccite{sec:results}
+To learn more about the function @{ML_ind [index] prove in Goal} see \isccite{sec:results}
 and the file @{ML_file "Pure/goal.ML"}.  See @{ML_file
 "Pure/tactic.ML"} and @{ML_file "Pure/tactical.ML"} for the code of basic
 tactics and tactic combinators; see also Chapters 3 and 4 in the old
 Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation Manual.
 \end{readmore}
 THEN' atac
 THEN' rtac @{thm disjI1}
 THEN' atac)*}text_raw{*\label{tac:footacprime}*}
 text {*
-where @{ML [index] THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give
+where @{ML_ind [index] THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give
 the number for the subgoal explicitly when the tactic is
 called. So in the next proof you can first discharge the second subgoal, and
 subsequently the first.
 *}
 By convention, if a tactic fails, then it should return the empty sequence.
 Therefore, if you write your own tactics, they  should not raise exceptions
 willy-nilly; only in very grave failure situations should a tactic raise the
 exception @{text THM}.
-The simplest tactics are @{ML [index] no_tac} and @{ML [index] all_tac}. The first returns
+The simplest tactics are @{ML_ind [index] no_tac} and @{ML_ind [index] all_tac}. The first returns
 the empty sequence and is defined as
 *}
 ML{*fun no_tac thm = Seq.empty*}
 *}
 section {* Simple Tactics\label{sec:simpletacs} *}
 text {*
-Let us start with explaining the simple tactic @{ML [index] print_tac}, which is quite useful
+Let us start with explaining the simple tactic @{ML_ind [index] print_tac}, which is quite useful
 for low-level debugging of tactics. It just prints out a message and the current
 goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state
 as the user would see it.  For example, processing the proof
 *}
 *}
 (*<*)oops(*>*)
 text {*
 A simple tactic for easy discharge of any proof obligations is
-@{ML [index] cheat_tac in SkipProof}. This tactic corresponds to
+@{ML_ind [index] cheat_tac in SkipProof}. This tactic corresponds to
 the Isabelle command \isacommand{sorry} and is sometimes useful
 during the development of tactics.
 *}
 lemma shows "False" and "Goldbach_conjecture"
 text {*
 This tactic works however only if the quick-and-dirty mode of Isabelle
 is switched on.
-Another simple tactic is the function @{ML [index] atac}, which, as shown in the previous
+Another simple tactic is the function @{ML_ind [index] atac}, which, as shown in the previous
 section, corresponds to the assumption command.
 *}
 lemma shows "P \<Longrightarrow> P"
 apply(tactic {* atac 1 *})
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-Similarly, @{ML [index] rtac}, @{ML [index] dtac}, @{ML [index] etac} and
+Similarly, @{ML_ind [index] rtac}, @{ML_ind [index] dtac}, @{ML_ind [index] etac} and
-@{ML [index] ftac} correspond (roughly)
+@{ML_ind [index] ftac} correspond (roughly)
 to @{text rule}, @{text drule}, @{text erule} and @{text frule},
 respectively. Each of them takes a theorem as argument and attempts to
 apply it to a goal. Below are three self-explanatory examples.
 *}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-The function @{ML [index] resolve_tac} is similar to @{ML [index] rtac}, except that it
+The function @{ML_ind [index] resolve_tac} is similar to @{ML_ind [index] rtac}, except that it
 expects a list of theorems as arguments. 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
 *}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
 Similar versions taking a list of theorems exist for the tactics
-@{ML dtac} (@{ML [index] dresolve_tac}), @{ML etac}
+@{ML dtac} (@{ML_ind [index] dresolve_tac}), @{ML etac}
-(@{ML [index] eresolve_tac}) and so on.
+(@{ML_ind [index] eresolve_tac}) and so on.
-Another simple tactic is @{ML [index] cut_facts_tac}. It inserts a list of theorems
+Another simple tactic is @{ML_ind [index] cut_facts_tac}. It inserts a list of theorems
 into the assumptions of the current goal state. For example
 *}
 lemma shows "True \<noteq> False"
 apply(tactic {* cut_facts_tac [@{thm True_def}, @{thm False_def}] 1 *})
 applied to the first subgoal might instantiate this meta-variable in such a
 way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"}
 should be, then this situation can be avoided by introducing a more
 constrained version of the @{text bspec}-rule. Such constraints can be given by
 pre-instantiating theorems with other theorems. One function to do this is
-@{ML [index] RS}
+@{ML_ind [index] "RS"}
 @{ML_response_fake [display,gray]
 "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
 which in the example instantiates the first premise of the @{text conjI}-rule
 @{ML_response_fake_both [display,gray]
 "@{thm conjI} RS @{thm mp}"
 "*** Exception- THM (\"RSN: no unifiers\", 1,
 [\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}
-then the function raises an exception. The function @{ML [index] RSN} is similar to @{ML RS}, but
+then the function raises an exception. The function @{ML_ind [index] RSN} is similar to @{ML RS}, but
 takes an additional number as argument that makes explicit which premise
 should be instantiated.
 To improve readability of the theorems we shall produce below, we will use the
 function @{ML no_vars} from Section~\ref{sec:printing}, which transforms
 @{ML_response_fake [display,gray]
 "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"}
 If you want to instantiate more than one premise of a theorem, you can use
-the function @{ML [index] MRS}:
+the function @{ML_ind [index] MRS}:
 @{ML_response_fake [display,gray]
 "no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})"
 "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> (Pa \<or> Q)"}
 If you need to instantiate lists of theorems, you can use the
-functions @{ML RL} and @{ML [index] MRL}. For example in the code below,
+functions @{ML RL} and @{ML_ind [index] MRL}. For example in the code below,
 every theorem in the second list is instantiated with every
 theorem in the first.
 @{ML_response_fake [display,gray]
 "map (no_vars @{context})
 \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 in Subgoal} and
+safety is provided by the functions @{ML_ind [index] FOCUS in Subgoal} and
-@{ML [index] SUBPROOF}. These tactics fix the parameters
+@{ML_ind [index] SUBPROOF}. These tactics fix the parameters
 and bind the various components of a goal state to a record.
 To see what happens, use the function defined in Figure~\ref{fig:sptac}, which
 takes a record and just prints out the contents of this record. Consider
 now the proof:
 *}
 \isccite{sec:results}.
 \end{readmore}
 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
+@{ML_ind [index] SUBGOAL} and @{ML_ind [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
 it is consistently applied to the component tactics.
 For most tactic combinators such a ``primed'' version exists and
 in what follows we will usually prefer it over the ``unprimed'' one.
 If there is a list of tactics that should all be tried out in
-sequence, you can use the combinator @{ML [index] EVERY'}. For example
+sequence, you can use the combinator @{ML_ind [index] EVERY'}. For example
 the function @{ML foo_tac'} from page~\pageref{tac:footacprime} can also
 be written as:
 *}
 ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2},
 atac, rtac @{thm disjI1}, atac]*}
 text {*
 and call @{ML foo_tac1}.
-With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML [index] EVERY1} it must be
+With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML_ind [index] EVERY1} it must be
 guaranteed that all component tactics successfully apply; otherwise the
 whole tactic will fail. If you rather want to try out a number of tactics,
-then you can use the combinator @{ML [index] ORELSE'} for two tactics, and @{ML
+then you can use the combinator @{ML_ind [index] ORELSE'} for two tactics, and @{ML_ind
-[index] FIRST'} (or @{ML [index] FIRST1}) for a list of tactics. For example, the tactic
+[index] FIRST'} (or @{ML_ind [index] FIRST1}) for a list of tactics. For example, the tactic
 *}
 ML{*val orelse_xmp_tac = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
 (*<*)oops(*>*)
 text {*
 Since such repeated applications of a tactic to the reverse order of
 \emph{all} subgoals is quite common, there is the tactic combinator
-@{ML [index] ALLGOALS} that simplifies this. Using this combinator you can simply
+@{ML_ind [index] ALLGOALS} that simplifies this. Using this combinator you can simply
 write: *}
 lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
 apply(tactic {* ALLGOALS select_tac' *})
 txt{* \begin{minipage}{\textwidth}
 (*<*)oops(*>*)
 text {*
 Remember that we chose to implement @{ML select_tac'} so that it
 always  succeeds by adding @{ML all_tac} at the end of the tactic
-list. The same can be achieved with the tactic combinator @{ML [index] TRY}.
+list. The same can be achieved with the tactic combinator @{ML_ind [index] TRY}.
 For example:
 *}
 ML{*val select_tac'' = TRY o FIRST' [rtac @{thm conjI}, rtac @{thm impI},
 rtac @{thm notI}, rtac @{thm allI}]*}
 To comply with this convention, we could simply delete the @{ML "K all_tac"}
 from the end of the theorem list. As a result @{ML select_tac'} would only
 succeed on goals where it can make progress. But for the sake of argument,
 let us suppose that this deletion is \emph{not} an option. In such cases, you can
-use the combinator @{ML [index] CHANGED} to make sure the subgoal has been changed
+use the combinator @{ML_ind [index] CHANGED} to make sure the subgoal has been changed
 by the tactic. Because now
 *}
 lemma shows "E \<Longrightarrow> F"
 text {*
 We can further extend @{ML select_tac'} so that it not just applies to the topmost
 connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal
-completely. For this you can use the tactic combinator @{ML [index] REPEAT}. As an example
+completely. For this you can use the tactic combinator @{ML_ind [index] REPEAT}. As an example
 suppose the following tactic
 *}
 ML{*val repeat_xmp_tac = REPEAT (CHANGED (select_tac' 1)) *}
 text {*
 Here it is crucial that @{ML select_tac'} is prefixed with @{ML CHANGED},
 because otherwise @{ML REPEAT} runs into an infinite loop (it applies the
 tactic as long as it succeeds). The function
-@{ML [index] REPEAT1} is similar, but runs the tactic at least once (failing if
+@{ML_ind [index] REPEAT1} is similar, but runs the tactic at least once (failing if
 this is not possible).
 If you are after the ``primed'' version of @{ML repeat_xmp_tac}, then you
 can implement it as
 *}
 If you look closely at the goal state above, then you see the tactics @{ML repeat_xmp_tac}
 and @{ML repeat_xmp_tac'} are not yet quite what we are after: the problem is
 that goals 2 and 3 are not analysed. This is because the tactic
 is applied repeatedly only to the first subgoal. To analyse also all
-resulting subgoals, you can use the tactic combinator @{ML [index] REPEAT_ALL_NEW}.
+resulting subgoals, you can use the tactic combinator @{ML_ind [index] REPEAT_ALL_NEW}.
 Suppose the tactic
 *}
 ML{*val repeat_all_new_xmp_tac = REPEAT_ALL_NEW (CHANGED o select_tac')*}
 text {*
 Sometimes this leads to confusing behaviour of tactics and also has
 the potential to explode the search space for tactics.
 These problems can be avoided by prefixing the tactic with the tactic
-combinator @{ML [index] DETERM}.
+combinator @{ML_ind [index] DETERM}.
 *}
 lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
 apply(tactic {* DETERM (etac @{thm disjE} 1) *})
 txt {*\begin{minipage}{\textwidth}
 ML{*val select_tac''' = TRY o select_tac''*}
 text {*
 then the tactic @{ML select_tac''} will be tried out and any failure is harnessed.
 We again have to use the construction with \mbox{@{text "TRY o ..."}} since there is
-no primed version of @{ML [index] TRY}. The tactic combinator @{ML [index] TRYALL} will try out
+no primed version of @{ML_ind [index] TRY}. The tactic combinator @{ML_ind [index] TRYALL} will try out
 a tactic on all subgoals. For example the tactic
 *}
 ML{*val triv_tac = TRYALL (rtac @{thm TrueI} ORELSE' etac @{thm FalseE})*}
 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_ind [index] COND} and COND')
 (FIXME: PARALLEL-CHOICE PARALLEL-GOALS)
 \begin{readmore}
 Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}.
 Implement a tactic that explores all possibilites of applying these rules to
 a propositional formula until a goal state is reached in which all subgoals
 are discharged.  Note that in Isabelle the left-rules need to be implemented
 as elimination rules. You need to prove separate lemmas corresponding to
 $\longrightarrow_{L_{1..4}}$.  In order to explore all possibilities of applying
-the rules, use the tactic combinator @{ML [index] DEPTH_SOLVE}, which searches
+the rules, use the tactic combinator @{ML_ind [index] DEPTH_SOLVE}, which searches
 for a state in which all subgoals are solved. Add also rules for equality and
 run your tactic on the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}.
 \end{exercise}
 *}
 the simplifier (in parentheses is their user-level counterpart):
 \begin{isabelle}
 \begin{center}
 \begin{tabular}{l@ {\hspace{2cm}}l}
-@{ML [index] simp_tac}            & @{text "(simp (no_asm))"} \\
+@{ML_ind [index] simp_tac}            & @{text "(simp (no_asm))"} \\
-@{ML [index] asm_simp_tac}        & @{text "(simp (no_asm_simp))"} \\
+@{ML_ind [index] asm_simp_tac}        & @{text "(simp (no_asm_simp))"} \\
-@{ML [index] full_simp_tac}       & @{text "(simp (no_asm_use))"} \\
+@{ML_ind [index] full_simp_tac}       & @{text "(simp (no_asm_use))"} \\
-@{ML [index] asm_lr_simp_tac}     & @{text "(simp (asm_lr))"} \\
+@{ML_ind [index] asm_lr_simp_tac}     & @{text "(simp (asm_lr))"} \\
-@{ML [index] asm_full_simp_tac}   & @{text "(simp)"}
+@{ML_ind [index] asm_full_simp_tac}   & @{text "(simp)"}
 \end{tabular}
 \end{center}
 \end{isabelle}
 All of the tactics take a simpset and an integer as argument (the latter as usual
 The most common combinators to modify simpsets are:
 \begin{isabelle}
 \begin{tabular}{ll}
-@{ML [index] addsimps}    & @{ML [index] delsimps}\\
+@{ML_ind [index] addsimps}    & @{ML_ind [index] delsimps}\\
-@{ML [index] addcongs}    & @{ML [index] delcongs}\\
+@{ML_ind [index] addcongs}    & @{ML_ind [index] delcongs}\\
-@{ML [index] addsimprocs} & @{ML [index] delsimprocs}\\
+@{ML_ind [index] addsimprocs} & @{ML_ind [index] delsimprocs}\\
 \end{tabular}
 \end{isabelle}
 (FIXME: What about splitters? @{ML addsplits}, @{ML delsplits})
 *}
 |> tracing
 end*}
 text_raw {*
 \end{isabelle}
 \end{minipage}
-\caption{The function @{ML [index] dest_ss in Simplifier} returns a record containing
+\caption{The function @{ML_ind [index] dest_ss in Simplifier} returns a record containing
 all printable information stored in a simpset. We are here only interested in the
 simplification rules, congruence rules and simprocs.\label{fig:printss}}
 \end{figure} *}
 text {*
 To see how they work, consider the function in Figure~\ref{fig:printss}, which
 prints out some parts of a simpset. If you use it to print out the components of the
-empty simpset, i.e., @{ML [index] empty_ss}
+empty simpset, i.e., @{ML_ind [index] empty_ss}
 @{ML_response_fake [display,gray]
 "print_ss @{context} empty_ss"
 "Simplification rules:
 Congruences rules:
 Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss}
 expects this form of the simplification and congruence rules. However, even
 when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet.
-In the context of HOL, the first really useful simpset is @{ML [index] HOL_basic_ss}. While
+In the context of HOL, the first really useful simpset is @{ML_ind [index] HOL_basic_ss}. While
 printing out the components of this simpset
 @{ML_response_fake [display,gray]
 "print_ss @{context} HOL_basic_ss"
 "Simplification rules:
 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 [index] HOL_basic_ss}.
+and looper are set up in @{ML_ind [index] HOL_basic_ss}.
-The simpset @{ML [index] HOL_ss} is an extension of @{ML HOL_basic_ss} containing
+The simpset @{ML_ind [index] HOL_ss} is an extension of @{ML HOL_basic_ss} containing
 already many useful simplification and congruence rules for the logical
 connectives in HOL.
 @{ML_response_fake [display,gray]
 "print_ss @{context} HOL_ss"
 Simproc patterns:
 \<dots>"}
 The simplifier is often used to unfold definitions in a proof. For this the
-simplifier implements the tactic @{ML [index] rewrite_goals_tac}.\footnote{FIXME:
+simplifier implements the tactic @{ML_ind [index] rewrite_goals_tac}.\footnote{FIXME:
 see LocalDefs infrastructure.} Suppose for example the
 definition
 *}
 definition "MyTrue \<equiv> True"
 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 [index] addsimprocs} to a simpset whenever
+@{ML_ind [index] addsimprocs} to a simpset whenever
 needed.
 Simprocs are applied from inside to outside and from left to right. You can
 see this in the proof
 *}
 ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t
 | dest_suc_trm t = snd (HOLogic.dest_number t)*}
 text {*
-It uses the library function @{ML [index] dest_number in HOLogic} that transforms
+It uses the library function @{ML_ind [index] dest_number in HOLogic} that transforms
 (Isabelle) terms, like @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so
 on, into integer values. This function raises the exception @{ML TERM}, if
 the term is not a number. The next function expects a pair consisting of a term
 @{text t} (containing @{term Suc}s) and the corresponding integer value @{text n}.
 *}
 ML{*type conv = cterm -> thm*}
 text {*
 whereby the produced theorem is always a meta-equality. A simple conversion
-is the function @{ML [index] all_conv in Conv}, which maps a @{ML_type cterm} to an
+is the function @{ML_ind [index] all_conv in Conv}, which maps a @{ML_type cterm} to an
 instance of the (meta)reflexivity theorem. For example:
 @{ML_response_fake [display,gray]
 "Conv.all_conv @{cterm \"Foo \<or> Bar\"}"
 "Foo \<or> Bar \<equiv> Foo \<or> Bar"}
-Another simple conversion is @{ML [index] no_conv in Conv} which always raises the
+Another simple conversion is @{ML_ind [index] no_conv in Conv} which always raises the
 exception @{ML CTERM}.
 @{ML_response_fake [display,gray]
 "Conv.no_conv @{cterm True}"
 "*** Exception- CTERM (\"no conversion\", []) raised"}
-A more interesting conversion is the function @{ML [index] beta_conversion in Thm}: it
+A more interesting conversion is the function @{ML_ind [index] beta_conversion in Thm}: it
 produces a meta-equation between a term and its beta-normal form. For example
 @{ML_response_fake [display,gray]
 "let
 val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
 @{ML false} is given, then only a single beta-reduction is performed
 on the outer-most level.
 The main point of conversions is that they can be used for rewriting
 @{ML_type cterm}s. One example is the function
-@{ML [index] rewr_conv in Conv}, which expects a meta-equation as an
+@{ML_ind [index] rewr_conv in Conv}, which expects a meta-equation as an
 argument. Suppose the following meta-equation.
 *}
 lemma true_conj1: "True \<and> P \<equiv> P" by simp
 in
 Conv.rewr_conv @{thm true_conj1} ctrm
 end"
 "True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"}
-Note, however, that the function @{ML [index] rewr_conv in Conv} only rewrites the
+Note, however, that the function @{ML_ind [index] rewr_conv in Conv} only rewrites the
 outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match
 exactly the
-left-hand side of the theorem, then  @{ML [index] rewr_conv in Conv} fails, raising
+left-hand side of the theorem, then  @{ML_ind [index] 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 [index] then_conv},
+combinators. The simplest conversion combinator is @{ML_ind [index] then_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 [index] else_conv} tries out the
+The conversion combinator @{ML_ind [index] else_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 [index] try_conv in Conv} constructs a conversion
+The conversion combinator @{ML_ind [index] 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 [index] fun_conv in Conv}
+will lift this restriction. The combinators @{ML_ind [index] fun_conv in Conv}
-and @{ML [index] arg_conv in Conv} will apply
+and @{ML_ind [index] 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
 arguments.  Therefore the term must be of the form @{text "(Const \<dots> $ t1) $ t2"}. The
 conversion is then applied to @{text "t2"}, which in the example above
 stands for @{term "True \<and> Q"}. The function @{ML fun_conv in Conv} would apply
 the conversion to the term @{text "(Const \<dots> $ t1)"}.
-The function @{ML [index] abs_conv in Conv} applies a conversion under an
+The function @{ML_ind [index] abs_conv in Conv} applies a conversion under an
 abstraction. For example:
 @{ML_response_fake [display,gray]
 "let
 val conv = Conv.rewr_conv @{thm true_conj1}
 Note that this conversion needs a context as an argument. We also give the
 conversion as @{text "(K conv)"}, which is a function that ignores its
 argument (the argument being a sufficiently freshened version of the
 variable that is abstracted and a context). The conversion that goes under
-an application is @{ML [index] combination_conv in Conv}. It expects two
+an application is @{ML_ind [index] combination_conv in Conv}. It expects two
 conversions as arguments, each of which is applied to the corresponding
 ``branch'' of the application. An abbreviation for this conversion is the
-function @{ML [index] comb_conv in Conv}, which applies the same conversion
+function @{ML_ind [index] comb_conv in Conv}, which applies the same conversion
 to both branches.
 We can now apply all these functions in a conversion that recursively
 descends a term and applies a ``@{thm [source] true_conj1}''-conversion
 in all possible positions.
 \<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False"}
 *}
 text {*
 So far we only applied conversions to @{ML_type cterm}s. Conversions can, however,
-also work on theorems using the function @{ML [index] fconv_rule in Conv}. As an example,
+also work on theorems using the function @{ML_ind [index] fconv_rule in Conv}. As an example,
 consider the conversion @{ML all_true1_conv} and the lemma:
 *}
 lemma foo_test: "P \<or> (True \<and> \<not>P)" by simp
 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 [index] CONVERSION},
+goal states. This can be done with the help of the function @{ML_ind [index] CONVERSION},
 and also some predefined conversion combinators that traverse a goal
 state. The combinators for the goal state are:
 \begin{itemize}
-\item @{ML [index] params_conv in Conv} for converting under parameters
+\item @{ML_ind [index] 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 [index] prems_conv in Conv} for applying a conversion to all
+\item @{ML_ind [index] prems_conv in Conv} for applying a conversion to all
 premises of a goal, and
-\item @{ML [index] concl_conv in Conv} for applying a conversion to the
+\item @{ML_ind [index] 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.

changeset 315	de49d5780f57
parent 314	79202e2eab6a
child 316	74f0a06f751f