1 theory Ind_Interface

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

     3 begin

     4 

     5 section {* Parsing and Typing the Specification *}

     6 

     7 text {* 

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

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

    10   new command we chose \simpleinductive{}. In the package we want to support

    11   some ``advanced'' features: First, we want that the package can cope with

    12   specifications inside locales. For example it should be possible to declare

    13 *}

    14 

    15 locale rel =

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

    17 

    18 text {*

    19   and then define the transitive closure and the accessible part as follows:

    20 *}

    21 

    22 

    23 simple_inductive (in rel) 

    24   trcl' 

    25 where

    26   base: "trcl' x x"

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

    28 

    29 simple_inductive (in rel) 

    30   accpart'

    31 where

    32   accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"

    33 

    34 text {* 

    35   Second, we want that the user can specify fixed parameters.

    36   Remember in the previous section we stated that the user can give the 

    37   specification for the transitive closure of a relation @{text R} as 

    38 *}

    39 

    40 simple_inductive

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

    42 where

    43   base: "trcl\<iota>\<iota> R x x"

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

    45 

    46 text {*

    47   Note that there is no locale given in this specification---the parameter

    48   @{text "R"} therefore needs to be included explicitly in @{term trcl\<iota>\<iota>}, but

    49   stays fixed throughout the specification. The problem with this way of

    50   stating the specification for the transitive closure is that it derives the

    51   following induction principle.

    52 

    53   \begin{center}\small

    54   \mprset{flushleft}

    55   \mbox{\inferrule{

    56              @{thm_style prem1  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\

    57              @{thm_style prem2  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\

    58              @{thm_style prem3  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}

    59             {@{thm_style concl  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}}  

    60   \end{center}

    61 

    62   But this does not correspond to the induction principle we derived by hand, which

    63   was

    64   

    65   \begin{center}\small

    66   \mprset{flushleft}

    67   \mbox{\inferrule{

    68              @{thm_style prem1  trcl_induct[no_vars]}\\\\

    69              @{thm_style prem2  trcl_induct[no_vars]}\\\\

    70              @{thm_style prem3  trcl_induct[no_vars]}}

    71             {@{thm_style concl  trcl_induct[no_vars]}}}  

    72   \end{center}

    73 

    74   The difference is that in the one derived by hand the relation @{term R} is not

    75   a parameter of the proposition @{term P} to be proved and it is also not universally

    76   qunatified in the second and third premise. The point is that the parameter @{term R}

    77   stays fixed thoughout the definition and we do not want to regard it as an ``ordinary''

    78   argument of the transitive closure, but one that can be freely instantiated. 

    79   In order to recognise such parameters, we have to extend the specification

    80   to include a mechanism to state fixed parameters. The user should be able

    81   to write 

    82 

    83 *}

    84 

    85 simple_inductive

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

    87 where

    88   base: "trcl'' R x x"

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

    90 

    91 simple_inductive

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

    93 where

    94   accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x"

    95 

    96 text {*

    97   \begin{figure}[t]

    98   \begin{isabelle}

    99   \railnontermfont{\rmfamily\itshape}

   100   \railterm{simpleinductive,where,for}

   101   \railalias{simpleinductive}{\simpleinductive{}}

   102   \railalias{where}{\isacommand{where}}

   103   \railalias{for}{\isacommand{for}}

   104   \begin{rail}

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

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

   107   ;

   108   \end{rail}

   109   \end{isabelle}

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

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

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

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

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

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

   116   \label{fig:railroad}}

   117   \end{figure}

   118 *}

   119 

   120 text {*

   121   This leads directly to the railroad diagram shown in

   122   Figure~\ref{fig:railroad} for the syntax of \simpleinductive{}. This diagram

   123   more or less translates directly into the parser:

   124 

   125   @{ML_chunk [display,gray] parser}

   126 

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

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

   129   @{term odd}):

   130 

   131   @{ML_response [display,gray]

   132 "let

   133   val input = filtered_input

   134      (\"even and odd \" ^  

   135       \"where \" ^

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

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

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

   139 in

   140   parse spec_parser input

   141 end"

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

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

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

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

   146 *}

   147 

   148 

   149 text {*

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

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

   152   the specifications of the introduction rules. 

   153 

   154 

   155 

   156   This is all the information we

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

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

   159 

   160   @{ML_chunk [display,gray,linenos] syntax}

   161   

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

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

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

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

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

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

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

   169   is passed as argument to the function @{ML

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

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

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

   173   (Line 4).

   174 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   191   between our specific format and the general format expected by 

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

   193 

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

   195 

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

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

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

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

   200 

   201 

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

   203 

   204 

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

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

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

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

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

   210   specification of the inductive predicate, including type annotations and

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

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

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

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

   215   calls the inductive definition package to define the

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

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

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

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

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

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

   222   programming interface, which consists of two functions:

   223 

   224 

   225   @{ML_chunk [display,gray] SIMPLE_INDUCTIVE_PACKAGE}

   226 *}

   227 

   228 text {*

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

   230 

   231 

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

   233   add_inductive in SimpleInductivePackage}, whereas the one for internal

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

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

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

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

   238   definition and the induction principle as well introduction rules. 

   239 

   240   Note that @{ML add_inductive_i in SimpleInductivePackage} expects

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

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

   243   add_inductive in SimpleInductivePackage} expects them to be given as

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

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

   246   package. 

   247 

   248 

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

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

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

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

   253   The names of the

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

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

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

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

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

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

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

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

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

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

   264   An attribute specifies additional actions and transformations that should be

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

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

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

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

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

   270   SimpleInductivePackage} for external invocation of the package is quite

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

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

   273 

   274   @{ML_chunk [display] add_inductive}

   275 

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

   277   

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

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

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

   281   local_theory ->

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

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

   284   local_theory"}

   285 *}

   286 

   287 text {*

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

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

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

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

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

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

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

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

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

   297   has to be reversed later on by applying the function

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

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

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

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

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

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

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

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

   306   quantifier.

   307 *}

   308 

   309 text {*

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

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

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

   313 

   314   @{ML_response [display]

   315 "Specification.read_specification

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

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

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

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

   320   @{context}"

   321 "((\<dots>,

   322   [(\<dots>,

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

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

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

   326    (\<dots>,

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

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

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

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

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

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

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

   334  \<dots>)

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

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

   337 

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

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

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

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

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

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

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

   345 

   346 *}

   347 

   348 text {*

   349 

   350   \paragraph{Parsers for theory syntax}

   351 

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

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

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

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

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

   357   package.

   358 

   359 

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

   361 *}

   362 

   363 ML {* SpecParse.opt_thm_name *}

   364 

   365 text {*

   366 

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

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

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

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

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

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

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

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

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

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

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

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

   379   

   380   \begin{table}

   381   @{ML "opt_thm_name:

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

   383   \end{table}

   384 

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

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

   387   

   388  

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

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

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

   392   Isabelle/Isar are realized by transition transformers of type

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

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

   395   the function

   396 

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

   398   (local_theory -> local_theory) ->

   399   Toplevel.transition -> Toplevel.transition"}

   400  

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

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

   403 

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

   405 

   406   {\it

   407   The whole parser for our command has type

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

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

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

   411   to the system via the function

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

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

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

   415 

   416   In addition to the parser, this

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

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

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

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

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

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

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

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

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

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

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

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

   429 *}

   430 

   431 text {*

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

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

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

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

   436 

   437 

   438  

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

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

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

   442 *}

   443 

   444 text {*

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

   446 

   447 

   448 

   449 *}

   450 

   451 

   452 (*<*)

   453 end

   454 (*>*)