--- a/ProgTutorial/Tactical.thy Fri Mar 27 18:19:42 2009 +0000
+++ b/ProgTutorial/Tactical.thy Mon Mar 30 08:17:22 2009 +0000
@@ -5,7 +5,7 @@
chapter {* Tactical Reasoning\label{chp:tactical} *}
text {*
- The main reason for descending to the ML-level of Isabelle is to be able to
+ One of the main reason for descending to the ML-level of Isabelle is to be able to
implement automatic proof procedures. Such proof procedures usually lessen
considerably the burden of manual reasoning, for example, when introducing
new definitions. These proof procedures are centred around refining a goal
@@ -119,7 +119,8 @@
THEN' atac)*}
text {*
- and then give the number for the subgoal explicitly when the tactic is
+ where @{ML THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give
+ the number for the subgoal explicitly when the tactic is
called. So in the next proof you can first discharge the second subgoal, and
subsequently the first.
*}
@@ -310,7 +311,7 @@
the subgoals. So after setting up the lemma, the goal state is always of the
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 (in from of an outermost constant @{text
+ 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
@@ -347,13 +348,13 @@
(*<*)oops(*>*)
text {*
- A simple tactic for ``easily'' discharging proof obligations is
+ A simple tactic for easy discharge of any proof obligations is
@{ML SkipProof.cheat_tac}. This tactic corresponds to
the Isabelle command \isacommand{sorry} and is sometimes useful
during the development of tactics.
*}
-lemma shows "False" and "something_else_obviously_false"
+lemma shows "False" and "Goldbach_conjecture"
apply(tactic {* SkipProof.cheat_tac @{theory} *})
txt{*\begin{minipage}{\textwidth}
@{subgoals [display]}
@@ -375,7 +376,7 @@
text {*
Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond
to @{text rule}, @{text drule}, @{text erule} and @{text frule},
- respectively. Each of them takes a theorem as argument and attempts to
+ respectively. Each of them take a theorem as argument and attempt to
apply it to a goal. Below are three self-explanatory examples.
*}
@@ -401,20 +402,6 @@
(*<*)oops(*>*)
text {*
- Note the number in each tactic call. Also as mentioned in the previous section, most
- basic tactics take such a number as argument: this argument addresses the subgoal
- the tacics are analysing. In the proof below, we first split up the conjunction in
- the second subgoal by focusing on this subgoal first.
-*}
-
-lemma shows "Foo" and "P \<and> Q"
-apply(tactic {* rtac @{thm conjI} 2 *})
-txt {*\begin{minipage}{\textwidth}
- @{subgoals [display]}
- \end{minipage}*}
-(*<*)oops(*>*)
-
-text {*
The function @{ML resolve_tac} is similar to @{ML rtac}, except that it
expects a list of theorems as arguments. From this list it will apply the
first applicable theorem (later theorems that are also applicable can be
@@ -494,7 +481,7 @@
takes an additional number as argument that makes explicit which premise
should be instantiated.
- To improve readability of the theorems we produce below, we shall use the
+ To improve readability of the theorems we shall produce below, we will use the
function @{ML no_vars} from Section~\ref{sec:printing}, which transforms
schematic variables into free ones. Using this function for the first @{ML
RS}-expression above produces the more readable result:
@@ -764,7 +751,8 @@
(*<*)oops(*>*)
text {*
- If you want to avoid the hard-coded subgoal addressing, then you can use
+ If you want to avoid the hard-coded subgoal addressing, then, as
+ seen earlier, you can use
the ``primed'' version of @{ML THEN}. For example:
*}
@@ -776,7 +764,7 @@
(*<*)oops(*>*)
text {*
- Here you only have to specify the subgoal of interest only once and
+ Here you have to specify the subgoal of interest only once and
it is consistently applied to the component tactics.
For most tactic combinators such a ``primed'' version exists and
in what follows we will usually prefer it over the ``unprimed'' one.
@@ -1275,7 +1263,7 @@
lemma shows "MyTrue \<Longrightarrow> True \<and> True"
apply(rule conjI)
-apply(tactic {* rewrite_goals_tac [@{thm MyTrue_def}] *})
+apply(tactic {* rewrite_goals_tac @{thms MyTrue_def} *})
txt{* producing the goal state
\begin{minipage}{\textwidth}
@@ -1391,10 +1379,10 @@
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 not noticing anything about the auxiliary
+ into three phases without the user noticing anything about the auxiliary
contant. 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 pusing permutations over
+ then simplifiy 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.
@@ -1492,6 +1480,11 @@
(*<*)oops(*>*)
text {*
+ \begin{isabelle}
+ @{text "> The redex: Suc 0"}\\
+ @{text "> The redex: Suc 0"}\\
+ \end{isabelle}
+
This will print out the message twice: once for the left-hand side and
once for the right-hand side. The reason is that during simplification the
simplifier will at some point reduce the term @{term "1::nat"} to @{term "Suc