--- a/ProgTutorial/Package/Ind_General_Scheme.thy	Thu Mar 26 19:00:51 2009 +0000
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy	Fri Mar 27 12:49:28 2009 +0000
@@ -17,7 +17,7 @@
 | fresh_lam2: "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
 (*>*)
 
-section {* The Code in a Nutshell *}
+section {* The Code in a Nutshell\label{sec:nutshell} *}
 
 text {*
   (FIXME: perhaps move somewhere else)
@@ -34,14 +34,14 @@
   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 this case of the
-  predicates there must be at least a single one in order to obtain a meaningful
-  definition.
+  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 predicate will be some @{text "preds"} with possible 
+  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 
   introduction rules short as @{text "rules"}. Borrowing some idealised Isabelle 
-  notation, one such @{text "rule"} is of the form
+  notation, one such @{text "rule"} is assumed to be of the form
 
   \begin{isabelle}
   @{text "rule ::= 
@@ -50,17 +50,20 @@
   \<Longrightarrow> pred ts"}
   \end{isabelle}
   
-  We actually assume the user will always state rules of this form and we omit
-  any code that test this format. So 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 predicates @{text "preds"}; the instances @{text
-  "pred ss"} and @{text "pred ts"} can stand for different predicates.
-  Everything left of @{text [quotes] "\<Longrightarrow> pred ts"} are called the premises of
-  the rule. The variables @{text "xs"} are usually omitted in the user's
-  input. The variables @{text "ys"} are local with respect to on recursive
-  premise. Some examples of @{text "rule"}s the user might write are:
-
+  For the purposes here, we will assume the @{text rules} have
+  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
+  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]
+  "\<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 
+  one recursive premise and must be given. Some examples of @{text "rule"}s 
+  are
 
   @{thm [display] fresh_var[no_vars]}
 
@@ -72,15 +75,16 @@
 
   @{thm [display] accpartI[no_vars]}
 
-  has a recursive premise which has a precondition. In the examples, all 
+  has a 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 involving
-  the definitions, the induction principles and the introduction rules, 
-  respectively. For the definitions we need to have the @{text rules}
-  in a form where the meta-quantifiers and meta-implications are replaced
-  by their object logic equivalent. Therefore an @{text "orule"} is of the
-  form 
+  The code of the inductive package falls roughly in tree parts: the first
+  deals with the definitions, the second with the induction principles and 
+  the third with the introduction rules. 
+  
+  For the definitions we need to have the @{text rules} in a form where 
+  the meta-quantifiers and meta-implications are replaced by their object 
+  logic equivalents. Therefore an @{text "orule"} is of the form 
 
   @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}
 
@@ -88,17 +92,17 @@
 
   @{text [display] "def ::= pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
 
-  The induction principles for the predicate @{text "pred"} are of the
+  The induction principles for every predicate @{text "pred"} are of the
   form
 
   @{text [display] "ind ::= pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"}
 
-  where in the @{text "rules"} every @{text pred} is replaced by a new
-  (meta)variable @{text "?P"}.
+  where in the @{text "rules"} every @{text pred} is replaced by a fresh
+  meta-variable @{text "?P"}.
 
-  In order to derive an induction principle for the predicate @{text "pred"}
-  we first transform it into the object logic and fix the meta-variables. Hence 
-  we have to prove a formula of the form
+  In order to derive an induction principle for the predicate @{text "pred"},
+  we first transform @{text ind} into the object logic and fix the meta-variables. 
+  Hence we have to prove a formula of the form
 
   @{text [display] "pred zs \<longrightarrow> orules[preds := Ps] \<longrightarrow> P zs"}
 
@@ -110,11 +114,13 @@
 
   @{text [display] "orules[preds := Ps] \<longrightarrow> P zs"}
 
-  This can be done by instantiating the @{text "\<forall>preds"} with the @{text "Ps"}. 
-  Then we are done since we are left with a simple identity.
+  This can be done by instantiating the @{text "\<forall>preds"}-quantification 
+  with the @{text "Ps"}. Then we are done since we are left with a simple 
+  identity.
   
-  The proofs for the introduction rules are more involved. Assuming we want to
-  prove the introduction rule 
+  Although the user declares introduction rules @{text rules}, they must 
+  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"}
 
@@ -143,8 +149,8 @@
 
   In the last step we removed some quantifiers and moved the precondition @{text "orules"}  
   into the assumtion. The @{text "orules"} stand for all introduction rules that are given 
-  by the user. We apply the one which corresponds to introduction rule we are proving.
-  This introduction rule must be of the form 
+  by the user. We apply the @{text orule} that corresponds to introduction rule we are 
+  proving. This introduction rule must necessarily be of the form 
 
   @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
 
@@ -155,20 +161,22 @@
   (b)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"}
   \end{isabelle}
 
-  The goals @{text "As"} we can immediately discharge with the assumption in @{text "(i)"}.
-  The goals in @{text "(b)"} we discharge as follows: we assume the @{text "(iv)"} 
-  @{text "Bs"} and prove @{text "(c)"} @{text "pred ss"}. We then resolve the 
-  @{text "Bs"}  with the assumptions in @{text "(ii)"}. This gives us
+  We can immediately discharge the goals @{text "As"} using the assumption 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 
+  assumptions
 
   @{text [display] "(\<forall>preds. orules \<longrightarrow> pred ss)\<^isup>*"}
 
   Instantiating the universal quantifiers and then resolving with the assumptions 
   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. 
-  For building testcases, we use some shorthands for the definitions 
-  of @{text "even/odd"}, @{term "fresh"} and @{term "accpart"}. 
+  What remains is to implement the reasoning outlined above. We do this in
+  the next section. For building testcases, we use the shorthands for 
+  @{text "even/odd"}, @{term "fresh"} and @{term "accpart"}
+  given in Figure~\ref{fig:shorthands}.
 *}
 
 
@@ -219,14 +227,15 @@
 (* accessible-part example *)
 val acc_rules = 
      [@{prop "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}]
-val acc_pred = @{term "accpart:: ('a \<Rightarrow>'a\<Rightarrow>bool)\<Rightarrow>'a \<Rightarrow>bool"}*}
+val acc_pred = @{term "accpart::('a \<Rightarrow>'a\<Rightarrow>bool)\<Rightarrow>'a \<Rightarrow>bool"}*}
 text_raw{*
 \end{isabelle}
 \end{minipage}
-\caption{Shorthands for the inductive predicates of @{text "even"}-@{text "odd"}, 
-  @{text "fresh"} and @{text "accpart"}. The follow the convention @{text "rules"}, 
-  @{text "orules"}, @{text "preds"} and so on as used in Section ???. The purpose 
-  of these shorthands is to simplify the construction of testcases.}
+\caption{Shorthands for the inductive predicates @{text "even"}-@{text "odd"}, 
+  @{text "fresh"} and @{text "accpart"}. The names of these shorthands follow 
+  the convention @{text "rules"}, @{text "orules"}, @{text "preds"} and so on. 
+  The purpose of these shorthands is to simplify the construction of testcases
+  in Section~\ref{sec:code}.\label{fig:shorthands}}
 \end{figure}
 *}