theory Ind_Interface
imports "../Base" Simple_Inductive_Package
begin

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
  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 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
  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 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_specification in Specification}. Note that the format
  for rules supported by @{ML read_specification 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_specification 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_specification 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_specification 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:
*}

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 -> token list -> Attrib.binding * token list" in SpecParse}
  \end{table}

  We now have all the necessary tools to write the parser for our
  \isa{\isacommand{simple{\isacharunderscore}inductive}} command:
  
 

  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
  @{ML_struct OuterParse} and @{ML_struct OuterKeyword} are abbreviated by
  \texttt{P} and \texttt{K}, respectively. Note how the parser combinator
  @{ML "!!!" in OuterParse} is used: once the keyword \texttt{where}
  has been parsed, a non-empty list of introduction rules must follow.
  Had we not used the combinator @{ML "!!!" in OuterParse}, a
  \texttt{where} not followed by a list of rules would have caused the parser
  to respond with the somewhat misleading error message

  \begin{verbatim}
  Outer syntax error: end of input expected, but keyword where was found
  \end{verbatim}

  rather than with the more instructive message

  \begin{verbatim}
  Outer syntax error: proposition expected, but terminator was found
  \end{verbatim}

  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.
*}

(*<*)
end
(*>*)