118 |
118 |
119 simple_inductive (in rel) |
119 simple_inductive (in rel) |
120 accpart' |
120 accpart' |
121 where |
121 where |
122 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x" |
122 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x" |
123 |
123 (*<*)ML %no{*fun filtered_input str = |
|
124 filter OuterLex.is_proper (OuterSyntax.scan Position.none str) |
|
125 fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input*}(*>*) |
124 text {* |
126 text {* |
125 Note that in these definitions the parameter @{text R}, standing for the |
127 Note that in these definitions the parameter @{text R}, standing for the |
126 relation, is left implicit. For the moment we will ignore this kind |
128 relation, is left implicit. For the moment we will ignore this kind |
127 of implicit parameters and rely on the fact that the infrastructure will |
129 of implicit parameters and rely on the fact that the infrastructure will |
128 deal with them. Later, however, we will come back to them. |
130 deal with them. Later, however, we will come back to them. |
150 and specifications of the introduction rules. This is all the information we |
152 and specifications of the introduction rules. This is all the information we |
151 need for calling the package and setting up the keyword. The latter is |
153 need for calling the package and setting up the keyword. The latter is |
152 done in Lines 5 to 7 in the code below. |
154 done in Lines 5 to 7 in the code below. |
153 *} |
155 *} |
154 |
156 |
155 (*<*)ML %linenos{*fun add_inductive pred_specs rule_specs lthy = lthy |
157 (*<*) |
156 fun add_inductive_cmd pred_specs rule_specs lthy = |
158 ML %linenos |
157 let |
159 {* fun add_inductive_cmd pred_specs rule_specs lthy = lthy |
158 val ((pred_specs', rule_specs'), _) = |
160 fun add_inductive pred_specs rule_specs lthy = lthy *} |
159 Specification.read_spec pred_specs rule_specs lthy |
161 (*>*) |
160 in |
162 |
161 add_inductive pred_specs' rule_specs' lthy |
|
162 end*}(*>*) |
|
163 ML_val %linenosgray{*val specification = |
163 ML_val %linenosgray{*val specification = |
164 spec_parser >> |
164 spec_parser >> |
165 (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs) |
165 (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs) |
166 |
166 |
167 val _ = OuterSyntax.local_theory "simple_inductive" |
167 val _ = OuterSyntax.local_theory "simple_inductive2" |
168 "definition of simple inductive predicates" |
168 "definition of simple inductive predicates" |
169 OuterKeyword.thy_decl specification*} |
169 OuterKeyword.thy_decl specification*} |
170 |
170 |
171 text {* |
171 text {* |
172 We call @{ML local_theory in OuterSyntax} with the kind-indicator |
172 We call @{ML local_theory in OuterSyntax} with the kind-indicator |
189 the type for the predicates and also returns typed terms for the |
189 the type for the predicates and also returns typed terms for the |
190 introduction rules. So at the heart of the function |
190 introduction rules. So at the heart of the function |
191 @{text "add_inductive_cmd"} is a call to @{ML read_spec in Specification}. |
191 @{text "add_inductive_cmd"} is a call to @{ML read_spec in Specification}. |
192 *} |
192 *} |
193 |
193 |
194 ML{*fun add_inductive_cmd pred_specs rule_specs lthy = |
194 ML_val{*fun add_inductive_cmd pred_specs rule_specs lthy = |
195 let |
195 let |
196 val ((pred_specs', rule_specs'), _) = |
196 val ((pred_specs', rule_specs'), _) = |
197 Specification.read_spec pred_specs rule_specs lthy |
197 Specification.read_spec pred_specs rule_specs lthy |
198 in |
198 in |
199 add_inductive pred_specs' rule_specs' lthy |
199 add_inductive pred_specs' rule_specs' lthy |
200 end*} |
200 end*} |
201 |
201 |
202 ML {* Specification.read_spec *} |
|
203 |
|
204 text {* |
202 text {* |
205 Once we have the input data as some internal datastructure, we call |
203 Once we have the input data as some internal datastructure, we call |
206 the function @{ML add_inductive}. This function does the heavy duty |
204 the function @{text add_inductive}. This function does the heavy duty |
207 lifting in the package: it generates definitions for the |
205 lifting in the package: it generates definitions for the |
208 predicates and derives from them corresponding induction principles and |
206 predicates and derives from them corresponding induction principles and |
209 introduction rules. The description of this function will span over |
207 introduction rules. The description of this function will span over |
210 the next two sections. |
208 the next two sections. |
211 *} |
209 *} |