1104 text {* 

  1105   Second, we want that the user can specify fixed parameters.

  1106   Remember in the previous section we stated that the user can give the 

  1107   specification for the transitive closure of a relation @{text R} as 

  1108 *}

  1109 

  1110 simple_inductive

  1111   trcl\<iota>\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"

  1112 where

  1113   base: "trcl\<iota>\<iota> R x x"

  1114 | step: "trcl\<iota>\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota>\<iota> R x z"

  1115 

  1116 text {*

  1117   Note that there is no locale given in this specification---the parameter

  1118   @{text "R"} therefore needs to be included explicitly in @{term trcl\<iota>\<iota>}, but

  1119   stays fixed throughout the specification. The problem with this way of

  1120   stating the specification for the transitive closure is that it derives the

  1121   following induction principle.

  1122 

  1123   \begin{center}\small

  1124   \mprset{flushleft}

  1125   \mbox{\inferrule{

  1126              @{thm_style prem1  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\

  1127              @{thm_style prem2  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\

  1128              @{thm_style prem3  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}

  1129             {@{thm_style concl  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}}  

  1130   \end{center}

  1131 

  1132   But this does not correspond to the induction principle we derived by hand, which

  1133   was

  1134   

  1135   \begin{center}\small

  1136   \mprset{flushleft}

  1137   \mbox{\inferrule{

  1138              @{thm_style prem1  trcl_induct[no_vars]}\\\\

  1139              @{thm_style prem2  trcl_induct[no_vars]}\\\\

  1140              @{thm_style prem3  trcl_induct[no_vars]}}

  1141             {@{thm_style concl  trcl_induct[no_vars]}}}  

  1142   \end{center}

  1143 

  1144   The difference is that in the one derived by hand the relation @{term R} is not

  1145   a parameter of the proposition @{term P} to be proved and it is also not universally

  1146   qunatified in the second and third premise. The point is that the parameter @{term R}

  1147   stays fixed thoughout the definition and we do not want to regard it as an ``ordinary''

  1148   argument of the transitive closure, but one that can be freely instantiated. 

  1149   In order to recognise such parameters, we have to extend the specification

  1150   to include a mechanism to state fixed parameters. The user should be able

  1151   to write 

  1152 

  1153 *}

  1154 

  1155 (*

  1156 simple_inductive

  1157   trcl'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

  1158 where

  1159   base: "trcl'' R x x"

  1160 | step: "trcl'' R x y \<Longrightarrow> R y z \<Longrightarrow> trcl'' R x z"

  1161 

  1162 simple_inductive

  1163   accpart'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

  1164 where

  1165   accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x"

  1166 *)

  1167