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{*fun filtered_input str = |
99 filter Token.is_proper (Outer_Syntax.scan (Keyword.get_lexicons ()) 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*}(*>*) |
101 text {* |
101 text {* |
102 Note that in these definitions the parameter @{text R}, standing for the |
102 Note that in these definitions the parameter @{text R}, 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 |
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 *} |
131 (*<*)ML %no{*fun add_inductive_cmd pred_specs rule_specs lthy = lthy |
131 (*<*)ML %no{*fun add_inductive_cmd pred_specs rule_specs lthy = lthy |
132 fun add_inductive 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*) |
133 ML_val %linenosgray{*val specification : (local_theory -> local_theory) parser = |
133 ML %linenosgray{*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_spec "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*} |
140 |
140 |
141 text {* |
141 text {* |
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 |
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 |
153 to do first is to transform the parser's output into some internal |
153 to do first is to transform the parser's output into some internal |
154 datastructures that can be processed further. For this we can use the |
154 datastructures that can be processed further. For this we can use the |
155 function @{ML_ind read_spec in Specification}. This function takes some strings |
155 function @{ML_ind read_multi_specs in Specification}. This function takes some strings |
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_spec in Specification}. |
161 @{text "add_inductive_cmd"} is a call to @{ML read_multi_specs in Specification}. |
162 *} |
162 *} |
163 |
163 |
164 ML_val%grayML{*fun add_inductive_cmd pred_specs rule_specs lthy = |
164 ML_val%grayML{*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_spec 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*} |
171 |
171 |
172 text {* |
172 text {* |