# HG changeset patch # User berghofe # Date 1223651601 -7200 # Node ID 5bb2d29553c2f7dbd299ff3b12ced1a33e6abe8c # Parent 53460ac408b5e6b3395bd91574a7fc0c8acba1f6 Added new chapter about writing packages. diff -r 53460ac408b5 -r 5bb2d29553c2 CookBook/Package/Ind_Examples.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/CookBook/Package/Ind_Examples.thy Fri Oct 10 17:13:21 2008 +0200 @@ -0,0 +1,274 @@ +theory Ind_Examples +imports Main +begin + +section{* Examples of inductive definitions *} + +text {* +\label{sec:ind-examples} +In this section, we will give three examples showing how to define inductive +predicates by hand and prove characteristic properties such as introduction +rules and an induction rule. From these examples, we will then figure out a +general method for defining inductive predicates, which will be described in +\S\ref{sec:ind-general-method}. This description will serve as a basis for the +actual implementation to be developed in \S\ref{sec:ind-interface} -- \S\ref{sec:ind-proofs}. +It should be noted that our aim in this section is not to write proofs that +are as beautiful as possible, but as close as possible to the ML code producing +the proofs that we will develop later. +As a first example, we consider the \emph{transitive closure} @{text "trcl R"} +of a relation @{text R}. It is characterized by the following +two introduction rules +\[ +\begin{array}{l} +@{term "trcl R x x"} \\ +@{term [mode=no_brackets] "R x y \ trcl R y z \ trcl R x z"} +\end{array} +\] +Note that the @{text trcl} predicate has two different kinds of parameters: the +first parameter @{text R} stays \emph{fixed} throughout the definition, whereas +the second and third parameter changes in the ``recursive call''. +Since an inductively defined predicate is the \emph{least} predicate closed under +a collection of introduction rules, we define the predicate @{text "trcl R x y"} in +such a way that it holds if and only if @{text "P x y"} holds for every predicate +@{text P} closed under the above rules. This gives rise to a definition containing +a universal quantifier over the predicate @{text P}: +*} + +definition "trcl \ \R x y. + \P. (\x. P x x) \ (\x y z. R x y \ P y z \ P x z) \ P x y" + +text {* +\noindent +Since the predicate @{term "trcl R x y"} yields an element of the type of object +level truth values @{text bool}, the meta-level implications @{text "\"} in the +above introduction rules have to be converted to object-level implications +@{text "\"}. Moreover, we use object-level universal quantifiers @{text "\"} +rather than meta-level universal quantifiers @{text "\"} for quantifying over +the variable parameters of the introduction rules. Isabelle already offers some +infrastructure for converting between meta-level and object-level connectives, +which we will use later on. + +With this definition of the transitive closure, the proof of the (weak) induction +theorem is almost immediate. It suffices to convert all the meta-level connectives +in the induction rule to object-level connectives using the @{text atomize} proof +method, expand the definition of @{text trcl}, eliminate the universal quantifier +contained in it, and then solve the goal by assumption. +*} + +lemma trcl_induct: + assumes trcl: "trcl R x y" + shows "(\x. P x x) \ (\x y z. R x y \ P y z \ P x z) \ P x y" + apply (atomize (full)) + apply (cut_tac trcl) + apply (unfold trcl_def) + apply (drule spec [where x=P]) + apply assumption + done +(*<*) +lemma "trcl R x x" + apply (unfold trcl_def) + apply (rule allI impI)+ +(*>*) +txt {* +\noindent +The above induction rule is \emph{weak} in the sense that the induction step may +only be proved using the assumptions @{term "R x y"} and @{term "P y z"}, but not +using the additional assumption \mbox{@{term "trcl R y z"}}. A stronger induction rule +containing this additional assumption can be derived from the weaker one with the +help of the introduction rules for @{text trcl}. + +We now turn to the proofs of the introduction rules, which are slightly more complicated. +In order to prove the first introduction rule, we again unfold the definition and +then apply the introdution rules for @{text "\"} and @{text "\"} as often as possible. +We then end up in a proof state of the following form: +@{subgoals [display]} +The two assumptions correspond to the introduction rules, where @{term "trcl R"} has been +replaced by @{term "P"}. Thus, all we have to do is to eliminate the universal quantifier +in front of the first assumption, and then solve the goal by assumption: +*} +(*<*)oops(*>*) +lemma trcl_base: "trcl R x x" + apply (unfold trcl_def) + apply (rule allI impI)+ + apply (drule spec) + apply assumption + done +(*<*) +lemma "R x y \ trcl R y z \ trcl R x z" + apply (unfold trcl_def) + apply (rule allI impI)+ +(*>*) +txt {* +\noindent +Since the second introduction rule has premises, its proof is not as easy as the previous +one. After unfolding the definitions and applying the introduction rules for @{text "\"} +and @{text "\"}, we get the proof state +@{subgoals [display]} +The third and fourth assumption corresponds to the first and second introduction rule, +respectively, whereas the first and second assumption corresponds to the premises of +the introduction rule. Since we want to prove the second introduction rule, we apply +the fourth assumption to the goal @{term "P x z"}. In order for the assumption to +be applicable, we have to eliminate the universal quantifiers and turn the object-level +implications into meta-level ones. This can be accomplished using the @{text rule_format} +attribute. Applying the assumption produces two new subgoals, which can be solved using +the first and second assumption. The second assumption again involves a quantifier and +implications that have to be eliminated before it can be applied. To avoid problems +with higher order unification, it is advisable to provide an instantiation for the +universally quantified predicate variable in the assumption. +*} +(*<*)oops(*>*) +lemma trcl_step: "R x y \ trcl R y z \ trcl R x z" + apply (unfold trcl_def) + apply (rule allI impI)+ + proof - + case goal1 + show ?case + apply (rule goal1(4) [rule_format]) + apply (rule goal1(1)) + apply (rule goal1(2) [THEN spec [where x=P], THEN mp, THEN mp, + OF goal1(3-4)]) + done + qed + +text {* +\noindent +This method of defining inductive predicates easily generalizes to mutually inductive +predicates, like the predicates @{text even} and @{text odd} characterized by the +following introduction rules: +\[ +\begin{array}{l} +@{term "even (0::nat)"} \\ +@{term "odd m \ even (Suc m)"} \\ +@{term "even m \ odd (Suc m)"} +\end{array} +\] +Since the predicates are mutually inductive, each of the definitions contain two +quantifiers over the predicates @{text P} and @{text Q}. +*} + +definition "even \ \n. + \P Q. P 0 \ (\m. Q m \ P (Suc m)) \ (\m. P m \ Q (Suc m)) \ P n" + +definition "odd \ \n. + \P Q. P 0 \ (\m. Q m \ P (Suc m)) \ (\m. P m \ Q (Suc m)) \ Q n" + +text {* +\noindent +For proving the induction rule, we use exactly the same technique as in the transitive +closure example: +*} + +lemma even_induct: + assumes even: "even n" + shows "P 0 \ (\m. Q m \ P (Suc m)) \ (\m. P m \ Q (Suc m)) \ P n" + apply (atomize (full)) + apply (cut_tac even) + apply (unfold even_def) + apply (drule spec [where x=P]) + apply (drule spec [where x=Q]) + apply assumption + done + +text {* +\noindent +A similar induction rule having @{term "Q n"} as a conclusion can be proved for +the @{text odd} predicate. +The proofs of the introduction rules are also very similar to the ones in the +previous example. We only show the proof of the second introduction rule, +since it is almost the same as the one for the third introduction rule, +and the proof of the first rule is trivial. +*} + +lemma evenS: "odd m \ even (Suc m)" + apply (unfold odd_def even_def) + apply (rule allI impI)+ + proof - + case goal1 + show ?case + apply (rule goal1(3) [rule_format]) + apply (rule goal1(1) [THEN spec [where x=P], THEN spec [where x=Q], + THEN mp, THEN mp, THEN mp, OF goal1(2-4)]) + done + qed +(*<*) +lemma even0: "even 0" + apply (unfold even_def) + apply (rule allI impI)+ + apply assumption + done + +lemma oddS: "even m \ odd (Suc m)" + apply (unfold odd_def even_def) + apply (rule allI impI)+ + proof - + case goal1 + show ?case + apply (rule goal1(4) [rule_format]) + apply (rule goal1(1) [THEN spec [where x=P], THEN spec [where x=Q], + THEN mp, THEN mp, THEN mp, OF goal1(2-4)]) + done + qed +(*>*) +text {* +\noindent +As a final example, we will consider the definition of the accessible +part of a relation @{text R} characterized by the introduction rule +\[ +@{term "(\y. R y x \ accpart R y) \ accpart R x"} +\] +whose premise involves a universal quantifier and an implication. The +definition of @{text accpart} is as follows: +*} + +definition "accpart \ \R x. \P. (\x. (\y. R y x \ P y) \ P x) \ P x" + +text {* +\noindent +The proof of the induction theorem is again straightforward: +*} + +lemma accpart_induct: + assumes acc: "accpart R x" + shows "(\x. (\y. R y x \ P y) \ P x) \ P x" + apply (atomize (full)) + apply (cut_tac acc) + apply (unfold accpart_def) + apply (drule spec [where x=P]) + apply assumption + done +(*<*) +lemma accpartI: "(\y. R y x \ accpart R y) \ accpart R x" + apply (unfold accpart_def) + apply (rule allI impI)+ +(*>*) +txt {* +\noindent +Proving the introduction rule is a little more complicated, due to the quantifier +and the implication in the premise. We first convert the meta-level universal quantifier +and implication to their object-level counterparts. Unfolding the definition of +@{text accpart} and applying the introduction rules for @{text "\"} and @{text "\"} +yields the following proof state: +@{subgoals [display]} +Applying the second assumption produces a proof state with the new local assumption +@{term "R y x"}, which will then be used to solve the goal @{term "P y"} using the +first assumption. +*} +(*<*)oops(*>*) +lemma accpartI: "(\y. R y x \ accpart R y) \ accpart R x" + apply (unfold accpart_def) + apply (rule allI impI)+ + proof - + case goal1 + note goal1' = this + show ?case + apply (rule goal1'(2) [rule_format]) + proof - + case goal1 + show ?case + apply (rule goal1'(1) [OF goal1, THEN spec [where x=P], + THEN mp, OF goal1'(2)]) + done + qed + qed + +end diff -r 53460ac408b5 -r 5bb2d29553c2 CookBook/Package/Ind_General_Scheme.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/CookBook/Package/Ind_General_Scheme.thy Fri Oct 10 17:13:21 2008 +0200 @@ -0,0 +1,71 @@ +theory Ind_General_Scheme +imports Main +begin + +section{* The general construction principle *} + +text {* +\label{sec:ind-general-method} +Before we start with the implementation, it is useful to describe the general +form of inductive definitions that our package should accept. We closely follow +the notation for inductive definitions introduced by Schwichtenberg +\cite{Schwichtenberg-MLCF} for the Minlog system. +Let $R_1,\ldots,R_n$ be mutually inductive predicates and $\vec{p}$ be +parameters. Then the introduction rules for $R_1,\ldots,R_n$ may have +the form +\[ +\bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow + R_{k_{ij}}~\vec{p}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \Longrightarrow R_{l_i}~\vec{p}~\vec{t}_i +\qquad \mbox{for\ } i=1,\ldots,r +\] +where $\vec{A}_i$ and $\vec{B}_{ij}$ are formulae not containing $R_1,\ldots,R_n$. +Note that by disallowing the inductive predicates to occur in $\vec{B}_{ij}$ we make sure +that all occurrences of the predicates in the premises of the introduction rules are +\emph{strictly positive}. This condition guarantees the existence of predicates +that are closed under the introduction rules shown above. The inductive predicates +$R_1,\ldots,R_n$ can then be defined as follows: +\[ +\begin{array}{l@ {\qquad}l} + R_i \equiv \lambda\vec{p}~\vec{z}_i.~\forall P_1 \ldots P_n.~K_1 \longrightarrow \cdots \longrightarrow K_r \longrightarrow P_i~\vec{z}_i & + \mbox{for\ } i=1,\ldots,n \\[1.5ex] + \mbox{where} \\ + K_i \equiv \forall\vec{x}_i.~\vec{A}_i \longrightarrow \left(\forall\vec{y}_{ij}.~\vec{B}_{ij} \longrightarrow + P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \longrightarrow P_{l_i}~\vec{t}_i & + \mbox{for\ } i=1,\ldots,r +\end{array} +\] +The (weak) induction rules for the inductive predicates $R_1,\ldots,R_n$ are +\[ +\begin{array}{l@ {\qquad}l} + R_i~\vec{p}~\vec{z}_i \Longrightarrow I_1 \Longrightarrow \cdots \Longrightarrow I_r \Longrightarrow P_i~\vec{z}_i & + \mbox{for\ } i=1,\ldots,n \\[1.5ex] + \mbox{where} \\ + I_i \equiv \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow + P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \Longrightarrow P_{l_i}~\vec{t}_i & + \mbox{for\ } i=1,\ldots,r +\end{array} +\] +Since $K_i$ and $I_i$ are equivalent modulo conversion between meta-level and object-level +connectives, it is clear that the proof of the induction theorem is straightforward. We will +therefore focus on the proof of the introduction rules. When proving the introduction rule +shown above, we start by unfolding the definition of $R_1,\ldots,R_n$, which yields +\[ +\bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow + \forall P_1 \ldots P_n.~\vec{K} \longrightarrow P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \Longrightarrow \forall P_1 \ldots P_n.~\vec{K} \longrightarrow P_{l_i}~\vec{t}_i +\] +where $\vec{K}$ abbreviates $K_1,\ldots,K_r$. Applying the introduction rules for +$\forall$ and $\longrightarrow$ yields a proof state in which we have to prove $P_{l_i}~\vec{t}_i$ +from the additional assumptions $\vec{K}$. When using $K_{l_i}$ (converted to meta-logic format) +to prove $P_{l_i}~\vec{t}_i$, we get subgoals $\vec{A}_i$ that are trivially solvable by assumption, +as well as subgoals of the form +\[ +\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow P_{k_{ij}}~\vec{s}_{ij} \qquad \mbox{for\ } j=1,\ldots,m_i +\] +that can be solved using the assumptions +\[ +\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow + \forall P_1 \ldots P_n.~\vec{K} \longrightarrow P_{k_{ij}}~\vec{s}_{ij} \qquad \mbox{and} \qquad \vec{K} +\] +*} + +end diff -r 53460ac408b5 -r 5bb2d29553c2 CookBook/Package/Ind_Interface.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/CookBook/Package/Ind_Interface.thy Fri Oct 10 17:13:21 2008 +0200 @@ -0,0 +1,449 @@ +theory Ind_Interface +imports Base Simple_Inductive_Package +begin + +(*<*) +ML {* +structure SIP = SimpleInductivePackage +*} +(*>*) + +section{* The interface *} + +text {* +\label{sec:ind-interface} +In order to add a new inductive predicate to a theory with the help of our package, the user +must \emph{invoke} it. For every package, there are essentially two different ways of invoking +it, which we will refer to as \emph{external} and \emph{internal}. By external +invocation we mean that the package is called from within a theory document. In this case, +the type of the inductive predicate, as well as its introduction rules, are given as strings +by the user. Before the package can actually make the definition, the type and introduction +rules have to be parsed. In contrast, internal invocation means that the package is called +by some other package. For example, the function definition package \cite{Krauss-IJCAR06} +calls the inductive definition package to define the graph of the function. However, it is +not a good idea for the function definition package to pass the introduction rules for the +function graph to the inductive definition package as strings. In this case, it is better +to directly pass the rules to the package as a list of terms, which is more robust than +handling strings that are lacking the additional structure of terms. These two ways of +invoking the package are reflected in its ML programming interface, which consists of two +functions: +@{ML_chunk [display] SIMPLE_INDUCTIVE_PACKAGE} +The function for external invocation of the package is called @{ML_open add_inductive (SIP)}, +whereas the one for internal invocation is called @{ML_open add_inductive_i (SIP)}. Both +of these functions take as arguments the names and types of the inductive predicates, the +names and types of their parameters, the actual introduction rules and a \emph{local theory}. +They return a local theory containing the definition, together with a tuple containing +the introduction and induction rules, which are stored in the local theory, too. +In contrast to an ordinary theory, which simply consists of a type signature, as +well as tables for constants, axioms and theorems, a local theory also contains +additional context information, such as locally fixed variables and local assumptions +that may be used by the package. The type @{ML_type local_theory} is identical to the +type of \emph{proof contexts} @{ML_type "Proof.context"}, although not every proof context +constitutes a valid local theory. +Note that @{ML_open add_inductive_i (SIP)} expects the types +of the predicates and parameters to be specified using the datatype @{ML_type typ} of Isabelle's +logical framework, whereas @{ML_open add_inductive (SIP)} +expects them to be given as optional strings. If no string is +given for a particular predicate or parameter, this means that the type should be +inferred by the package. Additional \emph{mixfix syntax} may be associated with +the predicates and parameters as well. Note that @{ML_open add_inductive_i (SIP)} does not +allow mixfix syntax to be associated with parameters, since it can only be used +for parsing. The names of the predicates, parameters and rules are represented by the +type @{ML_type Name.binding}. Strings can be turned into elements of the type +@{ML_type Name.binding} using the function +@{ML [display] "Name.binding : string -> Name.binding"} +Each introduction rule is given as a tuple containing its name, a list of \emph{attributes} +and a logical formula. Note that the type @{ML_type Attrib.binding} used in the list of +introduction rules is just a shorthand for the type @{ML_type "Name.binding * Attrib.src list"}. +The function @{ML_open add_inductive_i (SIP)} expects the formula to be specified using the datatype +@{ML_type term}, whereas @{ML_open add_inductive (SIP)} expects it to be given as a string. +An attribute specifies additional actions and transformations that should be applied to +a theorem, such as storing it in the rule databases used by automatic tactics +like the simplifier. The code of the package, which will be described in the following +section, will mostly treat attributes as a black box and just forward them to other +functions for storing theorems in local theories. +The implementation of the function @{ML_open add_inductive (SIP)} for external invocation +of the package is quite simple. Essentially, it just parses the introduction rules +and then passes them on to @{ML_open add_inductive_i (SIP)}: +@{ML_chunk [display] add_inductive} +For parsing and type checking the introduction rules, we use the function +@{ML_open [display] "Specification.read_specification: + (Name.binding * string option * mixfix) list -> (*{variables}*) + (Attrib.binding * string list) list list -> (*{rules}*) + local_theory -> + (((Name.binding * typ) * mixfix) list * + (Attrib.binding * term list) list) * + local_theory"} +During parsing, both predicates and parameters are treated as variables, so +the lists \verb!preds_syn! and \verb!params_syn! are just appended +before being passed to @{ML_open read_specification (Specification)}. Note that the format +for rules supported by @{ML_open read_specification (Specification)} is more general than +what is required for our package. It allows several rules to be associated +with one name, and the list of rules can be partitioned into several +sublists. In order for the list \verb!intro_srcs! of introduction rules +to be acceptable as an input for @{ML_open read_specification (Specification)}, we first +have to turn it into a list of singleton lists. This transformation +has to be reversed later on by applying the function +@{ML [display] "the_single: 'a list -> 'a"} +to the list \verb!specs! containing the parsed introduction rules. +The function @{ML_open read_specification (Specification)} also returns the list \verb!vars! +of predicates and parameters that contains the inferred types as well. +This list has to be chopped into the two lists \verb!preds_syn'! and +\verb!params_syn'! for predicates and parameters, respectively. +All variables occurring in a rule but not in the list of variables passed to +@{ML_open read_specification (Specification)} will be bound by a meta-level universal +quantifier. +Finally, @{ML_open read_specification (Specification)} also returns another local theory, +but we can safely discard it. As an example, let us look at how we can use this +function to parse the introduction rules of the @{text trcl} predicate: +@{ML_response [display] +"Specification.read_specification + [(Name.binding \"trcl\", NONE, NoSyn), + (Name.binding \"r\", SOME \"'a \ 'a \ bool\", NoSyn)] + [[((Name.binding \"base\", []), [\"trcl r x x\"])], + [((Name.binding \"step\", []), [\"trcl r x y \ r y z \ trcl r x z\"])]] + @{context}" +"((\, + [(\, + [Const (\"all\", \) $ Abs (\"x\", TFree (\"'a\", \), + Const (\"Trueprop\", \) $ + (Free (\"trcl\", \) $ Free (\"r\", \) $ Bound 0 $ Bound 0))]), + (\, + [Const (\"all\", \) $ Abs (\"x\", TFree (\"'a\", \), + Const (\"all\", \) $ Abs (\"y\", TFree (\"'a\", \), + Const (\"all\", \) $ Abs (\"z\", TFree (\"'a\", \), + Const (\"==>\", \) $ + (Const (\"Trueprop\", \) $ + (Free (\"trcl\", \) $ Free (\"r\", \) $ Bound 2 $ Bound 1)) $ + (Const (\"==>\", \) $ \ $ \))))])]), + \) +: (((Name.binding * typ) * mixfix) list * + (Attrib.binding * term list) list) * local_theory"} +In the list of variables passed to @{ML_open read_specification (Specification)}, we have +used the mixfix annotation @{ML NoSyn} to indicate that we do not want to associate any +mixfix syntax with the variable. Moreover, we have only specified the type of \texttt{r}, +whereas the type of \texttt{trcl} is computed using type inference. +The local variables \texttt{x}, \texttt{y} and \texttt{z} of the introduction rules +are turned into bound variables with the de Bruijn indices, +whereas \texttt{trcl} and \texttt{r} remain free variables. + +\paragraph{Parsers for theory syntax} + +Although the function @{ML_open add_inductive (SIP)} parses terms and types, it still +cannot be used to invoke the package directly from within a theory document. +In order to do this, we have to write another parser. Before we describe +the process of writing parsers for theory syntax in more detail, we first +show some examples of how we would like to use the inductive definition +package. + +\noindent +The definition of the transitive closure should look as follows: +*} + +simple_inductive + trcl for r :: "'a \ 'a \ bool" +where + base: "trcl r x x" +| step: "trcl r x y \ r y z \ trcl r x z" +(*<*) +thm trcl_def +thm trcl.induct +thm base +thm step +thm trcl.intros + +lemma trcl_strong_induct: + assumes trcl: "trcl r x y" + and I1: "\x. P x x" + and I2: "\x y z. P x y \ trcl r x y \ r y z \ P x z" + shows "P x y" +proof - + from trcl + have "P x y \ trcl r x y" + proof induct + case (base x) + from I1 and trcl.base show ?case .. + next + case (step x y z) + then have "P x y" and "trcl r x y" by simp_all + from `P x y` `trcl r x y` `r y z` have "P x z" + by (rule I2) + moreover from `trcl r x y` `r y z` have "trcl r x z" + by (rule trcl.step) + ultimately show ?case .. + qed + then show ?thesis .. +qed +(*>*) + +text {* +\noindent +Even and odd numbers can be defined by +*} + +simple_inductive + even and odd +where + even0: "even 0" +| evenS: "odd n \ even (Suc n)" +| oddS: "even n \ odd (Suc n)" +(*<*) +thm even_def odd_def +thm even.induct odd.induct +thm even0 +thm evenS +thm oddS +thm even_odd.intros +(*>*) + +text {* +\noindent +The accessible part of a relation can be introduced as follows: +*} + +simple_inductive + accpart for r :: "'a \ 'a \ bool" +where + accpartI: "(\y. r y x \ accpart r y) \ accpart r x" +(*<*) +thm accpart_def +thm accpart.induct +thm accpartI +(*>*) + +text {* +\noindent +Moreover, it should also be possible to define the accessible part +inside a locale fixing the relation @{text r}: +*} + +locale rel = + fixes r :: "'a \ 'a \ bool" + +simple_inductive (in rel) accpart' +where + accpartI': "\x. (\y. r y x \ accpart' y) \ accpart' x" +(*<*) +context rel +begin + +thm accpartI' +thm accpart'.induct + +end + +thm rel.accpartI' +thm rel.accpart'.induct + +ML {* +val (result, lthy) = SimpleInductivePackage.add_inductive + [(Name.binding "trcl'", NONE, NoSyn)] [(Name.binding "r", SOME "'a \ 'a \ bool", NoSyn)] + [((Name.binding "base", []), "\x. trcl' r x x"), ((Name.binding "step", []), "\x y z. trcl' r x y \ r y z \ trcl' r x z")] + (TheoryTarget.init NONE @{theory}) +*} +(*>*) + +text {* +\noindent +In this context, it is important to note that Isabelle distinguishes +between \emph{outer} and \emph{inner} syntax. Theory commands such as +\isa{\isacommand{simple{\isacharunderscore}inductive} $\ldots$ \isacommand{for} $\ldots$ \isacommand{where} $\ldots$} +belong to the outer syntax, whereas items in quotation marks, in particular +terms such as @{text [source] "trcl r x x"} and types such as +@{text [source] "'a \ 'a \ bool"} belong to the inner syntax. +Separating the two layers of outer and inner syntax greatly simplifies +matters, because the parser for terms and types does not have to know +anything about the possible syntax of theory commands, and the parser +for theory commands need not be concerned about the syntactic structure +of terms and types. + +\medskip +\noindent +The syntax of the \isa{\isacommand{simple{\isacharunderscore}inductive}} command +can be described by the following railroad diagram: +\begin{rail} + 'simple\_inductive' target? fixes ('for' fixes)? \\ + ('where' (thmdecl? prop + '|'))? + ; +\end{rail} + +\paragraph{Functional parsers} + +For parsing terms and types, Isabelle uses a rather general and sophisticated +algorithm due to Earley, which is driven by \emph{priority grammars}. +In contrast, parsers for theory syntax are built up using a set of combinators. +Functional parsing using combinators is a well-established technique, which +has been described by many authors, including Paulson \cite{paulson-ML-91} +and Wadler \cite{Wadler-AFP95}. +The central idea is that a parser is a function of type @{ML_type "'a list -> 'b * 'a list"}, +where @{ML_type "'a"} is a type of \emph{tokens}, and @{ML_type "'b"} is a type for +encoding items that the parser has recognized. When a parser is applied to a +list of tokens whose prefix it can recognize, it returns an encoding of the +prefix as an element of type @{ML_type "'b"}, together with the suffix of the list +containing the remaining tokens. Otherwise, the parser raises an exception +indicating a syntax error. The library for writing functional parsers in +Isabelle can roughly be split up into two parts. The first part consists of a +collection of generic parser combinators that are contained in the structure +@{ML_struct Scan} defined in the file @{ML_file "Pure/General/scan.ML"} in the Isabelle +sources. While these combinators do not make any assumptions about the concrete +structure of the tokens used, the second part of the library consists of combinators +for dealing with specific token types. +The following is an excerpt from the signature of @{ML_struct Scan}: +\begin{mytable} +@{ML "|| : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b"} \\ +@{ML "-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e"} \\ +@{ML "|-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e"} \\ +@{ML "--| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e"} \\ +@{ML_open "optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a" (Scan)} \\ +@{ML_open "repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" (Scan)} \\ +@{ML_open "repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" (Scan)} \\ +@{ML ">> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c"} \\ +@{ML "!! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b"} +\end{mytable} +Interestingly, the functions shown above are so generic that they do not +even rely on the input and output of the parser being a list of tokens. +If \texttt{p} succeeds, i.e.\ does not raise an exception, the parser +@{ML_open "p || q" for p q} returns the result of \texttt{p}, otherwise it returns +the result of \texttt{q}. The parser @{ML_open "p -- q" for p q} first parses an +item of type @{ML_type "'b"} using \texttt{p}, then passes the remaining tokens +of type @{ML_type "'c"} to \texttt{q}, which parses an item of type @{ML_type "'d"} +and returns the remaining tokens of type @{ML_type "'e"}, which are finally +returned together with a pair of type @{ML_type "'b * 'd"} containing the two +parsed items. The parsers @{ML_open "p |-- q" for p q} and @{ML_open "p --| q" for p q} +work in a similar way as the previous one, with the difference that they +discard the item parsed by the first and the second parser, respectively. +If \texttt{p} succeeds, the parser @{ML_open "optional p x" for p x (Scan)} returns the result +of \texttt{p}, otherwise it returns the default value \texttt{x}. The parser +@{ML_open "repeat p" for p (Scan)} applies \texttt{p} as often as it can, returning a possibly +empty list of parsed items. The parser @{ML_open "repeat1 p" for p (Scan)} is similar, +but requires \texttt{p} to succeed at least once. The parser +@{ML_open "p >> f" for p f} uses \texttt{p} to parse an item of type @{ML_type "'b"}, to which +it applies the function \texttt{f} yielding a value of type @{ML_type "'d"}, which +is returned together with the remaining tokens of type @{ML_type "'c"}. +Finally, @{ML "!!"} is used for transforming exceptions produced by parsers. +If \texttt{p} raises an exception indicating that it cannot parse a given input, +then an enclosing parser such as +@{ML_open [display] "q -- p || r" for p q r} +will try the alternative parser \texttt{r}. By writing +@{ML_open [display] "q -- !! err p || r" for err p q r} +instead, one can achieve that a failure of \texttt{p} causes the whole parser to abort. +The @{ML "!!"} operator is similar to the \emph{cut} operator in Prolog, which prevents +the interpreter from backtracking. The \texttt{err} function supplied as an argument +to @{ML "!!"} can be used to produce an error message depending on the current +state of the parser, as well as the optional error message returned by \texttt{p}. + +So far, we have only looked at combinators that construct more complex parsers +from simpler parsers. In order for these combinators to be useful, we also need +some basic parsers. As an example, we consider the following two parsers +defined in @{ML_struct Scan}: +\begin{mytable} +@{ML_open "one: ('a -> bool) -> 'a list -> 'a * 'a list" (Scan)} \\ +@{ML_open "$$ : string -> string list -> string * string list"} +\end{mytable} +The parser @{ML_open "one pred" for pred (Scan)} parses exactly one token that +satisfies the predicate \texttt{pred}, whereas @{ML_open "$$ s" for s} only +accepts a token that equals the string \texttt{s}. Note that we can easily +express @{ML_open "$$ s" for s} using @{ML_open "one" (Scan)}: +@{ML_open [display] "one (fn s' => s' = s)" for s (Scan)} +As an example, let us look at how we can use @{ML "$$"} and @{ML "--"} to parse +the prefix ``\texttt{hello}'' of the character list ``\texttt{hello world}'': +@{ML_response [display] +"($$ \"h\" -- $$ \"e\" -- $$ \"l\" -- $$ \"l\" -- $$ \"o\") +[\"h\", \"e\", \"l\", \"l\", \"o\", \" \", \"w\", \"o\", \"r\", \"l\", \"d\"]" +"(((((\"h\", \"e\"), \"l\"), \"l\"), \"o\"), [\" \", \"w\", \"o\", \"r\", \"l\", \"d\"]) +: ((((string * string) * string) * string) * string) * string list"} +Most of the time, however, we will have to deal with tokens that are not just strings. +The parsers for the theory syntax, as well as the parsers for the argument syntax +of proof methods and attributes use the token type @{ML_type OuterParse.token}, +which is identical to the type @{ML_type OuterLex.token}. +The parser functions for the theory syntax are contained in the structure +@{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/outer_parse.ML"}. +In our parser, we will use the following functions: +\begin{mytable} +@{ML_open "$$$ : string -> token list -> string * token list" (OuterParse)} \\ +@{ML_open "enum1: string -> (token list -> 'a * token list) -> token list -> + 'a list * token list" (OuterParse)} \\ +@{ML_open "prop: token list -> string * token list" (OuterParse)} \\ +@{ML_open "opt_target: token list -> string option * token list" (OuterParse)} \\ +@{ML_open "fixes: token list -> + (Name.binding * string option * mixfix) list * token list" (OuterParse)} \\ +@{ML_open "for_fixes: token list -> + (Name.binding * string option * mixfix) list * token list" (OuterParse)} \\ +@{ML_open "!!! : (token list -> 'a) -> token list -> 'a" (OuterParse)} +\end{mytable} +The parsers @{ML_open "$$$" (OuterParse)} and @{ML_open "!!!" (OuterParse)} are +defined using the parsers @{ML_open "one" (Scan)} and @{ML "!!"} from +@{ML_struct Scan}. +The parser @{ML_open "enum1 s p" for s p (OuterParse)} parses a non-emtpy list of items +recognized by the parser \texttt{p}, where the items are separated by \texttt{s}. +A proposition can be parsed using the function @{ML_open prop (OuterParse)}. +Essentially, a proposition is just a string or an identifier, but using the +specific parser function @{ML_open prop (OuterParse)} leads to more instructive +error messages, since the parser will complain that a proposition was expected +when something else than a string or identifier is found. +An optional locale target specification of the form \isa{(\isacommand{in}\ $\ldots$)} +can be parsed using @{ML_open opt_target (OuterParse)}. +The lists of names of the predicates and parameters, together with optional +types and syntax, are parsed using the functions @{ML_open "fixes" (OuterParse)} +and @{ML_open for_fixes (OuterParse)}, respectively. +In addition, the following function from @{ML_struct SpecParse} for parsing +an optional theorem name and attribute, followed by a delimiter, will be useful: +\begin{mytable} +@{ML_open "opt_thm_name: + string -> token list -> Attrib.binding * token list" (SpecParse)} +\end{mytable} +We now have all the necessary tools to write the parser for our +\isa{\isacommand{simple{\isacharunderscore}inductive}} command: +@{ML_chunk [display] syntax} +The definition of the parser \verb!ind_decl! closely follows the railroad +diagram shown above. In order to make the code more readable, the structures +@{ML_struct OuterParse} and @{ML_struct OuterKeyword} are abbreviated by +\texttt{P} and \texttt{K}, respectively. Note how the parser combinator +@{ML_open "!!!" (OuterParse)} is used: once the keyword \texttt{where} +has been parsed, a non-empty list of introduction rules must follow. +Had we not used the combinator @{ML_open "!!!" (OuterParse)}, a +\texttt{where} not followed by a list of rules would have caused the parser +to respond with the somewhat misleading error message +\begin{verbatim} + Outer syntax error: end of input expected, but keyword where was found +\end{verbatim} +rather than with the more instructive message +\begin{verbatim} + Outer syntax error: proposition expected, but terminator was found +\end{verbatim} +Once all arguments of the command have been parsed, we apply the function +@{ML_open add_inductive (SimpleInductivePackage)}, which yields a local theory +transformer of type @{ML_type "local_theory -> local_theory"}. Commands in +Isabelle/Isar are realized by transition transformers of type +@{ML_type [display] "Toplevel.transition -> Toplevel.transition"} +We can turn a local theory transformer into a transition transformer by using +the function +@{ML [display] "Toplevel.local_theory : string option -> + (local_theory -> local_theory) -> + Toplevel.transition -> Toplevel.transition"} +which, apart from the local theory transformer, takes an optional name of a locale +to be used as a basis for the local theory. The whole parser for our command has type +@{ML_type [display] "OuterLex.token list -> + (Toplevel.transition -> Toplevel.transition) * OuterLex.token list"} +which is abbreviated by @{ML_type OuterSyntax.parser_fn}. The new command can be added +to the system via the function +@{ML [display] "OuterSyntax.command : + string -> string -> OuterKeyword.T -> OuterSyntax.parser_fn -> unit"} +which imperatively updates the parser table behind the scenes. In addition to the parser, this +function takes two strings representing the name of the command and a short description, +as well as an element of type @{ML_type OuterKeyword.T} describing which \emph{kind} of +command we intend to add. Since we want to add a command for declaring new concepts, +we choose the kind @{ML "OuterKeyword.thy_decl"}. Other kinds include +@{ML "OuterKeyword.thy_goal"}, which is similar to @{ML_open thy_decl (OuterKeyword)}, +but requires the user to prove a goal before making the declaration, or +@{ML "OuterKeyword.diag"}, which corresponds to a purely diagnostic command that does +not change the context. For example, the @{ML_open thy_goal (OuterKeyword)} kind is used +by the \isa{\isacommand{function}} command \cite{Krauss-IJCAR06}, which requires the user +to prove that a given set of equations is non-overlapping and covers all cases. The kind +of the command should be chosen with care, since selecting the wrong one can cause strange +behaviour of the user interface, such as failure of the undo mechanism. +*} + +(*<*) +end +(*>*) diff -r 53460ac408b5 -r 5bb2d29553c2 CookBook/Package/Ind_Intro.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/CookBook/Package/Ind_Intro.thy Fri Oct 10 17:13:21 2008 +0200 @@ -0,0 +1,104 @@ +theory Ind_Intro +imports Main +begin + +chapter {* How to write a definitional package *} + +section{* Introduction *} + +text {* +\begin{flushright} + {\em + ``My thesis is that programming is not at the bottom of the intellectual \\ + pyramid, but at the top. It's creative design of the highest order. It \\ + isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\ + claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex] + Richard Bornat, In defence of programming +\end{flushright} + +\medskip + +\noindent +Higher order logic, as implemented in Isabelle/HOL, is based on just a few primitive +constants, like equality, implication, and the description operator, whose properties are +described as axioms. All other concepts, such as inductive predicates, datatypes, or +recursive functions are \emph{defined} using these constants, and the desired +properties, for example induction theorems, or recursion equations are \emph{derived} +from the definitions by a \emph{formal proof}. Since it would be very tedious +for the average user to define complex inductive predicates or datatypes ``by hand'' +just using the primitive operators of higher order logic, Isabelle/HOL already contains +a number of \emph{packages} automating such tedious work. Thanks to those packages, +the user can give a high-level specification, like a list of introduction rules or +constructors, and the package then does all the low-level definitions and proofs +behind the scenes. The packages are written in Standard ML, the implementation +language of Isabelle, and can be invoked by the user from within theory documents +written in the Isabelle/Isar language via specific commands. Most of the time, +when using Isabelle for applications, users do not have to worry about the inner +workings of packages, since they can just use the packages that are already part +of the Isabelle distribution. However, when developing a general theory that is +intended to be applied by other users, one may need to write a new package from +scratch. Recent examples of such packages include the verification environment +for sequential imperative programs by Schirmer \cite{Schirmer-LPAR04}, the +package for defining general recursive functions by Krauss \cite{Krauss-IJCAR06}, +as well as the nominal datatype package by Berghofer and Urban \cite{Urban-Berghofer06}. + +The scientific value of implementing a package should not be underestimated: +it is often more than just the automation of long-established scientific +results. Of course, a carefully-developed theory on paper is indispensable +as a basis. However, without an implementation, such a theory will only be of +very limited practical use, since only an implementation enables other users +to apply the theory on a larger scale without too much effort. Moreover, +implementing a package is a bit like formalizing a paper proof in a theorem +prover. In the literature, there are many examples of paper proofs that +turned out to be incomplete or even faulty, and doing a formalization is +a good way of uncovering such errors and ensuring that a proof is really +correct. The same applies to the theory underlying definitional packages. +For example, the general form of some complicated induction rules for nominal +datatypes turned out to be quite hard to get right on the first try, so +an implementation is an excellent way to find out whether the rules really +work in practice. + +Writing a package is a particularly difficult task for users that are new +to Isabelle, since its programming interface consists of thousands of functions. +Rather than just listing all those functions, we give a step-by-step tutorial +for writing a package, using an example that is still simple enough to be +easily understandable, but at the same time sufficiently complex to demonstrate +enough of Isabelle's interesting features. As a running example, we have +chosen a rather simple package for defining inductive predicates. To keep +things simple, we will not use the general Knaster-Tarski fixpoint +theorem on complete lattices, which forms the basis of Isabelle's standard +inductive definition package originally due to Paulson \cite{Paulson-ind-defs}. +Instead, we will use a simpler \emph{impredicative} (i.e.\ involving +quantification on predicate variables) encoding of inductive predicates +suggested by Melham \cite{Melham:1992:PIR}. Due to its simplicity, this +package will necessarily have a reduced functionality. It does neither +support introduction rules involving arbitrary monotone operators, nor does +it prove case analysis (or inversion) rules. Moreover, it only proves a weaker +form of the rule induction theorem. + +Reading this article does not require any prior knowledge of Isabelle's programming +interface. However, we assume the reader to already be familiar with writing +proofs in Isabelle/HOL using the Isar language. For further information on +this topic, consult the book by Nipkow, Paulson, and Wenzel +\cite{isa-tutorial}. Moreover, in order to understand the pieces of +code given in this tutorial, some familiarity with the basic concepts of the Standard +ML programming language, as described for example in the textbook by Paulson +\cite{paulson-ml2}, is required as well. + +The rest of this article is structured as follows. In \S\ref{sec:ind-examples}, +we will illustrate the ``manual'' definition of inductive predicates using +some examples. Starting from these examples, we will describe in +\S\ref{sec:ind-general-method} how the construction works in general. +The following sections are then dedicated to the implementation of a +package that carries out the construction of such inductive predicates. +First of all, a parser for a high-level notation for specifying inductive +predicates via a list of introduction rules is developed in \S\ref{sec:ind-interface}. +Having parsed the specification, a suitable primitive definition must be +added to the theory, which will be explained in \S\ref{sec:ind-definition}. +Finally, \S\ref{sec:ind-proofs} will focus on methods for proving introduction +and induction rules from the definitions introduced in \S\ref{sec:ind-definition}. + +\nocite{Bornat-lecture} +*} + +end diff -r 53460ac408b5 -r 5bb2d29553c2 CookBook/Package/Simple_Inductive_Package.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/CookBook/Package/Simple_Inductive_Package.thy Fri Oct 10 17:13:21 2008 +0200 @@ -0,0 +1,8 @@ +theory Simple_Inductive_Package +imports Main +uses ("simple_inductive_package.ML") +begin + +use_chunks "simple_inductive_package.ML" + +end diff -r 53460ac408b5 -r 5bb2d29553c2 CookBook/Package/simple_inductive_package.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/CookBook/Package/simple_inductive_package.ML Fri Oct 10 17:13:21 2008 +0200 @@ -0,0 +1,170 @@ +(* @chunk SIMPLE_INDUCTIVE_PACKAGE *) +signature SIMPLE_INDUCTIVE_PACKAGE = +sig + val add_inductive_i: + ((Name.binding * typ) * mixfix) list -> (*{predicates}*) + (Name.binding * typ) list -> (*{parameters}*) + (Attrib.binding * term) list -> (*{rules}*) + local_theory -> (thm list * thm list) * local_theory + val add_inductive: + (Name.binding * string option * mixfix) list -> (*{predicates}*) + (Name.binding * string option * mixfix) list -> (*{parameters}*) + (Attrib.binding * string) list -> (*{rules}*) + local_theory -> (thm list * thm list) * local_theory +end; +(* @end *) + +structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE = +struct + +fun add_inductive_i preds_syn params intrs lthy = + let + val params' = map (fn (p, T) => Free (Name.name_of p, T)) params; + val preds = map (fn ((R, T), _) => + list_comb (Free (Name.name_of R, T), params')) preds_syn; + val Tss = map (binder_types o fastype_of) preds; + + (* making the definition *) + + val intrs' = map + (ObjectLogic.atomize_term (ProofContext.theory_of lthy) o snd) intrs; + + fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P; + + val (defs, lthy1) = fold_map (fn ((((R, _), syn), pred), Ts) => + let val zs = map Free (Variable.variant_frees lthy intrs' + (map (pair "z") Ts)) + in + LocalTheory.define Thm.internalK + ((R, syn), (Attrib.no_binding, fold_rev lambda (params' @ zs) + (fold_rev mk_all preds (fold_rev (curry HOLogic.mk_imp) + intrs' (list_comb (pred, zs)))))) #>> snd #>> snd + end) (preds_syn ~~ preds ~~ Tss) lthy; + + val (_, lthy2) = Variable.add_fixes (map (Name.name_of o fst) params) lthy1; + + + (* proving the induction rules *) + + val (Pnames, lthy3) = + Variable.variant_fixes (replicate (length preds) "P") lthy2; + val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT)) + (Pnames ~~ Tss); + val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps; + val intrs'' = map (subst_free (preds ~~ Ps) o snd) intrs; + + fun inst_spec ct = Drule.instantiate' + [SOME (ctyp_of_term ct)] [NONE, SOME ct] spec; + + fun prove_indrule ((R, P), Ts) = + let + val (znames, lthy4) = + Variable.variant_fixes (replicate (length Ts) "z") lthy3; + val zs = map Free (znames ~~ Ts) + in + Goal.prove lthy4 [] + [HOLogic.mk_Trueprop (list_comb (R, zs))] + (Logic.list_implies (intrs'', + HOLogic.mk_Trueprop (list_comb (P, zs)))) + (fn {prems, ...} => EVERY + ([ObjectLogic.full_atomize_tac 1, + cut_facts_tac prems 1, + rewrite_goals_tac defs] @ + map (fn ct => dtac (inst_spec ct) 1) cPs @ + [assume_tac 1])) |> + singleton (ProofContext.export lthy4 lthy1) + end; + + val indrules = map prove_indrule (preds ~~ Ps ~~ Tss); + + + (* proving the introduction rules *) + + val all_elims = fold (fn ct => fn th => th RS inst_spec ct); + val imp_elims = fold (fn th => fn th' => [th', th] MRS mp); + + fun prove_intr (i, (_, r)) = + Goal.prove lthy2 [] [] r + (fn {prems, context = ctxt} => EVERY + [ObjectLogic.rulify_tac 1, + rewrite_goals_tac defs, + REPEAT (resolve_tac [allI, impI] 1), + SUBPROOF (fn {params, prems, context = ctxt', ...} => + let + val (prems1, prems2) = + chop (length prems - length intrs) prems; + val (params1, params2) = + chop (length params - length preds) params + in + rtac (ObjectLogic.rulify + (all_elims params1 (nth prems2 i))) 1 THEN + EVERY (map (fn prem => + SUBPROOF (fn {prems = prems', concl, ...} => + let + val prem' = prems' MRS prem; + val prem'' = case prop_of prem' of + _ $ (Const (@{const_name All}, _) $ _) => + prem' |> all_elims params2 |> + imp_elims prems2 + | _ => prem' + in rtac prem'' 1 end) ctxt' 1) prems1) + end) ctxt 1]) |> + singleton (ProofContext.export lthy2 lthy1); + + val intr_ths = map_index prove_intr intrs; + + + (* storing the theorems *) + + val mut_name = space_implode "_" (map (Name.name_of o fst o fst) preds_syn); + val case_names = map (Name.name_of o fst o fst) intrs + in + lthy1 |> + LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => + ((Name.qualified mut_name a, atts), [([th], [])])) + (intrs ~~ intr_ths)) |-> + (fn intr_thss => LocalTheory.note Thm.theoremK + ((Name.qualified mut_name (Name.binding "intros"), []), maps snd intr_thss)) |>> + snd ||>> + (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) => + ((Name.qualified (Name.name_of R) (Name.binding "induct"), + [Attrib.internal (K (RuleCases.case_names case_names)), + Attrib.internal (K (RuleCases.consumes 1)), + Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) + (preds_syn ~~ indrules)) #>> maps snd) + end; + +(* @chunk add_inductive *) +fun add_inductive preds_syn params_syn intro_srcs lthy = + let + val ((vars, specs), _) = Specification.read_specification + (preds_syn @ params_syn) (map (fn (a, s) => [(a, [s])]) intro_srcs) + lthy; + val (preds_syn', params_syn') = chop (length preds_syn) vars; + val intrs = map (apsnd the_single) specs + in + add_inductive_i preds_syn' (map fst params_syn') intrs lthy + end; +(* @end *) + + +(* outer syntax *) + +(* @chunk syntax *) +local structure P = OuterParse and K = OuterKeyword in + +val ind_decl = + P.opt_target -- + P.fixes -- P.for_fixes -- + Scan.optional (P.$$$ "where" |-- + P.!!! (P.enum1 "|" (SpecParse.opt_thm_name ":" -- P.prop))) [] >> + (fn (((loc, preds), params), specs) => + Toplevel.local_theory loc (add_inductive preds params specs #> snd)); + +val _ = OuterSyntax.command "simple_inductive" "define inductive predicates" + K.thy_decl ind_decl; + +end; +(* @end *) + +end;