--- a/ProgTutorial/Package/Ind_Interface.thy Tue Mar 31 20:31:18 2009 +0100
+++ b/ProgTutorial/Package/Ind_Interface.thy Wed Apr 01 12:26:56 2009 +0100
@@ -1,15 +1,106 @@
theory Ind_Interface
-imports "../Base" "../Parsing" Ind_Prelims Simple_Inductive_Package
+imports "../Base" "../Parsing" Simple_Inductive_Package
begin
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{}. The ``infrastructure'' already
- provides an ``advanced'' feature for this command. For example we will
- be able to declare the locale
+ 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 =
@@ -32,44 +123,8 @@
accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' 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
- (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); \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 %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
+ 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}):
@@ -88,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
@@ -399,8 +469,4 @@
the third with the introduction rules.
*}
-
-
-(*<*)
-end
-(*>*)
+(*<*)end(*>*)
\ No newline at end of file