theory Ind_Interface
imports Ind_Intro Simple_Inductive_Package
keywords "simple_inductive2" :: thy_decl
begin

section \<open>Parsing and Typing the Specification\label{sec:interface}\<close>

text_raw \<open>
\begin{figure}[t]
\begin{boxedminipage}{\textwidth}
\begin{isabelle}
\<close>
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 \<open>
\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}  
\<close>

text \<open>
  To be able to write down the specifications of 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 from the previous section are shown in
  Figure~\ref{fig:specs}. The syntax used in these examples more or
  less translates directly into the parser:

\<close>

ML %grayML\<open>val spec_parser = 
   Parse.vars -- 
   Scan.optional 
     (Parse.$$$ "where" |--
        Parse.!!! 
          (Parse.enum1 "|" 
             (Parse_Spec.opt_thm_name ":" -- Parse.prop))) []\<close>

text \<open>
  which we explained in Section~\ref{sec:parsingspecs}.  There is no code included 
  for parsing the keyword and what is called a \emph{target}. The latter  can be given 
  optionally after the keyword. The target 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
\<close>

locale rel =
  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

text \<open>
  and then define the transitive closure and the accessible part of this 
  locale as follows:
\<close>

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\<open>fun filtered_input str = 
  filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str) 
fun parse p input = Scan.finite Token.stopper (Scan.error p) input\<close>(*>*)
text \<open>
  Note that in these definitions the parameter \<open>R\<close>, 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,_), _),
      ((evenS,_), _),
      ((oddS,_), _)]), [])"}

  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.
\<close>
(*<*)ML %no\<open>fun add_inductive_cmd pred_specs rule_specs lthy = lthy 
   fun add_inductive pred_specs rule_specs lthy = lthy\<close>(*>*) (* FIXME: Is the dummy simple_inductive2 installed with ML, before there was ML_val*)
ML %linenosgray\<open>val specification : (local_theory -> local_theory) parser =
  spec_parser >>
    (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)

val _ = Outer_Syntax.local_theory @{command_keyword "simple_inductive2"}
          "definition of simple inductive predicates"
             specification\<close>

text \<open>
  We call @{ML_ind  local_theory in Outer_Syntax} with the kind-indicator 
  @{ML_ind  thy_decl in Keyword} since the package does not need to open 
  up any proof (see Section~\ref{sec:newcommand}). 
  The auxiliary function \<open>specification\<close> in Lines 1 to 3
  gathers the information from the parser to be processed further
  by the function \<open>add_inductive_cmd\<close>, 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_ind  read_multi_specs 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 
  \<open>add_inductive_cmd\<close> is a call to @{ML read_multi_specs in Specification}.
\<close>

ML_val%grayML\<open>fun add_inductive_cmd pred_specs rule_specs lthy =
let
  val ((pred_specs', rule_specs'), _) = 
         Specification.read_multi_specs pred_specs rule_specs lthy
in
  add_inductive pred_specs' rule_specs' lthy
end\<close>

text \<open>
  Once we have the input data as some internal datastructure, we call
  the function \<open>add_inductive\<close>. 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.
\<close>
(*<*)end(*>*)