# HG changeset patch # User griff # Date 1239175327 -7200 # Node ID f4c9dd7bcb28b981f6e99b31dc1f39766cd15632 # Parent 8def5082432010e633afe782a77d1b0f3385ef19 ran spell-checker diff -r 8def50824320 -r f4c9dd7bcb28 ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Tue Apr 07 23:59:39 2009 +0100 +++ b/ProgTutorial/Tactical.thy Wed Apr 08 09:22:07 2009 +0200 @@ -70,7 +70,7 @@ 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 @@ -314,7 +314,7 @@ a ``protector'' wrapped around it (the wrapper is the outermost constant @{text "Const (\"prop\", bool \ 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 @@ -1020,7 +1020,7 @@ 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 @@ -1038,7 +1038,7 @@ \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 *} @@ -1067,7 +1067,7 @@ 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 @@ -1082,7 +1082,7 @@ 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. @@ -1095,7 +1095,7 @@ 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} @@ -1149,7 +1149,7 @@ \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 {* @@ -1231,7 +1231,7 @@ 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. @@ -1394,9 +1394,9 @@ 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. @@ -1560,7 +1560,7 @@ 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 @@ -1686,7 +1686,7 @@ 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