1 theory Ind_Interface |
1 theory Ind_Interface |
2 imports Ind_Intro Simple_Inductive_Package |
2 imports Ind_Intro Simple_Inductive_Package |
3 keywords "simple_inductive2" :: thy_decl |
3 keywords "simple_inductive2" :: thy_decl |
4 begin |
4 begin |
5 |
5 |
6 section {* Parsing and Typing the Specification\label{sec:interface} *} |
6 section \<open>Parsing and Typing the Specification\label{sec:interface}\<close> |
7 |
7 |
8 text_raw {* |
8 text_raw \<open> |
9 \begin{figure}[t] |
9 \begin{figure}[t] |
10 \begin{boxedminipage}{\textwidth} |
10 \begin{boxedminipage}{\textwidth} |
11 \begin{isabelle} |
11 \begin{isabelle} |
12 *} |
12 \<close> |
13 simple_inductive |
13 simple_inductive |
14 trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
14 trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
15 where |
15 where |
16 base: "trcl R x x" |
16 base: "trcl R x x" |
17 | step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z" |
17 | step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z" |
40 where |
40 where |
41 fresh_var: "a\<noteq>b \<Longrightarrow> fresh a (Var b)" |
41 fresh_var: "a\<noteq>b \<Longrightarrow> fresh a (Var b)" |
42 | fresh_app: "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)" |
42 | fresh_app: "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)" |
43 | fresh_lam1: "fresh a (Lam a t)" |
43 | fresh_lam1: "fresh a (Lam a t)" |
44 | fresh_lam2: "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)" |
44 | fresh_lam2: "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)" |
45 text_raw {* |
45 text_raw \<open> |
46 \end{isabelle} |
46 \end{isabelle} |
47 \end{boxedminipage} |
47 \end{boxedminipage} |
48 \caption{Specification given by the user for the inductive predicates |
48 \caption{Specification given by the user for the inductive predicates |
49 @{term "trcl"}, @{term "even"} and @{term "odd"}, @{term "accpart"} and |
49 @{term "trcl"}, @{term "even"} and @{term "odd"}, @{term "accpart"} and |
50 @{term "fresh"}.\label{fig:specs}} |
50 @{term "fresh"}.\label{fig:specs}} |
51 \end{figure} |
51 \end{figure} |
52 *} |
52 \<close> |
53 |
53 |
54 text {* |
54 text \<open> |
55 To be able to write down the specifications of inductive predicates, we have |
55 To be able to write down the specifications of inductive predicates, we have |
56 to introduce a new command (see Section~\ref{sec:newcommand}). As the |
56 to introduce a new command (see Section~\ref{sec:newcommand}). As the |
57 keyword for the new command we chose \simpleinductive{}. Examples of |
57 keyword for the new command we chose \simpleinductive{}. Examples of |
58 specifications from the previous section are shown in |
58 specifications from the previous section are shown in |
59 Figure~\ref{fig:specs}. The syntax used in these examples more or |
59 Figure~\ref{fig:specs}. The syntax used in these examples more or |
60 less translates directly into the parser: |
60 less translates directly into the parser: |
61 |
61 |
62 *} |
62 \<close> |
63 |
63 |
64 ML %grayML{*val spec_parser = |
64 ML %grayML\<open>val spec_parser = |
65 Parse.vars -- |
65 Parse.vars -- |
66 Scan.optional |
66 Scan.optional |
67 (Parse.$$$ "where" |-- |
67 (Parse.$$$ "where" |-- |
68 Parse.!!! |
68 Parse.!!! |
69 (Parse.enum1 "|" |
69 (Parse.enum1 "|" |
70 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) []*} |
70 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) []\<close> |
71 |
71 |
72 text {* |
72 text \<open> |
73 which we explained in Section~\ref{sec:parsingspecs}. There is no code included |
73 which we explained in Section~\ref{sec:parsingspecs}. There is no code included |
74 for parsing the keyword and what is called a \emph{target}. The latter can be given |
74 for parsing the keyword and what is called a \emph{target}. The latter can be given |
75 optionally after the keyword. The target is an ``advanced'' feature which we will |
75 optionally after the keyword. The target is an ``advanced'' feature which we will |
76 inherit for ``free'' from the infrastructure on which we shall build the package. |
76 inherit for ``free'' from the infrastructure on which we shall build the package. |
77 The target stands for a locale and allows us to specify |
77 The target stands for a locale and allows us to specify |
78 *} |
78 \<close> |
79 |
79 |
80 locale rel = |
80 locale rel = |
81 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
81 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
82 |
82 |
83 text {* |
83 text \<open> |
84 and then define the transitive closure and the accessible part of this |
84 and then define the transitive closure and the accessible part of this |
85 locale as follows: |
85 locale as follows: |
86 *} |
86 \<close> |
87 |
87 |
88 simple_inductive (in rel) |
88 simple_inductive (in rel) |
89 trcl' |
89 trcl' |
90 where |
90 where |
91 base: "trcl' x x" |
91 base: "trcl' x x" |
93 |
93 |
94 simple_inductive (in rel) |
94 simple_inductive (in rel) |
95 accpart' |
95 accpart' |
96 where |
96 where |
97 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x" |
97 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x" |
98 (*<*)ML %no{*fun filtered_input str = |
98 (*<*)ML %no\<open>fun filtered_input str = |
99 filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str) |
99 filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str) |
100 fun parse p input = Scan.finite Token.stopper (Scan.error p) input*}(*>*) |
100 fun parse p input = Scan.finite Token.stopper (Scan.error p) input\<close>(*>*) |
101 text {* |
101 text \<open> |
102 Note that in these definitions the parameter @{text R}, standing for the |
102 Note that in these definitions the parameter \<open>R\<close>, standing for the |
103 relation, is left implicit. For the moment we will ignore this kind |
103 relation, is left implicit. For the moment we will ignore this kind |
104 of implicit parameters and rely on the fact that the infrastructure will |
104 of implicit parameters and rely on the fact that the infrastructure will |
105 deal with them. Later, however, we will come back to them. |
105 deal with them. Later, however, we will come back to them. |
106 |
106 |
107 If we feed into the parser the string that corresponds to our definition |
107 If we feed into the parser the string that corresponds to our definition |
125 |
125 |
126 then we get back the specifications of the predicates (with type and syntax annotations), |
126 then we get back the specifications of the predicates (with type and syntax annotations), |
127 and specifications of the introduction rules. This is all the information we |
127 and specifications of the introduction rules. This is all the information we |
128 need for calling the package and setting up the keyword. The latter is |
128 need for calling the package and setting up the keyword. The latter is |
129 done in Lines 5 to 7 in the code below. |
129 done in Lines 5 to 7 in the code below. |
130 *} |
130 \<close> |
131 (*<*)ML %no{*fun add_inductive_cmd pred_specs rule_specs lthy = lthy |
131 (*<*)ML %no\<open>fun add_inductive_cmd pred_specs rule_specs lthy = lthy |
132 fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*) (* FIXME: Is the dummy simple_inductive2 installed with ML, before there was ML_val*) |
132 fun add_inductive pred_specs rule_specs lthy = lthy\<close>(*>*) (* FIXME: Is the dummy simple_inductive2 installed with ML, before there was ML_val*) |
133 ML %linenosgray{*val specification : (local_theory -> local_theory) parser = |
133 ML %linenosgray\<open>val specification : (local_theory -> local_theory) parser = |
134 spec_parser >> |
134 spec_parser >> |
135 (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs) |
135 (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs) |
136 |
136 |
137 val _ = Outer_Syntax.local_theory @{command_keyword "simple_inductive2"} |
137 val _ = Outer_Syntax.local_theory @{command_keyword "simple_inductive2"} |
138 "definition of simple inductive predicates" |
138 "definition of simple inductive predicates" |
139 specification*} |
139 specification\<close> |
140 |
140 |
141 text {* |
141 text \<open> |
142 We call @{ML_ind local_theory in Outer_Syntax} with the kind-indicator |
142 We call @{ML_ind local_theory in Outer_Syntax} with the kind-indicator |
143 @{ML_ind thy_decl in Keyword} since the package does not need to open |
143 @{ML_ind thy_decl in Keyword} since the package does not need to open |
144 up any proof (see Section~\ref{sec:newcommand}). |
144 up any proof (see Section~\ref{sec:newcommand}). |
145 The auxiliary function @{text specification} in Lines 1 to 3 |
145 The auxiliary function \<open>specification\<close> in Lines 1 to 3 |
146 gathers the information from the parser to be processed further |
146 gathers the information from the parser to be processed further |
147 by the function @{text "add_inductive_cmd"}, which we describe below. |
147 by the function \<open>add_inductive_cmd\<close>, which we describe below. |
148 |
148 |
149 Note that the predicates when they come out of the parser are just some |
149 Note that the predicates when they come out of the parser are just some |
150 ``naked'' strings: they have no type yet (even if we annotate them with |
150 ``naked'' strings: they have no type yet (even if we annotate them with |
151 types) and they are also not defined constants yet (which the predicates |
151 types) and they are also not defined constants yet (which the predicates |
152 eventually will be). Also the introduction rules are just strings. What we have |
152 eventually will be). Also the introduction rules are just strings. What we have |
156 (with possible typing annotations) and some rule specifications, and attempts |
156 (with possible typing annotations) and some rule specifications, and attempts |
157 to find a typing according to the given type constraints given by the |
157 to find a typing according to the given type constraints given by the |
158 user and the type constraints by the ``ambient'' theory. It returns |
158 user and the type constraints by the ``ambient'' theory. It returns |
159 the type for the predicates and also returns typed terms for the |
159 the type for the predicates and also returns typed terms for the |
160 introduction rules. So at the heart of the function |
160 introduction rules. So at the heart of the function |
161 @{text "add_inductive_cmd"} is a call to @{ML read_multi_specs in Specification}. |
161 \<open>add_inductive_cmd\<close> is a call to @{ML read_multi_specs in Specification}. |
162 *} |
162 \<close> |
163 |
163 |
164 ML_val%grayML{*fun add_inductive_cmd pred_specs rule_specs lthy = |
164 ML_val%grayML\<open>fun add_inductive_cmd pred_specs rule_specs lthy = |
165 let |
165 let |
166 val ((pred_specs', rule_specs'), _) = |
166 val ((pred_specs', rule_specs'), _) = |
167 Specification.read_multi_specs pred_specs rule_specs lthy |
167 Specification.read_multi_specs pred_specs rule_specs lthy |
168 in |
168 in |
169 add_inductive pred_specs' rule_specs' lthy |
169 add_inductive pred_specs' rule_specs' lthy |
170 end*} |
170 end\<close> |
171 |
171 |
172 text {* |
172 text \<open> |
173 Once we have the input data as some internal datastructure, we call |
173 Once we have the input data as some internal datastructure, we call |
174 the function @{text add_inductive}. This function does the heavy duty |
174 the function \<open>add_inductive\<close>. This function does the heavy duty |
175 lifting in the package: it generates definitions for the |
175 lifting in the package: it generates definitions for the |
176 predicates and derives from them corresponding induction principles and |
176 predicates and derives from them corresponding induction principles and |
177 introduction rules. The description of this function will span over |
177 introduction rules. The description of this function will span over |
178 the next two sections. |
178 the next two sections. |
179 *} |
179 \<close> |
180 (*<*)end(*>*) |
180 (*<*)end(*>*) |