isabelle-cookbook: comparison ProgTutorial/Tactical.thy

equal deleted inserted replaced

-:74ba778b09c9
+:2494b5b7a85d
 \end{readmore}
 *}
 text {*
 \begin{exercise}\label{ex:dyckhoff}
-Dyckhoff presents in \cite{Dyckhoff92} inference rules for a sequent
+Dyckhoff presents in \cite{Dyckhoff92} inference rules of a sequent
 calculus, called G4ip, for intuitionistic propositional logic. The
 interesting feature of this calculus is that no contraction rule is needed
-in order to be complete. As a result applying the rules exhaustively leads
+in order to be complete. As a result the rules can be applied exhaustively, which
-to simple decision procedure for propositional intuitionistic logic. The task
+in turn leads to simple decision procedure for propositional intuitionistic logic.
-is to implement this decision procedure as a tactic. His rules are
+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}
-Note that in Isabelle the left-rules need to be implemented as elimination
+Note that in Isabelle right rules need to be implemented as
-rules. You need to prove separate lemmas corresponding to
+introduction rule, the left rules as elimination rules. You have to to
-$\longrightarrow_{L_{1..4}}$. The tactic should explore all possibilites of
+prove separate theorems corresponding to $\longrightarrow_{L_{1..4}}$. The
-applying these rules to a propositional formula until a goal state is
+tactic should explore all possibilites of applying these rules to a
-reached in which all subgoals are discharged. For this you can use the tactic
+propositional formula until a goal state is reached in which all subgoals
-combinator @{ML_ind DEPTH_SOLVE in Search}.
+are discharged. For this you can use the tactic combinator @{ML_ind
+DEPTH_SOLVE in Search} in the structure @{ML_struct Search}.
 \end{exercise}
 \begin{exercise}
-Add to the previous exercise also rules for equality and run your tactic on
+Add to the sequent calculus from the previous exercise also rules for
-the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}.
+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 reasoning with Isabelle derives from its
-powerful simplifier. We will describe it in this section, whereby
+powerful simplifier. We will describe it in this section. However,
-we can, however, only scratch the surface due to its complexity.
+due to its complexity, we can mostly only scratch the surface.
 The power of the simplifier is a strength and a weakness at the same time,
 because you can easily make the simplifier run into a loop and in general
 its behaviour can be difficult to predict. There is also a multitude of
 options that you can configure to change the behaviour of the
 @{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
+All these tactics take a simpset and an integer as argument (the latter as usual
 to specify  the goal to be analysed). So the proof
 *}
 lemma
 shows "Suc (1 + 2) < 3 + 2"
 \end{isabelle}
 with @{text "constr"} being a constant, like @{const "If"}, @{const "Let"}
 and so on. Every simpset contains only 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,
+lemmas to be congruence rules using the attribute @{text "[cong]"}. Note that
-the user usually states these lemmas as equations, which are then internally
+in HOL these congruence theorems are usually stated as equations, which are
-transformed into meta-equations.
+then internally transformed into meta-equations.
 The rewriting with theorems involving premises requires what is in Isabelle
 called a subgoaler, a solver and a looper. These can be arbitrary tactics
 that can be installed in a simpset and which are executed at various stages
-during simplification. However, simpsets also include simprocs, which can
+during simplification.
-produce rewrite rules on demand (see next section). Another component are
-split-rules, which can simplify for example the ``then'' and ``else''
+Simpsets can also include simprocs, which produce rewrite rules on
-branches of if-statements under the corresponding preconditions.
+demand according to a pattern (see next section for a detailed description
+of simpsets). Another component are split-rules, which can simplify for
+example 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 generic splitter is implemented in
 @{ML_file "Provers/splitter.ML"}.
 \footnote{\bf FIXME: Find the right place to mention this: Discrimination
 nets are implemented in @{ML_file "Pure/net.ML"}.}
-The most common combinators to modify simpsets are:
+The most common combinators for modifying simpsets are:
 \begin{isabelle}
-\begin{tabular}{ll}
+\begin{tabular}{l@ {\hspace{10mm}}l}
 @{ML_ind addsimps in MetaSimplifier}    & @{ML_ind delsimps in MetaSimplifier}\\
 @{ML_ind addcongs in MetaSimplifier}    & @{ML_ind delcongs in MetaSimplifier}\\
 @{ML_ind addsimprocs in MetaSimplifier} & @{ML_ind delsimprocs in MetaSimplifier}\\
 \end{tabular}
 \end{isabelle}
 Congruences rules:
 UNION: \<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk> \<Longrightarrow> \<Union>x\<in>A. C x \<equiv> \<Union>x\<in>B. D x
 Simproc patterns:"}
 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
+expects this form of the simplification and congruence rules. This is
+different, if we use for example the simpset @{ML HOL_basic_ss} (see below),
+where rules are usually added as equation. 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 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:
 Simproc patterns:"}
-also produces ``nothing'', the printout is misleading. In fact
+also produces ``nothing'', the printout is somewhat misleading. In fact
 the @{ML HOL_basic_ss} is setup so that it can solve goals of the
 form
 \begin{isabelle}
 @{thm TrueI}, @{thm refl[no_vars]}, @{term "t \<equiv> t"} and @{thm FalseE[no_vars]};
 *}
 definition "MyTrue \<equiv> True"
 text {*
-then we can use this tactic to unfold the definition of the constant.
+then we can use this tactic to unfold the definition of this constant.
 *}
 lemma
 shows "MyTrue \<Longrightarrow> True"
 apply(tactic {* rewrite_goal_tac @{thms MyTrue_def} 1 *})
 @{subgoals [display]}
 \end{isabelle} *}
 (*<*)oops(*>*)
 text {*
-If you want to unfold definitions in \emph{all} subgoals not just one,
+If you want to unfold definitions in \emph{all} subgoals, not just one,
 then use the the tactic @{ML_ind rewrite_goals_tac in MetaSimplifier}.
 *}
 text_raw {*

changeset 370	2494b5b7a85d
parent 369	74ba778b09c9
child 378	8d160d79b48c