theory Ind_Interface

imports "../Base" Simple_Inductive_Package

begin

section {* Parsing and Typing the Specification\label{sec:interface} *}

text_raw {*

\begin{figure}[p]

\begin{boxedminipage}{\textwidth}

\begin{isabelle}

*}

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: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"

(*<*)

datatype trm =

  Var "string"

| App "trm" "trm"

| Lam "string" "trm"

(*>*)

simple_inductive 

  fresh :: "string \<Rightarrow> trm \<Rightarrow> bool" 

where

  fresh_var: "a\<noteq>b \<Longrightarrow> fresh a (Var b)"

| fresh_app: "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"

| fresh_lam1: "fresh a (Lam a t)"

| fresh_lam2: "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"

text_raw {*

\end{isabelle}

\end{boxedminipage}

\caption{Specification given by the user for the inductive predicates

@{term "trcl"}, @{term "even"} and @{term "odd"}, @{term "accpart"} and 

@{term "fresh"}.\label{fig:specs}}

\end{figure}  

*}

text {*

  \begin{figure}[p]

  \begin{boxedminipage}{\textwidth}

  \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

  (where (thmdecl? prop + '|'))?

  ;

  \end{rail}

  \end{isabelle}

  \end{boxedminipage}

  \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 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 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}. This diagram more 

  or less translates directly into the parser:

*}

ML{*val spec_parser = 

   OuterParse.fixes -- 

   Scan.optional 

     (OuterParse.$$$ "where" |--

        OuterParse.!!! 

          (OuterParse.enum1 "|" 

             (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}

text {*

  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 =

  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

text {*

  and then define the transitive closure and the accessible part of this 

  locale 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"

(*<*)ML %no{*fun filtered_input str = 

  filter OuterLex.is_proper (OuterSyntax.scan Position.none str) 

fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input*}(*>*)

text {*

  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

  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\")]), [])"}

  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 5 to 7 in the code below.\footnote{FIXME: Is there a way to state 

  here @{text "simple_inductive"}?}

*}

(*<*)ML %no{*fun add_inductive_cmd pred_specs rule_specs lthy = lthy 

   fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*)

ML_val %linenosgray{*val specification =

  spec_parser >>

    (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)

val _ = OuterSyntax.local_theory "simple_inductive2" 

          "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_val{*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*}

text {*

  Once we have the input data as some internal datastructure, we call

  the function @{text 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(*>*)