isabelle-cookbook: comparison CookBook/Tactical.thy

equal deleted inserted replaced

-:5dcad9348e4d
+:f49dc7e96235
 begin
 chapter {* Tactical Reasoning\label{chp:tactical} *}
 text {*
+The main reason for descending to the ML-level of Isabelle is to be able to
-The main reason for descending to the ML-level of Isabelle is to be
+implement automatic proof procedures. Such proof procedures usually lessen
-able to implement automatic proof procedures. Such proof procedures usually
+considerably the burden of manual reasoning, for example, when introducing
-lessen considerably the burden of manual reasoning, for example, when
+new definitions. These proof procedures are centred around refining a goal
-introducing new definitions. These proof procedures are centred around
+state using tactics. This is similar to the \isacommand{apply}-style
-refining a goal state using tactics. This is similar to the @{text
+reasoning at the user level, where goals are modified in a sequence of proof
-apply}-style reasoning at the user level, where goals are modified in a
+steps until all of them are solved. However, there are also more structured
-sequence of proof steps until all of them are solved. However, there are
+operations available on the ML-level that help with the handling of
-also more structured operations available on the ML-level that help with
+variables and assumptions.
-the handling of variables and assumptions.
 *}
 section {* Basics of Reasoning with Tactics*}
 @{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 functions @{ML etac}, @{ML rtac} and @{ML atac} correspond to
 @{text erule}, @{text rule} and @{text assumption}, respectively.
-The operator @{ML THEN} strings the tactics together. A difference
+The operator @{ML THEN} strings the tactics together.
-between the \isacommand{apply}-script and the ML-code is that the
-former causes the lemma to be stored under the name @{text "disj_swap"},
-whereas the latter does not include any code for this.
 \begin{readmore}
 To learn more about the function @{ML Goal.prove} see \isccite{sec:results}
 and the file @{ML_file "Pure/goal.ML"}. For more information about the
 internals of goals see \isccite{sec:tactical-goals}.  See @{ML_file
 "Pure/tactic.ML"} and @{ML_file "Pure/tctical.ML"} for the code of basic
 tactics and tactic combinators; see also Chapters 3 and 4 in the old
 Isabelle Reference Manual.
 \end{readmore}
-Note that we used antiquotations for referencing the theorems. We could also
+Note that we used antiquotations for referencing the theorems. Many theorems
-just have written @{ML "etac disjE 1"} and so on, but this is considered bad
+also have ML-bindings with the same name. Therefore, we could also just have
-style. The reason is that the binding for @{ML disjE} can be re-assigned by
+written @{ML "etac disjE 1"}, or in case there are no ML-binding obtained
-the user and thus one does not have complete control over which theorem is
+the theorem dynamically using the theorem @{ML thm}; for example @{ML "etac
-actually applied. This problem is nicely prevented by using antiquotations,
+(thm \"disjE\") 1"}. Both ways however are considered bad style. The reason
-because then the theorems are fixed statically at compile-time.
+is that the binding for @{ML disjE} can be re-assigned by the user and thus
+one does not have complete control over which theorem is actually
+applied. This problem is nicely prevented by using antiquotations, because
+then the theorems are fixed statically at compile-time.
 During the development of automatic proof procedures, you will often find it
 necessary to test a tactic on examples. This can be conveniently
 done with the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}.
 Consider the following sequence of tactics
 any other function that returns a tactic.
 The tactic @{ML foo_tac} is just a sequence of simple tactics stringed
 together by @{ML THEN}. As can be seen, each simple tactic in @{ML foo_tac}
 has a hard-coded number that stands for the subgoal analysed by the
-tactic (@{text "1"} stands for the first, or top-most, subgoal). This is
+tactic (@{text "1"} stands for the first, or top-most, subgoal). This hard-coding
-sometimes wanted, but usually not. To avoid the explicit numbering in
+of goals is sometimes wanted, but usually it is not. To avoid the explicit numbering,
-the tactic, you can write
+you can write
 *}
 ML{*val foo_tac' =
 (etac @{thm disjE}
 THEN' rtac @{thm disjI2}
 THEN' rtac @{thm disjI1}
 THEN' atac)*}
 text {*
 and then give the number for the subgoal explicitly when the tactic is
-called. For every operator that combines tactics (@{ML THEN} is only one
+called. So in the next proof you can first discharge the second subgoal, and
-such operator), a primed version exists. So in the next proof you
+after that the first.
-can first discharge the second subgoal, and after that the first.
 *}
 lemma "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1"
 and "P2 \<or> Q2 \<Longrightarrow> Q2 \<or> P2"
 apply(tactic {* foo_tac' 2 *})
 apply(tactic {* foo_tac' 1 *})
 done
 text {*
 This kind of addressing is more difficult to achieve when the goal is
-hard-coded inside the tactic.
+hard-coded inside the tactic. For every operator that combines tactics
+(@{ML THEN} is only one such operator) a ``primed'' version exists.
 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 @{ML foo_tac} throws the error message:
+of this form, then they throw the error message:
 \begin{isabelle}
 @{text "*** empty result sequence -- proof command failed"}\\
 @{text "*** At command \"apply\"."}
 \end{isabelle}
-Meaning the tactic failed. The reason for this error message is that tactics
+Meaning the tactics failed. The reason for this error message is that tactics
 are functions that map a goal state to a (lazy) sequence of successor states,
 hence the type of a tactic is:
 @{text [display, gray] "type tactic = thm -> thm Seq.seq"}
 It is custom that if a tactic fails, it should return the empty sequence:
-your own tactics should not raise exceptions willy-nilly.
+therefore your own tactics should not raise exceptions willy-nilly.
 The simplest tactics are @{ML no_tac} and @{ML all_tac}. The first returns
 the empty sequence and is defined as
 *}
 text {*
 which means @{ML all_tac} always succeeds (but also does not make any progress
 with the proof).
-The lazy list of possible successor states shows through to the user-level
+The lazy list of possible successor states shows through at the user-level
 of Isabelle when using the command \isacommand{back}. For instance in the
 following proof, there are two possibilities for how to apply
 @{ML foo_tac'}.
 *}
 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}. We
-now can inspect every proof state in the follwing proof. On the left-hand
+now can inspect every proof state in a proof. Consider the proof below: on
-side we show the goal state as shown by the system; on the right-hand
+the left-hand side we show the goal state as shown by Isabelle; on the
-side the print out from @{ML my_print_tac}.
+right-hand side the print out from @{ML my_print_tac}.
 *}
 lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
 apply(tactic {* my_print_tac @{context} *})
 txt{* \small
 \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}}
 \begin{minipage}[t]{0.3\textwidth}
 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 in the first step the goal state is always of the form
+subgoals. So after setting up the lemma, the goal state is always of the form
 @{text "C \<Longrightarrow> (C)"}. Since the goal @{term C} can potentially be an implication,
 there is a ``protector'' wrapped around it (in from of an outermost constant
 @{text "Const (\"prop\", bool \<Rightarrow> bool)"} applied to each goal;
 however this constant is invisible in the print out above). This
-prevents that premises are misinterpreted as open subgoals.
+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.
 *}
 section {* Simple Tactics *}
 text {*
-As seen above, the function @{ML atac} corresponds to the assumption tactic.
+A simple tactic is @{ML print_tac}, which is useful for low-level debugging of tactics.
+It just prints out a message and the current goal state.
+*}
+lemma shows "False \<Longrightarrow> True"
+apply(tactic {* print_tac "foo message" *})
+(*<*)oops(*>*)
+text {*
+Another simple tactic is the function @{ML atac}, which, as shown in the previous
+section, corresponds to the assumption command.
 *}
 lemma shows "P \<Longrightarrow> P"
 apply(tactic {* atac 1 *})
 done
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-As mentioned above, most basic tactics take a number as argument, which
+As mentioned in the previous section, most basic tactics take a number as
-addresses to subgoal they are analysing.
+argument, which addresses the subgoal they are analysing. In the proof below,
+we first break up the second subgoal by focusing on this subgoal first.
 *}
 lemma shows "Foo" and "P \<and> Q"
 apply(tactic {* rtac @{thm conjI} 2 *})
 txt {*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-Corresponding to @{ML rtac}, there is also the tactic @{ML resolve_tac}, which
+The function @{ML resolve_tac} is similar to @{ML rtac}, except that it
-however expects a list of theorems as arguments. From this list it will apply with
+expects a list of theorems as arguments. From this list it will apply the
-the first applicable theorem (later theorems that are also applicable can be
+first applicable theorem (later theorems that are also applicable can be
-explored via the lazy sequences mechanism). Given the abbreviation
+explored via the lazy sequences mechanism). Given the code
 *}
 ML{*val resolve_tac_xmp = resolve_tac [@{thm impI}, @{thm conjI}]*}
 text {*
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
 Similarly versions exists for @{ML atac} (@{ML assume_tac}), @{ML etac}
 (@{ML eresolve_tac}) and so on.
-The tactic @{ML print_tac} is useful for low-level debugging of tactics: it
+(FIXME: @{ML cut_facts_tac})
-prints out a message and the current goal state.
-*}
+Since rules are applied using higher-order unification, an automatic proof
+procedure might become too fragile, if it just applies inference rules shown
-lemma shows "False \<Longrightarrow> True"
+in the fashion above.  More constraints can be introduced by
-apply(tactic {* print_tac "foo message" *})
+pre-instantiating theorems with other theorems. You can do this using the
-(*<*)oops(*>*)
+function @{ML RS}. For example
-text {*
-(FIXME explain RS MRS)
+@{ML_response_fake [display,gray]
+"@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
+instantiates the first premise of the @{text conjI}-rule with the
+rule @{text disjI1}. The function @{ML RSN} is similar, but
+takes a number and makes explicit which premise should be instantiated.
+To improve readability we are going use the following function
+*}
+ML{*fun no_vars ctxt thm =
+let
+val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt
+in
+thm'
+end*}
+text {*
+to transform the schematic variables of a theorem into free variables.
+This means for the @{ML RS}-expression above:
+@{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, you can use the function
+@{ML 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 MRL}. For example below every
+theorem in the first list is instantiated against every theorem
+in the second.
+@{ML_response_fake [display,gray]
+"[@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}]"
+"[\<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]"}
+\begin{readmore}
+The combinators for instantiating theorems are defined in @{ML_file "Pure/drule.ML"}.
+\end{readmore}
 Often proofs involve elaborate operations on assumptions and
 @{text "\<And>"}-quantified variables. To do such operations on the ML-level
 using the basic tactics is very unwieldy and brittle. Some convenience and
 safety is provided by the tactic @{ML SUBPROOF}. This tactic fixes the parameters
 and binds the various components of a proof state into a record.
+To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
+takes a record as argument and just prints out the content of this record (using the
+string transformation functions defined in Section~\ref{sec:printing}). Consider
+now the proof
 *}
 text_raw{*
 \begin{figure}
 \begin{isabelle}
 no_tac
 end*}
 text_raw{*
 \end{isabelle}
 \caption{A function that prints out the various parameters provided by the tactic
-@{ML SUBPROOF}. It uses the functions extracting strings from @{ML_type cterm}s
+@{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for
-and @{ML_type thm}s, which are defined in Section~\ref{sec:printing}.\label{fig:sptac}}
+extracting strings from @{ML_type cterm}s and @{ML_type thm}s.\label{fig:sptac}}
 \end{figure}
 *}
-text {*
-To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
-takes a record as argument and just prints out the content of this record (using the
-string transformation functions defined in Section~\ref{sec:printing}). Consider
-now the proof
-*}
 lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
 apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
 txt {*
 premises:    & @{term "A x y"}
 \end{tabular}
 \end{quote}
 Note in the actual output the brown colour of the variables @{term x} and
-@{term y}. Although parameters in the original goal, they are fixed inside
+@{term y}. Although they are parameters in the original goal, they are fixed inside
 the subproof. Similarly the schematic variable @{term z}. The assumption
-@{prop "A x y"} is bound once as @{ML_type cterm} to the record-variable
+@{prop "A x y"} is bound as @{ML_type cterm} to the record-variable
-@{text asms} and another time as @{ML_type thm} to @{text prems}.
+@{text asms} but also as @{ML_type thm} to @{text prems}.
 Notice also that we had to append @{text "?"} to \isacommand{apply}. The
 reason is that @{ML SUBPROOF} normally expects that the subgoal is solved completely.
 Since in the function @{ML sp_tac} we returned the tactic @{ML no_tac}, the subproof
 obviously fails. The question-mark allows us to recover from this failure
 (*<*)oops(*>*)
 text {*
 where we now also have @{term "B y x"} as an assumption.
-One convenience of @{ML SUBPROOF} is that we can apply assumption
+One convenience of @{ML SUBPROOF} is that we can apply the assumptions
 using the usual tactics, because the parameter @{text prems}
-contains the assumptions as theorems. With this we can easily
+contains them as theorems. With this we can easily
-implement a tactic that almost behaves like @{ML atac}:
+implement a tactic that almost behaves like @{ML atac}, namely:
 *}
 ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*}
 lemma shows "\<And>x y. \<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
 apply(tactic {* atac' @{context} 1 *})
 Notice that @{ML atac'} 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"}. Another advantage
 of @{ML SUBGOAL} is that the addressing  inside it is completely
-local to the proof inside. It is therefore possible to also apply
+local to the subproof inside. It is therefore possible to also apply
 @{ML atac'} to the second goal:
 *}
 lemma shows "True" and "\<And>x y. \<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
 apply(tactic {* atac' @{context} 2 *})
-txt{* This gives:
+apply(rule TrueI)
-@{subgoals [display]} *}
+done
-(*<*)oops(*>*)
+text {*
-text {*
+\begin{readmore}
+The function @{ML SUBPROOF} is defined in @{ML_file "Pure/subgoal.ML"} and
+also described in \isccite{sec:results}.
+\end{readmore}
 A similar but less powerful function than @{ML SUBPROOF} is @{ML SUBGOAL}.
-It allows you to inspect a subgoal specified by a number. With this we can
+It allows you to inspect a specified subgoal. With this you can implement
-implement a little tactic that applies a rule corresponding to its
+a tactic that applies a rule according to its topmost connective (we only
-topmost connective. The tactic should only apply ``safe'' rules (that is
+analyse a few connectives). The tactic is as follows:
-which do not render the goal unprovable). For this we can write:
 *}
 ML %linenumbers{*fun select_tac (t,i) =
 case t of
 @{term "Trueprop"} $ t' => select_tac (t',i)
 | @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i
 | @{term "Not"} $ _ => rtac @{thm notI} i
 | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i
 | _ => all_tac*}
-lemma shows "A \<and> B" "A \<longrightarrow> B" "\<forall>x. C x" "D \<Longrightarrow> E"
+text {*
+In line 3 you need to decend under the outermost @{term "Trueprop"} in order
+to get to the connective you like to analyse. Otherwise goals @{prop "A \<and> B"}
+are not bropek up. In line 7, the pattern cannot be constructed using the
+@{text "@term"}-antiquotation, because that would fix the type of the
+quantified variable. In this case you really have to construct the pattern
+by using the term-constructors. The other cases work, because their type
+is always bool. In case that the goal does not fall into any of the categorories,
+then we chose to just return @{ML all_tac} (i.e., the tactic never fails).
+Let us now see how to apply this tactic.
+*}
+lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
 apply(tactic {* SUBGOAL select_tac 4 *})
 apply(tactic {* SUBGOAL select_tac 3 *})
 apply(tactic {* SUBGOAL select_tac 2 *})
 apply(tactic {* SUBGOAL select_tac 1 *})
 txt{* @{subgoals [display]} *}
 (*<*)oops(*>*)
 text {*
-However, this example is contrived, as there are much simpler ways
+Note that we applied it in ``reverse'' order. This is a trick in
-to implement a proof procedure like the one above. They will be explained
+order to be independent from what subgoals the rule produced. If we had
-in the next section.
+it applied in the other order
+*}
-(Notice that we applied the goals in reverse order)
+lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
-A variant of @{ML SUBGOAL} is @{ML CSUBGOAL} which allows access to the goal
+apply(tactic {* SUBGOAL select_tac 1 *})
-as @{ML_type cterm} instead of a @{ML_type term}.
+apply(tactic {* SUBGOAL select_tac 3 *})
-*}
+apply(tactic {* SUBGOAL select_tac 4 *})
+apply(tactic {* SUBGOAL select_tac 5 *})
+(*<*)oops(*>*)
-section {* Operations on Tactics *}
+text {*
-text {* @{ML THEN} *}
+then we have to be careful to not apply the tactic to the two subgoals the
+first goal produced. This can be messy in an automated proof script. The
+reverse application, on the other hand, is easy to implement.
+However, this example is contrived: there are much simpler ways to implement
+such proof procedure that analyses a goal according to its topmost
+connective. They will be explained in the next section.
+*}
+section {* Tactic Combinators *}
+text {*
+To be able to implement powerful tactics out of smaller component tactics,
+Isabelle provides tactic combinators. In the previous section we already
+used @{ML THEN} which strings two tactics together in sequence. For example:
+*}
 lemma shows "(Foo \<and> Bar) \<and> False"
-apply(tactic {* (rtac @{thm conjI} 1)
+apply(tactic {* rtac @{thm conjI} 1 THEN rtac @{thm conjI} 1 *})
-THEN (rtac @{thm conjI} 1) *})
+txt {* \begin{minipage}{\textwidth}
-txt {* @{subgoals [display]} *}
+@{subgoals [display]}
-(*<*)oops(*>*)
+\end{minipage} *}
+(*<*)oops(*>*)
+text {*
+If you want to avoid the hard-coded subgoal addressing, then you can use
+@{ML THEN'}. For example:
+*}
+lemma shows "(Foo \<and> Bar) \<and> False"
+apply(tactic {* (rtac @{thm conjI} THEN' rtac @{thm conjI}) 1 *})
+txt {* \begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage} *}
+(*<*)oops(*>*)
+text {*
+For most tactic combinators such a ``primed'' version exists.
+In what follows we will, whenever appropriate, prefer the primed version of
+the tactic combinator and omit to mention the simple one.
+With @{ML THEN} and @{ML THEN'} it must be guaranteed that both tactics
+sucessfully apply; otherwise the whole tactic will fail. If you want to
+try out either one tactic, then you can use @{ML ORELSE'}. For
+example
+*}
 ML{*val orelse_xmp = (rtac @{thm disjI1} ORELSE' rtac @{thm conjI})*}
+text {*
+will first try out rule @{text disjI} and after that @{text conjI}.
+*}
 lemma shows "True \<and> False" and "Foo \<or> Bar"
 apply(tactic {* orelse_xmp 1 *})
 apply(tactic {* orelse_xmp 3 *})
 txt {* @{subgoals [display]} *}
 (*<*)oops(*>*)
 text {*
-@{ML EVERY} @{ML REPEAT} @{ML DETERM}
+applies
+@{ML REPEAT} @{ML DETERM}
+*}
+section {* Rewriting and Simplifier Tactics *}
+text {*
 @{ML rewrite_goals_tac}
-@{ML cut_facts_tac}
 @{ML ObjectLogic.full_atomize_tac}
 @{ML ObjectLogic.rulify_tac}
-@{ML resolve_tac}
+*}
-*}
 section {* Structured Proofs *}
 lemma True
 proof

changeset 105	f49dc7e96235
parent 104	5dcad9348e4d
child 107	258ce361ba1b