1 theory Ind_Interface

     2 imports Base Simple_Inductive_Package

     3 begin

     4 

     5 (*<*)

     6 ML {*

     7 structure SIP = SimpleInductivePackage

     8 *}

     9 (*>*)

    10 

    11 section{* The interface *}

    12 

    13 text {*

    14 \label{sec:ind-interface}

    15 In order to add a new inductive predicate to a theory with the help of our package, the user

    16 must \emph{invoke} it. For every package, there are essentially two different ways of invoking

    17 it, which we will refer to as \emph{external} and \emph{internal}. By external

    18 invocation we mean that the package is called from within a theory document. In this case,

    19 the type of the inductive predicate, as well as its introduction rules, are given as strings

    20 by the user. Before the package can actually make the definition, the type and introduction

    21 rules have to be parsed. In contrast, internal invocation means that the package is called

    22 by some other package. For example, the function definition package \cite{Krauss-IJCAR06}

    23 calls the inductive definition package to define the graph of the function. However, it is

    24 not a good idea for the function definition package to pass the introduction rules for the

    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

    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

    29 functions:

    30 @{ML_chunk [display] SIMPLE_INDUCTIVE_PACKAGE}

    31 The function for external invocation of the package is called @{ML_open add_inductive (SIP)},

    32 whereas the one for internal invocation is called @{ML_open add_inductive_i (SIP)}. Both

    33 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}.

    35 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.

    37 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

    39 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

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

    42 constitutes a valid local theory.

    43 Note that @{ML_open add_inductive_i (SIP)} expects the types

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

    45 logical framework, whereas @{ML_open add_inductive (SIP)}

    46 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

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

    49 the predicates and parameters as well. Note that @{ML_open add_inductive_i (SIP)} does not

    50 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

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

    53 @{ML_type Name.binding} using the function

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

    55 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

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

    58 The function @{ML_open add_inductive_i (SIP)} expects the formula to be specified using the datatype

    59 @{ML_type term}, whereas @{ML_open add_inductive (SIP)} expects it to be given as a string.

    60 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

    62 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

    64 functions for storing theorems in local theories.

    65 The implementation of the function @{ML_open add_inductive (SIP)} for external invocation

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

    67 and then passes them on to @{ML_open add_inductive_i (SIP)}:

    68 @{ML_chunk [display] add_inductive}

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

    70 @{ML_open [display] "Specification.read_specification:

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

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

    73   local_theory ->

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

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

    76   local_theory"}

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

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

    79 before being passed to @{ML_open read_specification (Specification)}. Note that the format

    80 for rules supported by @{ML_open read_specification (Specification)} is more general than

    81 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

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

    84 to be acceptable as an input for @{ML_open read_specification (Specification)}, we first

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

    86 has to be reversed later on by applying the function

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

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

    89 The function @{ML_open read_specification (Specification)} also returns the list \verb!vars!

    90 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

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

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

    94 @{ML_open read_specification (Specification)} will be bound by a meta-level universal

    95 quantifier.

    96 Finally, @{ML_open read_specification (Specification)} also returns another local theory,

    97 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:

    99 @{ML_response [display]

   100 "Specification.read_specification

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

   102    (Name.binding \"r\", SOME \"'a \<Rightarrow> 'a \<Rightarrow> bool\", NoSyn)]

   103   [[((Name.binding \"base\", []), [\"trcl r x x\"])],

   104    [((Name.binding \"step\", []), [\"trcl r x y \<Longrightarrow> r y z \<Longrightarrow> trcl r x z\"])]]

   105   @{context}"

   106 "((\<dots>,

   107   [(\<dots>,

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

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

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

   111    (\<dots>,

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

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

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

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

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

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

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

   119  \<dots>)

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

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

   122 In the list of variables passed to @{ML_open read_specification (Specification)}, we have

   123 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},

   125 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

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

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

   129 

   130 \paragraph{Parsers for theory syntax}

   131 

   132 Although the function @{ML_open add_inductive (SIP)} parses terms and types, it still

   133 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

   135 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

   137 package.

   138 

   139 \noindent

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

   141 *}

   142 

   143 simple_inductive

   144   trcl for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

   145 where

   146   base: "trcl r x x"

   147 | step: "trcl r x y \<Longrightarrow> r y z \<Longrightarrow> trcl r x z"

   148 (*<*)

   149 thm trcl_def

   150 thm trcl.induct

   151 thm base

   152 thm step

   153 thm trcl.intros

   154 

   155 lemma trcl_strong_induct:

   156   assumes trcl: "trcl r x y"

   157   and I1: "\<And>x. P x x"

   158   and I2: "\<And>x y z. P x y \<Longrightarrow> trcl r x y \<Longrightarrow> r y z \<Longrightarrow> P x z"

   159   shows "P x y" 

   160 proof -

   161   from trcl

   162   have "P x y \<and> trcl r x y"

   163   proof induct

   164     case (base x)

   165     from I1 and trcl.base show ?case ..

   166   next

   167     case (step x y z)

   168     then have "P x y" and "trcl r x y" by simp_all

   169     from `P x y` `trcl r x y` `r y z` have "P x z"

   170       by (rule I2)

   171     moreover from `trcl r x y` `r y z` have "trcl r x z"

   172       by (rule trcl.step)

   173     ultimately show ?case ..

   174   qed

   175   then show ?thesis ..

   176 qed

   177 (*>*)

   178 

   179 text {*

   180 \noindent

   181 Even and odd numbers can be defined by

   182 *}

   183 

   184 simple_inductive

   185   even and odd

   186 where

   187   even0: "even 0"

   188 | evenS: "odd n \<Longrightarrow> even (Suc n)"

   189 | oddS: "even n \<Longrightarrow> odd (Suc n)"

   190 (*<*)

   191 thm even_def odd_def

   192 thm even.induct odd.induct

   193 thm even0

   194 thm evenS

   195 thm oddS

   196 thm even_odd.intros

   197 (*>*)

   198 

   199 text {*

   200 \noindent

   201 The accessible part of a relation can be introduced as follows:

   202 *}

   203 

   204 simple_inductive

   205   accpart for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

   206 where

   207   accpartI: "(\<And>y. r y x \<Longrightarrow> accpart r y) \<Longrightarrow> accpart r x"

   208 (*<*)

   209 thm accpart_def

   210 thm accpart.induct

   211 thm accpartI

   212 (*>*)

   213 

   214 text {*

   215 \noindent

   216 Moreover, it should also be possible to define the accessible part

   217 inside a locale fixing the relation @{text r}:

   218 *}

   219 

   220 locale rel =

   221   fixes r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

   222 

   223 simple_inductive (in rel) accpart'

   224 where

   225   accpartI': "\<And>x. (\<And>y. r y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"

   226 (*<*)

   227 context rel

   228 begin

   229 

   230 thm accpartI'

   231 thm accpart'.induct

   232 

   233 end

   234 

   235 thm rel.accpartI'

   236 thm rel.accpart'.induct

   237 

   238 ML {*

   239 val (result, lthy) = SimpleInductivePackage.add_inductive

   240   [(Name.binding "trcl'", NONE, NoSyn)] [(Name.binding "r", SOME "'a \<Rightarrow> 'a \<Rightarrow> bool", NoSyn)]

   241   [((Name.binding "base", []), "\<And>x. trcl' r x x"), ((Name.binding "step", []), "\<And>x y z. trcl' r x y \<Longrightarrow> r y z \<Longrightarrow> trcl' r x z")]

   242   (TheoryTarget.init NONE @{theory})

   243 *}

   244 (*>*)

   245 

   246 text {*

   247 \noindent

   248 In this context, it is important to note that Isabelle distinguishes

   249 between \emph{outer} and \emph{inner} syntax. Theory commands such as

   250 \isa{\isacommand{simple{\isacharunderscore}inductive} $\ldots$ \isacommand{for} $\ldots$ \isacommand{where} $\ldots$}

   251 belong to the outer syntax, whereas items in quotation marks, in particular

   252 terms such as @{text [source] "trcl r x x"} and types such as

   253 @{text [source] "'a \<Rightarrow> 'a \<Rightarrow> bool"} belong to the inner syntax.

   254 Separating the two layers of outer and inner syntax greatly simplifies

   255 matters, because the parser for terms and types does not have to know

   256 anything about the possible syntax of theory commands, and the parser

   257 for theory commands need not be concerned about the syntactic structure

   258 of terms and types.

   259 

   260 \medskip

   261 \noindent

   262 The syntax of the \isa{\isacommand{simple{\isacharunderscore}inductive}} command

   263 can be described by the following railroad diagram:

   264 \begin{rail}

   265   'simple\_inductive' target? fixes ('for' fixes)? \\

   266   ('where' (thmdecl? prop + '|'))?

   267   ;

   268 \end{rail}

   269 

   270 \paragraph{Functional parsers}

   271 

   272 For parsing terms and types, Isabelle uses a rather general and sophisticated

   273 algorithm due to Earley, which is driven by \emph{priority grammars}.

   274 In contrast, parsers for theory syntax are built up using a set of combinators.

   275 Functional parsing using combinators is a well-established technique, which

   276 has been described by many authors, including Paulson \cite{paulson-ML-91}

   277 and Wadler \cite{Wadler-AFP95}. 

   278 The central idea is that a parser is a function of type @{ML_type "'a list -> 'b * 'a list"},

   279 where @{ML_type "'a"} is a type of \emph{tokens}, and @{ML_type "'b"} is a type for

   280 encoding items that the parser has recognized. When a parser is applied to a

   281 list of tokens whose prefix it can recognize, it returns an encoding of the

   282 prefix as an element of type @{ML_type "'b"}, together with the suffix of the list

   283 containing the remaining tokens. Otherwise, the parser raises an exception

   284 indicating a syntax error. The library for writing functional parsers in

   285 Isabelle can roughly be split up into two parts. The first part consists of a

   286 collection of generic parser combinators that are contained in the structure

   287 @{ML_struct Scan} defined in the file @{ML_file "Pure/General/scan.ML"} in the Isabelle

   288 sources. While these combinators do not make any assumptions about the concrete

   289 structure of the tokens used, the second part of the library consists of combinators

   290 for dealing with specific token types.

   291 The following is an excerpt from the signature of @{ML_struct Scan}:

   292 \begin{mytable}

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

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

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

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

   297 @{ML_open "optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a" (Scan)} \\

   298 @{ML_open "repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" (Scan)} \\

   299 @{ML_open "repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" (Scan)} \\

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

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

   302 \end{mytable}

   303 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.

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

   306 @{ML_open "p || q" for p q} returns the result of \texttt{p}, otherwise it returns

   307 the result of \texttt{q}. The parser @{ML_open "p -- q" for p q} first parses an

   308 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"}

   310 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

   312 parsed items. The parsers @{ML_open "p |-- q" for p q} and @{ML_open "p --| q" for p q}

   313 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.

   315 If \texttt{p} succeeds, the parser @{ML_open "optional p x" for p x (Scan)} returns the result

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

   317 @{ML_open "repeat p" for p (Scan)} applies \texttt{p} as often as it can, returning a possibly

   318 empty list of parsed items. The parser @{ML_open "repeat1 p" for p (Scan)} is similar,

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

   320 @{ML_open "p >> f" for p f} uses \texttt{p} to parse an item of type @{ML_type "'b"}, to which

   321 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"}.

   323 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,

   325 then an enclosing parser such as

   326 @{ML_open [display] "q -- p || r" for p q r}

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

   328 @{ML_open [display] "q -- !! err p || r" for err p q r}

   329 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

   331 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

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

   334 

   335 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

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

   338 defined in @{ML_struct Scan}:

   339 \begin{mytable}

   340 @{ML_open "one: ('a -> bool) -> 'a list -> 'a * 'a list" (Scan)} \\

   341 @{ML_open "$$ : string -> string list -> string * string list"}

   342 \end{mytable}

   343 The parser @{ML_open "one pred" for pred (Scan)} parses exactly one token that

   344 satisfies the predicate \texttt{pred}, whereas @{ML_open "$$ s" for s} only

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

   346 express @{ML_open "$$ s" for s} using @{ML_open "one" (Scan)}:

   347 @{ML_open [display] "one (fn s' => s' = s)" for s (Scan)}

   348 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}'':

   350 @{ML_response [display]

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

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

   353 "(((((\"h\", \"e\"), \"l\"), \"l\"), \"o\"), [\" \", \"w\", \"o\", \"r\", \"l\", \"d\"])

   354 : ((((string * string) * string) * string) * string) * string list"}

   355 Most of the time, however, we will have to deal with tokens that are not just strings.

   356 The parsers for the theory syntax, as well as the parsers for the argument syntax

   357 of proof methods and attributes use the token type @{ML_type OuterParse.token},

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

   359 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"}.

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

   362 \begin{mytable}

   363 @{ML_open "$$$ : string -> token list -> string * token list" (OuterParse)} \\

   364 @{ML_open "enum1: string -> (token list -> 'a * token list) -> token list ->

   365   'a list * token list" (OuterParse)} \\

   366 @{ML_open "prop: token list -> string * token list" (OuterParse)} \\

   367 @{ML_open "opt_target: token list -> string option * token list" (OuterParse)} \\

   368 @{ML_open "fixes: token list ->

   369   (Name.binding * string option * mixfix) list * token list" (OuterParse)} \\

   370 @{ML_open "for_fixes: token list ->

   371   (Name.binding * string option * mixfix) list * token list" (OuterParse)} \\

   372 @{ML_open "!!! : (token list -> 'a) -> token list -> 'a" (OuterParse)}

   373 \end{mytable}

   374 The parsers @{ML_open "$$$" (OuterParse)} and @{ML_open "!!!" (OuterParse)} are

   375 defined using the parsers @{ML_open "one" (Scan)} and @{ML "!!"} from

   376 @{ML_struct Scan}.

   377 The parser @{ML_open "enum1 s p" for s p (OuterParse)} parses a non-emtpy list of items

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

   379 A proposition can be parsed using the function @{ML_open prop (OuterParse)}.

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

   381 specific parser function @{ML_open prop (OuterParse)} leads to more instructive

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

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

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

   385 can be parsed using @{ML_open opt_target (OuterParse)}.

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

   387 types and syntax, are parsed using the functions @{ML_open "fixes" (OuterParse)}

   388 and @{ML_open for_fixes (OuterParse)}, respectively.

   389 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:

   391 \begin{mytable}

   392 @{ML_open "opt_thm_name:

   393   string -> token list -> Attrib.binding * token list" (SpecParse)}

   394 \end{mytable}

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

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

   397 @{ML_chunk [display] syntax}

   398 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

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

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

   402 @{ML_open "!!!" (OuterParse)} is used: once the keyword \texttt{where}

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

   404 Had we not used the combinator @{ML_open "!!!" (OuterParse)}, a

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

   406 to respond with the somewhat misleading error message

   407 \begin{verbatim}

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

   409 \end{verbatim}

   410 rather than with the more instructive message

   411 \begin{verbatim}

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

   413 \end{verbatim}

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

   415 @{ML_open add_inductive (SimpleInductivePackage)}, which yields a local theory

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

   417 Isabelle/Isar are realized by transition transformers of type

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

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

   420 the function

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

   422   (local_theory -> local_theory) ->

   423   Toplevel.transition -> Toplevel.transition"}

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

   425 to be used as a basis for the local theory. The whole parser for our command has type

   426 @{ML_type [display] "OuterLex.token list ->

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

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

   429 to the system via the function

   430 @{ML [display] "OuterSyntax.command :

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

   432 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,

   434 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,

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

   437 @{ML "OuterKeyword.thy_goal"}, which is similar to @{ML_open thy_decl (OuterKeyword)},

   438 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

   440 not change the context. For example, the @{ML_open thy_goal (OuterKeyword)} kind is used

   441 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

   443 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.

   445 *}

   446 

   447 (*<*)

   448 end

   449 (*>*)