--- a/ProgTutorial/Package/Ind_Code.thy	Tue Mar 31 16:50:13 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Tue Mar 31 20:31:18 2009 +0100
@@ -1101,4 +1101,68 @@
 thm Even_def
 thm Odd_def
 
+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 {*
+  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 
+
+*}
+
+(*
+simple_inductive
+  trcl'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  base: "trcl'' R x x"
+| step: "trcl'' R x y \<Longrightarrow> R y z \<Longrightarrow> trcl'' R x z"
+
+simple_inductive
+  accpart'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x"
+*)
+
 end