7 text {*

     7 text {* 

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

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

    10   makes the equivalent definition and derives from it useful properties.

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

    12   a new command (see Section~\ref{sec:newcommand}).  As the keyword for the new

    13   command we use \simpleinductive{}. The specifications corresponding to our

    14   examples described earlier are:

    15 *}

    16 

    17 simple_inductive

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

    19 where

    20   base: "trcl R x x"

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

    22 

    23 simple_inductive

    24   even and odd

    25 where

    26   even0: "even 0"

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

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

    29 

    30 simple_inductive

    31   accpart :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"

    32 where

    33   accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"

    34 

    35 text {*

    36   We expect a constant (or constants) with possible typing annotations and a

    37   list of introduction rules. While these specifications are all

    38   straightforward, there is a technicality we like to deal with to do with

    39   fixed parameters and locales. Remember we pointed out that the parameter

    40   @{text R} is fixed throughout the specifications of @{text trcl} and @{text

    41   accpart}. The point is that they might be fixed in a locale and we like to

    42   support this. Accordingly we treat some parameters of the inductive

    43   definition specially; see Figure~\ref{fig:inddefsfixed} where the transitive

    44   closure and accessible part are defined with a fixed parameter @{text R} and

    45   also inside a locale fixing @{text R}.

    46 *}

    47 

    48 text_raw {*

    49 \begin{figure}[p]

    50 \begin{isabelle}

    51 *}

    52 simple_inductive

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

    54 where

    55   base: "trcl' R x x"

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

    57 

    58 simple_inductive

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

    60 where

    61   accpartI: "(\<forall>y. R y x \<longrightarrow> accpart' R y) \<Longrightarrow> accpart' R x"

    62 

    63 locale rel =

    64   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

    65 

    66 simple_inductive (in rel) trcl'' 

    67 where

    68   base: "trcl'' x x"

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

    70 

    71 simple_inductive (in rel) accpart''

    72 where

    73   accpartI: "(\<forall>y. R y x \<longrightarrow> accpart'' y) \<Longrightarrow> accpart'' x"

    74 text_raw {*

    75 \end{isabelle}

    76 \caption{The first definition is for the transitive closure where the

    77 relation @{text R} is explicitly fixed. Simiraly the second definition

    78 of the accessible part of the relation @{text R}. The last two definitions

    79 specify the same inductive predicates, but this time defined inside

    80 a locale.\label{fig:inddefsfixed}}

    81 \end{figure}

    82 *}

    83 

    84 text {*

    85 \begin{figure}[p]

    86 \begin{isabelle}

    87   \railnontermfont{\rmfamily\itshape}

    88   \railterm{simpleinductive,where,for}

    89   \railalias{simpleinductive}{\simpleinductive{}}

    90   \railalias{where}{\isacommand{where}}

    91   \railalias{for}{\isacommand{for}}

    92   \begin{rail}

    93   simpleinductive target? fixes (for fixes)? \\

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

    95   ;

    96   \end{rail}

    97 \end{isabelle}

    98 \caption{A railroad diagram describing the syntax of \simpleinductive{}. 

    99 The \emph{target} indicates an optional locale; the \emph{fixes} are an 

   100 \isacommand{and}-separated list of names for the inductive predicates (they

   101 can also contain typing- and syntax anotations); similarly the \emph{fixes} 

   102 after \isacommand{for} to indicate fixed parameters; \emph{prop} stands for a 

   103 introduction rule with an optional theorem declaration (\emph{thmdecl}).

   104 \label{fig:railroad}}

   105 \end{figure}

   106 *}

   107 

   108 text {*

   109   The syntax of the \simpleinductive{} command can be described by the

   110   railroad diagram in Figure~\ref{fig:railroad}. This diagram more or less

   111   translates directly into the parser

   112 

   113    @{ML_chunk [display,gray] parser}

   114 

   115   which we also described in Section~\ref{sec:parsingspecs}

    13   package is called from within a theory document. In this case, the type of

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

    14   the inductive predicate, as well as its introduction rules, are given as

   122   specification of the inductive predicate, including type annotations and

    15   strings by the user. Before the package can actually make the definition,

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

    16   the type and introduction rules have to be parsed. In contrast, internal

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

    17   invocation means that the package is called by some other package. For

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

    18   example, the function definition package \cite{Krauss-IJCAR06} calls the

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

    19   inductive definition package to define the graph of the function. However,

   127   \cite{Krauss-IJCAR06} calls the inductive definition package to define the

    20   it is not a good idea for the function definition package to pass the

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

    21   introduction rules for the function graph to the inductive definition

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

    22   package as strings. In this case, it is better to directly pass the rules to

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

    23   the package as a list of terms, which is more robust than handling strings

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

    24   that are lacking the additional structure of terms. These two ways of

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

    25   invoking the package are reflected in its ML programming interface, which

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

    26   consists of two functions:

   134   programming interface, which consists of two functions:

   135 

    38   definition, together with a tuple containing the introduction and induction

   150   definition and the induction principle as well introduction rules. 

    39   rules, which are stored in the local theory, too.  In contrast to an

   151   

    40   ordinary theory, which simply consists of a type signature, as well as

   152   In contrast to an ordinary theory, which simply consists of a type

    41   tables for constants, axioms and theorems, a local theory also contains

   153   signature, as well as tables for constants, axioms and theorems, a local

    42   additional context information, such as locally fixed variables and local

   154   theory also contains additional context information, such as locally fixed

    43   assumptions that may be used by the package. The type @{ML_type

   155   variables and local assumptions that may be used by the package. The type

    44   local_theory} is identical to the type of \emph{proof contexts} @{ML_type

   156   @{ML_type local_theory} is identical to the type of \emph{proof contexts}

    45   "Proof.context"}, although not every proof context constitutes a valid local

   157   @{ML_type "Proof.context"}, although not every proof context constitutes a

    46   theory.  Note that @{ML add_inductive_i in SimpleInductivePackage} expects

   158   valid local theory.

   159 

   160 

   161   Note that @{ML add_inductive_i in SimpleInductivePackage} expects

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

   167   package. 

   168 

   169 

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

    55   parameters, since it can only be used for parsing. The names of the

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

   174   The names of the

   165 simple_inductive

   284 text {*

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

   285 

   167 where

   168   base: "trcl r x x"

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

   170 (*<*)

   171 thm trcl_def

   172 thm trcl.induct

   173 thm base

   174 thm step

   175 thm trcl.intros

   176 

   177 lemma trcl_strong_induct:

   178   assumes trcl: "trcl r x y"

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

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

   181   shows "P x y" 

   182 proof -

   183   from trcl

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

   185   proof induct

   186     case (base x)

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

   188   next

   189     case (step x y z)

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

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

   192       by (rule I2)

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

   194       by (rule trcl.step)

   195     ultimately show ?case ..

   196   qed

   197   then show ?thesis ..

   198 qed

   199 (*>*)

   200 

   201 text {* Even and odd numbers can be defined by *}

   202 

   203 simple_inductive

   204   even and odd

   205 where

   206   even0: "even 0"

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

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

   209 (*<*)

   210 thm even_def odd_def

   211 thm even.induct odd.induct

   212 thm even0

   213 thm evenS

   214 thm oddS

   215 thm even_odd.intros

   216 (*>*)

   217 

   218 text {* The accessible part of a relation can be introduced as follows: *}

   219 

   220 simple_inductive

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

   222 where

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

   224 (*<*)

   225 thm accpart_def

   226 thm accpart.induct

   227 thm accpartI

   228 (*>*)

   229 

   230 text {*

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

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

   233 *}

   234 

   235 locale rel =

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

   237 

   238 simple_inductive (in rel) accpart'

   239 where

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

   241 (*<*)

   242 context rel

   243 begin

   244 

   245 thm accpartI'

   246 thm accpart'.induct

   247 

   248 end

   249 

   250 thm rel.accpartI'

   251 thm rel.accpart'.induct

   252 

   253 (*>*)

   254 

   255 text {*

   256 

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

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

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

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

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

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

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

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

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

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

   267   of terms and types.

   268 

   269   \medskip

   270   \noindent

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

   272   can be described by the following railroad diagram:

   273   \begin{rail}

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

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

   276   ;

   277   \end{rail}

   278 

   279   \paragraph{Functional parsers}

   280 

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

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

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

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

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

   286   and Wadler \cite{Wadler-AFP95}. 

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

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

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

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

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

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

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

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

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

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

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

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

   299   for dealing with specific token types.

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

   301 

   302   \begin{table}

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

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

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

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

   307   @{ML "optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a" in Scan} \\

   308   @{ML "repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" in Scan} \\

   309   @{ML "repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" in Scan} \\

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

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

   312   \end{table}

   313 

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

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

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

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

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

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

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

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

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

   323   parsed items. The parsers @{ML "p |-- q" for p q} and @{ML "p --| q" for p q}

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

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

   326   If \texttt{p} succeeds, the parser @{ML "optional p x" for p x in Scan} returns the result

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

   328   @{ML "repeat p" for p in Scan} applies \texttt{p} as often as it can, returning a possibly

   329   empty list of parsed items. The parser @{ML "repeat1 p" for p in Scan} is similar,

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

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

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

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

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

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

   336   then an enclosing parser such as

   337   @{ML [display] "q -- p || r" for p q r}

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

   339   @{ML [display] "q -- !! err p || r" for err p q r}

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

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

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

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

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

   345   

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

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

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

   349   defined in @{ML_struct Scan}:

   350   

   351   \begin{table}

   352   @{ML "one: ('a -> bool) -> 'a list -> 'a * 'a list" in Scan} \\

   353   @{ML "$$ : string -> string list -> string * string list"}

   354   \end{table}

   355   

   356   The parser @{ML "one pred" for pred in Scan} parses exactly one token that

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

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

   359   express @{ML "$$ s" for s} using @{ML "one" in Scan}:

   360   @{ML [display] "one (fn s' => s' = s)" for s in Scan}

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

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

   363   

   364   @{ML_response [display]

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

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

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

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

   369 

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

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

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

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

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

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

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

   377   

   378   \begin{table}

   379   @{ML "$$$ : string -> token list -> string * token list" in OuterParse} \\

   380   @{ML "enum1: string -> (token list -> 'a * token list) -> token list ->

   381   'a list * token list" in OuterParse} \\

   382   @{ML "prop: token list -> string * token list" in OuterParse} \\

   383   @{ML "opt_target: token list -> string option * token list" in OuterParse} \\

   384   @{ML "fixes: token list ->

   385   (Binding.binding * string option * mixfix) list * token list" in OuterParse} \\

   386   @{ML "for_fixes: token list ->

   387   (Binding.binding * string option * mixfix) list * token list" in OuterParse} \\

   388   @{ML "!!! : (token list -> 'a) -> token list -> 'a" in OuterParse}

   389   \end{table}

   390 

   391   The parsers @{ML "$$$" in OuterParse} and @{ML "!!!" in OuterParse} are

   392   defined using the parsers @{ML "one" in Scan} and @{ML "!!"} from

   393   @{ML_struct Scan}.

   394   The parser @{ML "enum1 s p" for s p in OuterParse} parses a non-emtpy list of items

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

   417   @{ML_chunk [display] syntax}

   307