theory Ind_Interface+ −
imports "../Base" Simple_Inductive_Package+ −
begin+ −
+ −
section {* Parsing and Typing the Specification\label{sec:interface} *}+ −
+ −
text_raw {*+ −
\begin{figure}[t]+ −
\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 + −
@{term "fresh"}.\label{fig:specs}}+ −
\end{figure} + −
*}+ −
+ −
text {* + −
To be able to write down the specifications of inductive predicates, we have+ −
to introduce a new command (see Section~\ref{sec:newcommand}). As the+ −
keyword for the new command we chose \simpleinductive{}. Examples of+ −
specifications from the previous section are shown in+ −
Figure~\ref{fig:specs}. The syntax used in these examples 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 explained in Section~\ref{sec:parsingspecs}. There is no code included + −
for parsing the keyword and what is called a \emph{target}. The latter can be given + −
optionally after the keyword. The target is an ``advanced'' feature which we will + −
inherit for ``free'' from the infrastructure on which we shall build the package. + −
The target stands for a locale and allows us to specify+ −
*}+ −
+ −
locale rel =+ −
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"+ −
+ −
text {*+ −
and then define the transitive closure and the accessible part of this + −
locale as follows:+ −
*}+ −
+ −
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: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"+ −
(*<*)ML %no{*fun filtered_input str = + −
filter OuterLex.is_proper (OuterSyntax.scan Position.none str) + −
fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input*}(*>*)+ −
text {*+ −
Note that in these definitions the parameter @{text R}, standing for the+ −
relation, is left implicit. For the moment we will ignore this kind+ −
of implicit parameters and rely on the fact that the infrastructure will+ −
deal with them. Later, however, we will come back to them.+ −
+ −
If we feed into the parser the string that corresponds to our definition + −
of @{term even} and @{term odd}+ −
+ −
@{ML_response [display,gray]+ −
"let+ −
val input = filtered_input+ −
(\"even and odd \" ^ + −
\"where \" ^+ −
\" even0[intro]: \\\"even 0\\\" \" ^ + −
\"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ + −
\"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\" \")+ −
in+ −
parse spec_parser input+ −
end"+ −
"(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],+ −
[((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 specifications of the predicates (with type and syntax annotations), + −
and 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 5 to 7 in the code below.+ −
*}+ −
(*<*)ML %no{*fun add_inductive_cmd pred_specs rule_specs lthy = lthy + −
fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*)+ −
ML_val %linenosgray{*val specification =+ −
spec_parser >>+ −
(fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)+ −
+ −
val _ = OuterSyntax.local_theory "simple_inductive2" + −
"definition of simple inductive predicates"+ −
OuterKeyword.thy_decl specification*}+ −
+ −
text {*+ −
We call @{ML_ind local_theory in OuterSyntax} with the kind-indicator + −
@{ML_ind thy_decl in OuterKeyword} since the package does not need to open + −
up any proof (see Section~\ref{sec:newcommand}). + −
The auxiliary function @{text specification} in Lines 1 to 3+ −
gathers the information from the parser to be processed further+ −
by the function @{text "add_inductive_cmd"}, which we describe below. + −
+ −
Note that the predicates when they come out of the parser are just some+ −
``naked'' strings: they have no type yet (even if we annotate them with+ −
types) and they are also not defined constants yet (which the predicates + −
eventually will be). Also the introduction rules are just strings. What we have+ −
to do first is to transform the parser's output into some internal+ −
datastructures that can be processed further. For this we can use the+ −
function @{ML_ind read_spec in Specification}. This function takes some strings+ −
(with possible typing annotations) and some rule specifications, and attempts+ −
to find a typing according to the given type constraints given by the + −
user and the type constraints by the ``ambient'' theory. It returns + −
the type for the predicates and also returns typed terms for the+ −
introduction rules. So at the heart of the function + −
@{text "add_inductive_cmd"} is a call to @{ML read_spec in Specification}.+ −
*}+ −
+ −
ML_val{*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*}+ −
+ −
text {*+ −
Once we have the input data as some internal datastructure, we call+ −
the function @{text add_inductive}. This function does the heavy duty + −
lifting in the package: it generates definitions for the + −
predicates and derives from them corresponding induction principles and + −
introduction rules. The description of this function will span over+ −
the next two sections.+ −
*}+ −
(*<*)end(*>*)+ −