isabelle-cookbook: comparison ProgTutorial/Tactical.thy

equal deleted inserted replaced

-:643b1e1d7d29
+:b1a458a03a8e
 \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 describe the simplifier, simprocs and conversions.
 *}
 section {* Basics of Reasoning with Tactics*}
 text {*
 To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof
 for @{ML disjE} can be re-assigned and thus one does not have
 complete control over which theorem is actually applied. Similarly with the
 lookup of @{text [quotes] "disjE"}. Although theorems must have a unique name
 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
+These problems can be nicely prevented by using antiquotations
-the theorems are fixed statically at compile-time.
+@{ML_response_fake [gray,display]
+"@{thm \"disjE\"}"
+"\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"}
+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
 *}
 section {* Simple Tactics\label{sec:simpletacs} *}
 text {*
-In this section we will introduce more simple tactics. The
+In this section we will introduce more of the simple tactics in Isabelle. The
 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
 *}
 lemma
 shows "False \<Longrightarrow> True"
 apply(tactic {* print_tac "foo message" *})
-txt{*gives:\medskip
+txt{*gives:
+\begin{isabelle}
-\begin{minipage}{\textwidth}\small
 @{text "foo message"}\\[3mm]
 @{prop "False \<Longrightarrow> True"}\\
 @{text " 1. False \<Longrightarrow> True"}\\
-\end{minipage}
+\end{isabelle}
 *}
 (*<*)oops(*>*)
 text {*
 A simple tactic for easy discharge of any proof obligations, even difficult ones, is
 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 be done manually in the ``batch mode''
-with for example the assignment
+with the assignment
 *}
 ML{*quick_and_dirty := true*}
 text {*
 *}
 lemma
 shows "True \<noteq> False"
 apply(tactic {* cut_facts_tac [@{thm True_def}, @{thm False_def}] 1 *})
-txt{*produces the goal state\medskip
+txt{*produces the goal state
+\begin{isabelle}
-\begin{minipage}{\textwidth}
 @{subgoals [display]}
-\end{minipage}*}
+\end{isabelle}*}
 (*<*)oops(*>*)
 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
 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
+The @{text params} and @{text schematics} stand for list of pairs where the
 left-hand side of @{text ":="} is replaced by the right-hand side inside the
 tactic.  Notice that in the actual output the variables @{term x} and @{term
 y} have a brown colour. 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
 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
 tactic application can be constrained.
-Since rules are applied using higher-order unification, an automatic proof
+\begin{readmore}
-procedure might become too fragile, if it just applies inference rules as
+The functions @{ML SUBGOAL} and @{ML CSUBGOAL} are defined in @{ML_file "Pure/tactical.ML"}.
-shown above. The reason is that a number of rules introduce schematic variables
+\end{readmore}
-into the goal state. Consider for example the proof
+Since @{ML_ind rtac in Tactic} and the like use higher-order unification, an
+automatic proof procedure based on them might become too fragile, if it just
+applies theorems as shown above. The reason is that a number of theorems
+introduce schematic 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 *})
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-where the application of rule @{text bspec} generates two subgoals involving the
+where the application of theorem @{text bspec} generates two subgoals involving the
-schematic variable @{text "?x"}. Now, if you are not careful, tactics
+new schematic variable @{text "?x"}. Now, if you are not careful, tactics
 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
+constrained version of the @{text bspec}-theorem. One way to give such
 constraints is by pre-instantiating theorems with other theorems.
 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
+In this example it instantiates the first premise of the @{text conjI}-theorem
-with the rule @{text disjI1}. If the instantiation is impossible, as in the
+with the theorem @{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>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"}.
+The combinators for instantiating theorems with other 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}
 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.
+with applying congruence theorems and finding the intended instantiation.
 For example
 *}
 lemma
 fixes x y u w::"'a"
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-However, frequently it is necessary to explicitly match a theorem against a proof
+However, frequently it is necessary to explicitly match a theorem against a goal
 state and in doing so construct manually an appropriate instantiation. Imagine
 you have the theorem
 *}
 lemma rule:
 (*<*)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 appropriately constrain the application of inference
+necessary in order to appropriately constrain the application of theorems.
-rules. Otherwise one would end up with ``wild'' higher-order unification
+Otherwise one can end up with ``wild'' higher-order unification  problems
-problems that make automatic proofs fail.
+that make automatic proofs fail.
+\begin{readmore}
+Functions for matching @{ML_type cterm}s are defined in @{ML_file "Pure/thm.ML"}.
+Functions for instantiating schematic variables in theorems are defined
+in @{ML_file "Pure/drule.ML"}.
+\end{readmore}
 *}
 section {* Tactic Combinators *}
 text {*
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 text {*
-If you want to avoid the hard-coded subgoal addressing, then, as
+If you want to avoid the hard-coded subgoal addressing in each component,
-seen earlier, you can use
+then, as seen earlier, you can use the ``primed'' version of @{ML THEN}.
-the ``primed'' version of @{ML THEN}. For example:
+For example:
 *}
 lemma
 shows "(Foo \<and> Bar) \<and> False"
 apply(tactic {* (rtac @{thm conjI} THEN' rtac @{thm conjI}) 1 *})
 \end{minipage} *}
 (*<*)oops(*>*)
 text {*
 Here you have to specify the subgoal of interest only once and
-it is consistently applied to the component tactics.
+it is consistently applied to the component.
 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' in Tactical}. For example
 *}
 ML{*val orelse_xmp_tac = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
 text {*
-will first try out whether rule @{text disjI} applies and in case of failure
+will first try out whether theorem @{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"
 apply(tactic {* orelse_xmp_tac 2 *})
 apply(tactic {* orelse_xmp_tac 1 *})
 txt {* which results in the goal state
+\begin{isabelle}
-\begin{minipage}{\textwidth}
 @{subgoals [display]}
-\end{minipage}
+\end{isabelle}
 *}
 (*<*)oops(*>*)
 text {*
 rtac @{thm notI}, rtac @{thm allI}, K all_tac]*}text_raw{*\label{tac:selectprime}*}
 text {*
 Since we like to mimic the behaviour of @{ML select_tac} as closely as possible,
 we must include @{ML all_tac} at the end of the list, otherwise the tactic will
-fail if no rule applies (we also have to wrap @{ML all_tac} using the
+fail if no theorem 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
 \end{minipage} *}
 (*<*)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
+always  succeeds by fact of having @{ML all_tac} at the end of the tactic
 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},
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 text {*
-In this case no rule applies, but because of @{ML TRY} or the inclusion of @{ML all_tac}
+In this case no theorem applies. But because we wrapped the tactic in a @{ML
-the tactics do not fail. The problem with this is that for the user there is little
+TRY}, it does not fail anymore. The problem is that for the user there is
-chance to see whether or not progress in the proof has been made. By convention
+little chance to see whether progress in the proof has been made, or not. By
-therefore, tactics visible to the user should either change something or fail.
+convention therefore, tactics visible to the user should either change
+something or fail.
 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
+in @{ML select_tac'} or delete @{ML TRY} from @{ML select_tac''}. But for
-succeed on goals where it can make progress. But for the sake of argument,
+the sake of argument, let us suppose that this deletion is \emph{not} an
-let us suppose that this deletion is \emph{not} an option. In such cases, you can
+option. In such cases, you can use the combinator @{ML_ind CHANGED in
-use the combinator @{ML_ind  CHANGED in Tactical} to make sure the subgoal has been changed
+Tactical} to make sure the subgoal has been changed by the tactic. Because
-by the tactic. Because now
+now
 *}
 lemma
 shows "E \<Longrightarrow> F"
 apply(tactic {* CHANGED (select_tac' 1) *})(*<*)?(*>*)
 \end{isabelle}
 *}(*<*)oops(*>*)
 text {*
-We can further extend @{ML select_tac'} so that it not just applies to the topmost
+We can further extend the @{ML select_tac}s so that they not just apply 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 in Tactical}. 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)) *}
 lemma
 shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
 apply(tactic {* repeat_xmp_tac *})
 txt{* produces
+\begin{isabelle}
-\begin{minipage}{\textwidth}
 @{subgoals [display]}
-\end{minipage} *}
+\end{isabelle} *}
 (*<*)oops(*>*)
 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
+tactic as long as it succeeds). The function @{ML_ind REPEAT1 in Tactical}
-@{ML_ind  REPEAT1 in Tactical} is similar, but runs the tactic at least once (failing if
+is similar, but runs the tactic at least once (failing if this is not
-this is not possible).
+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 in Tactical}.
-Suppose the tactic
+Supposing the tactic
 *}
 ML{*val repeat_all_new_xmp_tac = REPEAT_ALL_NEW (CHANGED o select_tac')*}
 text {*
-you see that the following goal
+you can see that the following goal
 *}
 lemma
 shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
 apply(tactic {* repeat_all_new_xmp_tac 1 *})
 *}
 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
+txt{* applies the rule to the first assumption yielding the goal state:
+\begin{isabelle}
-\begin{minipage}{\textwidth}
 @{subgoals [display]}
-\end{minipage}\smallskip
+\end{isabelle}
 After typing
 *}
 (*<*)
 oops
 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
+txt{* the rule now applies to the second assumption.
+\begin{isabelle}
-\begin{minipage}{\textwidth}
 @{subgoals [display]}
-\end{minipage} *}
+\end{isabelle} *}
 (*<*)oops(*>*)
 text {*
 Sometimes this leads to confusing behaviour of tactics and also has
 the potential to explode the search space for tactics.
 \begin{isabelle}
 @{text "*** back: no alternatives"}\\
 @{text "*** At command \"back\"."}
 \end{isabelle}
-Recall that we implemented @{ML select_tac'} on Page~\pageref{tac:selectprime} specifically
-so that it always succeeds. We achieved this by adding at the end the tactic @{ML all_tac}.
+\footnote{\bf FIXME: say something about @{ML_ind  COND} and COND'}
-We can achieve this also by using the combinator @{ML TRY}. Suppose, for example the
+\footnote{\bf FIXME: PARALLEL-CHOICE PARALLEL-GOALS}
-tactic
-*}
-ML{*val select_tac'' = FIRST' [rtac @{thm conjI}, rtac @{thm impI},
-rtac @{thm notI}, rtac @{thm allI}]*}
-text {*
-which will fail if none of the rules applies. However, if you prefix it as follows
-*}
-ML{*val select_tac''' = TRY o select_tac''*}
-text {*
-then the tactic @{ML select_tac''} will be tried out and any failure is harnessed.
-We again have to use the construction with \mbox{@{text "TRY o ..."}} since there is
-no primed version of @{ML_ind  TRY}. The tactic combinator @{ML_ind  TRYALL} will try out
-a tactic on all subgoals. For example the tactic
-*}
-ML{*val triv_tac = TRYALL (rtac @{thm TrueI} ORELSE' etac @{thm FalseE})*}
-text {*
-will solve all trivial subgoals involving @{term True} or @{term "False"}.
-(FIXME: say something about @{ML_ind  COND} and COND')
-(FIXME: PARALLEL-CHOICE PARALLEL-GOALS)
 \begin{readmore}
 Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}.
 Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}.
 \end{readmore}
 *}
 text {*
 \begin{exercise}\label{ex:dyckhoff}
 Dyckhoff presents in \cite{Dyckhoff92} inference rules for a sequent
-calculus, called G4ip, in which no contraction rule is needed in order to be
+calculus, called G4ip, for intuitionistic propositional logic. The
-complete. As a result the rules applied in any order give a simple decision
+interesting feature of this calculus is that no contraction rule is needed
-procedure for propositional intuitionistic logic. His rules are
+in order to be complete. As a result applying the rules exhaustively leads
+to simple decision procedure for propositional intuitionistic logic. The task
+is to implement this decision procedure as a tactic. His rules are
 \begin{center}
 \def\arraystretch{2.3}
 \begin{tabular}{cc}
 \infer[Ax]{A,\varGamma \Rightarrow A}{} &
 {D\longrightarrow B, \varGamma \Rightarrow C \longrightarrow D &
 B, \varGamma \Rightarrow G}}\\
 \end{tabular}
 \end{center}
-Implement a tactic that explores all possibilites of applying these rules to
+Note that in Isabelle the left-rules need to be implemented as elimination
-a propositional formula until a goal state is reached in which all subgoals
+rules. You need to prove separate lemmas corresponding to
-are discharged.  Note that in Isabelle the left-rules need to be implemented
+$\longrightarrow_{L_{1..4}}$. The tactic should explore all possibilites of
-as elimination rules. You need to prove separate lemmas corresponding to
+applying these rules to a propositional formula until a goal state is
-$\longrightarrow_{L_{1..4}}$.  In order to explore all possibilities of applying
+reached in which all subgoals are discharged. For this you can use the tactic
-the rules, use the tactic combinator @{ML_ind  DEPTH_SOLVE in Search}, which searches
+combinator @{ML_ind DEPTH_SOLVE in Search}.
-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}
+\begin{exercise}
+Add to the previous exercise also rules for equality and run your tactic on
+the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}.
+\end{exercise}
 *}
 section {* Simplifier Tactics *}
 text {*
-A lot of convenience in the reasoning with Isabelle derives from its
+A lot of convenience in reasoning with Isabelle derives from its
-powerful simplifier. The power of the simplifier is a strength and a weakness at
+powerful simplifier. We will describe it in this section, whereby
-the same time, because you can easily make the simplifier run into a loop and
+we can, however, only scratch the surface due to its complexity.
-in general its
-behaviour can be difficult to predict. There is also a multitude
+The power of the simplifier is a strength and a weakness at the same time,
-of options that you can configure to control the behaviour of the simplifier.
+because you can easily make the simplifier run into a loop and in general
-We describe some of them in this and the next section.
+its behaviour can be difficult to predict. There is also a multitude of
+options that you can configure to change the behaviour of the
-There are the following five main tactics behind
+simplifier. There are the following five main tactics behind the simplifier
-the simplifier (in parentheses is their user-level counterpart):
+(in parentheses is their user-level counterpart):
 \begin{isabelle}
 \begin{center}
 \begin{tabular}{l@ {\hspace{2cm}}l}
-@{ML_ind  simp_tac}            & @{text "(simp (no_asm))"} \\
+@{ML_ind simp_tac in Simplifier}            & @{text "(simp (no_asm))"} \\
-@{ML_ind  asm_simp_tac}        & @{text "(simp (no_asm_simp))"} \\
+@{ML_ind asm_simp_tac in Simplifier}        & @{text "(simp (no_asm_simp))"} \\
-@{ML_ind  full_simp_tac}       & @{text "(simp (no_asm_use))"} \\
+@{ML_ind full_simp_tac in Simplifier}       & @{text "(simp (no_asm_use))"} \\
-@{ML_ind  asm_lr_simp_tac}     & @{text "(simp (asm_lr))"} \\
+@{ML_ind asm_lr_simp_tac in Simplifier}     & @{text "(simp (asm_lr))"} \\
-@{ML_ind  asm_full_simp_tac}   & @{text "(simp)"}
+@{ML_ind asm_full_simp_tac in Simplifier}   & @{text "(simp)"}
 \end{tabular}
 \end{center}
 \end{isabelle}
 All of the tactics take a simpset and an integer as argument (the latter as usual
 If the simplifier cannot make any progress, then it leaves the goal unchanged,
 i.e., does not raise any error message. That means if you use it to unfold a
 definition for a constant and this constant is not present in the goal state,
 you can still safely apply the simplifier.
-(FIXME: show rewriting of cterms)
+\footnote{\bf FIXME: show rewriting of cterms}
 When using the simplifier, the crucial information you have to provide is
-the simpset. If this information is not handled with care, then the
+the simpset. If this information is not handled with care, then, as
-simplifier can easily run into a loop. Therefore a good rule of thumb is to
+mentioned above, the simplifier can easily run into a loop. Therefore a good
-use simpsets that are as minimal as possible. It might be surprising that a
+rule of thumb is to use simpsets that are as minimal as possible. It might
-simpset is more complex than just a simple collection of theorems used as
+be surprising that a simpset is more complex than just a simple collection
-simplification rules. One reason for the complexity is that the simplifier
+of theorems. One reason for the complexity is that the simplifier must be
-must be able to rewrite inside terms and should also be able to rewrite
+able to rewrite inside terms and should also be able to rewrite according to
-according to rules that have preconditions.
+theorems that have premises.
+The rewriting inside terms requires congruence theorems, which
-The rewriting inside terms requires congruence rules, which
+are typically meta-equalities of the form
-are meta-equalities typical of the form
 \begin{isabelle}
 \begin{center}
 \mbox{\inferrule{@{text "t\<^isub>1 \<equiv> s\<^isub>1 \<dots> t\<^isub>n \<equiv> s\<^isub>n"}}
 {@{text "constr t\<^isub>1\<dots>t\<^isub>n \<equiv> constr s\<^isub>1\<dots>s\<^isub>n"}}}
 \end{center}
 \end{isabelle}
-with @{text "constr"} being a constant, like @{const "If"} or @{const "Let"}.
+with @{text "constr"} being a constant, like @{const "If"}, @{const "Let"}
-Every simpset contains only
+and so on. Every simpset contains only one congruence rule for each
-one congruence rule for each term-constructor, which however can be
+term-constructor, which however can be overwritten. The user can declare
-overwritten. The user can declare lemmas to be congruence rules using the
+lemmas to be congruence rules using the attribute @{text "[cong]"}. In HOL,
-attribute @{text "[cong]"}. In HOL, the user usually states these lemmas as
+the user usually states these lemmas as equations, which are then internally
-equations, which are then internally transformed into meta-equations.
+transformed into meta-equations.
+The rewriting with theorems involving premises requires what is in Isabelle
-The rewriting with rules involving preconditions requires what is in
+called a subgoaler, a solver and a looper. These can be arbitrary tactics
-Isabelle called a subgoaler, a solver and a looper. These can be arbitrary
+that can be installed in a simpset and which are executed at various stages
-tactics that can be installed in a simpset and which are called at
+during simplification. However, simpsets also include simprocs, which can
-various stages during simplification. However, simpsets also include
+produce rewrite rules on demand (see next section). Another component are
-simprocs, which can produce rewrite rules on demand (see next
+split-rules, which can simplify for example the ``then'' and ``else''
-section). Another component are split-rules, which can simplify for example
+branches of if-statements under the corresponding preconditions.
-the ``then'' and ``else'' branches of if-statements under the corresponding
-preconditions.
 \begin{readmore}
 For more information about the simplifier see @{ML_file "Pure/meta_simplifier.ML"}
-and @{ML_file "Pure/simplifier.ML"}. The simplifier for HOL is set up in
+and @{ML_file "Pure/simplifier.ML"}. The generic splitter is implemented in
-@{ML_file "HOL/Tools/simpdata.ML"}. The generic splitter is implemented in
+@{ML_file "Provers/splitter.ML"}.
-@{ML_file  "Provers/splitter.ML"}.
 \end{readmore}
-\begin{readmore}
-FIXME: Find the right place: Discrimination nets are implemented
+\footnote{\bf FIXME: Find the right place to mention this: Discrimination
-in @{ML_file "Pure/net.ML"}.
+nets are implemented in @{ML_file "Pure/net.ML"}.}
-\end{readmore}
 The most common combinators to modify simpsets are:
 \begin{isabelle}
 \begin{tabular}{ll}
-@{ML_ind  addsimps}    & @{ML_ind  delsimps}\\
+@{ML_ind addsimps in MetaSimplifier}    & @{ML_ind delsimps in MetaSimplifier}\\
-@{ML_ind  addcongs}    & @{ML_ind  delcongs}\\
+@{ML_ind addcongs in MetaSimplifier}    & @{ML_ind delcongs in MetaSimplifier}\\
-@{ML_ind  addsimprocs} & @{ML_ind  delsimprocs}\\
+@{ML_ind addsimprocs in MetaSimplifier} & @{ML_ind delsimprocs in MetaSimplifier}\\
 \end{tabular}
 \end{isabelle}
-(FIXME: What about splitters? @{ML addsplits}, @{ML delsplits})
+\footnote{\bf FIXME: What about splitters? @{ML addsplits}, @{ML delsplits}}
 *}
 text_raw {*
 \begin{figure}[t]
 \begin{minipage}{\textwidth}
 text {*
 To see how they work, consider the function in Figure~\ref{fig:printss}, which
 prints out some parts of a simpset. If you use it to print out the components of the
-empty simpset, i.e., @{ML_ind  empty_ss}
+empty simpset, i.e., @{ML_ind empty_ss in MetaSimplifier}
 @{ML_response_fake [display,gray]
 "print_ss @{context} empty_ss"
 "Simplification rules:
 Congruences rules:
 "Simplification rules:
 ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
 Congruences rules:
 Simproc patterns:"}
-(FIXME: Why does it print out ??.unknown)
+\footnote{\bf FIXME: Why does it print out ??.unknown}
 Adding also the congruence rule @{thm [source] UN_cong}
 *}
 ML{*val ss2 = ss1 addcongs [@{thm UN_cong} RS @{thm eq_reflection}] *}
 Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss}
 expects this form of the simplification and congruence rules. However, even
 when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet.
-In the context of HOL, the first really useful simpset is @{ML_ind  HOL_basic_ss}. While
+In the context of HOL, the first really useful simpset is @{ML_ind
-printing out the components of this simpset
+HOL_basic_ss in Simpdata}. While printing out the components of this simpset
 @{ML_response_fake [display,gray]
 "print_ss @{context} HOL_basic_ss"
 "Simplification rules:
 Congruences rules:
 and also resolve with assumptions. For example:
 *}
 lemma
-"True" and "t = t" and "t \<equiv> t" and "False \<Longrightarrow> Foo" and "\<lbrakk>A; B; C\<rbrakk> \<Longrightarrow> A"
+shows "True"
+and  "t = t"
+and  "t \<equiv> t"
+and  "False \<Longrightarrow> Foo"
+and  "\<lbrakk>A; B; C\<rbrakk> \<Longrightarrow> A"
 apply(tactic {* ALLGOALS (simp_tac HOL_basic_ss) *})
 done
 text {*
 This behaviour is not because of simplification rules, but how the subgoaler, solver
-and looper are set up in @{ML_ind  HOL_basic_ss}.
+and looper are set up in @{ML_ind HOL_basic_ss}.
-The simpset @{ML_ind  HOL_ss} is an extension of @{ML HOL_basic_ss} containing
+The simpset @{ML_ind HOL_ss} is an extension of @{ML HOL_basic_ss} containing
 already many useful simplification and congruence rules for the logical
 connectives in HOL.
 @{ML_response_fake [display,gray]
 "print_ss @{context} HOL_ss"
 \<Longrightarrow> (PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')
 op -->: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'
 Simproc patterns:
 \<dots>"}
+\begin{readmore}
+The simplifier for HOL is set up in @{ML_file "HOL/Tools/simpdata.ML"}.
+The simpset @{ML HOL_ss} is implemented in @{ML_file "HOL/HOL.thy"}.
+\end{readmore}
 The simplifier is often used to unfold definitions in a proof. For this the
-simplifier implements the tactic @{ML_ind  rewrite_goal_tac}.\footnote{\bf FIXME:
+simplifier implements the tactic @{ML_ind rewrite_goal_tac in MetaSimplifier}.\footnote{\bf FIXME:
 see LocalDefs infrastructure.} Suppose for example the
 definition
 *}
 definition "MyTrue \<equiv> True"
 lemma
 shows "MyTrue \<Longrightarrow> True"
 apply(tactic {* rewrite_goal_tac @{thms MyTrue_def} 1 *})
 txt{* producing the goal state
+\begin{isabelle}
-\begin{minipage}{\textwidth}
 @{subgoals [display]}
-\end{minipage} *}
+\end{isabelle} *}
 (*<*)oops(*>*)
 text {*
-If you want to unfold definitions in all subgoals, then use the
+If you want to unfold definitions in \emph{all} subgoals not just one,
-the tactic @{ML_ind rewrite_goals_tac}.
+then use the the tactic @{ML_ind rewrite_goals_tac in MetaSimplifier}.
 *}
 text_raw {*
 \begin{figure}[p]
 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{isabelle}
-\begin{minipage}{\textwidth}
 @{subgoals[display]}
-\end{minipage}
+\end{isabelle}
 *}
 (*<*)oops(*>*)
 text {*
 As usual with rewriting you have to worry about looping: you already have
 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{isabelle}
-\begin{minipage}{\textwidth}
 @{subgoals [display]}
-\end{minipage}
+\end{isabelle}*}
-*}
 (*<*)oops(*>*)
 text {*
 where the simproc rewrites all @{term "Suc"}s except in the last argument. There it cannot
 rewrite anything, because it does not know how to transform the term @{term "Suc (0 + 0)"}
 lemma
 "if True \<and> P then P else True \<and> False \<Longrightarrow>
 (if True \<and> Q then True \<and> Q else P) \<longrightarrow> True \<and> (True \<and> Q)"
 apply(tactic {* true1_tac @{context} 1 *})
 txt {* where the tactic yields the goal state
+\begin{isabelle}
-\begin{minipage}{\textwidth}
 @{subgoals [display]}
-\end{minipage}*}
+\end{isabelle}*}
 (*<*)oops(*>*)
 text {*
 As you can see, the premises are rewritten according to @{ML if_true1_conv}, while
 the conclusion according to @{ML all_true1_conv}.
 val this = r OF this;
 val this = Assumption.export false ctxt ctxt0 this
 val this = Variable.export ctxt ctxt0 [this]
 *}
-text {*
+section {* Summary *}
-If a tactic should fail, return the empty sequence.
+text {*
+\begin{conventions}
+\begin{itemize}
+\item Reference theorems with the antiquotation @{text "@{thm \<dots>}"}.
+\item If a tactic is supposed to fail, return the empty sequence.
+\item If you apply a tactic to a sequence of subgoals, apply it
+in reverse order (i.e.~start with the last subgoal).
+\item Use simpsets that are as small as possible.
+\end{itemize}
+\end{conventions}
 *}
 end

changeset 368	b1a458a03a8e
parent 363	f7f1d8a98098
child 369	74ba778b09c9