--- a/CookBook/Package/Ind_Interface.thy Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,454 +0,0 @@
-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
-(*>*)