diff -r 693711a0c702 -r e0d368a45537 CookBook/Package/Ind_Interface.thy
--- a/CookBook/Package/Ind_Interface.thy	Sat Feb 21 11:38:14 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy	Sun Feb 22 03:44:03 2009 +0000
@@ -1,15 +1,15 @@
 theory Ind_Interface
-imports "../Base" "../Parsing" Simple_Inductive_Package
+imports "../Base" "../Parsing" Ind_Prelims Simple_Inductive_Package
 begin
 
-section {* Parsing the Specification *}
+section {* Parsing and Typing the Specification *}
 
 text {* 
   To be able to write down the specification in Isabelle, we have to introduce
-  a new command (see Section~\ref{sec:newcommand}).  As the keyword for the new
-  command we chose \simpleinductive{}. We want that the package can cope with
+  a new command (see Section~\ref{sec:newcommand}).  As the keyword for the
+  new command we chose \simpleinductive{}. In the package we want to support
+  some ``advanced'' features: First, we want that the package can cope with
   specifications inside locales. For example it should be possible to declare
-
 *}
 
 locale rel =
@@ -20,35 +20,68 @@
 *}
 
 
-simple_inductive (in rel) trcl' 
+simple_inductive (in rel) 
+  trcl' 
 where
   base: "trcl' x x"
 | step: "trcl' x y \<Longrightarrow> R y z \<Longrightarrow> trcl' x z"
 
-simple_inductive (in rel) accpart'
+simple_inductive (in rel) 
+  accpart'
 where
   accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
 
+text {* 
+  Second, we want that the user can specify fixed parameters.
+  Remember in the previous section we stated that the user can give the 
+  specification for the transitive closure of a relation @{text R} as 
+*}
 
+simple_inductive
+  trcl\<iota>\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  base: "trcl\<iota>\<iota> R x x"
+| step: "trcl\<iota>\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota>\<iota> R x z"
 
 text {*
-  After the keyword we expect a constant (or constants) with possible typing 
-  annotations and a
-  list of introduction rules. While these specifications are all
-  straightforward, there is a technicality we like to deal with to do with
-  fixed parameters and locales. Remember we pointed out that the parameter
-  @{text R} is fixed throughout the specifications of @{text trcl} and @{text
-  accpart}. The point is that they might be fixed in a locale and we like to
-  support this. Accordingly we treat some parameters of the inductive
-  definition specially; see Figure~\ref{fig:inddefsfixed} where the transitive
-  closure and accessible part are defined with a fixed parameter @{text R} and
-  also inside a locale fixing @{text R}.
+  Note that there is no locale given in this specification---the parameter
+  @{text "R"} therefore needs to be included explicitly in @{term trcl\<iota>\<iota>}, but
+  stays fixed throughout the specification. The problem with this way of
+  stating the specification for the transitive closure is that it derives the
+  following induction principle.
+
+  \begin{center}\small
+  \mprset{flushleft}
+  \mbox{\inferrule{
+             @{thm_style prem1  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
+             @{thm_style prem2  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
+             @{thm_style prem3  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}
+            {@{thm_style concl  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}}  
+  \end{center}
+
+  But this does not correspond to the induction principle we derived by hand, which
+  was
+  
+  \begin{center}\small
+  \mprset{flushleft}
+  \mbox{\inferrule{
+             @{thm_style prem1  trcl_induct[no_vars]}\\\\
+             @{thm_style prem2  trcl_induct[no_vars]}\\\\
+             @{thm_style prem3  trcl_induct[no_vars]}}
+            {@{thm_style concl  trcl_induct[no_vars]}}}  
+  \end{center}
+
+  The difference is that in the one derived by hand the relation @{term R} is not
+  a parameter of the proposition @{term P} to be proved and it is also not universally
+  qunatified in the second and third premise. The point is that the parameter @{term R}
+  stays fixed thoughout the definition and we do not want to regard it as an ``ordinary''
+  argument of the transitive closure, but one that can be freely instantiated. 
+  In order to recognise such parameters, we have to extend the specification
+  to include a mechanism to state fixed parameters. The user should be able
+  to write 
+
 *}
 
-text_raw {*
-  \begin{figure}[p]
-  \begin{isabelle}
-*}
 simple_inductive
   trcl'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 where
@@ -60,18 +93,8 @@
 where
   accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x"
 
-text_raw {*
-  \end{isabelle}
-  \caption{The first definition is for the transitive closure where the
-  relation @{text R} is explicitly fixed. Simiraly the second definition
-  of the accessible part of the relation @{text R}. The last two definitions
-  specify the same inductive predicates, but this time defined inside
-  a locale.\label{fig:inddefsfixed}}
-  \end{figure}
-*}
-
 text {*
-  \begin{figure}[p]
+  \begin{figure}[t]
   \begin{isabelle}
   \railnontermfont{\rmfamily\itshape}
   \railterm{simpleinductive,where,for}
@@ -95,11 +118,10 @@
 *}
 
 text {*
-  For the first subtask, the syntax of the \simpleinductive{} command can be
-  described by the railroad diagram in Figure~\ref{fig:railroad}. This diagram
+  This leads directly to the railroad diagram shown in
+  Figure~\ref{fig:railroad} for the syntax of \simpleinductive{}. This diagram
   more or less translates directly into the parser:
 
-
   @{ML_chunk [display,gray] parser}
 
   which we described in Section~\ref{sec:parsingspecs}. If we feed into the