25 function graph to the inductive definition package as strings. In this case, it is better

    25 function graph to the inductive definition package as strings. In this case, it is better

    26 to directly pass the rules to the package as a list of terms, which is more robust than

    26 to directly pass the rules to the package as a list of terms, which is more robust than

    27 handling strings that are lacking the additional structure of terms. These two ways of

    27 handling strings that are lacking the additional structure of terms. These two ways of

    28 invoking the package are reflected in its ML programming interface, which consists of two

    28 invoking the package are reflected in its ML programming interface, which consists of two

    29 functions:

    29 functions:

    30 @{ML_chunk [display] SIMPLE_INDUCTIVE_PACKAGE}

    31 @{ML_chunk [display] SIMPLE_INDUCTIVE_PACKAGE}

    33 of these functions take as arguments the names and types of the inductive predicates, the

    37 of these functions take as arguments the names and types of the inductive predicates, the

    34 names and types of their parameters, the actual introduction rules and a \emph{local theory}.

    38 names and types of their parameters, the actual introduction rules and a \emph{local theory}.

    35 They return a local theory containing the definition, together with a tuple containing

    39 They return a local theory containing the definition, together with a tuple containing

    36 the introduction and induction rules, which are stored in the local theory, too.

    40 the introduction and induction rules, which are stored in the local theory, too.

    37 In contrast to an ordinary theory, which simply consists of a type signature, as

    41 In contrast to an ordinary theory, which simply consists of a type signature, as

    38 well as tables for constants, axioms and theorems, a local theory also contains

    42 well as tables for constants, axioms and theorems, a local theory also contains

    39 additional context information, such as locally fixed variables and local assumptions

    43 additional context information, such as locally fixed variables and local assumptions

    40 that may be used by the package. The type @{ML_type local_theory} is identical to the

    44 that may be used by the package. The type @{ML_type local_theory} is identical to the

    41 type of \emph{proof contexts} @{ML_type "Proof.context"}, although not every proof context

    45 type of \emph{proof contexts} @{ML_type "Proof.context"}, although not every proof context

    42 constitutes a valid local theory.

    46 constitutes a valid local theory.

    44 of the predicates and parameters to be specified using the datatype @{ML_type typ} of Isabelle's

    48 of the predicates and parameters to be specified using the datatype @{ML_type typ} of Isabelle's

    46 expects them to be given as optional strings. If no string is

    50 expects them to be given as optional strings. If no string is

    47 given for a particular predicate or parameter, this means that the type should be

    51 given for a particular predicate or parameter, this means that the type should be

    48 inferred by the package. Additional \emph{mixfix syntax} may be associated with

    52 inferred by the package. Additional \emph{mixfix syntax} may be associated with

    50 allow mixfix syntax to be associated with parameters, since it can only be used

    54 allow mixfix syntax to be associated with parameters, since it can only be used

    51 for parsing. The names of the predicates, parameters and rules are represented by the

    55 for parsing. The names of the predicates, parameters and rules are represented by the

    52 type @{ML_type Name.binding}. Strings can be turned into elements of the type

    56 type @{ML_type Name.binding}. Strings can be turned into elements of the type

    53 @{ML_type Name.binding} using the function

    57 @{ML_type Name.binding} using the function

    54 @{ML [display] "Name.binding : string -> Name.binding"}

    58 @{ML [display] "Name.binding : string -> Name.binding"}

    55 Each introduction rule is given as a tuple containing its name, a list of \emph{attributes}

    59 Each introduction rule is given as a tuple containing its name, a list of \emph{attributes}

    56 and a logical formula. Note that the type @{ML_type Attrib.binding} used in the list of

    60 and a logical formula. Note that the type @{ML_type Attrib.binding} used in the list of

    57 introduction rules is just a shorthand for the type @{ML_type "Name.binding * Attrib.src list"}.

    61 introduction rules is just a shorthand for the type @{ML_type "Name.binding * Attrib.src list"}.

    60 An attribute specifies additional actions and transformations that should be applied to

    64 An attribute specifies additional actions and transformations that should be applied to

    61 a theorem, such as storing it in the rule databases used by automatic tactics

    65 a theorem, such as storing it in the rule databases used by automatic tactics

    62 like the simplifier. The code of the package, which will be described in the following

    66 like the simplifier. The code of the package, which will be described in the following

    63 section, will mostly treat attributes as a black box and just forward them to other

    67 section, will mostly treat attributes as a black box and just forward them to other

    64 functions for storing theorems in local theories.

    68 functions for storing theorems in local theories.

    66 of the package is quite simple. Essentially, it just parses the introduction rules

    70 of the package is quite simple. Essentially, it just parses the introduction rules

    68 @{ML_chunk [display] add_inductive}

    72 @{ML_chunk [display] add_inductive}

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

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

    71   (Name.binding * string option * mixfix) list ->  (*{variables}*)

    75   (Name.binding * string option * mixfix) list ->  (*{variables}*)

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

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

    73   local_theory ->

    77   local_theory ->

    74   (((Name.binding * typ) * mixfix) list *

    78   (((Name.binding * typ) * mixfix) list *

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

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

    76   local_theory"}

    80   local_theory"}

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

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

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

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

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

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

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

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

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

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

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

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

    86 has to be reversed later on by applying the function

    93 has to be reversed later on by applying the function

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

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

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

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

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

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

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

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

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

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

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

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

    95 quantifier.

   102 quantifier.

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

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

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

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

    99 @{ML_response [display]

   109 @{ML_response [display]

   100 "Specification.read_specification

   110 "Specification.read_specification

   101   [(Name.binding \"trcl\", NONE, NoSyn),

   111   [(Name.binding \"trcl\", NONE, NoSyn),

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

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

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

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

   119  \<dots>)

   129  \<dots>)

   120 : (((Name.binding * typ) * mixfix) list *

   130 : (((Name.binding * typ) * mixfix) list *

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   130 \paragraph{Parsers for theory syntax}

   142 \paragraph{Parsers for theory syntax}

   131 

   143 

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

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

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

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

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

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

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

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

   137 package.

   149 package.

   292 \begin{mytable}

   304 \begin{mytable}

   293 @{ML "|| : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b"} \\

   305 @{ML "|| : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b"} \\

   294 @{ML "-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e"} \\

   306 @{ML "-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e"} \\

   295 @{ML "|-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e"} \\

   307 @{ML "|-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e"} \\

   296 @{ML "--| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e"} \\

   308 @{ML "--| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e"} \\

   300 @{ML ">> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c"} \\

   312 @{ML ">> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c"} \\

   301 @{ML "!! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b"}

   313 @{ML "!! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b"}

   302 \end{mytable}

   314 \end{mytable}

   303 Interestingly, the functions shown above are so generic that they do not

   315 Interestingly, the functions shown above are so generic that they do not

   304 even rely on the input and output of the parser being a list of tokens.

   316 even rely on the input and output of the parser being a list of tokens.

   305 If \texttt{p} succeeds, i.e.\ does not raise an exception, the parser

   317 If \texttt{p} succeeds, i.e.\ does not raise an exception, the parser

   308 item of type @{ML_type "'b"} using \texttt{p}, then passes the remaining tokens

   320 item of type @{ML_type "'b"} using \texttt{p}, then passes the remaining tokens

   309 of type @{ML_type "'c"} to \texttt{q}, which parses an item of type @{ML_type "'d"}

   321 of type @{ML_type "'c"} to \texttt{q}, which parses an item of type @{ML_type "'d"}

   310 and returns the remaining tokens of type @{ML_type "'e"}, which are finally

   322 and returns the remaining tokens of type @{ML_type "'e"}, which are finally

   311 returned together with a pair of type @{ML_type "'b * 'd"} containing the two

   323 returned together with a pair of type @{ML_type "'b * 'd"} containing the two

   313 work in a similar way as the previous one, with the difference that they

   325 work in a similar way as the previous one, with the difference that they

   314 discard the item parsed by the first and the second parser, respectively.

   326 discard the item parsed by the first and the second parser, respectively.

   316 of \texttt{p}, otherwise it returns the default value \texttt{x}. The parser

   328 of \texttt{p}, otherwise it returns the default value \texttt{x}. The parser

   319 but requires \texttt{p} to succeed at least once. The parser

   331 but requires \texttt{p} to succeed at least once. The parser

   321 it applies the function \texttt{f} yielding a value of type @{ML_type "'d"}, which

   333 it applies the function \texttt{f} yielding a value of type @{ML_type "'d"}, which

   322 is returned together with the remaining tokens of type @{ML_type "'c"}.

   334 is returned together with the remaining tokens of type @{ML_type "'c"}.

   323 Finally, @{ML "!!"} is used for transforming exceptions produced by parsers.

   335 Finally, @{ML "!!"} is used for transforming exceptions produced by parsers.

   324 If \texttt{p} raises an exception indicating that it cannot parse a given input,

   336 If \texttt{p} raises an exception indicating that it cannot parse a given input,

   325 then an enclosing parser such as

   337 then an enclosing parser such as

   327 will try the alternative parser \texttt{r}. By writing

   339 will try the alternative parser \texttt{r}. By writing

   329 instead, one can achieve that a failure of \texttt{p} causes the whole parser to abort.

   341 instead, one can achieve that a failure of \texttt{p} causes the whole parser to abort.

   330 The @{ML "!!"} operator is similar to the \emph{cut} operator in Prolog, which prevents

   342 The @{ML "!!"} operator is similar to the \emph{cut} operator in Prolog, which prevents

   331 the interpreter from backtracking. The \texttt{err} function supplied as an argument

   343 the interpreter from backtracking. The \texttt{err} function supplied as an argument

   332 to @{ML "!!"} can be used to produce an error message depending on the current

   344 to @{ML "!!"} can be used to produce an error message depending on the current

   333 state of the parser, as well as the optional error message returned by \texttt{p}.

   345 state of the parser, as well as the optional error message returned by \texttt{p}.

   335 So far, we have only looked at combinators that construct more complex parsers

   347 So far, we have only looked at combinators that construct more complex parsers

   336 from simpler parsers. In order for these combinators to be useful, we also need

   348 from simpler parsers. In order for these combinators to be useful, we also need

   337 some basic parsers. As an example, we consider the following two parsers

   349 some basic parsers. As an example, we consider the following two parsers

   338 defined in @{ML_struct Scan}:

   350 defined in @{ML_struct Scan}:

   339 \begin{mytable}

   351 \begin{mytable}

   342 \end{mytable}

   354 \end{mytable}

   345 accepts a token that equals the string \texttt{s}. Note that we can easily

   357 accepts a token that equals the string \texttt{s}. Note that we can easily

   348 As an example, let us look at how we can use @{ML "$$"} and @{ML "--"} to parse

   360 As an example, let us look at how we can use @{ML "$$"} and @{ML "--"} to parse

   349 the prefix ``\texttt{hello}'' of the character list ``\texttt{hello world}'':

   361 the prefix ``\texttt{hello}'' of the character list ``\texttt{hello world}'':

   350 @{ML_response [display]

   362 @{ML_response [display]

   351 "($$ \"h\" -- $$ \"e\" -- $$ \"l\" -- $$ \"l\" -- $$ \"o\")

   363 "($$ \"h\" -- $$ \"e\" -- $$ \"l\" -- $$ \"l\" -- $$ \"o\")

   352 [\"h\", \"e\", \"l\", \"l\", \"o\", \" \", \"w\", \"o\", \"r\", \"l\", \"d\"]"

   364 [\"h\", \"e\", \"l\", \"l\", \"o\", \" \", \"w\", \"o\", \"r\", \"l\", \"d\"]"

   358 which is identical to @{ML_type OuterLex.token}.

   370 which is identical to @{ML_type OuterLex.token}.

   359 The parser functions for the theory syntax are contained in the structure

   371 The parser functions for the theory syntax are contained in the structure

   360 @{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/outer_parse.ML"}.

   372 @{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/outer_parse.ML"}.

   361 In our parser, we will use the following functions:

   373 In our parser, we will use the following functions:

   362 \begin{mytable}

   374 \begin{mytable}

   373 \end{mytable}

   385 \end{mytable}

   376 @{ML_struct Scan}.

   388 @{ML_struct Scan}.

   378 recognized by the parser \texttt{p}, where the items are separated by \texttt{s}.

   390 recognized by the parser \texttt{p}, where the items are separated by \texttt{s}.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   391 \begin{mytable}

   403 \begin{mytable}

   394 \end{mytable}

   406 \end{mytable}

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

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

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

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

   397 @{ML_chunk [display] syntax}

   409 @{ML_chunk [display] syntax}

   398 The definition of the parser \verb!ind_decl! closely follows the railroad

   410 The definition of the parser \verb!ind_decl! closely follows the railroad

   399 diagram shown above. In order to make the code more readable, the structures

   411 diagram shown above. In order to make the code more readable, the structures

   400 @{ML_struct OuterParse} and @{ML_struct OuterKeyword} are abbreviated by

   412 @{ML_struct OuterParse} and @{ML_struct OuterKeyword} are abbreviated by

   401 \texttt{P} and \texttt{K}, respectively. Note how the parser combinator

   413 \texttt{P} and \texttt{K}, respectively. Note how the parser combinator

   403 has been parsed, a non-empty list of introduction rules must follow.

   415 has been parsed, a non-empty list of introduction rules must follow.

   405 \texttt{where} not followed by a list of rules would have caused the parser

   417 \texttt{where} not followed by a list of rules would have caused the parser

   406 to respond with the somewhat misleading error message

   418 to respond with the somewhat misleading error message

   407 \begin{verbatim}

   419 \begin{verbatim}

   408   Outer syntax error: end of input expected, but keyword where was found

   420   Outer syntax error: end of input expected, but keyword where was found

   409 \end{verbatim}

   421 \end{verbatim}

   410 rather than with the more instructive message

   422 rather than with the more instructive message

   411 \begin{verbatim}

   423 \begin{verbatim}

   412   Outer syntax error: proposition expected, but terminator was found

   424   Outer syntax error: proposition expected, but terminator was found

   413 \end{verbatim}

   425 \end{verbatim}

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

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

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

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

   417 Isabelle/Isar are realized by transition transformers of type

   429 Isabelle/Isar are realized by transition transformers of type

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

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

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

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

   420 the function

   432 the function

   432 which imperatively updates the parser table behind the scenes. In addition to the parser, this

   444 which imperatively updates the parser table behind the scenes. In addition to the parser, this

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   445 *}

   457 *}