--- a/ProgTutorial/Package/Ind_General_Scheme.thy	Fri Mar 27 12:49:28 2009 +0000
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy	Fri Mar 27 18:19:42 2009 +0000
@@ -20,23 +20,15 @@
 section {* The Code in a Nutshell\label{sec:nutshell} *}
 
 text {*
-  (FIXME: perhaps move somewhere else)
-
-  The point of these examples is to get a feeling what the automatic proofs 
-  should do in order to solve all inductive definitions we throw at them. For this 
-  it is instructive to look at the general construction principle 
-  of inductive definitions, which we shall do in the next section.
-*}
-
-text {*
-  The inductive package will generate the reasoning infrastructure
-  for mutually recursive predicates @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what
-  follows we will have the convention that various, possibly empty collections of 
-  ``things'' are indicated either by adding an @{text "s"} or by adding 
-  a superscript @{text [quotes] "\<^isup>*"}. The shorthand for the predicates 
-  will therefore be @{text "preds"} or @{text "pred\<^sup>*"}. In the case of the
-  predicates there must be, of course, at least a single one in order to obtain a 
-  meaningful definition.
+  The inductive package will generate the reasoning infrastructure for
+  mutually recursive predicates @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what
+  follows we will have the convention that various, possibly empty collections
+  of ``things'' (lists, nested implications and so on) are indicated either by
+  adding an @{text [quotes] "s"} or by adding a superscript @{text [quotes]
+  "\<^isup>*"}. The shorthand for the predicates will therefore be @{text
+  "preds"} or @{text "pred\<^sup>*"}. In the case of the predicates there must
+  be, of course, at least a single one in order to obtain a meaningful
+  definition.
 
   The input for the inductive package will be some @{text "preds"} with possible 
   typing and syntax annotations, and also some introduction rules. We call below the 
@@ -54,11 +46,11 @@
   this format and omit any code that actually tests this. Therefore ``things'' 
   can go horribly wrong, if the @{text "rules"} are not of this
   form.\footnote{FIXME: Exercise to test this format.} The @{text As} and
-  @{text Bs} in a @{text "rule"} are formulae not involving the inductive
+  @{text Bs} in a @{text "rule"} stand for formulae not involving the inductive
   predicates @{text "preds"}; the instances @{text "pred ss"} and @{text "pred
   ts"} can stand for different predicates, like @{text "pred\<^isub>1 ss"} and 
   @{text "pred\<^isub>2 ts"}; @{text ss} and @{text ts} are the
-  arguments of the predicates. Every formula left of @{text [quotes]
+  arguments of these predicates. Every formula left of @{text [quotes]
   "\<Longrightarrow> pred ts"} is a premise of the rule. The outermost quantified 
   variables @{text "xs"} are usually omitted in the user's input. The 
   quantification for the variables @{text "ys"} is local with respect to 
@@ -75,7 +67,7 @@
 
   @{thm [display] accpartI[no_vars]}
 
-  has a recursive premise that has a precondition. As usual all 
+  has a single recursive premise that has a precondition. As usual all 
   rules are stated without the leading meta-quantification @{text "\<And>xs"}.
 
   The code of the inductive package falls roughly in tree parts: the first
@@ -106,11 +98,12 @@
 
   @{text [display] "pred zs \<longrightarrow> orules[preds := Ps] \<longrightarrow> P zs"}
 
-  If we assume @{text "pred zs"} and unfold its definition, then we have
+  If we assume @{text "pred zs"} and unfold its definition, then we have an
+  assumption
   
   @{text [display] "\<forall>preds. orules \<longrightarrow> pred zs"} 
 
-  and must prove
+  and must prove the goal
 
   @{text [display] "orules[preds := Ps] \<longrightarrow> P zs"}
 
@@ -119,23 +112,23 @@
   identity.
   
   Although the user declares introduction rules @{text rules}, they must 
-  be derived from the @{text defs}. These derivations are a bit involved. 
+  also be derived from the @{text defs}. These derivations are a bit involved. 
   Assuming we want to prove the introduction rule 
 
   @{text [display] "\<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
 
-  then we can assume
+  then we can have assumptions of the form
 
   \begin{isabelle}
   (i)~~@{text "As"}\\
   (ii)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"}
   \end{isabelle}
 
-  and must show
+  and must show the goal
 
   @{text [display] "pred ts"}
   
-  If we now unfold the definitions for the @{text preds}, we have
+  If we now unfold the definitions for the @{text preds}, we have assumptions
 
   \begin{isabelle}
   (i)~~~@{text "As"}\\
@@ -155,13 +148,14 @@
   @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
 
   When we apply this rule we end up in the goal state where we have to prove
+  goals of the form
 
   \begin{isabelle}
   (a)~@{text "As"}\\
   (b)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"}
   \end{isabelle}
 
-  We can immediately discharge the goals @{text "As"} using the assumption in 
+  We can immediately discharge the goals @{text "As"} using the assumptions in 
   @{text "(i)"}. The goals in @{text "(b)"} can be discharged as follows: we 
   assume the @{text "Bs"} and prove @{text "pred ss"}. For this we resolve the 
   @{text "Bs"}  with the assumptions in @{text "(ii)"}. This gives us the 
@@ -173,8 +167,8 @@
   in @{text "(iii)"} gives us @{text "pred ss"}, which is the goal we are after.
   This completes the proof for introduction rules.
 
-  What remains is to implement the reasoning outlined above. We do this in
-  the next section. For building testcases, we use the shorthands for 
+  What remains is to implement the reasoning outlined in this section. We do this  
+  next. For building testcases, we use the shorthands for 
   @{text "even/odd"}, @{term "fresh"} and @{term "accpart"}
   given in Figure~\ref{fig:shorthands}.
 *}