theory Ind_Interfaceimports Ind_Intro Simple_Inductive_Packagebeginsection {* 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 oddwhere 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 inputend""(([(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 : (local_theory -> local_theory) parser = 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 lthyin add_inductive pred_specs' rule_specs' lthyend*}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(*>*)