2 imports "../Base" Simple_Inductive_Package

     2 imports "../Base" "../Parsing" Simple_Inductive_Package

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

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

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

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

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

    36   After the keyword we expect a constant (or constants) with possible typing 

    37   annotations and a

    49 \begin{figure}[p]

    50   \begin{figure}[p]

    50 \begin{isabelle}

    51   \begin{isabelle}

    75 \end{isabelle}

    76   \end{isabelle}

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

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

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

    78   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   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   specify the same inductive predicates, but this time defined inside

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

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

    81 \end{figure}

    82   \end{figure}

    82 *}

    83 *}

    83 

    84 

    84 text {*

    85 text {*

    85 \begin{figure}[p]

    86   From a high-level perspective the package consists of 6 subtasks:

    86 \begin{isabelle}

    87 

    88   \begin{itemize}

    89   \item reading the various parts of specification (i.e.~parser),

    90   \item transforming the parser outut into an internal 

    91   (typed) datastructure,

    92   \item making the definitions, 

    93   \item deriving the induction principles,

    94   \item deriving the introduction rules, and

    95   \item storing the results in the given theory to be visible 

    96   to the user. 

    97   \end{itemize}

    98 

    99 *}

   100 

   101 text {*

   102   \begin{figure}[p]

   103   \begin{isabelle}

    97 \end{isabelle}

   114   \end{isabelle}

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

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

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

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

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

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

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

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

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

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

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

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

   104 \label{fig:railroad}}

   121   \label{fig:railroad}}

   105 \end{figure}

   122   \end{figure}

   106 *}

   123 *}

   107 

   124 

   108 text {*

   125 text {*

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

   126   For the first subtask, the syntax of the \simpleinductive{} command can be

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

   127   described by the railroad diagram in Figure~\ref{fig:railroad}. This diagram

   111   translates directly into the parser:

   128   more or less translates directly into the parser:

   129 

   115   which we also described in Section~\ref{sec:parsingspecs}. Its return value

   133   which we described in Section~\ref{sec:parsingspecs}. If we feed into the 

   116   of this parser is a locale, the predicates, parameters and specifications of 

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

   117   the introduction rules. This is all the information we need to call the package. 

   135   @{term odd}):

   136 

   137   @{ML_response [display,gray]

   138 "let

   139   val input = filtered_input

   140      (\"even and odd \" ^  

   141       \"where \" ^

   142       \"  even0[intro]: \\\"even 0\\\" \" ^ 

   143       \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ 

   144       \"| oddS[intro]:  \\\"even n \<Longrightarrow> odd (Suc n)\\\"\")

   145 in

   146   parse spec_parser input

   147 end"

   148 "((((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), []),

   149      [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),

   150       ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),

   151       ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}

   152 *}

   153 

   154 

   155 text {*

   156   then we get back a locale (in this case @{ML NONE}), the predicates (with type

   157   and syntax annotations), the parameters (similar as the predicates) and

   158   the specifications of the introduction rules. 

   159 

   160 

   161 

   162   This is all the information we

   163   need for calling the package and setting up the keyword. The latter is

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

   120 

   167   

   121   The locale is passed as argument to the function 

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

   122   @{ML Toplevel.local_theory}.\footnote{FIXME Is this already described?} The

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

   123   other arguments, i.e.~the predicates, parameters and specifications, are passed

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

   124   to the function @{ML add_inductive in SimpleInductivePackage} (Line 4). The

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

   125   actual command is defined in Lines 6 and 7. We called @{ML OuterSyntax.command}

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

   126   with the kind-indicator @{ML OuterKeyword.thy_decl} since the package does

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

   127   not need to open up any goal state (see Section~\ref{sec:newcommand}).

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

   175   is passed as argument to the function @{ML

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

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

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

   179   (Line 4).

   180 

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

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

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

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

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

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

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

   188   @{ML read_specification in Specification}. This function takes some constants

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

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

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

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

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

   194   The function @{ML read_specification in Specification} however allows more

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

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

   197   between our specific format and the general format expected by 

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

   199 

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

   201 

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

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

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

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

   206 

   207 

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

   209 

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

   221   calls the inductive definition package to define the