diff -r 7ff7325e3b4e -r 98d43270024f ProgTutorial/Package/Ind_Interface.thy
--- a/ProgTutorial/Package/Ind_Interface.thy	Tue Mar 31 20:31:18 2009 +0100
+++ b/ProgTutorial/Package/Ind_Interface.thy	Wed Apr 01 12:26:56 2009 +0100
@@ -1,15 +1,106 @@
 theory Ind_Interface
-imports "../Base" "../Parsing" Ind_Prelims Simple_Inductive_Package
+imports "../Base" "../Parsing" 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 
+@{text "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 anotations); \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
   a new command (see Section~\ref{sec:newcommand}).  As the keyword for the
-  new command we chose \simpleinductive{}. The ``infrastructure'' already 
-  provides an ``advanced'' feature for this command. For example we will 
-  be able to declare the locale
+  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:
+*}
+
+ML{*val spec_parser = 
+   OuterParse.fixes -- 
+   Scan.optional 
+     (OuterParse.$$$ "where" |--
+        OuterParse.!!! 
+          (OuterParse.enum1 "|" 
+             (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
 *}
 
 locale rel =
@@ -32,44 +123,8 @@
   accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
 
 text {*
-  \begin{figure}[t]
-  \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}
-  \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 
-  introduction rule with an optional theorem declaration (\emph{thmdecl}).
-  \label{fig:railroad}}
-  \end{figure}
-*}
-
-text {*
-  This leads directly to the railroad diagram shown in
-  Figure~\ref{fig:railroad} for the syntax of \simpleinductive{}. This diagram
-  more or less translates directly into the parser:
-*}
-
-ML %linenosgray{*val spec_parser = 
-     OuterParse.fixes -- 
-     Scan.optional 
-       (OuterParse.$$$ "where" |--
-          OuterParse.!!! 
-            (OuterParse.enum1 "|" 
-               (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
-
-text {*
-  which we described in Section~\ref{sec:parsingspecs}. If we feed into the 
+  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}):
 
@@ -88,22 +143,37 @@
      [((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 predicates (with type
+  and syntax annotations), and the 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.
 *}
 
+(*<*)
+ML{* fun add_inductive pred_specs rule_specs lthy = lthy *}
+(*>*)
+
+ML{*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 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 {*
-  then we get back a locale (in this case @{ML NONE}), the predicates (with type
-  and syntax annotations), the parameters (similar as the predicates) and
-  the 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.
-
-  @{ML_chunk [display,gray,linenos] syntax}
-  
   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
@@ -399,8 +469,4 @@
   the third with the introduction rules. 
   
 *}
-
-
-(*<*)
-end
-(*>*)
+(*<*)end(*>*)
\ No newline at end of file