10 signature NOMINAL_FUNCTION = |
10 signature NOMINAL_FUNCTION = |
11 sig |
11 sig |
12 include FUNCTION_DATA |
12 include FUNCTION_DATA |
13 |
13 |
14 val add_nominal_function: (binding * typ option * mixfix) list -> |
14 val add_nominal_function: (binding * typ option * mixfix) list -> |
15 (Attrib.binding * term) list -> Function_Common.function_config -> |
15 (Attrib.binding * term) list -> Nominal_Function_Common.nominal_function_config -> |
16 (Proof.context -> tactic) -> local_theory -> info * local_theory |
16 (Proof.context -> tactic) -> local_theory -> info * local_theory |
17 |
17 |
18 val add_nominal_function_cmd: (binding * string option * mixfix) list -> |
18 val add_nominal_function_cmd: (binding * string option * mixfix) list -> |
19 (Attrib.binding * string) list -> Function_Common.function_config -> |
19 (Attrib.binding * string) list -> Nominal_Function_Common.nominal_function_config -> |
20 (Proof.context -> tactic) -> local_theory -> info * local_theory |
20 (Proof.context -> tactic) -> local_theory -> info * local_theory |
21 |
21 |
22 val nominal_function: (binding * typ option * mixfix) list -> |
22 val nominal_function: (binding * typ option * mixfix) list -> |
23 (Attrib.binding * term) list -> Function_Common.function_config -> |
23 (Attrib.binding * term) list -> Nominal_Function_Common.nominal_function_config -> |
24 local_theory -> Proof.state |
24 local_theory -> Proof.state |
25 |
25 |
26 val nominal_function_cmd: (binding * string option * mixfix) list -> |
26 val nominal_function_cmd: (binding * string option * mixfix) list -> |
27 (Attrib.binding * string) list -> Function_Common.function_config -> |
27 (Attrib.binding * string) list -> Nominal_Function_Common.nominal_function_config -> |
28 local_theory -> Proof.state |
28 local_theory -> Proof.state |
29 |
29 |
30 val setup : theory -> theory |
30 val setup : theory -> theory |
31 val get_congs : Proof.context -> thm list |
31 val get_congs : Proof.context -> thm list |
32 |
32 |
142 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
141 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
143 val (eqs, post, sort_cont, cnames) = |
142 val (eqs, post, sort_cont, cnames) = |
144 empty_preproc nominal_check_defs config ctxt' fixes spec (* nominal *) |
143 empty_preproc nominal_check_defs config ctxt' fixes spec (* nominal *) |
145 |
144 |
146 val defname = mk_defname fixes |
145 val defname = mk_defname fixes |
147 val FunctionConfig {partials, default, ...} = config |
146 val NominalFunctionConfig {partials, default, ...} = config |
148 val _ = |
147 val _ = |
149 if is_some default then Output.legacy_feature |
148 if is_some default then Output.legacy_feature |
150 "'function (default)'. Use 'partial_function'." |
149 "'function (default)'. Use 'partial_function'." |
151 else () |
150 else () |
152 |
151 |
255 |> the_single |> snd |
254 |> the_single |> snd |
256 |
255 |
257 |
256 |
258 (* outer syntax *) |
257 (* outer syntax *) |
259 |
258 |
|
259 local |
|
260 val option_parser = Parse.group "option" |
|
261 ((Parse.reserved "sequential" >> K Sequential) |
|
262 || ((Parse.reserved "default" |-- Parse.term) >> Default) |
|
263 || (Parse.reserved "domintros" >> K DomIntros) |
|
264 || (Parse.reserved "no_partials" >> K No_Partials) |
|
265 || ((Parse.reserved "invariant" |-- Parse.term) >> Invariant)) |
|
266 |
|
267 fun config_parser default = |
|
268 (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") []) |
|
269 >> (fn opts => fold apply_opt opts default) |
|
270 in |
|
271 fun nominal_function_parser default_cfg = |
|
272 config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs |
|
273 end |
|
274 |
|
275 |
260 (* nominal *) |
276 (* nominal *) |
261 val _ = |
277 val _ = |
262 Outer_Syntax.local_theory_to_proof "nominal_primrec" "define general recursive nominal functions" |
278 Outer_Syntax.local_theory_to_proof "nominal_primrec" "define general recursive nominal functions" |
263 Keyword.thy_goal |
279 Keyword.thy_goal |
264 (function_parser default_config |
280 (nominal_function_parser nominal_default_config |
265 >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config)) |
281 >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config)) |
266 |
282 |
267 |
283 |
268 end |
284 end |