--- a/ProgTutorial/Package/Ind_Interface.thy Tue Mar 31 16:50:13 2009 +0100
+++ b/ProgTutorial/Package/Ind_Interface.thy Tue Mar 31 20:31:18 2009 +0100
@@ -7,19 +7,19 @@
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}):