--- a/IsaMakefile	Thu Jul 30 11:38:52 2009 +0200
+++ b/IsaMakefile	Thu Jul 30 15:51:51 2009 +0200
@@ -13,10 +13,6 @@
 
 USEDIR = $(ISATOOL) usedir -v true -D generated
 
-rail:
-	rail ProgTutorial/generated/root
-	cp ProgTutorial/generated/root.rao ProgTutorial/document
-
 tutorial: ProgTutorial/ROOT.ML \
           ProgTutorial/document/root.tex \
           ProgTutorial/document/root.bib \

--- a/ProgTutorial/Intro.thy	Thu Jul 30 11:38:52 2009 +0200
+++ b/ProgTutorial/Intro.thy	Thu Jul 30 15:51:51 2009 +0200
@@ -5,6 +5,16 @@
 chapter {* Introduction *}
 
 text {*
+   \begin{flushright}
+  {\em
+  ``My thesis is that programming is not at the bottom of the intellectual \\
+  pyramid, but at the top. It's creative design of the highest order. It \\
+  isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\
+  claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex]
+  Richard Bornat, In Defence of Programming \cite{Bornat-lecture}
+  \end{flushright}
+
+  \medskip
   If your next project requires you to program on the ML-level of Isabelle,
   then this tutorial is for you. It will guide you through the first steps of
   Isabelle programming, and also explain tricks of the trade. The best way to
@@ -27,13 +37,11 @@
   Isabelle is implemented. If you are unfamiliar with either of these two
   subjects, you should first work through the Isabelle/HOL tutorial
   \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}.
-
 *}
 
 section {* Existing Documentation *}
 
 text {*
-  
   The following documentation about Isabelle programming already exists (and is
   part of the distribution of Isabelle):
 
@@ -68,14 +76,11 @@
   for Isabelle  provides convenient interfaces to query the history of
   files and ``change sets''.
   \end{description}
-
-
 *}
 
 section {* Typographic Conventions *}
 
 text {*
-
   All ML-code in this tutorial is typeset in shaded boxes, like the following 
   ML-expression:
 
@@ -160,7 +165,6 @@
   with checking agains the distribution, but generally problems will be caught
   and the developer, who caused them, is expected to fix them. So also
   in this case code maintenance is done for you. 
-
 *}
 
 section {* Some Naming Conventions in the Isabelle Sources *}
@@ -227,7 +231,6 @@
   chapters that are under \underline{heavy} construction are marked 
   with TBD.}
 
-  
   \vfill
   This document was compiled with:\\
   \input{version}\\

--- a/ProgTutorial/Package/Ind_Code.thy	Thu Jul 30 11:38:52 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Thu Jul 30 15:51:51 2009 +0200
@@ -36,7 +36,7 @@
 text {*
   It returns the definition (as a theorem) and the local theory in which the
   definition has been made. In Line 4, @{ML [index] internalK in Thm} is a flag
-  attached to the theorem (others possibile flags are @{ML [index] definitionK in Thm}
+  attached to the theorem (other possibile flags are @{ML [index] definitionK in Thm}
   and @{ML [index] axiomK in Thm}). These flags just classify theorems and have no
   significant meaning, except for tools that, for example, find theorems in
   the theorem database.\footnote{FIXME: put in the section about theorems.} We
@@ -113,7 +113,7 @@
   predicate. A testcase for this function is
 *}
 
-local_setup %gray{* fn lthy =>
+local_setup %gray {* fn lthy =>
 let
   val def = defn_aux lthy eo_orules eo_preds (e_pred, e_arg_tys)
 in
@@ -132,10 +132,14 @@
   If we try out the function with the rules for freshness
 *}
 
-local_setup %gray{* fn lthy =>
- (writeln (Syntax.string_of_term lthy
-    (defn_aux lthy fresh_orules [fresh_pred] (fresh_pred, fresh_arg_tys)));
-  lthy) *}
+local_setup %gray {* fn lthy =>
+let
+  val def = defn_aux lthy fresh_orules 
+                             [fresh_pred] (fresh_pred, fresh_arg_tys)
+in
+  writeln (Syntax.string_of_term lthy def); lthy
+end *}
+
 
 text {*
   we obtain
@@ -169,7 +173,8 @@
   meta-quanti\-fications. In Line 4, we transform these introduction rules
   into the object logic (since definitions cannot be stated with
   meta-connectives). To do this transformation we have to obtain the theory
-  behind the local theory (Line 3); with this theory we can use the function
+  behind the local theory using the function @{ML [index] theory_of in ProofContext} 
+  (Line 3); with this theory we can use the function
   @{ML [index] atomize_term in ObjectLogic} to make the transformation (Line 4). The call
   to @{ML defn_aux} in Line 5 produces all right-hand sides of the
   definitions. The actual definitions are then made in Line 7.  The result of
@@ -187,7 +192,7 @@
 
 text {*
   where we feed into the function all parameters corresponding to
-  the @{text even}-@{text odd} example. The definitions we obtain
+  the @{text even}/@{text odd} example. The definitions we obtain
   are:
 
   @{text [display, break]
@@ -199,8 +204,8 @@
   Note that in the testcase we return the local theory @{text lthy} 
   (not the modified @{text lthy'}). As a result the test case has no effect
   on the ambient theory. The reason is that if we introduce the
-  definition again, we pollute the name space with two versions of @{text "even"} 
-  and @{text "odd"}.
+  definition again, we pollute the name space with two versions of 
+  @{text "even"} and @{text "odd"}. We want to avoid this here.
 
   This completes the code for introducing the definitions. Next we deal with
   the induction principles. 
@@ -234,12 +239,12 @@
 *}
 
 ML{*fun inst_spec ctrm = 
- Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*}
+  Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*}
 
 text {*
   This helper function instantiates the @{text "?x"} in the theorem 
   @{thm spec} with a given @{ML_type cterm}. We call this helper function
-  in the following tactic, called @{text inst_spec_tac}\label{fun:instspectac}.
+  in the following tactic.\label{fun:instspectac}.
 *}
 
 ML{*fun inst_spec_tac ctrms = 
@@ -278,11 +283,15 @@
 text {*
   We have to give it as arguments the definitions, the premise (a list of
   formulae) and the instantiations. The premise is @{text "even n"} in lemma
-  @{thm [source] manual_ind_prin_even}; in our code it will always be a list
+  @{thm [source] manual_ind_prin_even} shown above; in our code it will always be a list
   consisting of a single formula. Compare this tactic with the manual proof
   for the lemma @{thm [source] manual_ind_prin_even}: as you can see there is
   almost a one-to-one correspondence between the \isacommand{apply}-script and
-  the @{ML ind_tac}. Two testcases for this tactic are:
+  the @{ML ind_tac}. We first rewrite the goal to use only object connectives (Line 2),
+  "cut in" the premise (Line 3), unfold the definitions (Line 4), instantiate
+  the assumptions of the goal (Line 5) and then conclude with @{ML assume_tac}.
+
+  Two testcases for this tactic are:
 *}
 
 lemma automatic_ind_prin_even:
@@ -370,23 +379,24 @@
   the Isabelle's goal mechanism will fail.\footnote{FIXME: check with 
   Stefan...is this so?} 
 
-  In Line 11 we set up the goal to be proved; in the next line we call the
-  tactic for proving the induction principle. As mentioned before, this tactic
-  expects the definitions, the premise and the (certified) predicates with
-  which the introduction rules have been substituted. The code in these two
-  lines will return a theorem. However, it is a theorem
-  proved inside the local theory @{text "lthy'"}, where the variables @{text
-  "zs"} are free, but fixed (see Line 4). By exporting this theorem from @{text
-  "lthy'"} (which contains the @{text "zs"} as free variables) to @{text
-  "lthy"} (which does not), we obtain the desired schematic variables @{text "?zs"}.
-  A testcase for this function is
+  In Line 11 we set up the goal to be proved using the function @{ML [index]
+  prove in Goal}; in the next line we call the tactic for proving the
+  induction principle. As mentioned before, this tactic expects the
+  definitions, the premise and the (certified) predicates with which the
+  introduction rules have been substituted. The code in these two lines will
+  return a theorem. However, it is a theorem proved inside the local theory
+  @{text "lthy'"}, where the variables @{text "zs"} are free, but fixed (see
+  Line 4). By exporting this theorem from @{text "lthy'"} (which contains the
+  @{text "zs"} as free variables) to @{text "lthy"} (which does not), we
+  obtain the desired schematic variables @{text "?zs"}.  A testcase for this
+  function is
 *}
 
-local_setup %gray{* fn lthy =>
+local_setup %gray {* fn lthy =>
 let
-  val newpreds = [@{term "P::nat\<Rightarrow>bool"}, @{term "Q::nat\<Rightarrow>bool"}]
-  val cnewpreds = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
-  val newpred = @{term "P::nat\<Rightarrow>bool"}
+  val newpreds = [@{term "P::nat \<Rightarrow> bool"}, @{term "Q::nat \<Rightarrow> bool"}]
+  val cnewpreds = [@{cterm "P::nat \<Rightarrow> bool"}, @{cterm "Q::nat \<Rightarrow> bool"}]
+  val newpred = @{term "P::nat \<Rightarrow> bool"}
   val srules =  map (subst_free (eo_preds ~~ newpreds)) eo_rules
   val intro = 
       prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys)
@@ -529,8 +539,11 @@
   @{thm [source] imp_elims_test}:
 
   @{ML_response_fake [display, gray]
-"writeln (string_of_thm_no_vars @{context} 
-            (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))"
+"let
+  val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}
+in
+  writeln (string_of_thm_no_vars @{context} res)
+end"
   "C"}
 
   Now we set up the proof for the introduction rule as follows:
@@ -552,7 +565,8 @@
   THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *}
 
 text {*
-  The function in Line 2 ``rulifies'' the lemma. This will turn out to 
+  The function in Line 2 ``rulifies'' the lemma.\footnote{FIXME: explain this better} 
+  This will turn out to 
   be important later on. Applying this tactic in our proof of @{text "fresh_Lem"}
 *}
 
@@ -581,22 +595,13 @@
   "prems2"}. To do this separation, it is best to open a subproof with the
   tactic @{ML [index] SUBPROOF}, since this tactic provides us with the parameters (as
   list of @{ML_type cterm}s) and the assumptions (as list of @{ML_type thm}s). 
-  The problem we have to overcome with @{ML SUBPROOF}
-  is, however, that this tactic always expects us to completely discharge the
-  goal (see Section~\ref{sec:simpletacs}). This is inconvenient for our
-  gradual explanation of the proof here. To circumvent this inconvenience we
-  use the following modified tactic:
+  The problem with @{ML SUBPROOF}, however, is that it always expects us to 
+  completely discharge the goal (see Section~\ref{sec:simpletacs}). This is 
+  a bit inconvenient for our gradual explanation of the proof here. Therefore
+  we use first the function @{ML [index] FOCUS}, which does same as @{ML SUBPROOF} 
+  but does not require us to completely discharge the goal. 
 *}
 (*<*)oops(*>*)
-ML{*fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac*}
-
-text {*
-  If the tactic inside @{ML SUBPROOF} fails, then the overall tactic will
-  still succeed. With this testing tactic, we can gradually implement
-  all necessary proof steps inside a subproof. Once we are finished, we
-  just have to replace it with @{ML SUBPROOF}.
-*}
-
 text_raw {*
 \begin{figure}[t]
 \begin{minipage}{\textwidth}
@@ -611,7 +616,7 @@
 in 
   s |> separate "\n"
     |> implode
-    |> writeln
+    |> tracing
 end*}
 text_raw{*
 \end{isabelle}
@@ -625,18 +630,19 @@
   First we calculate the values for @{text "params1/2"} and @{text "prems1/2"}
   from @{text "params"} and @{text "prems"}, respectively. To better see what is
   going in our example, we will print out these values using the printing
-  function in Figure~\ref{fig:chopprint}. Since the tactic @{ML SUBPROOF} will
+  function in Figure~\ref{fig:chopprint}. Since @{ML FOCUS} will
   supply us the @{text "params"} and @{text "prems"} as lists, we can 
   separate them using the function @{ML [index] chop}. 
 *}
 
-ML{*fun chop_test_tac preds rules =
-  SUBPROOF_test (fn {params, prems, context, ...} =>
+ML %linenosgray{*fun chop_test_tac preds rules =
+  FOCUS (fn {params, prems, context, ...} =>
   let
-    val (params1, params2) = chop (length params - length preds) (map snd params)
+    val cparams = map snd params
+    val (params1, params2) = chop (length cparams - length preds) cparams
     val (prems1, prems2) = chop (length prems - length rules) prems
   in
-    chop_print params1 params2 prems1 prems2 context; no_tac
+    chop_print params1 params2 prems1 prems2 context; all_tac
   end) *}
 
 text {* 
@@ -644,12 +650,14 @@
   produces parameters and premises in a goal state. The last parameters
   that were introduced come from the quantifications in the definitions
   (see the tactic @{ML expand_tac}).
-  Therefore we only have to subtract the number of predicates (in this
+  Therefore we only have to subtract in Line 5 the number of predicates (in this
   case only @{text "1"}) from the lenghts of all parameters. Similarly
-  with the @{text "prems"}: the last premises in the goal state come from 
+  with the @{text "prems"} in line 6: the last premises in the goal state come from 
   unfolding the definition of the predicate in the conclusion. So we can 
   just subtract the number of rules from the number of all premises. 
-  Applying this tactic in our example 
+  To check our calculations we print them out in Line 8 using the
+  function @{ML chop_print} from Figure~\ref{fig:chopprint} and then 
+  just do nothing, that is @{ML all_tac}. Applying this tactic in our example 
 *}
 
 (*<*)
@@ -657,7 +665,7 @@
 shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
 apply(tactic {* expand_tac @{thms fresh_def} *})
 (*>*)
-apply(tactic {* chop_test_tac [fresh_pred] fresh_rules @{context} *})
+apply(tactic {* chop_test_tac [fresh_pred] fresh_rules @{context} 1 *})
 (*<*)oops(*>*)
 
 text {*
@@ -691,19 +699,18 @@
 
   To use this premise with @{ML rtac}, we need to instantiate its 
   quantifiers (with @{text params1}) and transform it into rule 
-  format (using @{ML [index] rulify in ObjectLogic}. So we can modify the 
-  subproof as follows:
+  format (using @{ML [index] rulify in ObjectLogic}). So we can modify the 
+  code as follows:
 *}
 
 ML %linenosgray{*fun apply_prem_tac i preds rules =
-  SUBPROOF_test (fn {params, prems, context, ...} =>
+  FOCUS (fn {params, prems, context, ...} =>
   let
-    val (params1, params2) = chop (length params - length preds) (map snd params)
+    val cparams = map snd params
+    val (params1, params2) = chop (length cparams - length preds) cparams
     val (prems1, prems2) = chop (length prems - length rules) prems
   in
     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
-    THEN print_tac ""
-    THEN no_tac
   end) *}
 
 text {* 
@@ -719,16 +726,15 @@
 shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
 apply(tactic {* expand_tac @{thms fresh_def} *})
 (*>*)
-apply(tactic {* apply_prem_tac 3 [fresh_pred] fresh_rules @{context} *})
+apply(tactic {* apply_prem_tac 3 [fresh_pred] fresh_rules @{context} 1 *})
 (*<*)oops(*>*)
 
 text {*
-  Since we print out the goal state just after the application of 
-  @{ML rtac} (Line 8), we can see the goal state we obtain: 
+  The goal state we obtain is: 
 
   \begin{isabelle}
-  @{text "1."}~@{prop "a \<noteq> b"}\\
-  @{text "2."}~@{prop "fresh a t"}
+  @{text "1."}~@{text "\<dots> \<Longrightarrow> "}~@{prop "a \<noteq> b"}\\
+  @{text "2."}~@{text "\<dots> \<Longrightarrow> "}~@{prop "fresh a t"}
   \end{isabelle}
 
   As expected there are two subgoals, where the first comes from the
@@ -773,7 +779,8 @@
 ML{*fun prove_intro_tac i preds rules =
   SUBPROOF (fn {params, prems, ...} =>
   let
-    val (params1, params2) = chop (length params - length preds) (map snd params)
+    val cparams = map snd params
+    val (params1, params2) = chop (length cparams - length preds) cparams
     val (prems1, prems2) = chop (length prems - length rules) prems
   in
     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
@@ -781,7 +788,7 @@
   end) *}
 
 text {*
-  Note that the tactic is now @{ML SUBPROOF}, not @{ML SUBPROOF_test}. 
+  Note that the tactic is now @{ML SUBPROOF}, not @{ML FOCUS} anymore. 
   The full proof of the introduction rule is as follows:
 *}
 
@@ -792,7 +799,9 @@
 done
 
 text {* 
-  Phew!  ...Unfortunately, not everything is done yet. If you look closely
+  Phew!\ldots  
+
+  Unfortunately, not everything is done yet. If you look closely
   at the general principle outlined for the introduction rules in 
   Section~\ref{sec:nutshell}, we have  not yet dealt with the case where 
   recursive premises have preconditions. The introduction rule
@@ -802,8 +811,8 @@
 lemma accpartI:
 shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
 apply(tactic {* expand_tac @{thms accpart_def} *})
-apply(tactic {* chop_test_tac [acc_pred] acc_rules @{context} *})
-apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} *})
+apply(tactic {* chop_test_tac [acc_pred] acc_rules @{context} 1 *})
+apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} 1 *})
 
 txt {*
   Here @{ML chop_test_tac} prints out the following
@@ -868,7 +877,8 @@
 ML %linenosgray{*fun prove_intro_tac i preds rules =
   SUBPROOF (fn {params, prems, context, ...} =>
   let
-    val (params1, params2) = chop (length params - length preds) (map snd params)
+    val cparams = map snd params
+    val (params1, params2) = chop (length cparams - length preds) cparams
     val (prems1, prems2) = chop (length prems - length rules) prems
   in
     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
@@ -952,15 +962,15 @@
   three wrappers this function:
 *}
 
-ML{*fun reg_many qname ((name, attrs), thms) = 
+ML{*fun note_many qname ((name, attrs), thms) = 
   LocalTheory.note Thm.theoremK 
     ((Binding.qualify false qname name, attrs), thms) 
 
-fun reg_single1 qname ((name, attrs), thm) = 
-  reg_many qname ((name, attrs), [thm]) 
+fun note_single1 qname ((name, attrs), thm) = 
+  note_many qname ((name, attrs), [thm]) 
 
-fun reg_single2 name attrs (qname, thm) = 
-  reg_many (Binding.name_of qname) ((name, attrs), [thm]) *}
+fun note_single2 name attrs (qname, thm) = 
+  note_many (Binding.name_of qname) ((name, attrs), [thm]) *}
 
 text {*
   The function that ``holds everything together'' is @{text "add_inductive"}. 
@@ -985,10 +995,10 @@
   val mut_name = space_implode "_" (map Binding.name_of prednames)
   val case_names = map (Binding.name_of o fst) namesattrs
 in
-  lthy' |> reg_many mut_name ((@{binding "intros"}, []), intro_rules) 
-        ||>> reg_many mut_name ((@{binding "inducts"}, []), ind_prins)
-        ||>> fold_map (reg_single1 mut_name) (namesattrs ~~ intro_rules)  
-        ||>> fold_map (reg_single2 @{binding "induct"} 
+  lthy' |> note_many mut_name ((@{binding "intros"}, []), intro_rules) 
+        ||>> note_many mut_name ((@{binding "inducts"}, []), ind_prins)
+        ||>> fold_map (note_single1 mut_name) (namesattrs ~~ intro_rules)  
+        ||>> fold_map (note_single2 @{binding "induct"} 
               [Attrib.internal (K (RuleCases.case_names case_names)),
                Attrib.internal (K (RuleCases.consumes 1)),
                Attrib.internal (K (Induct.induct_pred ""))]) 

--- a/ProgTutorial/Package/Ind_General_Scheme.thy	Thu Jul 30 11:38:52 2009 +0200
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy	Thu Jul 30 15:51:51 2009 +0200
@@ -41,9 +41,9 @@
 
 text {*
   The inductive package will generate the reasoning infrastructure for
-  mutually recursive predicates @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what
+  mutually recursive predicates, say @{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
+  of ``things'' (lists, terms, 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
@@ -64,18 +64,17 @@
   
   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"}
-  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"}, in case mutual recursive predicates are defined; the
-  terms @{text ss} and @{text ts} are the 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 one recursive premise and must be given. Some examples of
-  @{text "rule"}s are
+  wrong, if the @{text "rules"} are not of this form.  The @{text As} and
+  @{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"}, in case mutual recursive
+  predicates are defined; the terms @{text ss} and @{text ts} are the
+  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 one recursive premise and
+  must be given. Some examples of @{text "rule"}s are
 
 
   @{thm [display] fresh_var[no_vars]}
@@ -88,7 +87,7 @@
 
   @{thm [display] accpartI[no_vars]}
 
-  has a single recursive premise that has a precondition. As usual all 
+  has a single recursive premise that has a precondition. As is custom all 
   rules are stated without the leading meta-quantification @{text "\<And>xs"}.
 
   The output of the inductive package will be definitions for the predicates, 
@@ -108,7 +107,7 @@
 
   @{text [display] "ind ::= pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"}
 
-  where in the @{text "rules"} every @{text pred} is replaced by a fresh
+  where in the @{text "rules"}-part every @{text pred} is replaced by a fresh
   meta-variable @{text "?P"}.
 
   In order to derive an induction principle for the predicate @{text "pred"},
@@ -211,11 +210,11 @@
    @{prop "\<forall>n. odd n \<longrightarrow> even (Suc n)"},
    @{prop "\<forall>n. even n \<longrightarrow> odd (Suc n)"}]
 
-val eo_preds =  [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] 
+val eo_preds =  [@{term "even::nat \<Rightarrow> bool"}, @{term "odd::nat \<Rightarrow> bool"}] 
 val eo_prednames = [@{binding "even"}, @{binding "odd"}]
 val eo_mxs = [NoSyn, NoSyn] 
 val eo_arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]] 
-val e_pred = @{term "even::nat\<Rightarrow>bool"}
+val e_pred = @{term "even::nat \<Rightarrow> bool"}
 val e_arg_tys = [@{typ "nat"}] 
 
 
@@ -233,7 +232,7 @@
    @{prop "\<forall>a t. fresh a (Lam a t)"},
    @{prop "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)"}]
 
-val fresh_pred =  @{term "fresh::string\<Rightarrow>trm\<Rightarrow>bool"} 
+val fresh_pred =  @{term "fresh::string \<Rightarrow> trm \<Rightarrow> bool"} 
 val fresh_arg_tys = [@{typ "string"}, @{typ "trm"}]
 
 
@@ -241,11 +240,11 @@
 (* 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 @{text "even"}-@{text "odd"}, 
+\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

--- a/ProgTutorial/Package/Ind_Interface.thy	Thu Jul 30 11:38:52 2009 +0200
+++ b/ProgTutorial/Package/Ind_Interface.thy	Thu Jul 30 15:51:51 2009 +0200
@@ -50,40 +50,14 @@
 \end{figure}  
 *}
 
-text {*
-  \begin{figure}[p]
-  \begin{boxedminipage}{\textwidth}
-  \begin{isabelle}
-  \railnontermfont{\rmfamily\itshape}
-  \railterm{simpleinductive,where,for}
-  \railalias{simpleinductive}{\simpleinductive{}}
-  \railalias{where}{\isacommand{where}}
-  \railalias{for}{\isacommand{for}}
-  \begin{rail}
-  simpleinductive target?\\ fixes
-  (where (thmdecl? prop + '|'))?
-  ;
-  \end{rail}
-  \end{isabelle}
-  \end{boxedminipage}
-  \caption{A railroad diagram describing the syntax of \simpleinductive{}. 
-  The \emph{target} indicates an optional locale; the \emph{fixes} are an 
-  \isacommand{and}-separated list of names for the inductive predicates (they
-  can also contain typing- and syntax annotations); \emph{prop} stands for a 
-  introduction rule with an optional theorem declaration (\emph{thmdecl}).
-  \label{fig:railroad}}
-  \end{figure}
-*}
+text {* 
+  To be able to write down the specifications of inductive predicates, we have
+  to introduce a new command (see Section~\ref{sec:newcommand}).  As the
+  keyword for the new command we chose \simpleinductive{}. Examples of
+  specifications from the previous section are shown in
+  Figure~\ref{fig:specs}. The syntax used in these examples more or
+  less translates directly into the parser:
 
-text {* 
-  To be able to write down the specifications or inductive predicates, we have 
-  to introduce
-  a new command (see Section~\ref{sec:newcommand}).  As the keyword for the
-  new command we chose \simpleinductive{}. Examples of specifications we expect
-  the user gives for the inductive predicates from the previous section are
-  shown in Figure~\ref{fig:specs}. The general syntax we will parse is specified
-  in the railroad diagram shown in Figure~\ref{fig:railroad}. This diagram more 
-  or less translates directly into the parser:
 *}
 
 ML{*val spec_parser = 
@@ -95,11 +69,11 @@
              (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
 
 text {*
-  which we explained in Section~\ref{sec:parsingspecs}.  However, if you look
-  closely, there is no code for parsing the target given optionally after the
-  keyword. This is an ``advanced'' feature which we will inherit for ``free''
-  from the infrastructure on which we shall build the package. The target
-  stands for a locale and allows us to specify
+  which we explained in Section~\ref{sec:parsingspecs}.  There is no code included 
+  for parsing the keyword and what is called a \emph{target}. The latter  can be given 
+  optionally after the keyword. The target is an ``advanced'' feature which we will 
+  inherit for ``free'' from the infrastructure on which we shall build the package. 
+  The target stands for a locale and allows us to specify
 *}
 
 locale rel =
@@ -139,7 +113,7 @@
       \"where \" ^
       \"  even0[intro]: \\\"even 0\\\" \" ^ 
       \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ 
-      \"| oddS[intro]:  \\\"even n \<Longrightarrow> odd (Suc n)\\\"\")
+      \"| oddS[intro]:  \\\"even n \<Longrightarrow> odd (Suc n)\\\" \")
 in
   parse spec_parser input
 end"
@@ -151,8 +125,7 @@
   then we get back the specifications of the predicates (with type and syntax annotations), 
   and specifications of the introduction rules. This is all the information we
   need for calling the package and setting up the keyword. The latter is
-  done in Lines 5 to 7 in the code below.\footnote{FIXME: Is there a way to state 
-  here @{text "simple_inductive"}?}
+  done in Lines 5 to 7 in the code below.
 *}
 (*<*)ML %no{*fun add_inductive_cmd pred_specs rule_specs lthy = lthy 
    fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*)

--- a/ProgTutorial/Package/Ind_Intro.thy	Thu Jul 30 11:38:52 2009 +0200
+++ b/ProgTutorial/Package/Ind_Intro.thy	Thu Jul 30 15:51:51 2009 +0200
@@ -5,23 +5,13 @@
 chapter {* How to Write a Definitional Package\label{chp:package} *}
 
 text {*
-  \begin{flushright}
-  {\em
-  ``My thesis is that programming is not at the bottom of the intellectual \\
-  pyramid, but at the top. It's creative design of the highest order. It \\
-  isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\
-  claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex]
-  Richard Bornat, In Defence of Programming \cite{Bornat-lecture}
-  \end{flushright}
-
-  \medskip
   HOL is based on just a few primitive constants, like equality and
   implication, whose properties are described by axioms. All other concepts,
   such as inductive predicates, datatypes or recursive functions, are defined
   in terms of those primitives, and the desired properties, for example
   induction theorems or recursion equations, are derived from the definitions
   by a formal proof. Since it would be very tedious for a user to define
-  complex inductive predicates or datatypes ``by hand'' just using the
+  inductive predicates or datatypes ``by hand'' just using the
   primitive operators of higher order logic, \emph{definitional packages} have
   been implemented to automate such work. Thanks to those packages, the user
   can give a high-level specification, for example a list of introduction
@@ -39,7 +29,8 @@
   does neither support introduction rules involving arbitrary monotonic
   operators, nor does it prove case analysis rules (also called inversion rules). 
   Moreover, it only proves a weaker form of the induction principle for inductive
-  predicates.
+  predicates. But it illustrates the implementation pf a typical package in
+  Isabelle.
 *}
 
 end

--- a/ProgTutorial/Package/Ind_Prelims.thy	Thu Jul 30 11:38:52 2009 +0200
+++ b/ProgTutorial/Package/Ind_Prelims.thy	Thu Jul 30 15:51:51 2009 +0200
@@ -9,14 +9,15 @@
   expects from the package to produce a convenient reasoning
   infrastructure. This infrastructure needs to be derived from the definition
   that correspond to the specified predicate(s). Before we start with
-  explaining all parts of the package, let us first give some examples 
-  showing how to define inductive predicates and then also how
-  to generate a reasoning infrastructure for them. From the examples 
-  we will figure out a general method for
-  defining inductive predicates.  The aim in this section is \emph{not} to
+  explaining all parts of the package, let us first give some examples showing
+  how to define inductive predicates and then also how to generate a reasoning
+  infrastructure for them. From the examples we will figure out a general
+  method for defining inductive predicates. This is usually the first step in
+  writing a package for Isabelle. The aim in this section is \emph{not} to
   write proofs that are as beautiful as possible, but as close as possible to
   the ML-implementation we will develop in later sections.
 
+
   We first consider the transitive closure of a relation @{text R}. The 
   ``pencil-and-paper'' specification for the transitive closure is:
 
@@ -25,12 +26,12 @@
   @{prop[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}
   \end{center}
 
-  The package has to make an appropriate definition for @{term "trcl"}. 
-  Since an inductively
-  defined predicate is the least predicate closed under a collection of
-  introduction rules, the predicate @{text "trcl R x y"} can be defined so
-  that it holds if and only if @{text "P x y"} holds for every predicate
-  @{text P} closed under the rules above. This gives rise to the definition
+  As mentioned before, the package has to make an appropriate definition for
+  @{term "trcl"}. Since an inductively defined predicate is the least
+  predicate closed under a collection of introduction rules, the predicate
+  @{text "trcl R x y"} can be defined so that it holds if and only if @{text
+  "P x y"} holds for every predicate @{text P} closed under the rules
+  above. This gives rise to the definition
 *}
 
 definition "trcl \<equiv> 
@@ -38,11 +39,11 @@
                   \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P x y"
 
 text {*
-  We have to use the object implication @{text "\<longrightarrow>"} and object quantification
-  @{text "\<forall>"} for stating this definition (there is no other way for
-  definitions in HOL). However, the introduction rules and induction
-  principles associated with the transitive closure should use the meta-connectives, 
-  since they simplify the reasoning for the user.
+  Note we have to use the object implication @{text "\<longrightarrow>"} and object
+  quantification @{text "\<forall>"} for stating this definition (there is no other
+  way for definitions in HOL). However, the introduction rules and induction
+  principles associated with the transitive closure should use the
+  meta-connectives, since they simplify the reasoning for the user.
 
 
   With this definition, the proof of the induction principle for @{term trcl}
@@ -176,7 +177,7 @@
   declare new intro- or simplification rules that can throw automatic tactics
   off course) and also it is very hard to debug proofs involving automatic
   tactics whenever something goes wrong. Therefore if possible, automatic 
-  tactics should be avoided or be constrained sufficiently.
+  tactics in packages should be avoided or be constrained sufficiently.
 
   The method of defining inductive predicates by impredicative quantification
   also generalises to mutually inductive predicates. The next example defines
@@ -245,7 +246,7 @@
 qed
 
 text {*
-  The interesting lines are 7 to 15. The assumptions fall into two categories:
+  The interesting lines are 7 to 15. Again, the assumptions fall into two categories:
   @{text p1} corresponds to the premise of the introduction rule; @{text "r1"}
   to @{text "r3"} come from the definition of @{text "even"}.
   In Line 13, we apply the assumption @{text "r2"} (since we prove the second
@@ -262,6 +263,8 @@
   \mbox{\inferrule{@{term "\<And>y. R y x \<Longrightarrow> accpart R y"}}{@{term "accpart R x"}}}
   \end{center}
 
+  The interesting point of this definition is that it contains a quantification
+  that ranges only over the premise and the premise has also a precondition.
   The definition of @{text "accpart"} is:
 *}
 
@@ -294,7 +297,7 @@
 qed
 
 text {*
-  As you can see, there are now two subproofs. The assumptions fall again into
+  As you can see, there are now two subproofs. The assumptions fall as usual into
   two categories (Lines 7 to 9). In Line 11, applying the assumption @{text
   "r1"} generates a goal state with the new local assumption @{term "R y x"},
   named @{text "r1_prem"} in the second subproof (Line 14). This local assumption is

--- a/ProgTutorial/document/root.rao	Thu Jul 30 11:38:52 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-% This file was generated by 'rail' from 'ProgTutorial/generated/root.rai'
-\rail@t {simpleinductive}
-\rail@t {where}
-\rail@t {for}
-\rail@i {1}{ simpleinductive target?\\ fixes (where (thmdecl? prop + '|'))? ; }
-\rail@o {1}{
-\rail@begin{7}{}
-\rail@token{simpleinductive}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{target}[]
-\rail@endbar
-\rail@cr{3}
-\rail@nont{fixes}[]
-\rail@bar
-\rail@nextbar{4}
-\rail@token{where}[]
-\rail@plus
-\rail@bar
-\rail@nextbar{5}
-\rail@nont{thmdecl}[]
-\rail@endbar
-\rail@nont{prop}[]
-\rail@nextplus{6}
-\rail@cterm{|}[]
-\rail@endplus
-\rail@endbar
-\rail@end
-}

Binary file progtutorial.pdf has changed