isabelle-cookbook: comparison ProgTutorial/Tactical.thy

equal deleted inserted replaced

-:8ba963a3e039
+:a5e7ab090abf
 (*>*)
 chapter {* Tactical Reasoning\label{chp:tactical} *}
 text {*
-One of the main reason for descending to the ML-level of Isabelle is to be able to
+One of 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 can
-considerably the burden of manual reasoning, for example, when introducing
+considerably lessen the burden of manual reasoning. They are centred around
-new definitions. These proof procedures are centred around refining a goal
+the idea of refining a goal state using tactics. This is similar to the
-state using tactics. This is similar to the \isacommand{apply}-style
+\isacommand{apply}-style reasoning at the user-level, where goals are
-reasoning at the user-level, where goals are modified in a sequence of proof
+modified in a sequence of proof steps until all of them are discharged.
-steps until all of them are solved. However, there are also more structured
+In this chapter we will explain simple tactics and how to combine them using
-operations available on the ML-level that help with the handling of
+tactic combinators. We also explain briefly the simplifier and conversions.
-variables and assumptions.
 *}
 section {* Basics of Reasoning with Tactics*}
 text {*
 To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof
 into ML. Suppose the following proof.
 *}
-lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
+lemma disj_swap:
+shows "P \<or> Q \<Longrightarrow> Q \<or> P"
 apply(erule disjE)
 apply(rule disjI2)
 apply(assumption)
 apply(rule disjI1)
 apply(assumption)
 THEN atac 1
 THEN rtac @{thm disjI1} 1
 THEN atac 1)
 end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
-To start the proof, the function @{ML_ind "Goal.prove"}~@{text "ctxt xs As C
+To start the proof, the function @{ML_ind prove in Goal} sets up a goal
-tac"} sets up a goal state for proving the goal @{text C} (that is @{prop "P
+state for proving the goal @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. We can give this
-\<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the assumptions @{text As}
+function some assumptions in the third argument (there are no assumption in
-(happens to be empty) with the variables @{text xs} that will be generalised
+the proof at hand). The second argument stands for a list of variables
-once the goal is proved (in our case @{text P} and @{text
+(given as strings). This list contains the variables that will be turned
-Q}).\footnote{FIXME: explain prove earlier} The @{text "tac"} is the tactic
+into schematic variables once the goal is proved (in our case @{text P} and
-that proves the goal; it can make use of the local assumptions (there are
+@{text Q}). The last argument is the tactic that proves the goal. This
-none in this example). The tactics @{ML_ind etac}, @{ML_ind rtac} and
+tactic can make use of the local assumptions (there are none in this
-@{ML_ind atac} in the code above correspond roughly to @{text erule}, @{text
+example). The tactics @{ML_ind etac}, @{ML_ind rtac} and @{ML_ind atac} in
-rule} and @{text assumption}, respectively. The operator @{ML_ind THEN}
+the code above correspond roughly to @{text erule}, @{text rule} and @{text
-strings the tactics together.
+assumption}, respectively. The combinator @{ML_ind 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. Many theorems also have ML-bindings with the same name. Therefore,
+theorems. We  could also just have written @{ML "etac disjE 1"}. The reason
-we could also just have written @{ML "etac disjE 1"}, or in case where there
+is that many of the basic theorems have a corresponding ML-binding:
-is no ML-binding obtain the theorem dynamically using the function @{ML
-thm}; for example \mbox{@{ML "etac (thm \"disjE\") 1"}}. Both ways however
+@{ML_response_fake [gray,display]
-are considered bad style! The reason is that the binding for @{ML disjE} can
+"disjE"
-be re-assigned by the user and thus one does not have complete control over
+"\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"}
-which theorem is actually applied. This problem is nicely prevented by using
-antiquotations, because then the theorems are fixed statically at
+In case where there is no ML-binding theorems can also be obtained dynamically using
-compile-time.
+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
+for @{ML disjE} can be re-assigned by the user 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
+must have a unique name, the string can stand for a dynamically updated
+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.
 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
 THEN rtac @{thm disjI1} 1
 THEN atac 1)*}
 text {* and the Isabelle proof: *}
-lemma "P \<or> Q \<Longrightarrow> Q \<or> P"
+lemma
+shows "P \<or> Q \<Longrightarrow> Q \<or> P"
 apply(tactic {* foo_tac *})
 done
 text {*
 By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} you can call from the
 THEN' atac
 THEN' rtac @{thm disjI1}
 THEN' atac)*}text_raw{*\label{tac:footacprime}*}
 text {*
-where @{ML_ind  THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give
+where @{ML_ind THEN'} is used instead of @{ML THEN}. (For most combinators
-the number for the subgoal explicitly when the tactic is
+that combine tactics---@{ML THEN} is only one such combinator---a ``primed''
-called. So in the next proof you can first discharge the second subgoal, and
+version exists.)  With @{ML foo_tac'} you can give the number for the
-subsequently the first.
+subgoal explicitly when the tactic is called. So in the next proof you can
-*}
+first discharge the second subgoal, and subsequently the first.
+*}
-lemma "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1"
-and "P2 \<or> Q2 \<Longrightarrow> Q2 \<or> P2"
+lemma
+shows "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. For most operators that combine tactics
+hard-coded inside the tactic.
-(@{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
-The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for
+goals being only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not of
-analysing goals being only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not
+this form, then these tactics return the error message:\footnote{To be
-of this form, then these tactics return the error message:
+precise, tactics do not produce this error message, it originates from the
+\isacommand{apply} wrapper.}
 \begin{isabelle}
 @{text "*** empty result sequence -- proof command failed"}\\
 @{text "*** At command \"apply\"."}
 \end{isabelle}
-This means they failed.\footnote{To be precise, tactics do not produce this error
+This means they failed. The reason for this error message is that tactics
-message, it originates from the \isacommand{apply} wrapper.} The reason for this
+are functions mapping a goal state to a (lazy) sequence of successor
-error message is that tactics
+states. Hence the type of a tactic is:
-are functions mapping a goal state to a (lazy) sequence of successor states.
-Hence the type of a tactic is:
 *}
 ML{*type tactic = thm -> thm Seq.seq*}
 text {*
 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'}: either using the first assumption or the second.
 *}
-lemma "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"
+lemma
+shows "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"
 apply(tactic {* foo_tac' 1 *})
 back
 done
 \begin{boxedminipage}{\textwidth}
 \begin{isabelle}
 *}
 notation (output) "prop"  ("#_" [1000] 1000)
-lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
+lemma
+shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
 apply(tactic {* my_print_tac @{context} *})
 txt{* \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}\medskip
 *}
 (*<*)oops(*>*)
 text_raw {*
 \end{isabelle}
 \end{boxedminipage}
-\caption{The figure shows a proof where each intermediate goal state is
+\caption{The figure shows an Isabelle snippet of a proof where each
-printed by the Isabelle system and by @{ML my_print_tac}. The latter shows
+intermediate goal state is printed by the Isabelle system and by @{ML
-the goal state as represented internally (highlighted boxes). This
+my_print_tac}. The latter shows the goal state as represented internally
-tactic shows that every goal state in Isabelle is represented by a theorem:
+(highlighted boxes). This tactic shows that every goal state in Isabelle is
-when you start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is
+represented by a theorem: when you start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow>
-@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> #(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when you finish the proof the
+A \<and> B"}} the theorem is @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> #(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when
-theorem is @{text "#(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}.\label{fig:goalstates}}
+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
+tactic we are in the position to inspect every goal state in a proof. For
-proof. Consider now the proof in Figure~\ref{fig:goalstates}: as can be seen,
+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
 @{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. The instantiations of schematic variables can even be observed
+variables. This instantiations of schematic variables can be observed
-on the user level. For this consider the following definition and proof.
+on the user level. Have a look at the following definition and proof.
 *}
 definition
 EQ_TRUE
 where
 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
-expect, but @{thm test}:
+expect, but @{thm test}. We can test this with:
 \begin{isabelle}
 \isacommand{thm}~@{thm [source] test}\\
 @{text ">"}~@{thm test}
 \end{isabelle}
-As can be seen, the schematic variable @{text "?X"} has been instantiated inside the proof.
+The reason for this result is that the schematic variable @{text "?X"}
+is instantiated inside the proof and then the 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 {*
-Let us start with explaining the simple tactic @{ML_ind  print_tac}, which is quite useful
+In this section we will describe more of the simple tactics in Isabelle. The
+first one is @{ML_ind  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
 *}
-lemma shows "False \<Longrightarrow> True"
+lemma
+shows "False \<Longrightarrow> True"
 apply(tactic {* print_tac "foo message" *})
 txt{*gives:\medskip
 \begin{minipage}{\textwidth}\small
 @{text "foo message"}\\[3mm]
 *}
 (*<*)oops(*>*)
 text {*
 A simple tactic for easy discharge of any proof obligations is
-@{ML_ind  cheat_tac in Skip_Proof}. This tactic corresponds to
+@{ML_ind  cheat_tac in Skip_Proof} in the structure @{ML_struct Skip_Proof}.
-the Isabelle command \isacommand{sorry} and is sometimes useful
+This tactic corresponds to the Isabelle command \isacommand{sorry} and is
-during the development of tactics.
+sometimes useful during the development of tactics.
 *}
-lemma shows "False" and "Goldbach_conjecture"
+lemma
+shows "False" and "Goldbach_conjecture"
 apply(tactic {* Skip_Proof.cheat_tac @{theory} *})
 txt{*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
 This tactic works however only if the quick-and-dirty mode of Isabelle
-is switched on.
+is switched on. This is done automatically in the ``interactive
+mode'' of Isabelle, but must ne done manually in the ``batch mode''.
-Another simple tactic is the function @{ML_ind  atac}, which, as shown in the previous
-section, corresponds to the assumption command.
+Another simple tactic is the function @{ML_ind  atac}, which, as shown
-*}
+earlier, corresponds to the assumption method.
+*}
-lemma shows "P \<Longrightarrow> P"
+lemma
+shows "P \<Longrightarrow> P"
 apply(tactic {* atac 1 *})
 txt{*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 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.
 *}
-lemma shows "P \<and> Q"
+lemma
+shows "P \<and> Q"
 apply(tactic {* rtac @{thm conjI} 1 *})
 txt{*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
-lemma shows "P \<and> Q \<Longrightarrow> False"
+lemma
+shows "P \<and> Q \<Longrightarrow> False"
 apply(tactic {* etac @{thm conjE} 1 *})
 txt{*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
-lemma shows "False \<and> True \<Longrightarrow> False"
+lemma
+shows "False \<and> True \<Longrightarrow> False"
 apply(tactic {* dtac @{thm conjunct2} 1 *})
 txt{*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
 an example for @{ML resolve_tac} is the following proof where first an outermost
 implication is analysed and then an outermost conjunction.
 *}
-lemma shows "C \<longrightarrow> (A \<and> B)" and "(A \<longrightarrow> B) \<and> C"
+lemma
+shows "C \<longrightarrow> (A \<and> B)"
+and   "(A \<longrightarrow> B) \<and> C"
 apply(tactic {* resolve_xmp_tac 1 *})
 apply(tactic {* resolve_xmp_tac 2 *})
 txt{*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 @{ML dtac} (@{ML_ind  dresolve_tac}), @{ML etac}
 (@{ML_ind  eresolve_tac}) and so on.
 Another simple tactic is @{ML_ind  cut_facts_tac}. It inserts a list of theorems
-into the assumptions of the current goal state. For example
+into the assumptions of the current goal state. Below we will insert the definitions
-*}
+for the constants @{term True} and @{term False}. So
+*}
-lemma shows "True \<noteq> False"
+lemma
+shows "True \<noteq> False"
 apply(tactic {* cut_facts_tac [@{thm True_def}, @{thm False_def}] 1 *})
 txt{*produces the goal state\medskip
 \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-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
-into the goal state. Consider for example the proof
-*}
-lemma shows "\<forall>x \<in> A. P x \<Longrightarrow> Q x"
-apply(tactic {* dtac @{thm bspec} 1 *})
-txt{*\begin{minipage}{\textwidth}
-@{subgoals [display]}
-\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
-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_ind "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
-with the rule @{text disjI1}. If the instantiation is impossible, as in the
-case of
-@{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
-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
-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}:
-@{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,
-every theorem in the second list is instantiated with every
-theorem in the first.
-@{ML_response_fake [display,gray]
-"map (no_vars @{context})
-([@{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 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
 @{ML_ind  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
+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
 now the proof:
 *}
+ML {* Subgoal.FOCUS *}
 text_raw{*
 \begin{figure}[t]
 \begin{minipage}{\textwidth}
 \begin{isabelle}
 *}
 ML{*fun foc_tac {prems, params, asms, concl, context, schematics} =
 let
-val string_of_params = string_of_cterms context (map snd params)
+fun pairs1 f1 f2 xs =
+commas (map (fn (x, y) => f1 x ^ ":=" ^ f2 y) xs)
+fun pairs2 f xs = pairs1 f f xs
+val string_of_params = pairs1 I (string_of_cterm context) params
 val string_of_asms = string_of_cterms context asms
 val string_of_concl = string_of_cterm context concl
 val string_of_prems = string_of_thms_no_vars context prems
-val string_of_schms = string_of_cterms context (map fst (snd schematics))
+val string_of_schms = pairs2 (string_of_cterm context) (snd schematics)
 val strs = ["params: " ^ string_of_params,
 "schematics: " ^ string_of_schms,
 "assumptions: " ^ string_of_asms,
 "conclusion: " ^ string_of_concl,
 "premises: " ^ string_of_prems]
 in Section~\ref{sec:printing} for extracting strings from @{ML_type cterm}s
 and @{ML_type thm}s.\label{fig:sptac}}
 \end{figure}
 *}
-lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
+lemma
+shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
 apply(tactic {* Subgoal.FOCUS foc_tac @{context} 1 *})
 txt {*
 The tactic produces the following printout:
 \begin{quote}\small
 \begin{tabular}{ll}
-params:      & @{term x}, @{term y}\\
+params:      & @{text "x:=x"}, @{text "y:=y"}\\
-schematics:  & @{text ?z}\\
+schematics:  & @{text "?z:=z"}\\
 assumptions: & @{term "A x y"}\\
 conclusion:  & @{term "B y x \<longrightarrow> C (z y) x"}\\
 premises:    & @{term "A x y"}
 \end{tabular}
 \end{quote}
-(FIXME: Find out how nowadays the schematics are handled)
+The @{text params} and @{text schematics} stand or list of pairs where the left-hand
+side of @{text ":="} is replaced by the right-hand side inside the tactic.
-Notice in the actual output the brown colour of the variables @{term x},
+Notice that in the actual output the brown colour of the variables @{term x},
 and @{term y}. Although they are parameters in the original goal, they are fixed inside
 the tactic. By convention these fixed variables are printed in brown colour.
 Similarly the schematic variable @{text ?z}. The assumption, or premise,
 @{prop "A x y"} is bound as @{ML_type cterm} to the record-variable
 @{text asms}, but also as @{ML_type thm} to @{text prems}.
 txt {*
 then the tactic prints out:
 \begin{quote}\small
 \begin{tabular}{ll}
-params:      & @{term x}, @{term y}\\
+params:      & @{text "x:=x"}, @{text "y:=y"}\\
-schematics:  & @{text ?z}\\
+schematics:  & @{text "?z:=z"}\\
 assumptions: & @{term "A x y"}, @{term "B y x"}\\
 conclusion:  & @{term "C (z y) x"}\\
 premises:    & @{term "A x y"}, @{term "B y x"}
 \end{tabular}
 \end{quote}
 (*<*)oops(*>*)
 text {*
 Now also @{term "B y x"} is an assumption bound to @{text asms} and @{text prems}.
-The difference between the tactics @{ML SUBPROOF} and @{ML FOCUS in Subgoal}
+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. @{ML SUBPROOF} can also not instantiate an schematic
+latter does not. Another is that @{ML SUBPROOF} can not 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
 text {*
 If you apply @{ML atac'} to the next lemma
 *}
-lemma shows "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
+lemma
+shows "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
 apply(tactic {* atac' @{context} 1 *})
 txt{* it will produce
 @{subgoals [display]} *}
 (*<*)oops(*>*)
 subproof. It is therefore possible to also apply @{ML atac'} to the second
 goal by just writing:
 *}
-lemma shows "True" and "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
+lemma
+shows "True"
+and   "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
 apply(tactic {* atac' @{context} 2 *})
 apply(rule TrueI)
 done
 Let us now see how to apply this tactic. Consider the four goals:
 *}
-lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
+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{* \begin{minipage}{\textwidth}
 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
 *}
-lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
+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 1 *})
 apply(tactic {* SUBGOAL select_tac 3 *})
 apply(tactic {* SUBGOAL select_tac 4 *})
 apply(tactic {* SUBGOAL select_tac 5 *})
 (*<*)oops(*>*)
 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.
+explain in the next section, but before that we will show how
+tactic application can be constraint.
+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
+into the goal state. Consider for example the proof
+*}
+lemma
+shows "\<forall>x \<in> A. P x \<Longrightarrow> Q x"
+apply(tactic {* dtac @{thm bspec} 1 *})
+txt{*\begin{minipage}{\textwidth}
+@{subgoals [display]}
+\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
+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. One way to give such
+constraints is by pre-instantiating theorems with other theorems.
+The function @{ML_ind "RS"}, 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
+with the rule @{text disjI1}. If the instantiation is impossible, as in the
+case of
+@{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
+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
+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}:
+@{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,
+every theorem in the second list is instantiated with every
+theorem in the first.
+@{ML_response_fake [display,gray]
+"map (no_vars @{context})
+([@{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}
+Higher-order unification is also often in the way when applying certain
+congruence theorems. For example we would expect that the theorem
+@{thm [source] cong}
+\begin{isabelle}
+\isacommand{thm}~@{thm [source] cong}\\
+@{text "> "}~@{thm cong}
+\end{isabelle}
+is applicable in the following proof producing the subgoals
+@{term "t x = s u"} and @{term "y = w"}.
+*}
+lemma
+fixes x y u w::"'a"
+shows "t x y = s u w"
+apply(rule cong)
+txt{*\begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage}*}
+(*<*)oops(*>*)
+text {*
+As you can see this is unfortunately \emph{not} the case. 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.
+*}
+lemma
+fixes x y u w::"'a"
+shows "t x y = s u w"
+apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+txt{*\begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage}*}
+(*<*)oops(*>*)
+text {*
+However, sometimes it is necessary to expicitly match a theroem against a proof
+state and in doing so finding 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
+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
+we are only interested where @{term R} is instantiated to a constant and
+similarly the instantiation for the other variables is ``obvious'' from the
+proof state.  To use this rule we essentially match the conclusion of
+@{thm [source] rule} against the goal state reading of 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
+that can be used to instantiate the @{thm [source] rule}. 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 =
+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
+to the conclusion of the goal state and also because this function also
+takes care about correctly handling parameters that might be present
+in the goal state. An example for @{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 *})
+txt{*\begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage}*}
+(*<*)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
+one ends up with ``wild'' higher-order unification problems that make
+automatic proofs fails.
 *}
 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
 just strings together two tactics in a sequence. For example:
 *}
-lemma shows "(Foo \<and> Bar) \<and> False"
+lemma
+shows "(Foo \<and> Bar) \<and> False"
 apply(tactic {* rtac @{thm conjI} 1 THEN rtac @{thm conjI} 1 *})
 txt {* \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 If you want to avoid the hard-coded subgoal addressing, then, as
 seen earlier, you can use
 the ``primed'' version of @{ML THEN}. For example:
 *}
-lemma shows "(Foo \<and> Bar) \<and> False"
+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 {*
 will first try out whether rule @{text disjI} applies and in case of failure
 will try @{text conjI}. To see this consider the proof
 *}
-lemma shows "True \<and> False" and "Foo \<or> Bar"
+lemma
+shows "True \<and> False" and "Foo \<or> Bar"
 apply(tactic {* orelse_xmp_tac 2 *})
 apply(tactic {* orelse_xmp_tac 1 *})
 txt {* which results in the goal state
 \begin{minipage}{\textwidth}
 fail if no rule applies (we also have to wrap @{ML all_tac} using the
 @{ML K}-combinator, because it does not take a subgoal number as argument). You can
 test the tactic on the same goals:
 *}
-lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
+lemma
+shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
 apply(tactic {* select_tac' 4 *})
 apply(tactic {* select_tac' 3 *})
 apply(tactic {* select_tac' 2 *})
 apply(tactic {* select_tac' 1 *})
 txt{* \begin{minipage}{\textwidth}
 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
 write: *}
-lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
+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}
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 unchanged. This, however, can be potentially very confusing when visible to
 the user, for example,  in cases where the goal is the form
 *}
-lemma shows "E \<Longrightarrow> F"
+lemma
+shows "E \<Longrightarrow> F"
 apply(tactic {* select_tac' 1 *})
 txt{* \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 use the combinator @{ML_ind  CHANGED} to make sure the subgoal has been changed
 by the tactic. Because now
 *}
-lemma shows "E \<Longrightarrow> F"
+lemma
+shows "E \<Longrightarrow> F"
 apply(tactic {* CHANGED (select_tac' 1) *})(*<*)?(*>*)
 txt{* gives the error message:
 \begin{isabelle}
 @{text "*** empty result sequence -- proof command failed"}\\
 @{text "*** At command \"apply\"."}
 ML{*val repeat_xmp_tac = REPEAT (CHANGED (select_tac' 1)) *}
 text {* which applied to the proof *}
-lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
+lemma
+shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
 apply(tactic {* repeat_xmp_tac *})
 txt{* produces
 \begin{minipage}{\textwidth}
 @{subgoals [display]}
 text {*
 you see that the following goal
 *}
-lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
+lemma
+shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
 apply(tactic {* repeat_all_new_xmp_tac 1 *})
 txt{* \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 Recall that tactics produce a lazy sequence of successor goal states. These
 states can be explored using the command \isacommand{back}. For example
 *}
-lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
+lemma
+shows "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
 apply(tactic {* etac @{thm disjE} 1 *})
 txt{* applies the rule to the first assumption yielding the goal state:\smallskip
 \begin{minipage}{\textwidth}
 @{subgoals [display]}
 After typing
 *}
 (*<*)
 oops
-lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
+lemma
+shows "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
 apply(tactic {* etac @{thm disjE} 1 *})
 (*>*)
 back
 txt{* the rule now applies to the second assumption.\smallskip
 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}.
 *}
-lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
+lemma
+shows "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
 apply(tactic {* DETERM (etac @{thm disjE} 1) *})
 txt {*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 All of the tactics take a simpset and an integer as argument (the latter as usual
 to specify  the goal to be analysed). So the proof
 *}
-lemma "Suc (1 + 2) < 3 + 2"
+lemma
+shows "Suc (1 + 2) < 3 + 2"
 apply(simp)
 done
 text {*
 corresponds on the ML-level to the tactic
 *}
-lemma "Suc (1 + 2) < 3 + 2"
+lemma
+shows "Suc (1 + 2) < 3 + 2"
 apply(tactic {* asm_full_simp_tac @{simpset} 1 *})
 done
 text {*
 If the simplifier cannot make any progress, then it leaves the goal unchanged,
 text {*
 then we can use this tactic to unfold the definition of the constant.
 *}
-lemma shows "MyTrue \<Longrightarrow> True"
+lemma
+shows "MyTrue \<Longrightarrow> True"
 apply(tactic {* rewrite_goal_tac @{thms MyTrue_def} 1 *})
 txt{* producing the goal state
 \begin{minipage}{\textwidth}
 @{subgoals [display]}
 | "perm_list pi (x#xs) = (pi\<bullet>x)#(perm_list pi xs)"
 end
 lemma perm_append[simp]:
 fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 shows "((pi\<^isub>1@pi\<^isub>2)\<bullet>c) = (pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c))"
 by (induct pi\<^isub>1) (auto)
 lemma perm_bij[simp]:
 fixes c d::"nat" and pi::"prm"
 shows "(pi\<bullet>c = pi\<bullet>d) = (c = d)"
 by (induct pi) (auto)
 lemma perm_rev[simp]:
 fixes c::"nat" and pi::"prm"
 shows "pi\<bullet>((rev pi)\<bullet>c) = c"
 by (induct pi arbitrary: c) (auto)
 lemma perm_compose:
 fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>(pi\<^isub>1\<bullet>c)"
 this rule and so one ends up with clunky proofs like:
 *}
 lemma
 fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
 apply(simp)
 apply(rule trans)
 apply(rule perm_compose)
 apply(simp)
 done
 "pi \<bullet>aux c \<equiv> pi \<bullet> c"
 text {* Now the two lemmas *}
 lemma perm_aux_expand:
 fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = pi\<^isub>1 \<bullet>aux (pi\<^isub>2\<bullet>c)"
 unfolding perm_aux_def by (rule refl)
 lemma perm_compose_aux:
 fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>aux c) = (pi\<^isub>1\<bullet>pi\<^isub>2) \<bullet>aux (pi\<^isub>1\<bullet>c)"
 unfolding perm_aux_def by (rule perm_compose)
 text {*
 are simple consequence of the definition and @{thm [source] perm_compose}.
 More importantly, the lemma @{thm [source] perm_compose_aux} can be safely
 for our purposes here, we can add these lemmas to @{ML HOL_basic_ss} in order to obtain
 the desired results. Now we can solve the following lemma
 *}
 lemma
 fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
 apply(tactic {* perm_simp_tac 1 *})
 done
 text {*
 an argument about morphisms.
 After this, the simplifier is aware of the simproc and you can test whether
 it fires on the lemma:
 *}
-lemma shows "Suc 0 = 1"
+lemma
+shows "Suc 0 = 1"
 apply(simp)
 (*<*)oops(*>*)
 text {*
 \begin{isabelle}
 If you want to see what happens with just \emph{this} simproc, without any
 interference from other rewrite rules, you can call @{text fail}
 as follows:
 *}
-lemma shows "Suc 0 = 1"
+lemma
+shows "Suc 0 = 1"
 apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc fail}]) 1*})
 (*<*)oops(*>*)
 text {*
 Now the message shows up only once since the term @{term "1::nat"} is
 Simprocs are applied from inside to outside and from left to right. You can
 see this in the proof
 *}
-lemma shows "Suc (Suc 0) = (Suc 1)"
+lemma
+shows "Suc (Suc 0) = (Suc 1)"
 apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail']) 1*})
 (*<*)oops(*>*)
 text {*
 The simproc @{ML fail'} prints out the sequence
 of the form @{term "Suc n"}, but inside the simproc we only produce
 a theorem if the term is not @{term "Suc 0"}. The result you can see
 in the following proof
 *}
-lemma shows "P (Suc (Suc (Suc 0))) (Suc 0)"
+lemma
+shows "P (Suc (Suc (Suc 0))) (Suc 0)"
 apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one]) 1*})
 txt{*
 where the simproc produces the goal state
 \begin{minipage}{\textwidth}
 text {*
 Now in the lemma
 *}
-lemma "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
+lemma
+shows "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
 apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number]) 1*})
 txt {*
 you obtain the more legible goal state
 \begin{minipage}{\textwidth}
 @{ML_ind  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
+lemma true_conj1:
+shows "True \<and> P \<equiv> P" by simp
 text {*
 It can be used for example to rewrite @{term "True \<and> (Foo \<longrightarrow> Bar)"}
 to @{term "Foo \<longrightarrow> Bar"}. The code is as follows.
 So far we only applied conversions to @{ML_type cterm}s. Conversions can, however,
 also work on theorems using the function @{ML_ind  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
+lemma foo_test:
+shows "P \<or> (True \<and> \<not>P)" by simp
 text {*
 Using the conversion @{ML all_true1_conv} you can transform this theorem into a
 new theorem as follows

changeset 362	a5e7ab090abf
parent 361	8ba963a3e039
child 363	f7f1d8a98098