ProgTutorial/Tactical.thy
changeset 213 e60dbcba719d
parent 210 db8e302f44c8
child 214 7e04dc2368b0
--- 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