--- a/ProgTutorial/Package/Ind_Interface.thy Mon Mar 30 17:40:20 2009 +0200
+++ b/ProgTutorial/Package/Ind_Interface.thy Wed Apr 01 14:50:09 2009 +0200
@@ -2,24 +2,24 @@
imports "../Base" "../Parsing" Ind_Prelims Simple_Inductive_Package
begin
-section {* Parsing and Typing the Specification *}
+section {* Parsing and Typing the Specification\label{sec:interface} *}
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{}. The ``infrastructure'' already
+ provides an ``advanced'' feature for this command. For example we will
+ be able to declare the locale
*}
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,68 +31,6 @@
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}
@@ -102,7 +40,7 @@
\railalias{where}{\isacommand{where}}
\railalias{for}{\isacommand{for}}
\begin{rail}
- simpleinductive target? fixes (for fixes)? \\
+ simpleinductive target?\\ fixes
(where (thmdecl? prop + '|'))?
;
\end{rail}
@@ -110,8 +48,7 @@
\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
+ 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}
@@ -121,9 +58,17 @@
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}
+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
parser the string (which corresponds to our definition of @{term even} and
@{term odd}):
@@ -448,6 +393,11 @@
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.
+
*}