--- a/CookBook/Package/Ind_Interface.thy Sat Feb 21 11:38:14 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy Sun Feb 22 03:44:03 2009 +0000
@@ -1,15 +1,15 @@
theory Ind_Interface
-imports "../Base" "../Parsing" Simple_Inductive_Package
+imports "../Base" "../Parsing" Ind_Prelims Simple_Inductive_Package
begin
-section {* Parsing the Specification *}
+section {* Parsing and Typing 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{}. We want that the package can cope with
+ 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
-
*}
locale rel =
@@ -20,35 +20,68 @@
*}
-simple_inductive (in rel) trcl'
+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'
+simple_inductive (in rel)
+ accpart'
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 {*
- After the keyword we expect a constant (or constants) with possible typing
- annotations and a
- list of introduction rules. While these specifications are all
- straightforward, there is a technicality we like to deal with to do with
- fixed parameters and locales. Remember we pointed out that the parameter
- @{text R} is fixed throughout the specifications of @{text trcl} and @{text
- accpart}. The point is that they might be fixed in a locale and we like to
- support this. Accordingly we treat some parameters of the inductive
- definition specially; see Figure~\ref{fig:inddefsfixed} where the transitive
- closure and accessible part are defined with a fixed parameter @{text R} and
- also inside a locale fixing @{text R}.
+ 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
+
*}
-text_raw {*
- \begin{figure}[p]
- \begin{isabelle}
-*}
simple_inductive
trcl'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
where
@@ -60,18 +93,8 @@
where
accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x"
-text_raw {*
- \end{isabelle}
- \caption{The first definition is for the transitive closure where the
- relation @{text R} is explicitly fixed. Simiraly the second definition
- of the accessible part of the relation @{text R}. The last two definitions
- specify the same inductive predicates, but this time defined inside
- a locale.\label{fig:inddefsfixed}}
- \end{figure}
-*}
-
text {*
- \begin{figure}[p]
+ \begin{figure}[t]
\begin{isabelle}
\railnontermfont{\rmfamily\itshape}
\railterm{simpleinductive,where,for}
@@ -95,11 +118,10 @@
*}
text {*
- For the first subtask, the syntax of the \simpleinductive{} command can be
- described by the railroad diagram in Figure~\ref{fig:railroad}. This diagram
+ 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