
diff -r a9eb69749c93 -r 1dc03eaa7cb9 ProgTutorial/Package/Ind_Interface.thy
--- a/ProgTutorial/Package/Ind_Interface.thy	Mon Mar 30 17:40:20 2009 +0200
+++ b/ProgTutorial/Package/Ind_Interface.thy	Wed Apr 01 12:28:14 2009 +0100
@@ -1,25 +1,116 @@
 theory Ind_Interface
-imports "../Base" "../Parsing" Ind_Prelims Simple_Inductive_Package
+imports "../Base" "../Parsing" Simple_Inductive_Package
 begin
 
-section {* Parsing and Typing the Specification *}
+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{}. In the package we want to support
-  some ``advanced'' features: First, we want that the package can cope with
-  specifications inside locales. For example it should be possible to declare
+  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 =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 
 text {*
-  and then define the transitive closure and the accessible part as follows:
+  and then define the transitive closure and the accessible part of this 
+  locale as follows:
 *}
 
-
 simple_inductive (in rel) 
   trcl' 
 where
@@ -31,100 +122,9 @@
 where
   accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
 
-text {* 
-  Second, we want that the user can specify fixed parameters.
-  Remember in the previous section we stated that the user can give the 
-  specification for the transitive closure of a relation @{text R} as 
-*}
-
-simple_inductive
-  trcl\<iota>\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
-where
-  base: "trcl\<iota>\<iota> R x x"
-| step: "trcl\<iota>\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota>\<iota> R x z"
-
 text {*
-  Note that there is no locale given in this specification---the parameter
-  @{text "R"} therefore needs to be included explicitly in @{term trcl\<iota>\<iota>}, but
-  stays fixed throughout the specification. The problem with this way of
-  stating the specification for the transitive closure is that it derives the
-  following induction principle.
-
-  \begin{center}\small
-  \mprset{flushleft}
-  \mbox{\inferrule{
-             @{thm_style prem1  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
-             @{thm_style prem2  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
-             @{thm_style prem3  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}
-            {@{thm_style concl  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}}  
-  \end{center}
-
-  But this does not correspond to the induction principle we derived by hand, which
-  was
-  
-  \begin{center}\small
-  \mprset{flushleft}
-  \mbox{\inferrule{
-             @{thm_style prem1  trcl_induct[no_vars]}\\\\
-             @{thm_style prem2  trcl_induct[no_vars]}\\\\
-             @{thm_style prem3  trcl_induct[no_vars]}}
-            {@{thm_style concl  trcl_induct[no_vars]}}}  
-  \end{center}
-
-  The difference is that in the one derived by hand the relation @{term R} is not
-  a parameter of the proposition @{term P} to be proved and it is also not universally
-  qunatified in the second and third premise. The point is that the parameter @{term R}
-  stays fixed thoughout the definition and we do not want to regard it as an ``ordinary''
-  argument of the transitive closure, but one that can be freely instantiated. 
-  In order to recognise such parameters, we have to extend the specification
-  to include a mechanism to state fixed parameters. The user should be able
-  to write 
-
-*}
-
-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: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R 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 (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 {*
-  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_chunk [display,gray] parser}
-
-  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}):
 
@@ -143,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
@@ -448,9 +463,10 @@
   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. 
+  
 *}
-
-
-(*<*)
-end
-(*>*)
+(*<*)end(*>*)
\ No newline at end of file




