72   can also contain typing- and syntax anotations); \emph{prop} stands for a 

    72   can also contain typing- and syntax annotations); \emph{prop} stands for a 

    79   To be able to write down the specification in Isabelle, we have to introduce

    79   To be able to write down the specifications or inductive predicates, we have 

    80   to introduce

    83   shown in Figure~ref{fig:specs}. The general syntax we will parse is specified

    84   shown in Figure~\ref{fig:specs}. The general syntax we will parse is specified

    84   in the railroad diagram shown in Figure~\ref{fig:railroad} for the syntax of 

    85   in the railroad diagram shown in Figure~\ref{fig:railroad}. This diagram more 

    85   \simpleinductive{}. This diagram more or less translates directly into 

    86   or less translates directly into the parser:

    86   the parser:

    98   which we explaind in Section~\ref{sec:parsingspecs}.

    98   which we explained in Section~\ref{sec:parsingspecs}.  However, if you look

    99   If you look closely, there is no code for parsing the optional

    99   closely, there is no code for parsing the target given optionally after the

   100   target in Figure~\ref{fig:railroad}. This is an ``advanced'' feature

   100   keyword. This is an ``advanced'' feature which we will inherit for ``free''

   101   which we will inherit for ``free'' from the infrastructure on which

   101   from the infrastructure on which we shall build the package. The target

   102   we build the package. The target stands for a locale and allows us 

   102   stands for a locale and allows us to specify

   103   to specify

   126   Note that in these definitions the parameter @{text R} for the

   125   Note that in these definitions the parameter @{text R}, standing for the

   127   relation is left implicit.  If we feed into the 

   126   relation, is left implicit. For the moment we will ignore this kind

   128   parser the string (which corresponds to our definition of @{term even} and 

   127   of implicit parameters and rely on the fact that the infrastructure will

   129   @{term odd}):

   128   deal with them. Later, however, we will come back to them.

   129 

   130   If we feed into the parser the string that corresponds to our definition 

   131   of @{term even} and @{term odd}

   147   then we get back the predicates (with type

   149   then we get back the specifications of the predicates (with type and syntax annotations), 

   148   and syntax annotations), and the specifications of the introduction 

   150   and specifications of the introduction rules. This is all the information we

   149   rules. This is all the information we

   151   done in Lines 6 and 7 in the code below.

   152   done in Lines 5 to 7 in the code below.

   152 *}

   153 *}

   153 

   154 

   154 (*<*)

   155 (*<*)ML %linenos{*fun add_inductive pred_specs rule_specs lthy = lthy 

   155 ML{* fun add_inductive pred_specs rule_specs lthy = lthy *}

   156 fun add_inductive_cmd pred_specs rule_specs lthy =

   156 (*>*)

   157 let

   158   val ((pred_specs', rule_specs'), _) = 

   159          Specification.read_spec pred_specs rule_specs lthy

   160 in

   161   add_inductive pred_specs' rule_specs' lthy

   162 end*}(*>*)

   163 ML_val %linenosgray{*val specification =

   164   spec_parser >>

   165     (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)

   166 

   167 val _ = OuterSyntax.local_theory "simple_inductive" 

   168           "definition of simple inductive predicates"

   169              OuterKeyword.thy_decl specification*}

   170 

   171 text {*

   172   We call @{ML local_theory in OuterSyntax} with the kind-indicator 

   173   @{ML thy_decl in OuterKeyword} since the package does not need to open 

   174   up any proof (see Section~\ref{sec:newcommand}). 

   175   The auxiliary function @{text specification} in Lines 1 to 3

   176   gathers the information from the parser to be processed further

   177   by the function @{text "add_inductive_cmd"}, which we describe below. 

   178 

   179   Note that the predicates when they come out of the parser are just some

   180   ``naked'' strings: they have no type yet (even if we annotate them with

   181   types) and they are also not defined constants yet (which the predicates 

   182   eventually will be).  Also the introduction rules are just strings. What we have

   183   to do first is to transform the parser's output into some internal

   184   datastructures that can be processed further. For this we can use the

   185   function @{ML read_spec in Specification}. This function takes some strings

   186   (with possible typing annotations) and some rule specifications, and attempts

   187   to find a typing according to the given type constraints given by the 

   188   user and the type constraints by the ``ambient'' theory. It returns 

   189   the type for the predicates and also returns typed terms for the

   190   introduction rules. So at the heart of the function 

   191   @{text "add_inductive_cmd"} is a call to @{ML read_spec in Specification}.

   192 *}

   164 end*} 

   200 end*}

   165 

   201 

   166 

   202 ML {* Specification.read_spec *}

   167 ML{*val specification =

   203 

   168   spec_parser >>

   204 text {*

   169     (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)*}

   205   Once we have the input data as some internal datastructure, we call

   170 

   206   the function @{ML add_inductive}. This function does the  heavy duty 

   171 ML{*val _ = OuterSyntax.local_theory "simple_inductive" 

   207   lifting in the package: it generates definitions for the 

   172               "definition of simple inductive predicates"

   208   predicates and derives from them corresponding induction principles and 

   173                  OuterKeyword.thy_decl specification*}

   209   introduction rules. The description of this function will span over

   174 

   210   the next two sections.

   175 

   176 text {*

   177   We call @{ML OuterSyntax.command} with the kind-indicator @{ML

   178   OuterKeyword.thy_decl} since the package does not need to open up any goal

   179   state (see Section~\ref{sec:newcommand}). Note that the predicates and

   180   parameters are at the moment only some ``naked'' variables: they have no

   181   type yet (even if we annotate them with types) and they are also no defined

   182   constants yet (which the predicates will eventually be).  In Lines 1 to 4 we

   183   gather the information from the parser to be processed further. The locale

   184   is passed as argument to the function @{ML

   185   Toplevel.local_theory}.\footnote{FIXME Is this already described?} The other

   186   arguments, i.e.~the predicates, parameters and intro rule specifications,

   187   are passed to the function @{ML add_inductive in SimpleInductivePackage}

   188   (Line 4).

   189 

   190   We now come to the second subtask of the package, namely transforming the 

   191   parser output into some internal datastructures that can be processed further. 

   192   Remember that at the moment the introduction rules are just strings, and even

   193   if the predicates and parameters can contain some typing annotations, they

   194   are not yet in any way reflected in the introduction rules. So the task of

   195   @{ML add_inductive in SimpleInductivePackage} is to transform the strings

   196   into properly typed terms. For this it can use the function 

   197   @{ML read_spec in Specification}. This function takes some constants

   198   with possible typing annotations and some rule specifications and attempts to

   199   find a type according to the given type constraints and the type constraints

   200   by the surrounding (local theory). However this function is a bit

   201   too general for our purposes: we want that each introduction rule has only 

   202   name (for example @{text even0} or @{text evenS}), if a name is given at all.

   203   The function @{ML read_spec in Specification} however allows more

   204   than one rule. Since it is quite convenient to rely on this function (instead of

   205   building your own) we just quick ly write a wrapper function that translates

   206   between our specific format and the general format expected by 

   207   @{ML read_spec in Specification}. The code of this wrapper is as follows:

   208 

   209   @{ML_chunk [display,gray,linenos] read_specification}

   210 

   211   It takes a list of constants, a list of rule specifications and a local theory 

   212   as input. Does the transformation of the rule specifications in Line 3; calls

   213   the function and transforms the now typed rule specifications back into our

   214   format and returns the type parameter and typed rule specifications. 

   215 

   216 

   217    @{ML_chunk [display,gray,linenos] add_inductive}

   218 

   219 

   220   In order to add a new inductive predicate to a theory with the help of our

   221   package, the user must \emph{invoke} it. For every package, there are

   222   essentially two different ways of invoking it, which we will refer to as

   223   \emph{external} and \emph{internal}. By external invocation we mean that the

   224   package is called from within a theory document. In this case, the

   225   specification of the inductive predicate, including type annotations and

   226   introduction rules, are given as strings by the user. Before the package can

   227   actually make the definition, the type and introduction rules have to be

   228   parsed. In contrast, internal invocation means that the package is called by

   229   some other package. For example, the function definition package

   230   calls the inductive definition package to define the

   231   graph of the function. However, it is not a good idea for the function

   232   definition package to pass the introduction rules for the function graph to

   233   the inductive definition package as strings. In this case, it is better to

   234   directly pass the rules to the package as a list of terms, which is more

   235   robust than handling strings that are lacking the additional structure of

   236   terms. These two ways of invoking the package are reflected in its ML

   237   programming interface, which consists of two functions:

   238 

   239 

   240   @{ML_chunk [display,gray] SIMPLE_INDUCTIVE_PACKAGE}

   241 *}

   242 

   243 text {*

   244   (FIXME: explain Binding.binding; Attrib.binding somewhere else)

   245 

   246 

   247   The function for external invocation of the package is called @{ML

   248   add_inductive in SimpleInductivePackage}, whereas the one for internal

   249   invocation is called @{ML add_inductive_i in SimpleInductivePackage}. Both

   250   of these functions take as arguments the names and types of the inductive

   251   predicates, the names and types of their parameters, the actual introduction

   252   rules and a \emph{local theory}.  They return a local theory containing the

   253   definition and the induction principle as well introduction rules. 

   254 

   255   Note that @{ML add_inductive_i in SimpleInductivePackage} expects

   256   the types of the predicates and parameters to be specified using the

   257   datatype @{ML_type typ} of Isabelle's logical framework, whereas @{ML

   258   add_inductive in SimpleInductivePackage} expects them to be given as

   259   optional strings. If no string is given for a particular predicate or

   260   parameter, this means that the type should be inferred by the

   261   package. 

   262 

   263 

   264   Additional \emph{mixfix syntax} may be associated with the

   265   predicates and parameters as well. Note that @{ML add_inductive_i in

   266   SimpleInductivePackage} does not allow mixfix syntax to be associated with

   267   parameters, since it can only be used for parsing.\footnote{FIXME: why ist it there then?} 

   268   The names of the

   269   predicates, parameters and rules are represented by the type @{ML_type

   270   Binding.binding}. Strings can be turned into elements of the type @{ML_type

   271   Binding.binding} using the function @{ML [display] "Binding.name : string ->

   272   Binding.binding"} Each introduction rule is given as a tuple containing its

   273   name, a list of \emph{attributes} and a logical formula. Note that the type

   274   @{ML_type Attrib.binding} used in the list of introduction rules is just a

   275   shorthand for the type @{ML_type "Binding.binding * Attrib.src list"}.  The

   276   function @{ML add_inductive_i in SimpleInductivePackage} expects the formula

   277   to be specified using the datatype @{ML_type term}, whereas @{ML

   278   add_inductive in SimpleInductivePackage} expects it to be given as a string.

   279   An attribute specifies additional actions and transformations that should be

   280   applied to a theorem, such as storing it in the rule databases used by

   281   automatic tactics like the simplifier. The code of the package, which will

   282   be described in the following section, will mostly treat attributes as a

   283   black box and just forward them to other functions for storing theorems in

   284   local theories.  The implementation of the function @{ML add_inductive in

   285   SimpleInductivePackage} for external invocation of the package is quite

   286   simple. Essentially, it just parses the introduction rules and then passes

   287   them on to @{ML add_inductive_i in SimpleInductivePackage}:

   288 

   289   @{ML_chunk [display] add_inductive}

   290 

   291   For parsing and type checking the introduction rules, we use the function

   292   

   293   @{ML [display] "Specification.read_specification:

   294   (Binding.binding * string option * mixfix) list ->  (*{variables}*)

   295   (Attrib.binding * string list) list ->  (*{rules}*)

   296   local_theory ->

   297   (((Binding.binding * typ) * mixfix) list *

   298    (Attrib.binding * term list) list) *

   299   local_theory"}

   300 *}

   301 

   302 text {*

   303   During parsing, both predicates and parameters are treated as variables, so

   304   the lists \verb!preds_syn! and \verb!params_syn! are just appended

   305   before being passed to @{ML read_spec in Specification}. Note that the format

   306   for rules supported by @{ML read_spec in Specification} is more general than

   307   what is required for our package. It allows several rules to be associated

   308   with one name, and the list of rules can be partitioned into several

   309   sublists. In order for the list \verb!intro_srcs! of introduction rules

   310   to be acceptable as an input for @{ML read_spec in Specification}, we first

   311   have to turn it into a list of singleton lists. This transformation

   312   has to be reversed later on by applying the function

   313   @{ML [display] "the_single: 'a list -> 'a"}

   314   to the list \verb!specs! containing the parsed introduction rules.

   315   The function @{ML read_spec in Specification} also returns the list \verb!vars!

   316   of predicates and parameters that contains the inferred types as well.

   317   This list has to be chopped into the two lists \verb!preds_syn'! and

   318   \verb!params_syn'! for predicates and parameters, respectively.

   319   All variables occurring in a rule but not in the list of variables passed to

   320   @{ML read_spec in Specification} will be bound by a meta-level universal

   321   quantifier.

   322 *}

   323 

   324 text {*

   325   Finally, @{ML read_specification in Specification} also returns another local theory,

   326   but we can safely discard it. As an example, let us look at how we can use this

   327   function to parse the introduction rules of the @{text trcl} predicate:

   328 

   329   @{ML_response [display]

   330 "Specification.read_specification

   331   [(Binding.name \"trcl\", NONE, NoSyn),

   332    (Binding.name \"r\", SOME \"'a \<Rightarrow> 'a \<Rightarrow> bool\", NoSyn)]

   333   [((Binding.name \"base\", []), [\"trcl r x x\"]),

   334    ((Binding.name \"step\", []), [\"trcl r x y \<Longrightarrow> r y z \<Longrightarrow> trcl r x z\"])]

   335   @{context}"

   336 "((\<dots>,

   337   [(\<dots>,

   338     [Const (\"all\", \<dots>) $ Abs (\"x\", TFree (\"'a\", \<dots>),

   339        Const (\"Trueprop\", \<dots>) $

   340          (Free (\"trcl\", \<dots>) $ Free (\"r\", \<dots>) $ Bound 0 $ Bound 0))]),

   341    (\<dots>,

   342     [Const (\"all\", \<dots>) $ Abs (\"x\", TFree (\"'a\", \<dots>),

   343        Const (\"all\", \<dots>) $ Abs (\"y\", TFree (\"'a\", \<dots>),

   344          Const (\"all\", \<dots>) $ Abs (\"z\", TFree (\"'a\", \<dots>),

   345            Const (\"==>\", \<dots>) $

   346              (Const (\"Trueprop\", \<dots>) $

   347                (Free (\"trcl\", \<dots>) $ Free (\"r\", \<dots>) $ Bound 2 $ Bound 1)) $

   348              (Const (\"==>\", \<dots>) $ \<dots> $ \<dots>))))])]),

   349  \<dots>)

   350 : (((Binding.binding * typ) * mixfix) list *

   351    (Attrib.binding * term list) list) * local_theory"}

   352 

   353   In the list of variables passed to @{ML read_specification in Specification}, we have

   354   used the mixfix annotation @{ML NoSyn} to indicate that we do not want to associate any

   355   mixfix syntax with the variable. Moreover, we have only specified the type of \texttt{r},

   356   whereas the type of \texttt{trcl} is computed using type inference.

   357   The local variables \texttt{x}, \texttt{y} and \texttt{z} of the introduction rules

   358   are turned into bound variables with the de Bruijn indices,

   359   whereas \texttt{trcl} and \texttt{r} remain free variables.

   360 

   361 *}

   362 

   363 text {*

   364 

   365   \paragraph{Parsers for theory syntax}

   366 

   367   Although the function @{ML add_inductive in SimpleInductivePackage} parses terms and types, it still

   368   cannot be used to invoke the package directly from within a theory document.

   369   In order to do this, we have to write another parser. Before we describe

   370   the process of writing parsers for theory syntax in more detail, we first

   371   show some examples of how we would like to use the inductive definition

   372   package.

   373 

   374 

   375   The definition of the transitive closure should look as follows:

   376 *}

   377 

   378 ML {* SpecParse.opt_thm_name *}

   379 

   380 text {*

   381 

   382   A proposition can be parsed using the function @{ML prop in OuterParse}.

   383   Essentially, a proposition is just a string or an identifier, but using the

   384   specific parser function @{ML prop in OuterParse} leads to more instructive

   385   error messages, since the parser will complain that a proposition was expected

   386   when something else than a string or identifier is found.

   387   An optional locale target specification of the form \isa{(\isacommand{in}\ $\ldots$)}

   388   can be parsed using @{ML opt_target in OuterParse}.

   389   The lists of names of the predicates and parameters, together with optional

   390   types and syntax, are parsed using the functions @{ML "fixes" in OuterParse}

   391   and @{ML for_fixes in OuterParse}, respectively.

   392   In addition, the following function from @{ML_struct SpecParse} for parsing

   393   an optional theorem name and attribute, followed by a delimiter, will be useful:

   394   

   395   \begin{table}

   396   @{ML "opt_thm_name:

   397   string -> Attrib.binding parser" in SpecParse}

   398   \end{table}

   399 

   400   We now have all the necessary tools to write the parser for our

   401   \isa{\isacommand{simple{\isacharunderscore}inductive}} command:

   402   

   403  

   404   Once all arguments of the command have been parsed, we apply the function

   405   @{ML add_inductive in SimpleInductivePackage}, which yields a local theory

   406   transformer of type @{ML_type "local_theory -> local_theory"}. Commands in

   407   Isabelle/Isar are realized by transition transformers of type

   408   @{ML_type [display] "Toplevel.transition -> Toplevel.transition"}

   409   We can turn a local theory transformer into a transition transformer by using

   410   the function

   411 

   412   @{ML [display] "Toplevel.local_theory : string option ->

   413   (local_theory -> local_theory) ->

   414   Toplevel.transition -> Toplevel.transition"}

   415  

   416   which, apart from the local theory transformer, takes an optional name of a locale

   417   to be used as a basis for the local theory. 

   418 

   419   (FIXME : needs to be adjusted to new parser type)

   420 

   421   {\it

   422   The whole parser for our command has type

   423   @{text [display] "OuterLex.token list ->

   424   (Toplevel.transition -> Toplevel.transition) * OuterLex.token list"}

   425   which is abbreviated by @{text OuterSyntax.parser_fn}. The new command can be added

   426   to the system via the function

   427   @{text [display] "OuterSyntax.command :

   428   string -> string -> OuterKeyword.T -> OuterSyntax.parser_fn -> unit"}

   429   which imperatively updates the parser table behind the scenes. }

   430 

   431   In addition to the parser, this

   432   function takes two strings representing the name of the command and a short description,

   433   as well as an element of type @{ML_type OuterKeyword.T} describing which \emph{kind} of

   434   command we intend to add. Since we want to add a command for declaring new concepts,

   435   we choose the kind @{ML "OuterKeyword.thy_decl"}. Other kinds include

   436   @{ML "OuterKeyword.thy_goal"}, which is similar to @{ML thy_decl in OuterKeyword},

   437   but requires the user to prove a goal before making the declaration, or

   438   @{ML "OuterKeyword.diag"}, which corresponds to a purely diagnostic command that does

   439   not change the context. For example, the @{ML thy_goal in OuterKeyword} kind is used

   440   by the \isa{\isacommand{function}} command \cite{Krauss-IJCAR06}, which requires the user

   441   to prove that a given set of equations is non-overlapping and covers all cases. The kind

   442   of the command should be chosen with care, since selecting the wrong one can cause strange

   443   behaviour of the user interface, such as failure of the undo mechanism.

   444 *}

   445 

   446 text {*

   447   Note that the @{text trcl} predicate has two different kinds of parameters: the

   448   first parameter @{text R} stays \emph{fixed} throughout the definition, whereas

   449   the second and third parameter changes in the ``recursive call''. This will

   450   become important later on when we deal with fixed parameters and locales. 

   451 

   452 

   453  

   454   The purpose of the package we show next is that the user just specifies the

   455   inductive predicate by stating some introduction rules and then the packages

   456   makes the equivalent definition and derives from it the needed properties.

   457 *}

   458 

   459 text {*

   460   (FIXME: perhaps move somewhere else)

   461 

   462   The point of these examples is to get a feeling what the automatic proofs 

   463   should do in order to solve all inductive definitions we throw at them. For this 

   464   it is instructive to look at the general construction principle 

   465   of inductive definitions, which we shall do in the next section.

   466 

   467   The code of the inductive package falls roughly in tree parts: the first

   468   deals with the definitions, the second with the induction principles and 

   469   the third with the introduction rules. 

   470