
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: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> 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,\<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\")]), [])"}
 
-  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 \<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 {*
-  (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




