theory Ind_Interface+ −
imports "../Base" "../Parsing" Ind_Prelims Simple_Inductive_Package+ −
begin+ −
+ −
section {* Parsing and Typing the Specification *}+ −
+ −
text {* + −
To be able to write down the specification in Isabelle, we have to introduce+ −
a new command (see Section~\ref{sec:newcommand}). As the keyword for the+ −
new command we chose \simpleinductive{}. In the package we want to support+ −
some ``advanced'' features: First, we want that the package can cope with+ −
specifications inside locales. For example it should be possible to declare+ −
*}+ −
+ −
locale rel =+ −
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"+ −
+ −
text {*+ −
and then define the transitive closure and the accessible part as follows:+ −
*}+ −
+ −
+ −
simple_inductive (in rel) + −
trcl' + −
where+ −
base: "trcl' x x"+ −
| step: "trcl' x y \<Longrightarrow> R y z \<Longrightarrow> trcl' x z"+ −
+ −
simple_inductive (in rel) + −
accpart'+ −
where+ −
accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"+ −
+ −
text {* + −
Second, we want that the user can specify fixed parameters.+ −
Remember in the previous section we stated that the user can give the + −
specification for the transitive closure of a relation @{text R} as + −
*}+ −
+ −
simple_inductive+ −
trcl\<iota>\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"+ −
where+ −
base: "trcl\<iota>\<iota> R x x"+ −
| step: "trcl\<iota>\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota>\<iota> R x z"+ −
+ −
text {*+ −
Note that there is no locale given in this specification---the parameter+ −
@{text "R"} therefore needs to be included explicitly in @{term trcl\<iota>\<iota>}, but+ −
stays fixed throughout the specification. The problem with this way of+ −
stating the specification for the transitive closure is that it derives the+ −
following induction principle.+ −
+ −
\begin{center}\small+ −
\mprset{flushleft}+ −
\mbox{\inferrule{+ −
@{thm_style prem1 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\+ −
@{thm_style prem2 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\+ −
@{thm_style prem3 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}+ −
{@{thm_style concl trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}} + −
\end{center}+ −
+ −
But this does not correspond to the induction principle we derived by hand, which+ −
was+ −
+ −
\begin{center}\small+ −
\mprset{flushleft}+ −
\mbox{\inferrule{+ −
@{thm_style prem1 trcl_induct[no_vars]}\\\\+ −
@{thm_style prem2 trcl_induct[no_vars]}\\\\+ −
@{thm_style prem3 trcl_induct[no_vars]}}+ −
{@{thm_style concl trcl_induct[no_vars]}}} + −
\end{center}+ −
+ −
The difference is that in the one derived by hand the relation @{term R} is not+ −
a parameter of the proposition @{term P} to be proved and it is also not universally+ −
qunatified in the second and third premise. The point is that the parameter @{term R}+ −
stays fixed thoughout the definition and we do not want to regard it as an ``ordinary''+ −
argument of the transitive closure, but one that can be freely instantiated. + −
In order to recognise such parameters, we have to extend the specification+ −
to include a mechanism to state fixed parameters. The user should be able+ −
to write + −
+ −
*}+ −
+ −
simple_inductive+ −
trcl'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"+ −
where+ −
base: "trcl'' R x x"+ −
| step: "trcl'' R x y \<Longrightarrow> R y z \<Longrightarrow> trcl'' R x z"+ −
+ −
simple_inductive+ −
accpart'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"+ −
where+ −
accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x"+ −
+ −
text {*+ −
\begin{figure}[t]+ −
\begin{isabelle}+ −
\railnontermfont{\rmfamily\itshape}+ −
\railterm{simpleinductive,where,for}+ −
\railalias{simpleinductive}{\simpleinductive{}}+ −
\railalias{where}{\isacommand{where}}+ −
\railalias{for}{\isacommand{for}}+ −
\begin{rail}+ −
simpleinductive target? fixes (for fixes)? \\+ −
(where (thmdecl? prop + '|'))?+ −
;+ −
\end{rail}+ −
\end{isabelle}+ −
\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); similarly the \emph{fixes} + −
after \isacommand{for} to indicate fixed parameters; \emph{prop} stands for a + −
introduction rule with an optional theorem declaration (\emph{thmdecl}).+ −
\label{fig:railroad}}+ −
\end{figure}+ −
*}+ −
+ −
text {*+ −
This leads directly to the railroad diagram shown in+ −
Figure~\ref{fig:railroad} for the syntax of \simpleinductive{}. This diagram+ −
more or less translates directly into the parser:+ −
+ −
@{ML_chunk [display,gray] parser}+ −
+ −
which we described in Section~\ref{sec:parsingspecs}. If we feed into the + −
parser the string (which corresponds to our definition of @{term even} and + −
@{term odd}):+ −
+ −
@{ML_response [display,gray]+ −
"let+ −
val input = filtered_input+ −
(\"even and odd \" ^ + −
\"where \" ^+ −
\" even0[intro]: \\\"even 0\\\" \" ^ + −
\"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ + −
\"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\"\")+ −
in+ −
parse spec_parser input+ −
end"+ −
"(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],+ −
[((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),+ −
((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),+ −
((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}+ −
*}+ −
+ −
+ −
text {*+ −
then we get back a locale (in this case @{ML NONE}), the predicates (with type+ −
and syntax annotations), the parameters (similar as the predicates) and+ −
the 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.+ −
+ −
@{ML_chunk [display,gray,linenos] syntax}+ −
+ −
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}+ −
+ −
+ −
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"}+ −
*}+ −
+ −
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 \<Rightarrow> 'a \<Rightarrow> bool\", NoSyn)]+ −
[((Binding.name \"base\", []), [\"trcl r x x\"]),+ −
((Binding.name \"step\", []), [\"trcl r x y \<Longrightarrow> r y z \<Longrightarrow> trcl r x z\"])]+ −
@{context}"+ −
"((\<dots>,+ −
[(\<dots>,+ −
[Const (\"all\", \<dots>) $ Abs (\"x\", TFree (\"'a\", \<dots>),+ −
Const (\"Trueprop\", \<dots>) $+ −
(Free (\"trcl\", \<dots>) $ Free (\"r\", \<dots>) $ Bound 0 $ Bound 0))]),+ −
(\<dots>,+ −
[Const (\"all\", \<dots>) $ Abs (\"x\", TFree (\"'a\", \<dots>),+ −
Const (\"all\", \<dots>) $ Abs (\"y\", TFree (\"'a\", \<dots>),+ −
Const (\"all\", \<dots>) $ Abs (\"z\", TFree (\"'a\", \<dots>),+ −
Const (\"==>\", \<dots>) $+ −
(Const (\"Trueprop\", \<dots>) $+ −
(Free (\"trcl\", \<dots>) $ Free (\"r\", \<dots>) $ Bound 2 $ Bound 1)) $+ −
(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>))))])]),+ −
\<dots>)+ −
: (((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 {*+ −
From a high-level perspective the package consists of 6 subtasks:+ −
+ −
+ −
+ −
*}+ −
+ −
+ −
(*<*)+ −
end+ −
(*>*)+ −