--- a/CookBook/Package/Ind_Interface.thy Fri Feb 13 14:15:28 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy Sat Feb 14 00:11:50 2009 +0000
@@ -4,55 +4,174 @@
section {* The Interface \label{sec:ind-interface} *}
+text {*
+ 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 useful properties.
+ 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 use \simpleinductive{}. The specifications corresponding to our
+ examples described earlier are:
+*}
+
+simple_inductive
+ trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> '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
+ even and odd
+where
+ even0: "even 0"
+| evenS: "odd n \<Longrightarrow> even (Suc n)"
+| oddS: "even n \<Longrightarrow> odd (Suc n)"
+
+simple_inductive
+ accpart :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
+
text {*
+ We expect a constant (or constants) with possible typing annotations and a
+ list of introduction rules. While these specifications are all
+ straightforward, there is a technicality we like to deal with to do with
+ fixed parameters and locales. Remember we pointed out that the parameter
+ @{text R} is fixed throughout the specifications of @{text trcl} and @{text
+ accpart}. The point is that they might be fixed in a locale and we like to
+ support this. Accordingly we treat some parameters of the inductive
+ definition specially; see Figure~\ref{fig:inddefsfixed} where the transitive
+ closure and accessible part are defined with a fixed parameter @{text R} and
+ also inside a locale fixing @{text R}.
+*}
+
+text_raw {*
+\begin{figure}[p]
+\begin{isabelle}
+*}
+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: "(\<forall>y. R y x \<longrightarrow> accpart' R y) \<Longrightarrow> accpart' R x"
+
+locale rel =
+ fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+
+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: "(\<forall>y. R y x \<longrightarrow> accpart'' y) \<Longrightarrow> accpart'' x"
+text_raw {*
+\end{isabelle}
+\caption{The first definition is for the transitive closure where the
+relation @{text R} is explicitly fixed. Simiraly the second definition
+of the accessible part of the relation @{text R}. The last two definitions
+specify the same inductive predicates, but this time defined inside
+a locale.\label{fig:inddefsfixed}}
+\end{figure}
+*}
+
+text {*
+\begin{figure}[p]
+\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 {*
+ The syntax of the \simpleinductive{} command can be described by the
+ railroad diagram in Figure~\ref{fig:railroad}. This diagram more or less
+ translates directly into the parser
+
+ @{ML_chunk [display,gray] parser}
+
+ which we also described in Section~\ref{sec:parsingspecs}
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 type of
- the inductive predicate, as well as its 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 \cite{Krauss-IJCAR06} 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:
+ 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
+ \cite{Krauss-IJCAR06} 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; mixfix; Attrib.src; Attrib.src 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, together with a tuple containing the introduction and induction
- rules, which are stored in the local theory, too. In contrast to an
- ordinary theory, which simply consists of a type signature, as well as
- tables for constants, axioms and theorems, a local theory also contains
- additional context information, such as locally fixed variables and local
- assumptions that may be used by the package. The type @{ML_type
- local_theory} is identical to the type of \emph{proof contexts} @{ML_type
- "Proof.context"}, although not every proof context constitutes a valid local
- theory. Note that @{ML add_inductive_i in SimpleInductivePackage} expects
+ definition and the induction principle as well introduction rules.
+
+ In contrast to an ordinary theory, which simply consists of a type
+ signature, as well as tables for constants, axioms and theorems, a local
+ theory also contains additional context information, such as locally fixed
+ variables and local assumptions that may be used by the package. The type
+ @{ML_type local_theory} is identical to the type of \emph{proof contexts}
+ @{ML_type "Proof.context"}, although not every proof context constitutes a
+ valid local theory.
+
+
+ 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
+ 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. The names of the
+ 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 ->
@@ -162,237 +281,8 @@
The definition of the transitive closure should look as follows:
*}
-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"
-(*<*)
-thm trcl_def
-thm trcl.induct
-thm base
-thm step
-thm trcl.intros
-
-lemma trcl_strong_induct:
- assumes trcl: "trcl r x y"
- and I1: "\<And>x. P x x"
- and I2: "\<And>x y z. P x y \<Longrightarrow> trcl r x y \<Longrightarrow> r y z \<Longrightarrow> P x z"
- shows "P x y"
-proof -
- from trcl
- have "P x y \<and> trcl r x y"
- proof induct
- case (base x)
- from I1 and trcl.base show ?case ..
- next
- case (step x y z)
- then have "P x y" and "trcl r x y" by simp_all
- from `P x y` `trcl r x y` `r y z` have "P x z"
- by (rule I2)
- moreover from `trcl r x y` `r y z` have "trcl r x z"
- by (rule trcl.step)
- ultimately show ?case ..
- qed
- then show ?thesis ..
-qed
-(*>*)
-
-text {* Even and odd numbers can be defined by *}
-
-simple_inductive
- even and odd
-where
- even0: "even 0"
-| evenS: "odd n \<Longrightarrow> even (Suc n)"
-| oddS: "even n \<Longrightarrow> odd (Suc n)"
-(*<*)
-thm even_def odd_def
-thm even.induct odd.induct
-thm even0
-thm evenS
-thm oddS
-thm even_odd.intros
-(*>*)
-
-text {* The accessible part of a relation can be introduced as follows: *}
-
-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"
-(*<*)
-thm accpart_def
-thm accpart.induct
-thm accpartI
-(*>*)
-
-text {*
- Moreover, it should also be possible to define the accessible part
- inside a locale fixing the relation @{text r}:
-*}
-
-locale rel =
- fixes r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-
-simple_inductive (in rel) accpart'
-where
- accpartI': "\<And>x. (\<And>y. r y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
-(*<*)
-context rel
-begin
-
-thm accpartI'
-thm accpart'.induct
-
-end
-
-thm rel.accpartI'
-thm rel.accpart'.induct
-
-(*>*)
-
text {*
- In this context, it is important to note that Isabelle distinguishes
- between \emph{outer} and \emph{inner} syntax. Theory commands such as
- \isa{\isacommand{simple{\isacharunderscore}inductive} $\ldots$ \isacommand{for} $\ldots$ \isacommand{where} $\ldots$}
- belong to the outer syntax, whereas items in quotation marks, in particular
- terms such as @{text [source] "trcl r x x"} and types such as
- @{text [source] "'a \<Rightarrow> 'a \<Rightarrow> bool"} belong to the inner syntax.
- Separating the two layers of outer and inner syntax greatly simplifies
- matters, because the parser for terms and types does not have to know
- anything about the possible syntax of theory commands, and the parser
- for theory commands need not be concerned about the syntactic structure
- of terms and types.
-
- \medskip
- \noindent
- The syntax of the \isa{\isacommand{simple{\isacharunderscore}inductive}} command
- can be described by the following railroad diagram:
- \begin{rail}
- 'simple\_inductive' target? fixes ('for' fixes)? \\
- ('where' (thmdecl? prop + '|'))?
- ;
- \end{rail}
-
- \paragraph{Functional parsers}
-
- For parsing terms and types, Isabelle uses a rather general and sophisticated
- algorithm due to Earley, which is driven by \emph{priority grammars}.
- In contrast, parsers for theory syntax are built up using a set of combinators.
- Functional parsing using combinators is a well-established technique, which
- has been described by many authors, including Paulson \cite{paulson-ML-91}
- and Wadler \cite{Wadler-AFP95}.
- The central idea is that a parser is a function of type @{ML_type "'a list -> 'b * 'a list"},
- where @{ML_type "'a"} is a type of \emph{tokens}, and @{ML_type "'b"} is a type for
- encoding items that the parser has recognized. When a parser is applied to a
- list of tokens whose prefix it can recognize, it returns an encoding of the
- prefix as an element of type @{ML_type "'b"}, together with the suffix of the list
- containing the remaining tokens. Otherwise, the parser raises an exception
- indicating a syntax error. The library for writing functional parsers in
- Isabelle can roughly be split up into two parts. The first part consists of a
- collection of generic parser combinators that are contained in the structure
- @{ML_struct Scan} defined in the file @{ML_file "Pure/General/scan.ML"} in the Isabelle
- sources. While these combinators do not make any assumptions about the concrete
- structure of the tokens used, the second part of the library consists of combinators
- for dealing with specific token types.
- The following is an excerpt from the signature of @{ML_struct Scan}:
-
- \begin{table}
- @{ML "|| : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b"} \\
- @{ML "-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e"} \\
- @{ML "|-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e"} \\
- @{ML "--| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e"} \\
- @{ML "optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a" in Scan} \\
- @{ML "repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" in Scan} \\
- @{ML "repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" in Scan} \\
- @{ML ">> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c"} \\
- @{ML "!! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b"}
- \end{table}
-
- Interestingly, the functions shown above are so generic that they do not
- even rely on the input and output of the parser being a list of tokens.
- If \texttt{p} succeeds, i.e.\ does not raise an exception, the parser
- @{ML "p || q" for p q} returns the result of \texttt{p}, otherwise it returns
- the result of \texttt{q}. The parser @{ML "p -- q" for p q} first parses an
- item of type @{ML_type "'b"} using \texttt{p}, then passes the remaining tokens
- of type @{ML_type "'c"} to \texttt{q}, which parses an item of type @{ML_type "'d"}
- and returns the remaining tokens of type @{ML_type "'e"}, which are finally
- returned together with a pair of type @{ML_type "'b * 'd"} containing the two
- parsed items. The parsers @{ML "p |-- q" for p q} and @{ML "p --| q" for p q}
- work in a similar way as the previous one, with the difference that they
- discard the item parsed by the first and the second parser, respectively.
- If \texttt{p} succeeds, the parser @{ML "optional p x" for p x in Scan} returns the result
- of \texttt{p}, otherwise it returns the default value \texttt{x}. The parser
- @{ML "repeat p" for p in Scan} applies \texttt{p} as often as it can, returning a possibly
- empty list of parsed items. The parser @{ML "repeat1 p" for p in Scan} is similar,
- but requires \texttt{p} to succeed at least once. The parser
- @{ML "p >> f" for p f} uses \texttt{p} to parse an item of type @{ML_type "'b"}, to which
- it applies the function \texttt{f} yielding a value of type @{ML_type "'d"}, which
- is returned together with the remaining tokens of type @{ML_type "'c"}.
- Finally, @{ML "!!"} is used for transforming exceptions produced by parsers.
- If \texttt{p} raises an exception indicating that it cannot parse a given input,
- then an enclosing parser such as
- @{ML [display] "q -- p || r" for p q r}
- will try the alternative parser \texttt{r}. By writing
- @{ML [display] "q -- !! err p || r" for err p q r}
- instead, one can achieve that a failure of \texttt{p} causes the whole parser to abort.
- The @{ML "!!"} operator is similar to the \emph{cut} operator in Prolog, which prevents
- the interpreter from backtracking. The \texttt{err} function supplied as an argument
- to @{ML "!!"} can be used to produce an error message depending on the current
- state of the parser, as well as the optional error message returned by \texttt{p}.
-
- So far, we have only looked at combinators that construct more complex parsers
- from simpler parsers. In order for these combinators to be useful, we also need
- some basic parsers. As an example, we consider the following two parsers
- defined in @{ML_struct Scan}:
-
- \begin{table}
- @{ML "one: ('a -> bool) -> 'a list -> 'a * 'a list" in Scan} \\
- @{ML "$$ : string -> string list -> string * string list"}
- \end{table}
-
- The parser @{ML "one pred" for pred in Scan} parses exactly one token that
- satisfies the predicate \texttt{pred}, whereas @{ML "$$ s" for s} only
- accepts a token that equals the string \texttt{s}. Note that we can easily
- express @{ML "$$ s" for s} using @{ML "one" in Scan}:
- @{ML [display] "one (fn s' => s' = s)" for s in Scan}
- As an example, let us look at how we can use @{ML "$$"} and @{ML "--"} to parse
- the prefix ``\texttt{hello}'' of the character list ``\texttt{hello world}'':
-
- @{ML_response [display]
- "($$ \"h\" -- $$ \"e\" -- $$ \"l\" -- $$ \"l\" -- $$ \"o\")
- [\"h\", \"e\", \"l\", \"l\", \"o\", \" \", \"w\", \"o\", \"r\", \"l\", \"d\"]"
- "(((((\"h\", \"e\"), \"l\"), \"l\"), \"o\"), [\" \", \"w\", \"o\", \"r\", \"l\", \"d\"])
- : ((((string * string) * string) * string) * string) * string list"}
-
- Most of the time, however, we will have to deal with tokens that are not just strings.
- The parsers for the theory syntax, as well as the parsers for the argument syntax
- of proof methods and attributes use the token type @{ML_type OuterParse.token},
- which is identical to @{ML_type OuterLex.token}.
- The parser functions for the theory syntax are contained in the structure
- @{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/outer_parse.ML"}.
- In our parser, we will use the following functions:
-
- \begin{table}
- @{ML "$$$ : string -> token list -> string * token list" in OuterParse} \\
- @{ML "enum1: string -> (token list -> 'a * token list) -> token list ->
- 'a list * token list" in OuterParse} \\
- @{ML "prop: token list -> string * token list" in OuterParse} \\
- @{ML "opt_target: token list -> string option * token list" in OuterParse} \\
- @{ML "fixes: token list ->
- (Binding.binding * string option * mixfix) list * token list" in OuterParse} \\
- @{ML "for_fixes: token list ->
- (Binding.binding * string option * mixfix) list * token list" in OuterParse} \\
- @{ML "!!! : (token list -> 'a) -> token list -> 'a" in OuterParse}
- \end{table}
-
- The parsers @{ML "$$$" in OuterParse} and @{ML "!!!" in OuterParse} are
- defined using the parsers @{ML "one" in Scan} and @{ML "!!"} from
- @{ML_struct Scan}.
- The parser @{ML "enum1 s p" for s p in OuterParse} parses a non-emtpy list of items
- recognized by the parser \texttt{p}, where the items are separated by \texttt{s}.
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
@@ -414,7 +304,7 @@
We now have all the necessary tools to write the parser for our
\isa{\isacommand{simple{\isacharunderscore}inductive}} command:
- @{ML_chunk [display] syntax}
+
The definition of the parser \verb!ind_decl! closely follows the railroad
diagram shown above. In order to make the code more readable, the structures