diff -r 1aaa15ef731b -r 647cab4a72c2 ProgTutorial/Package/Ind_Interface.thy --- a/ProgTutorial/Package/Ind_Interface.thy Wed Apr 01 12:29:10 2009 +0100 +++ b/ProgTutorial/Package/Ind_Interface.thy Wed Apr 01 15:42:47 2009 +0100 @@ -69,21 +69,21 @@ \caption{A railroad diagram describing the syntax of \simpleinductive{}. The \emph{target} indicates an optional locale; the \emph{fixes} are an \isacommand{and}-separated list of names for the inductive predicates (they - can also contain typing- and syntax anotations); \emph{prop} stands for a + can also contain typing- and syntax annotations); \emph{prop} stands for a introduction rule with an optional theorem declaration (\emph{thmdecl}). \label{fig:railroad}} \end{figure} *} text {* - To be able to write down the specification in Isabelle, we have to introduce + To be able to write down the specifications or inductive predicates, we have + to introduce a new command (see Section~\ref{sec:newcommand}). As the keyword for the new command we chose \simpleinductive{}. Examples of specifications we expect the user gives for the inductive predicates from the previous section are - shown in Figure~ref{fig:specs}. The general syntax we will parse is specified - in the railroad diagram shown in Figure~\ref{fig:railroad} for the syntax of - \simpleinductive{}. This diagram more or less translates directly into - the parser: + shown in Figure~\ref{fig:specs}. The general syntax we will parse is specified + in the railroad diagram shown in Figure~\ref{fig:railroad}. This diagram more + or less translates directly into the parser: *} ML{*val spec_parser = @@ -95,12 +95,11 @@ (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} text {* - which we explaind in Section~\ref{sec:parsingspecs}. - If you look closely, there is no code for parsing the optional - target in Figure~\ref{fig:railroad}. This is an ``advanced'' feature - which we will inherit for ``free'' from the infrastructure on which - we build the package. The target stands for a locale and allows us - to specify + which we explained in Section~\ref{sec:parsingspecs}. However, if you look + closely, there is no code for parsing the target given optionally after the + keyword. This is an ``advanced'' feature which we will inherit for ``free'' + from the infrastructure on which we shall build the package. The target + stands for a locale and allows us to specify *} locale rel = @@ -123,10 +122,13 @@ accpartI: "(\y. R y x \ accpart' y) \ accpart' x" text {* - Note that in these definitions the parameter @{text R} for the - relation is left implicit. If we feed into the - parser the string (which corresponds to our definition of @{term even} and - @{term odd}): + Note that in these definitions the parameter @{text R}, standing for the + relation, is left implicit. For the moment we will ignore this kind + of implicit parameters and rely on the fact that the infrastructure will + deal with them. Later, however, we will come back to them. + + If we feed into the parser the string that corresponds to our definition + of @{term even} and @{term odd} @{ML_response [display,gray] "let @@ -144,16 +146,50 @@ ((evenS,\), \"\\^E\\^Ftoken\\^Eodd n \ even (Suc n)\\^E\\^F\\^E\"), ((oddS,\), \"\\^E\\^Ftoken\\^Eeven n \ odd (Suc n)\\^E\\^F\\^E\")]), [])"} - then we get back the predicates (with type - and syntax annotations), and the specifications of the introduction - rules. This is all the information we + then we get back the specifications of the predicates (with type and syntax annotations), + and specifications of the introduction rules. This is all the information we need for calling the package and setting up the keyword. The latter is - done in Lines 6 and 7 in the code below. + done in Lines 5 to 7 in the code below. *} -(*<*) -ML{* fun add_inductive pred_specs rule_specs lthy = lthy *} -(*>*) +(*<*)ML %linenos{*fun add_inductive pred_specs rule_specs lthy = lthy +fun add_inductive_cmd pred_specs rule_specs lthy = +let + val ((pred_specs', rule_specs'), _) = + Specification.read_spec pred_specs rule_specs lthy +in + add_inductive pred_specs' rule_specs' lthy +end*}(*>*) +ML_val %linenosgray{*val specification = + spec_parser >> + (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs) + +val _ = OuterSyntax.local_theory "simple_inductive" + "definition of simple inductive predicates" + OuterKeyword.thy_decl specification*} + +text {* + We call @{ML local_theory in OuterSyntax} with the kind-indicator + @{ML thy_decl in OuterKeyword} since the package does not need to open + up any proof (see Section~\ref{sec:newcommand}). + The auxiliary function @{text specification} in Lines 1 to 3 + gathers the information from the parser to be processed further + by the function @{text "add_inductive_cmd"}, which we describe below. + + Note that the predicates when they come out of the parser are just some + ``naked'' strings: they have no type yet (even if we annotate them with + types) and they are also not defined constants yet (which the predicates + eventually will be). Also the introduction rules are just strings. What we have + to do first is to transform the parser's output into some internal + datastructures that can be processed further. For this we can use the + function @{ML read_spec in Specification}. This function takes some strings + (with possible typing annotations) and some rule specifications, and attempts + to find a typing according to the given type constraints given by the + user and the type constraints by the ``ambient'' theory. It returns + the type for the predicates and also returns typed terms for the + introduction rules. So at the heart of the function + @{text "add_inductive_cmd"} is a call to @{ML read_spec in Specification}. +*} ML{*fun add_inductive_cmd pred_specs rule_specs lthy = let @@ -161,312 +197,16 @@ Specification.read_spec pred_specs rule_specs lthy in add_inductive pred_specs' rule_specs' lthy -end*} - - -ML{*val specification = - spec_parser >> - (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)*} - -ML{*val _ = OuterSyntax.local_theory "simple_inductive" - "definition of simple inductive predicates" - OuterKeyword.thy_decl specification*} - - -text {* - We call @{ML OuterSyntax.command} with the kind-indicator @{ML - OuterKeyword.thy_decl} since the package does not need to open up any goal - state (see Section~\ref{sec:newcommand}). Note that the predicates and - parameters are at the moment only some ``naked'' variables: they have no - type yet (even if we annotate them with types) and they are also no defined - constants yet (which the predicates will eventually be). In Lines 1 to 4 we - gather the information from the parser to be processed further. The locale - is passed as argument to the function @{ML - Toplevel.local_theory}.\footnote{FIXME Is this already described?} The other - arguments, i.e.~the predicates, parameters and intro rule specifications, - are passed to the function @{ML add_inductive in SimpleInductivePackage} - (Line 4). - - We now come to the second subtask of the package, namely transforming the - parser output into some internal datastructures that can be processed further. - Remember that at the moment the introduction rules are just strings, and even - if the predicates and parameters can contain some typing annotations, they - are not yet in any way reflected in the introduction rules. So the task of - @{ML add_inductive in SimpleInductivePackage} is to transform the strings - into properly typed terms. For this it can use the function - @{ML read_spec in Specification}. This function takes some constants - with possible typing annotations and some rule specifications and attempts to - find a type according to the given type constraints and the type constraints - by the surrounding (local theory). However this function is a bit - too general for our purposes: we want that each introduction rule has only - name (for example @{text even0} or @{text evenS}), if a name is given at all. - The function @{ML read_spec in Specification} however allows more - than one rule. Since it is quite convenient to rely on this function (instead of - building your own) we just quick ly write a wrapper function that translates - between our specific format and the general format expected by - @{ML read_spec in Specification}. The code of this wrapper is as follows: - - @{ML_chunk [display,gray,linenos] read_specification} - - It takes a list of constants, a list of rule specifications and a local theory - as input. Does the transformation of the rule specifications in Line 3; calls - the function and transforms the now typed rule specifications back into our - format and returns the type parameter and typed rule specifications. - - - @{ML_chunk [display,gray,linenos] add_inductive} - +end*} - In order to add a new inductive predicate to a theory with the help of our - package, the user must \emph{invoke} it. For every package, there are - essentially two different ways of invoking it, which we will refer to as - \emph{external} and \emph{internal}. By external invocation we mean that the - package is called from within a theory document. In this case, the - specification of the inductive predicate, including type annotations and - introduction rules, are given as strings by the user. Before the package can - actually make the definition, the type and introduction rules have to be - parsed. In contrast, internal invocation means that the package is called by - some other package. For example, the function definition package - calls the inductive definition package to define the - graph of the function. However, it is not a good idea for the function - definition package to pass the introduction rules for the function graph to - the inductive definition package as strings. In this case, it is better to - directly pass the rules to the package as a list of terms, which is more - robust than handling strings that are lacking the additional structure of - terms. These two ways of invoking the package are reflected in its ML - programming interface, which consists of two functions: - - - @{ML_chunk [display,gray] SIMPLE_INDUCTIVE_PACKAGE} -*} - -text {* - (FIXME: explain Binding.binding; Attrib.binding somewhere else) - - - The function for external invocation of the package is called @{ML - add_inductive in SimpleInductivePackage}, whereas the one for internal - invocation is called @{ML add_inductive_i in SimpleInductivePackage}. Both - of these functions take as arguments the names and types of the inductive - predicates, the names and types of their parameters, the actual introduction - rules and a \emph{local theory}. They return a local theory containing the - definition and the induction principle as well introduction rules. - - Note that @{ML add_inductive_i in SimpleInductivePackage} expects - the types of the predicates and parameters to be specified using the - datatype @{ML_type typ} of Isabelle's logical framework, whereas @{ML - add_inductive in SimpleInductivePackage} expects them to be given as - optional strings. If no string is given for a particular predicate or - parameter, this means that the type should be inferred by the - package. - - - Additional \emph{mixfix syntax} may be associated with the - predicates and parameters as well. Note that @{ML add_inductive_i in - SimpleInductivePackage} does not allow mixfix syntax to be associated with - parameters, since it can only be used for parsing.\footnote{FIXME: why ist it there then?} - The names of the - predicates, parameters and rules are represented by the type @{ML_type - Binding.binding}. Strings can be turned into elements of the type @{ML_type - Binding.binding} using the function @{ML [display] "Binding.name : string -> - Binding.binding"} Each introduction rule is given as a tuple containing its - name, a list of \emph{attributes} and a logical formula. Note that the type - @{ML_type Attrib.binding} used in the list of introduction rules is just a - shorthand for the type @{ML_type "Binding.binding * Attrib.src list"}. The - function @{ML add_inductive_i in SimpleInductivePackage} expects the formula - to be specified using the datatype @{ML_type term}, whereas @{ML - add_inductive in SimpleInductivePackage} expects it to be given as a string. - An attribute specifies additional actions and transformations that should be - applied to a theorem, such as storing it in the rule databases used by - automatic tactics like the simplifier. The code of the package, which will - be described in the following section, will mostly treat attributes as a - black box and just forward them to other functions for storing theorems in - local theories. The implementation of the function @{ML add_inductive in - SimpleInductivePackage} for external invocation of the package is quite - simple. Essentially, it just parses the introduction rules and then passes - them on to @{ML add_inductive_i in SimpleInductivePackage}: - - @{ML_chunk [display] add_inductive} - - For parsing and type checking the introduction rules, we use the function - - @{ML [display] "Specification.read_specification: - (Binding.binding * string option * mixfix) list -> (*{variables}*) - (Attrib.binding * string list) list -> (*{rules}*) - local_theory -> - (((Binding.binding * typ) * mixfix) list * - (Attrib.binding * term list) list) * - local_theory"} -*} +ML {* Specification.read_spec *} text {* - During parsing, both predicates and parameters are treated as variables, so - the lists \verb!preds_syn! and \verb!params_syn! are just appended - before being passed to @{ML read_spec in Specification}. Note that the format - for rules supported by @{ML read_spec in Specification} is more general than - what is required for our package. It allows several rules to be associated - with one name, and the list of rules can be partitioned into several - sublists. In order for the list \verb!intro_srcs! of introduction rules - to be acceptable as an input for @{ML read_spec in Specification}, we first - have to turn it into a list of singleton lists. This transformation - has to be reversed later on by applying the function - @{ML [display] "the_single: 'a list -> 'a"} - to the list \verb!specs! containing the parsed introduction rules. - The function @{ML read_spec in Specification} also returns the list \verb!vars! - of predicates and parameters that contains the inferred types as well. - This list has to be chopped into the two lists \verb!preds_syn'! and - \verb!params_syn'! for predicates and parameters, respectively. - All variables occurring in a rule but not in the list of variables passed to - @{ML read_spec in Specification} will be bound by a meta-level universal - quantifier. -*} - -text {* - Finally, @{ML read_specification in Specification} also returns another local theory, - but we can safely discard it. As an example, let us look at how we can use this - function to parse the introduction rules of the @{text trcl} predicate: - - @{ML_response [display] -"Specification.read_specification - [(Binding.name \"trcl\", NONE, NoSyn), - (Binding.name \"r\", SOME \"'a \ 'a \ bool\", NoSyn)] - [((Binding.name \"base\", []), [\"trcl r x x\"]), - ((Binding.name \"step\", []), [\"trcl r x y \ r y z \ trcl r x z\"])] - @{context}" -"((\, - [(\, - [Const (\"all\", \) $ Abs (\"x\", TFree (\"'a\", \), - Const (\"Trueprop\", \) $ - (Free (\"trcl\", \) $ Free (\"r\", \) $ Bound 0 $ Bound 0))]), - (\, - [Const (\"all\", \) $ Abs (\"x\", TFree (\"'a\", \), - Const (\"all\", \) $ Abs (\"y\", TFree (\"'a\", \), - Const (\"all\", \) $ Abs (\"z\", TFree (\"'a\", \), - Const (\"==>\", \) $ - (Const (\"Trueprop\", \) $ - (Free (\"trcl\", \) $ Free (\"r\", \) $ Bound 2 $ Bound 1)) $ - (Const (\"==>\", \) $ \ $ \))))])]), - \) -: (((Binding.binding * typ) * mixfix) list * - (Attrib.binding * term list) list) * local_theory"} - - In the list of variables passed to @{ML read_specification in Specification}, we have - used the mixfix annotation @{ML NoSyn} to indicate that we do not want to associate any - mixfix syntax with the variable. Moreover, we have only specified the type of \texttt{r}, - whereas the type of \texttt{trcl} is computed using type inference. - The local variables \texttt{x}, \texttt{y} and \texttt{z} of the introduction rules - are turned into bound variables with the de Bruijn indices, - whereas \texttt{trcl} and \texttt{r} remain free variables. - -*} - -text {* - - \paragraph{Parsers for theory syntax} - - Although the function @{ML add_inductive in SimpleInductivePackage} parses terms and types, it still - cannot be used to invoke the package directly from within a theory document. - In order to do this, we have to write another parser. Before we describe - the process of writing parsers for theory syntax in more detail, we first - show some examples of how we would like to use the inductive definition - package. - - - The definition of the transitive closure should look as follows: -*} - -ML {* SpecParse.opt_thm_name *} - -text {* - - A proposition can be parsed using the function @{ML prop in OuterParse}. - Essentially, a proposition is just a string or an identifier, but using the - specific parser function @{ML prop in OuterParse} leads to more instructive - error messages, since the parser will complain that a proposition was expected - when something else than a string or identifier is found. - An optional locale target specification of the form \isa{(\isacommand{in}\ $\ldots$)} - can be parsed using @{ML opt_target in OuterParse}. - The lists of names of the predicates and parameters, together with optional - types and syntax, are parsed using the functions @{ML "fixes" in OuterParse} - and @{ML for_fixes in OuterParse}, respectively. - In addition, the following function from @{ML_struct SpecParse} for parsing - an optional theorem name and attribute, followed by a delimiter, will be useful: - - \begin{table} - @{ML "opt_thm_name: - string -> Attrib.binding parser" in SpecParse} - \end{table} - - We now have all the necessary tools to write the parser for our - \isa{\isacommand{simple{\isacharunderscore}inductive}} command: - - - Once all arguments of the command have been parsed, we apply the function - @{ML add_inductive in SimpleInductivePackage}, which yields a local theory - transformer of type @{ML_type "local_theory -> local_theory"}. Commands in - Isabelle/Isar are realized by transition transformers of type - @{ML_type [display] "Toplevel.transition -> Toplevel.transition"} - We can turn a local theory transformer into a transition transformer by using - the function - - @{ML [display] "Toplevel.local_theory : string option -> - (local_theory -> local_theory) -> - Toplevel.transition -> Toplevel.transition"} - - which, apart from the local theory transformer, takes an optional name of a locale - to be used as a basis for the local theory. - - (FIXME : needs to be adjusted to new parser type) - - {\it - The whole parser for our command has type - @{text [display] "OuterLex.token list -> - (Toplevel.transition -> Toplevel.transition) * OuterLex.token list"} - which is abbreviated by @{text OuterSyntax.parser_fn}. The new command can be added - to the system via the function - @{text [display] "OuterSyntax.command : - string -> string -> OuterKeyword.T -> OuterSyntax.parser_fn -> unit"} - which imperatively updates the parser table behind the scenes. } - - In addition to the parser, this - function takes two strings representing the name of the command and a short description, - as well as an element of type @{ML_type OuterKeyword.T} describing which \emph{kind} of - command we intend to add. Since we want to add a command for declaring new concepts, - we choose the kind @{ML "OuterKeyword.thy_decl"}. Other kinds include - @{ML "OuterKeyword.thy_goal"}, which is similar to @{ML thy_decl in OuterKeyword}, - but requires the user to prove a goal before making the declaration, or - @{ML "OuterKeyword.diag"}, which corresponds to a purely diagnostic command that does - not change the context. For example, the @{ML thy_goal in OuterKeyword} kind is used - by the \isa{\isacommand{function}} command \cite{Krauss-IJCAR06}, which requires the user - to prove that a given set of equations is non-overlapping and covers all cases. The kind - of the command should be chosen with care, since selecting the wrong one can cause strange - behaviour of the user interface, such as failure of the undo mechanism. -*} - -text {* - Note that the @{text trcl} predicate has two different kinds of parameters: the - first parameter @{text R} stays \emph{fixed} throughout the definition, whereas - the second and third parameter changes in the ``recursive call''. This will - become important later on when we deal with fixed parameters and locales. - - - - The purpose of the package we show next is that the user just specifies the - inductive predicate by stating some introduction rules and then the packages - makes the equivalent definition and derives from it the needed properties. -*} - -text {* - (FIXME: perhaps move somewhere else) - - The point of these examples is to get a feeling what the automatic proofs - should do in order to solve all inductive definitions we throw at them. For this - it is instructive to look at the general construction principle - of inductive definitions, which we shall do in the next section. - - The code of the inductive package falls roughly in tree parts: the first - deals with the definitions, the second with the induction principles and - the third with the introduction rules. - + Once we have the input data as some internal datastructure, we call + the function @{ML add_inductive}. This function does the heavy duty + lifting in the package: it generates definitions for the + predicates and derives from them corresponding induction principles and + introduction rules. The description of this function will span over + the next two sections. *} (*<*)end(*>*) \ No newline at end of file