isabelle-cookbook: comparison CookBook/Tactical.thy

equal deleted inserted replaced

-:fe10da5354a3
+:5dcad9348e4d
 lemma "P \<or> Q \<Longrightarrow> Q \<or> P"
 apply(tactic {* foo_tac *})
 done
 text {*
-By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} in the apply-step,
+By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} you can call from the
-you can call from the user level of Isabelle the tactic @{ML foo_tac} or
+user level of Isabelle the tactic @{ML foo_tac} or
 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
 sequences. However in day-to-day Isabelle programming, one rarely
 constructs sequences explicitly, but uses the predefined functions
 instead.
 \end{readmore}
-For a beginner it might be surprising that tactics, which transform
+It might be surprising that tactics, which transform
 one proof state to the next, are functions from theorems to theorem
 (sequences). The surprise resolves by knowing that every
-proof state is indeed a theorem. To shed more light on this,
+goal state is indeed a theorem. To shed more light on this,
 let us modify the code of @{ML all_tac} to obtain the following
 tactic
 *}
 ML{*fun my_print_tac ctxt thm =
 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
 side we show the goal state as shown by the system; on the right-hand
-side the print out from our @{ML my_print_tac}.
+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} *})
 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. Since the goal @{term C} can potentially be an implication,
+subgoals. So in the first step the goal state is always of the form
-there is a protector (invisible in the print out above) wrapped around
+@{text "C \<Longrightarrow> (C)"}. Since the goal @{term C} can potentially be an implication,
-it. This prevents that premises are misinterpreted as open subgoals.
+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.
 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.
 *}
 done
 text {*
 Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond
 to @{text rule}, @{text drule}, @{text erule} and @{text frule},
-respectively. Below are three examples with the resulting goal state. How
+respectively. Each of them takes a theorem as argument. Below are three
-they work should therefore be self-explanatory.
+examples with the resulting goal state. How
+they work should be self-explanatory.
 *}
 lemma shows "P \<and> Q"
 apply(tactic {* rtac @{thm conjI} 1 *})
-txt{*@{subgoals [display]}*}
+txt{*\begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage}*}
 (*<*)oops(*>*)
 lemma shows "P \<and> Q \<Longrightarrow> False"
 apply(tactic {* etac @{thm conjE} 1 *})
-txt{*@{subgoals [display]}*}
+txt{*\begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage}*}
 (*<*)oops(*>*)
 lemma shows "False \<and> True \<Longrightarrow> False"
 apply(tactic {* dtac @{thm conjunct2} 1 *})
-txt{*@{subgoals [display]}*}
+txt{*\begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage}*}
 (*<*)oops(*>*)
 text {*
 As mentioned above, most basic tactics take a number as argument, which
 addresses to subgoal they are analysing.
 *}
 lemma shows "Foo" and "P \<and> Q"
 apply(tactic {* rtac @{thm conjI} 2 *})
-txt {*@{subgoals [display]}*}
+txt {*\begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage}*}
 (*<*)oops(*>*)
 text {*
 Corresponding to @{ML rtac}, there is also the tactic @{ML resolve_tac}, which
 however expects a list of theorems as arguments. From this list it will apply with
 *}
 lemma shows "C \<longrightarrow> (A \<and> B)" and "(A \<longrightarrow> B) \<and> C"
 apply(tactic {* resolve_tac_xmp 1 *})
 apply(tactic {* resolve_tac_xmp 2 *})
-txt{* @{subgoals [display]} *}
+txt{*\begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage}*}
 (*<*)oops(*>*)
 text {*
 Similarly versions exists for @{ML atac} (@{ML assume_tac}), @{ML etac}
 (@{ML eresolve_tac}) and so on.
 lemma shows "False \<Longrightarrow> True"
 apply(tactic {* print_tac "foo message" *})
 (*<*)oops(*>*)
 text {*
-Also for useful for debugging purposes are the tactics @{ML all_tac} and
-@{ML no_tac}. The former always succeeds (but does not change the goal state), and
-the latter always fails.
 (FIXME explain RS MRS)
-Often proofs involve elaborate operations on assumptions and variables
+Often proofs involve elaborate operations on assumptions and
-@{text "\<And>"}-quantified in the goal state. To do such operations on the ML-level
+@{text "\<And>"}-quantified variables. To do such operations on the ML-level
-using the basic tactics, is very unwieldy and brittle. Some convenience and
+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.
 *}
 text_raw{*
 \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
 the subproof. Similarly the schematic variable @{term z}. The assumption
-is bound once as @{ML_type cterm} to the record-variable @{text asms} and
+@{prop "A x y"} is bound once as @{ML_type cterm} to the record-variable
-another time as @{ML_type thm} to @{text prems}.
+@{text asms} and another time 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
 in a graceful manner so that the warning messages are not overwritten
-by the error message.
+by an error message.
 If we continue the proof script by applying the @{text impI}-rule
 *}
 apply(rule impI)
 \end{quote}
 *}
 (*<*)oops(*>*)
 text {*
-where we now also have @{term "B y x"} as assumption.
+where we now also have @{term "B y x"} as an assumption.
 One convenience of @{ML SUBPROOF} is that we can apply assumption
 using the usual tactics, because the parameter @{text prems}
 contains the assumptions as theorems. With this we can easily
 implement a tactic that almost behaves like @{ML atac}:
 *}
+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
+apply(tactic {* atac' @{context} 1 *})
-{* SUBPROOF (fn {prems, ...} => resolve_tac prems 1) @{context} 1 *})
 txt{* yields
 @{subgoals [display]} *}
 (*<*)oops(*>*)
 text {*
 The restriction in this tactic is that it cannot instantiate any
 schematic variables. This might be seen as a defect, but is actually
 an advantage in the situations for which @{ML SUBPROOF} was designed:
-the reason is that instantiation of schematic variables can potentially
+the reason is that instantiation of schematic variables can affect
-has affect several goals and can render them unprovable.
+several goals and can render them unprovable. @{ML SUBPROOF} is meant
+to avoid this.
-A similar but less powerful function is @{ML SUBGOAL}. It allows you to
-inspect a subgoal specified by a number.
+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
+@{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:
+@{subgoals [display]} *}
+(*<*)oops(*>*)
+text {*
+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
+implement a little tactic that applies a rule corresponding to its
+topmost connective. The tactic should only apply ``safe'' rules (that is
+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 \<and>"} $ _ $ _ => rtac @{thm conjI} i
 | @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i
 | @{term "Not"} $ _ => rtac @{thm notI} i
 | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i
-| _ => no_tac*}
+| _ => all_tac*}
-lemma shows "A \<and> B" "A \<longrightarrow> B" "\<forall>x. C x"
+lemma shows "A \<and> B" "A \<longrightarrow> B" "\<forall>x. C x" "D \<Longrightarrow> E"
+apply(tactic {* SUBGOAL select_tac 4 *})
+apply(tactic {* SUBGOAL select_tac 3 *})
+apply(tactic {* SUBGOAL select_tac 2 *})
 apply(tactic {* SUBGOAL select_tac 1 *})
-apply(tactic {* SUBGOAL select_tac 3 *})
-apply(tactic {* SUBGOAL select_tac 4 *})
 txt{* @{subgoals [display]} *}
 (*<*)oops(*>*)
 text {*
 However, this example is contrived, as there are much simpler ways
 to implement a proof procedure like the one above. They will be explained
 in the next section.
+(Notice that we applied the goals in reverse order)
 A variant of @{ML SUBGOAL} is @{ML CSUBGOAL} which allows access to the goal
 as @{ML_type cterm} instead of a @{ML_type term}.
 *}

changeset 104	5dcad9348e4d
parent 102	5e309df58557
child 105	f49dc7e96235