--- a/ProgTutorial/Tactical.thy Sun Nov 01 10:49:25 2009 +0100
+++ b/ProgTutorial/Tactical.thy Mon Nov 02 12:47:00 2009 +0100
@@ -1253,12 +1253,12 @@
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
- to simple decision procedure for propositional intuitionistic logic. The task
- is to implement this decision procedure as a tactic. His rules are
+ in order to be complete. As a result the rules can be applied exhaustively, which
+ in turn 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}
@@ -1298,17 +1298,19 @@
\end{tabular}
\end{center}
- Note that in Isabelle the left-rules need to be implemented as elimination
- rules. You need to prove separate lemmas corresponding to
- $\longrightarrow_{L_{1..4}}$. The tactic should explore all possibilites of
- applying these rules to a propositional formula until a goal state is
- reached in which all subgoals are discharged. For this you can use the tactic
- combinator @{ML_ind DEPTH_SOLVE in Search}.
+ Note that in Isabelle right rules need to be implemented as
+ introduction rule, the left rules as elimination rules. You have to to
+ prove separate theorems corresponding to $\longrightarrow_{L_{1..4}}$. The
+ tactic should explore all possibilites of applying these rules to a
+ propositional formula until a goal state is reached in which all subgoals
+ 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
- the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}.
+ Add to the sequent calculus from the previous exercise also rules for
+ equality and run your tactic on the de Bruijn formulae discussed
+ in Exercise~\ref{ex:debruijn}.
\end{exercise}
*}
@@ -1316,8 +1318,8 @@
text {*
A lot of convenience in reasoning with Isabelle derives from its
- powerful simplifier. We will describe it in this section, whereby
- we can, however, only scratch the surface due to its complexity.
+ powerful simplifier. We will describe it in this section. However,
+ 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
@@ -1338,7 +1340,7 @@
\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
*}
@@ -1386,17 +1388,20 @@
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,
- the user usually states these lemmas as equations, which are then internally
- transformed into meta-equations.
+ lemmas to be congruence rules using the attribute @{text "[cong]"}. Note that
+ in HOL these congruence theorems are usually stated as equations, which are
+ 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
- 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 preconditions.
+ during simplification.
+
+ Simpsets can also include simprocs, which produce rewrite rules on
+ 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"}
@@ -1408,10 +1413,10 @@
\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}\\
@@ -1497,9 +1502,10 @@
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
@@ -1509,7 +1515,7 @@
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
@@ -1565,7 +1571,7 @@
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
@@ -1578,7 +1584,7 @@
(*<*)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}.
*}