--- a/CookBook/Package/Ind_Interface.thy	Thu Feb 19 14:44:53 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy	Fri Feb 20 23:19:41 2009 +0000
@@ -2,54 +2,34 @@
 imports "../Base" "../Parsing" 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 the needed properties.
-*}
-
-text {*
-  From a high-level perspective the package consists of 6 subtasks:
-
-  \begin{itemize}
-  \item reading the various parts of specification (i.e.~parser),
-  \item transforming the parser outut into an internal 
-  (typed) datastructure,
-  \item making the definitions, 
-  \item deriving the induction principles,
-  \item deriving the introduction rules, and
-  \item storing the results in the given theory. 
-  to the user. 
-  \end{itemize}
-
-*}
+section {* Parsing the Specification *}
 
 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 specifications corresponding to our
-  examples described earlier are:
+  command we chose \simpleinductive{}. We want that the package can cope with
+  specifications inside locales. For example it should be possible to declare
+
+*}
+
+locale rel =
+  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+
+text {*
+  and then define the transitive closure and the accessible part as follows:
 *}
 
-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
+simple_inductive (in rel) trcl' 
 where
-  even0: "even 0"
-| evenS: "odd n \<Longrightarrow> even (Suc n)"
-| oddS: "even n \<Longrightarrow> odd (Suc n)"
+  base: "trcl' x x"
+| step: "trcl' x y \<Longrightarrow> R y z \<Longrightarrow> trcl' x z"
 
-simple_inductive
-  accpart :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
+simple_inductive (in rel) accpart'
 where
-  accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
+  accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
+
+
 
 text {*
   After the keyword we expect a constant (or constants) with possible typing 
@@ -70,27 +50,16 @@
   \begin{isabelle}
 *}
 simple_inductive
-  trcl' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  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"
+  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"
+  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"
+  accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x"
 
-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
@@ -435,6 +404,27 @@
   behaviour of the user interface, such as failure of the undo mechanism.
 *}
 
+text {*
+  Note that the @{text trcl} predicate has two different kinds of parameters: the
+  first parameter @{text R} stays \emph{fixed} throughout the definition, whereas
+  the second and third parameter changes in the ``recursive call''. This will
+  become important later on when we deal with fixed parameters and locales. 
+
+
+ 
+  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 the needed properties.
+*}
+
+text {*
+  From a high-level perspective the package consists of 6 subtasks:
+
+
+
+*}
+
+
 (*<*)
 end
 (*>*)