isabelle-cookbook: comparison ProgTutorial/Tactical.thy

equal deleted inserted replaced

-:a5e7ab090abf
+:f7f1d8a98098
 considerably lessen the burden of manual reasoning. They are centred around
 the idea of refining a goal state using tactics. This is similar to the
 \isacommand{apply}-style reasoning at the user-level, where goals are
 modified in a sequence of proof steps until all of them are discharged.
 In this chapter we will explain simple tactics and how to combine them using
-tactic combinators. We also explain briefly the simplifier and conversions.
+tactic combinators. We also describe the simplifier, simprocs and conversions.
 *}
 section {* Basics of Reasoning with Tactics*}
 "let
 val ctxt = @{context}
 val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
 in
 Goal.prove ctxt [\"P\", \"Q\"] [] goal
-(fn _ =>
+(fn _ =>  etac @{thm disjE} 1
-etac @{thm disjE} 1
+THEN rtac @{thm disjI2} 1
-THEN rtac @{thm disjI2} 1
+THEN atac 1
-THEN atac 1
+THEN rtac @{thm disjI1} 1
-THEN rtac @{thm disjI1} 1
+THEN atac 1)
-THEN atac 1)
 end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
 To start the proof, the function @{ML_ind prove in Goal} sets up a goal
 state for proving the goal @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. We can give this
 function some assumptions in the third argument (there are no assumption in
 the proof at hand). The second argument stands for a list of variables
 (given as strings). This list contains the variables that will be turned
 into schematic variables once the goal is proved (in our case @{text P} and
 @{text Q}). The last argument is the tactic that proves the goal. This
 tactic can make use of the local assumptions (there are none in this
-example). The tactics @{ML_ind etac}, @{ML_ind rtac} and @{ML_ind atac} in
+example). The tactics @{ML_ind etac in Tactic}, @{ML_ind rtac in Tactic} and
-the code above correspond roughly to @{text erule}, @{text rule} and @{text
+@{ML_ind atac in Tactic} in the code above correspond roughly to @{text
-assumption}, respectively. The combinator @{ML_ind THEN} strings the tactics
+erule}, @{text rule} and @{text assumption}, respectively. The combinator
-together.
+@{ML THEN} strings the tactics together.
 \begin{readmore}
 To learn more about the function @{ML_ind 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
 Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation
 Manual.
 \end{readmore}
 Note that in the code above we use antiquotations for referencing the
-theorems. We  could also just have written @{ML "etac disjE 1"}. The reason
+theorems. We  could also just have written @{ML "etac disjE 1"} because
-is that many of the basic theorems have a corresponding ML-binding:
+many of the basic theorems have a corresponding ML-binding:
 @{ML_response_fake [gray,display]
 "disjE"
 "\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"}
-In case where there is no ML-binding theorems can also be obtained dynamically using
+In case where no ML-binding exists, theorems can also be looked up dynamically
-the function @{ML thm} and the (string) name of the theorem; for example:
+using the function @{ML thm} and the (string) name of the theorem. For example:
 @{ML_response_fake [gray,display]
 "thm \"disjE\""
 "\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"}
-Both ways however are considered bad style! The reason is that the binding
+Both ways however are considered \emph{bad} style! The reason is that the binding
-for @{ML disjE} can be re-assigned by the user and thus one does not have
+for @{ML disjE} can be re-assigned and thus one does not have
 complete control over which theorem is actually applied. Similarly with the
-string @{text [quotes] "disjE"}. Although theorems in the theorem database
+lookup of @{text [quotes] "disjE"}. Although theorems must have a unique name
-must have a unique name, the string can stand for a dynamically updated
+in the theorem database, the string can stand for a dynamically updatable
 theorem list. Also in this case we cannot be sure which theorem is applied.
 These problems can be nicely prevented by using antiquotations, because then
 the theorems are fixed statically at compile-time.
 THEN' atac
 THEN' rtac @{thm disjI1}
 THEN' atac)*}text_raw{*\label{tac:footacprime}*}
 text {*
-where @{ML_ind THEN'} is used instead of @{ML THEN}. (For most combinators
+where @{ML_ind THEN' in Tactical} is used instead of @{ML THEN in
-that combine tactics---@{ML THEN} is only one such combinator---a ``primed''
+Tactical}. (For most combinators that combine tactics---@{ML THEN} is only
-version exists.)  With @{ML foo_tac'} you can give the number for the
+one such combinator---a ``primed'' version exists.)  With @{ML foo_tac'} you
-subgoal explicitly when the tactic is called. So in the next proof you can
+can give the number for the subgoal explicitly when the tactic is called. So
-first discharge the second subgoal, and subsequently the first.
+in the next proof you can first discharge the second subgoal, and
+subsequently the first.
 *}
 lemma
 shows "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1"
 and   "P2 \<or> Q2 \<Longrightarrow> Q2 \<or> P2"
 hard-coded inside the tactic.
 The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for analysing
 goals being only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not of
 this form, then these tactics return the error message:\footnote{To be
-precise, tactics do not produce this error message, it originates from the
+precise, tactics do not produce this error message; the message originates from the
-\isacommand{apply} wrapper.}
+\isacommand{apply} wrapper that calls the tactic.}
 \begin{isabelle}
 @{text "*** empty result sequence -- proof command failed"}\\
 @{text "*** At command \"apply\"."}
 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_ind  no_tac} and @{ML_ind  all_tac}. The first returns
+The simplest tactics are @{ML_ind no_tac in Tactical} and
-the empty sequence and is defined as
+@{ML_ind all_tac in Tactical}. The first returns the empty sequence and
+is defined as
 *}
 ML{*fun no_tac thm = Seq.empty*}
 text {*
 let
 val _ = tracing (string_of_thm_no_vars ctxt thm)
 in
 Seq.single thm
 end*}
+text {*
+which prints out the given theorem (using the string-function defined in
+Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. With this
+tactic we are in the position to inspect every goal state in a proof. For
+this consider the proof in Figure~\ref{fig:goalstates}: as can be seen,
+internally every goal state is an implication of the form
+@{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #C"}
+where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are
+the subgoals. So after setting up the lemma, the goal state is always of the
+form @{text "C \<Longrightarrow> #C"}; when the proof is finished we are left with @{text
+"#C"}. Since the goal @{term C} can potentially be an implication, there is a
+``protector'' wrapped around it (the wrapper is the outermost constant
+@{text "Const (\"prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible
+as a @{text #}). This wrapper prevents that premises of @{text C} are
+misinterpreted as open subgoals. While tactics can operate on the subgoals
+(the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
+@{term C} intact, with the exception of possibly instantiating schematic
+variables. This instantiations of schematic variables can be observed
+on the user level. Have a look at the following definition and proof.
+*}
 text_raw {*
 \begin{figure}[p]
 \begin{boxedminipage}{\textwidth}
 \begin{isabelle}
 you finish the proof the theorem is @{text "#(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and>
 B)"}.\label{fig:goalstates}}
 \end{figure}
 *}
-text {*
-which prints out the given theorem (using the string-function defined in
-Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. With this
-tactic we are in the position to inspect every goal state in a proof. For
-this consider the proof in Figure~\ref{fig:goalstates}: as can be seen,
-internally every goal state is an implication of the form
-@{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #C"}
-where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are
-the subgoals. So after setting up the lemma, the goal state is always of the
-form @{text "C \<Longrightarrow> #C"}; when the proof is finished we are left with @{text
-"#C"}. Since the goal @{term C} can potentially be an implication, there is a
-``protector'' wrapped around it (the wrapper is the outermost constant
-@{text "Const (\"prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible
-as an @{text #}). This wrapper prevents that premises of @{text C} are
-misinterpreted as open subgoals. While tactics can operate on the subgoals
-(the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
-@{term C} intact, with the exception of possibly instantiating schematic
-variables. This instantiations of schematic variables can be observed
-on the user level. Have a look at the following definition and proof.
-*}
 definition
 EQ_TRUE
 where
 "EQ_TRUE X \<equiv> (X = True)"
 lemma test:
 shows "EQ_TRUE ?X"
 unfolding EQ_TRUE_def
 by (rule refl)
 text {*
 Although Isabelle issues a warning message when stating goals involving
 meta-variables, it is possible to prove this theorem. The reason for the warning
 message is that the proved theorem is not @{text "EQ_TRUE ?X"}, as one might
 \isacommand{thm}~@{thm [source] test}\\
 @{text ">"}~@{thm test}
 \end{isabelle}
 The reason for this result is that the schematic variable @{text "?X"}
-is instantiated inside the proof and then the instantiation propagated
+is instantiated inside the proof to be @{term True} and then the
-to the ``outside''.
+instantiation propagated to the ``outside''.
 \begin{readmore}
 For more information about the internals of goals see \isccite{sec:tactical-goals}.
 \end{readmore}
 *}
 section {* Simple Tactics\label{sec:simpletacs} *}
 text {*
-In this section we will describe more of the simple tactics in Isabelle. The
+In this section we will introduce more simple tactics. The
-first one is @{ML_ind  print_tac}, which is quite useful
+first one is @{ML_ind print_tac in Tactical}, 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
 *}
 \end{minipage}
 *}
 (*<*)oops(*>*)
 text {*
-A simple tactic for easy discharge of any proof obligations is
+A simple tactic for easy discharge of any proof obligations, even difficult ones, is
-@{ML_ind  cheat_tac in Skip_Proof} in the structure @{ML_struct Skip_Proof}.
+@{ML_ind cheat_tac in Skip_Proof} in the structure @{ML_struct Skip_Proof}.
 This tactic corresponds to the Isabelle command \isacommand{sorry} and is
 sometimes useful during the development of tactics.
 *}
 lemma
 (*<*)oops(*>*)
 text {*
 This tactic works however only if the quick-and-dirty mode of Isabelle
 is switched on. This is done automatically in the ``interactive
-mode'' of Isabelle, but must ne done manually in the ``batch mode''.
+mode'' of Isabelle, but must be done manually in the ``batch mode''
+with for example the assignment
-Another simple tactic is the function @{ML_ind  atac}, which, as shown
+*}
+ML{*quick_and_dirty := true*}
+text {*
+Another simple tactic is the function @{ML_ind atac in Tactic}, which, as shown
 earlier, corresponds to the assumption method.
 *}
 lemma
 shows "P \<Longrightarrow> P"
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-Similarly, @{ML_ind  rtac}, @{ML_ind  dtac}, @{ML_ind  etac} and
+Similarly, @{ML_ind rtac in Tactic}, @{ML_ind dtac in Tactic}, @{ML_ind etac
-@{ML_ind  ftac} correspond (roughly)
+in Tactic} and @{ML_ind ftac in Tactic} correspond (roughly) to @{text
-to @{text rule}, @{text drule}, @{text erule} and @{text frule},
+rule}, @{text drule}, @{text erule} and @{text frule}, respectively. Each of
-respectively. Each of them takes a theorem as argument and attempts to
+them takes a theorem as argument and attempts to apply it to a goal. Below
-apply it to a goal. Below are three self-explanatory examples.
+are three self-explanatory examples.
 *}
 lemma
 shows "P \<and> Q"
 apply(tactic {* rtac @{thm conjI} 1 *})
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-The function @{ML_ind  resolve_tac} is similar to @{ML_ind  rtac}, except that it
+The function @{ML_ind  resolve_tac} is similar to @{ML rtac}, except that it
-expects a list of theorems as arguments. From this list it will apply the
+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
 *}
 ML{*val resolve_xmp_tac = resolve_tac [@{thm impI}, @{thm conjI}]*}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
 Similar versions taking a list of theorems exist for the tactics
-@{ML dtac} (@{ML_ind  dresolve_tac}), @{ML etac}
+@{ML dtac} (@{ML_ind dresolve_tac in Tactic}), @{ML etac}
-(@{ML_ind  eresolve_tac}) and so on.
+(@{ML_ind eresolve_tac in Tactic}) and so on.
+Another simple tactic is @{ML_ind cut_facts_tac in Tactic}. It inserts a
-Another simple tactic is @{ML_ind  cut_facts_tac}. It inserts a list of theorems
+list of theorems into the assumptions of the current goal state. Below we
-into the assumptions of the current goal state. Below we will insert the definitions
+will insert the definitions for the constants @{term True} and @{term
-for the constants @{term True} and @{term False}. So
+False}. So
 *}
 lemma
 shows "True \<noteq> False"
 apply(tactic {* cut_facts_tac [@{thm True_def}, @{thm False_def}] 1 *})
 text {*
 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_ind  FOCUS in Subgoal} and
+safety is provided by the functions @{ML_ind FOCUS in Subgoal} and
-@{ML_ind  SUBPROOF}. These tactics fix the parameters
+@{ML_ind SUBPROOF in Subgoal}. These tactics fix the parameters
 and bind the various components of a goal state to a record.
 To see what happens, suppose the function defined in Figure~\ref{fig:sptac}, which
-takes a record and just prints out the contents of this record. Consider
+takes a record and just prints out the contents of this record. Then consider
-now the proof:
+the proof:
 *}
-ML {* Subgoal.FOCUS *}
 text_raw{*
 \begin{figure}[t]
 \begin{minipage}{\textwidth}
 \begin{isabelle}
 conclusion:  & @{term "B y x \<longrightarrow> C (z y) x"}\\
 premises:    & @{term "A x y"}
 \end{tabular}
 \end{quote}
-The @{text params} and @{text schematics} stand or list of pairs where the left-hand
+The @{text params} and @{text schematics} stand or list of pairs where the
-side of @{text ":="} is replaced by the right-hand side inside the tactic.
+left-hand side of @{text ":="} is replaced by the right-hand side inside the
-Notice that in the actual output the brown colour of the variables @{term x},
+tactic.  Notice that in the actual output the variables @{term x} and @{term
-and @{term y}. Although they are parameters in the original goal, they are fixed inside
+y} have a brown colour. Although they are parameters in the original goal,
-the tactic. By convention these fixed variables are printed in brown colour.
+they are fixed inside the tactic. By convention these fixed variables are
-Similarly the schematic variable @{text ?z}. The assumption, or premise,
+printed in brown colour.  Similarly the schematic variable @{text ?z}. The
-@{prop "A x y"} is bound as @{ML_type cterm} to the record-variable
+assumption, or premise, @{prop "A x y"} is bound as @{ML_type cterm} to the
-@{text asms}, but also as @{ML_type thm} to @{text prems}.
+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
 *}
 apply(rule impI)
 text {*
 Now also @{term "B y x"} is an assumption bound to @{text asms} and @{text prems}.
 One difference between the tactics @{ML SUBPROOF} and @{ML FOCUS in Subgoal}
 is that the former expects that the goal is solved completely, which the
-latter does not. Another is that @{ML SUBPROOF} can not instantiate any schematic
+latter does not. Another is that @{ML SUBPROOF} cannot instantiate any schematic
 variables.
 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
 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
 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
+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
 follows.
 *}
 analyse. Otherwise goals like @{prop "A \<and> B"} are not properly
 analysed. Similarly with meta-implications in the next line.  While for the
 first five patterns we can use the @{text "@term"}-antiquotation to
 construct the patterns, the pattern in Line 8 cannot be constructed in this
 way. The reason is that an antiquotation would fix the type of the
-quantified variable. So you really have to construct the pattern using the
+quantified variable. So you really have to construct this pattern using the
-basic term-constructors. This is not necessary in other cases, because their
+basic term-constructors. This is not necessary in the other cases, because their
 type is always fixed to function types involving only the type @{typ
 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.
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 text {*
-where in all but the last the tactic applied an introduction rule.
+where in all but the last the tactic applies an introduction rule.
 Note that we applied the tactic to the goals in ``reverse'' order.
 This is a trick in order to be independent from the subgoals that are
 produced by the rule. If we had applied it in the other order
 *}
 Of course, this example is
 contrived: there are much simpler methods available in Isabelle for
 implementing a tactic analysing a goal according to its topmost
 connective. These simpler methods use tactic combinators, which we will
-explain in the next section, but before that we will show how
+explain in the next section. But before that we will show how
-tactic application can be constraint.
+tactic application can be constrained.
 Since rules are applied using higher-order unification, an automatic proof
 procedure might become too fragile, if it just applies inference rules as
-shown above. The reason is that a number of rules introduce meta-variables
+shown above. The reason is that a number of rules introduce schematic variables
 into the goal state. Consider for example the proof
 *}
 lemma
 shows "\<forall>x \<in> A. P x \<Longrightarrow> Q x"
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
 where the application of rule @{text bspec} generates two subgoals involving the
-meta-variable @{text "?x"}. Now, if you are not careful, tactics
+schematic variable @{text "?x"}. Now, if you are not careful, tactics
-applied to the first subgoal might instantiate this meta-variable in such a
+applied to the first subgoal might instantiate this schematic 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. One way to give such
 constraints is by pre-instantiating theorems with other theorems.
-The function @{ML_ind "RS"}, for example, does this.
+The function @{ML_ind RS in Drule}, for example, does this.
 @{ML_response_fake [display,gray]
 "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
 In this example it 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_ind  RSN} is similar to @{ML RS}, but
+then the function raises an exception. The function @{ML_ind  RSN in Drule}
-takes an additional number as argument that makes explicit which premise
+is similar to @{ML RS}, but takes an additional number as argument. This
-should be instantiated.
+number 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
 schematic variables into free ones.  Using this function for the first @{ML
 RS}-expression above produces the more readable result:
 @{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_ind  MRS}:
+the function @{ML_ind MRS in Drule}:
 @{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_ind  MRL}. For example in the code below,
+functions @{ML_ind RL in Drule} and @{ML_ind MRL in Drule}. For
-every theorem in the second list is instantiated with every
+example in the code below, every theorem in the second list is
-theorem in the first.
+instantiated with every theorem in the first.
 @{ML_response_fake [display,gray]
-"map (no_vars @{context})
+"let
-([@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}])"
+val list1 = [@{thm impI}, @{thm disjI2}]
+val list2 = [@{thm conjI}, @{thm disjI1}]
+in
+map (no_vars @{context}) (list1 RL list2)
+end"
 "[\<lbrakk>P \<Longrightarrow> Q; Qa\<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) \<and> Qa,
 \<lbrakk>Q; Qa\<rbrakk> \<Longrightarrow> (P \<or> Q) \<and> Qa,
 (P \<Longrightarrow> Q) \<Longrightarrow> (P \<longrightarrow> Q) \<or> Qa,
 Q \<Longrightarrow> (P \<or> Q) \<or> Qa]"}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-As you can see this is unfortunately \emph{not} the case. The problem is
+As you can see this is unfortunately \emph{not} the case if we apply @{thm [source]
+cong} with the method @{text rule}. The problem is
 that higher-order unification produces an instantiation that is not the
 intended one. While we can use \isacommand{back} to interactively find the
 intended instantiation, this is not an option for an automatic proof
 procedure. Fortunately, the tactic @{ML_ind cong_tac in Cong_Tac} helps
 with applying congruence rules and finding the intended instantiation.
+For example
 *}
 lemma
 fixes x y u w::"'a"
 shows "t x y = s u w"
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-However, sometimes it is necessary to expicitly match a theroem against a proof
+However, frequently it is necessary to explicitly match a theorem against a proof
-state and in doing so finding manually an appropriate instantiation. Imagine
+state and in doing so construct manually an appropriate instantiation. Imagine
 you have the theorem
 *}
 lemma rule:
 shows "\<lbrakk>f = g; x = y\<rbrakk> \<Longrightarrow> R (f x) (g y)"
 sorry
 text {*
 and you want to apply it to the goal @{term "(t\<^isub>1 t\<^isub>2) \<le>
-(s\<^isub>1 s\<^isub>2)"}. Since in this theorem, all variables are
+(s\<^isub>1 s\<^isub>2)"}. Since in the theorem all variables are
 schematic, we have a nasty higher-order unification problem and @{text rtac}
-will not be able to apply this rule as we want. However, in the proof below
+will not be able to apply this rule in the way we want. For the goal at hand
-we are only interested where @{term R} is instantiated to a constant and
+we want to use it so that @{term R} is instantiated to the constant @{text \<le>} and
-similarly the instantiation for the other variables is ``obvious'' from the
+similarly ``obvious'' instantiations for the other variables.  To achieve this
-proof state.  To use this rule we essentially match the conclusion of
+we need to match the conclusion of
-@{thm [source] rule} against the goal state reading of an instantiation for
+@{thm [source] rule} against the goal reading off an instantiation for
 @{thm [source] rule}. For this the function @{ML_ind first_order_match in Thm}
-matches two @{ML_type cterm}s and produces, in the sucessful case, a matcher
+matches two @{ML_type cterm}s and produces, in the successful case, a matcher
-that can be used to instantiate the @{thm [source] rule}. The instantiation
+that can be used to instantiate the theorem. The instantiation
 can be done with the function @{ML_ind instantiate in Drule}. To automate
 this we implement the following function.
 *}
-ML{*fun fo_rtac thm =
+ML %linenosgray{*fun fo_rtac thm = Subgoal.FOCUS (fn {concl, ...} =>
-Subgoal.FOCUS (fn {concl, ...} =>
 let
 val concl_pat = Drule.strip_imp_concl (cprop_of thm)
 val insts = Thm.first_order_match (concl_pat, concl)
 in
 rtac (Drule.instantiate insts thm) 1
 end)*}
 text {*
-Note that we use @{ML FOCUS in Subgoal} because we have directly access
+Note that we use @{ML FOCUS in Subgoal} because it gives us directly access
-to the conclusion of the goal state and also because this function also
+to the conclusion of the goal state, but also because this function
-takes care about correctly handling parameters that might be present
+takes care of correctly handling parameters that might be present
-in the goal state. An example for @{ML fo_rtac} is as follows.
+in the goal state. In Line 3 we use the function @{ML_ind strip_imp_concl in Drule}
+for calculating the conclusion of a theorem (produced as @{ML_type cterm}).
+An example of @{ML fo_rtac} is as follows.
 *}
 lemma
 shows "\<And>t\<^isub>1 s\<^isub>1 (t\<^isub>2::'a) (s\<^isub>2::'a). (t\<^isub>1 t\<^isub>2) \<le> (s\<^isub>1 s\<^isub>2)"
 apply(tactic {* fo_rtac @{thm rule} @{context} 1 *})
 (*<*)oops(*>*)
 text {*
 We obtain the intended subgoals and also the parameters are correctly
 introduced in both of them. Such manual instantiations are quite frequently
-necessary in order to contrain the application of inference rules. Otherwise
+necessary in order to appropriately constrain the application of inference
-one ends up with ``wild'' higher-order unification problems that make
+rules. Otherwise one would end up with ``wild'' higher-order unification
-automatic proofs fails.
+problems that make automatic proofs fail.
 *}
 section {* Tactic Combinators *}
 text {*
 The purpose of tactic combinators is to build compound tactics out of
-smaller tactics. In the previous section we already used @{ML THEN}, which
+smaller tactics. In the previous section we already used @{ML_ind THEN in Tactical},
-just strings together two tactics in a sequence. For example:
+which just strings together two tactics in a sequence. For example:
 *}
 lemma
 shows "(Foo \<and> Bar) \<and> False"
 apply(tactic {* rtac @{thm conjI} 1 THEN rtac @{thm conjI} 1 *})
 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_ind  EVERY'}. For example
+sequence, you can use the combinator @{ML_ind  EVERY' in Tactical}. 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_ind  EVERY1} it must be
+With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML_ind  EVERY1 in Tactical} 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_ind  ORELSE'} for two tactics, and @{ML_ind
+then you can use the combinator @{ML_ind  ORELSE' in Tactical} for two tactics, and @{ML_ind
-FIRST'} (or @{ML_ind  FIRST1}) for a list of tactics. For example, the tactic
+FIRST' in Tactical} (or @{ML_ind  FIRST1 in Tactical}) 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_ind  ALLGOALS} that simplifies this. Using this combinator you can simply
+@{ML_ind  ALLGOALS in Tactical} 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' *})
 (*<*)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_ind  TRY}.
+list. The same can be achieved with the tactic combinator @{ML_ind  TRY in Tactical}.
 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_ind  CHANGED} to make sure the subgoal has been changed
+use the combinator @{ML_ind  CHANGED in Tactical} to make sure the subgoal has been changed
 by the tactic. Because now
 *}
 lemma
 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_ind  REPEAT}. As an example
+completely. For this you can use the tactic combinator @{ML_ind  REPEAT in Tactical}. 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_ind  REPEAT1} is similar, but runs the tactic at least once (failing if
+@{ML_ind  REPEAT1 in Tactical} 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_ind  REPEAT_ALL_NEW}.
+resulting subgoals, you can use the tactic combinator @{ML_ind  REPEAT_ALL_NEW in Tactical}.
 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_ind  DETERM}.
+combinator @{ML_ind  DETERM in Tactical}.
 *}
 lemma
 shows "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
 apply(tactic {* DETERM (etac @{thm disjE} 1) *})
 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_ind  DEPTH_SOLVE}, which searches
+the rules, use the tactic combinator @{ML_ind  DEPTH_SOLVE in Search}, 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}
-\footnote{\bf FIXME: explain @{ML_ind Cong_Tac.cong_tac}}
 *}
 section {* Simplifier Tactics *}
 text {*
 val this = r OF this;
 val this = Assumption.export false ctxt ctxt0 this
 val this = Variable.export ctxt ctxt0 [this]
 *}
+text {*
+If a tactic should fail, return the empty sequence.
+*}
 end

changeset 363	f7f1d8a98098
parent 362	a5e7ab090abf
child 368	b1a458a03a8e