isabelle-cookbook: comparison ProgTutorial/Tactical.thy

equal deleted inserted replaced

-:8def50824320
+:f4c9dd7bcb28
 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, we could also just have
-written @{ML "etac disjE 1"}, or in case where there are no ML-binding obtain
+written @{ML "etac disjE 1"}, or in case where there is no ML-binding obtain
 the theorem dynamically using the function @{ML thm}; for example
 \mbox{@{ML  "etac (thm \"disjE\") 1"}}. 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
 form @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text
 "(C)"}. Since the goal @{term C} can potentially be an implication, there is
 a ``protector'' wrapped around it (the wrapper is the outermost constant @{text
 "Const (\"prop\", bool \<Rightarrow> bool)"}; however this constant
 is invisible in the figure). This wrapper prevents that premises of @{text C} are
-mis-interpreted as open subgoals. While tactics can operate on the subgoals
+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. If you use the predefined tactics, which we describe in the next
 section, this will always be the case.
 text {*
 A lot of convenience in the reasoning with Isabelle derives from its
 powerful simplifier. The power of simplifier is a strength and a weakness at
 the same time, because you can easily make the simplifier to run into a  loop and its
 behaviour can be difficult to predict. There is also a multitude
-of options that you can configurate to control the behaviour of the simplifier.
+of options that you can configure to control the behaviour of the simplifier.
 We describe some of them in this and the next section.
 There are the following five main tactics behind
 the simplifier (in parentheses is their user-level counterpart):
 @{ML asm_full_simp_tac}   & @{text "(simp)"}
 \end{tabular}
 \end{center}
 \end{isabelle}
-All of the tactics take a simpset and an interger as argument (the latter as usual
+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"
 apply(simp)
 simplifier can easily run into a loop. Therefore a good rule of thumb is to
 use simpsets that are as minimal as possible. It might be surprising that a
 simpset is more complex than just a simple collection of theorems used as
 simplification rules. One reason for the complexity is that the simplifier
 must be able to rewrite inside terms and should also be able to rewrite
-according to rules that have precoditions.
+according to rules that have preconditions.
 The rewriting inside terms requires congruence rules, which
 are meta-equalities typical of the form
 \end{center}
 \end{isabelle}
 with @{text "constr"} being a term-constructor, like @{const "If"} or @{const "Let"}.
 Every simpset contains only
-one concruence rule for each term-constructor, which however can be
+one congruence rule for each term-constructor, which however can be
 overwritten. The user can declare lemmas to be congruence rules using the
 attribute @{text "[cong]"}. In HOL, the user usually states these lemmas as
 equations, which are then internally transformed into meta-equations.
 tactics that can be installed in a simpset and which are called during
 various stages during simplification. However, simpsets also include
 simprocs, which can produce rewrite rules on demand (see next
 section). Another component are split-rules, which can simplify for example
 the ``then'' and ``else'' branches of if-statements under the corresponding
-precoditions.
+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
 text_raw {*
 \end{isabelle}
 \end{minipage}
 \caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing
 all printable information stored in a simpset. We are here only interested in the
-simplifcation rules, congruence rules and simprocs.\label{fig:printss}}
+simplification rules, congruence rules and simprocs.\label{fig:printss}}
 \end{figure} *}
 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
 text {*
 This behaviour is not because of simplification rules, but how the subgoaler, solver
 and looper are set up in @{ML HOL_basic_ss}.
-The simpset @{ML HOL_ss} is an extention of @{ML HOL_basic_ss} containing
+The simpset @{ML 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"
 More importantly, the lemma @{thm [source] perm_compose_aux} can be safely
 added to the simplifier, because now the right-hand side is not anymore an instance
 of the left-hand side. In a sense it freezes all redexes of permutation compositions
 after one step. In this way, we can split simplification of permutations
 into three phases without the user noticing anything about the auxiliary
-contant. We first freeze any instance of permutation compositions in the term using
+constant. We first freeze any instance of permutation compositions in the term using
 lemma @{thm [source] "perm_aux_expand"} (Line 9);
-then simplifiy all other permutations including pushing permutations over
+then simplify all other permutations including pushing permutations over
 other permutations by rule @{thm [source] perm_compose_aux} (Line 10); and
 finally ``unfreeze'' all instances of permutation compositions by unfolding
 the definition of the auxiliary constant.
 *}
 text {*
 Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
 The function also takes a list of patterns that can trigger the simproc.
 Now the simproc is set up and can be explicitly added using
-@{ML addsimprocs} to a simpset whenerver
+@{ML addsimprocs} to a simpset whenever
 needed.
 Simprocs are applied from inside to outside and from left to right. You can
 see this in the proof
 *}
 text {*
 The advantage of @{ML get_thm_alt} is that it leaves very little room for
 something to go wrong; in contrast it is much more difficult to predict
 what happens with @{ML arith_tac in Arith_Data}, especially in more complicated
-circumstances. The disatvantage of @{ML get_thm_alt} is to find a simpset
+circumstances. The disadvantage of @{ML get_thm_alt} is to find a simpset
 that is sufficiently powerful to solve every instance of the lemmas
 we like to prove. This requires careful tuning, but is often necessary in
 ``production code''.\footnote{It would be of great help if there is another
 way than tracing the simplifier to obtain the lemmas that are successfully
 applied during simplification. Alas, there is none.}

changeset 231	f4c9dd7bcb28
parent 230	8def50824320
child 232	0d03e1304ef6