10 signature NOMINAL_FUNCTION = |
10 signature NOMINAL_FUNCTION = |
11 sig |
11 sig |
12 include NOMINAL_FUNCTION_DATA |
12 include NOMINAL_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 -> Nominal_Function_Common.nominal_function_config -> |
15 Specification.multi_specs -> Nominal_Function_Common.nominal_function_config -> |
16 (Proof.context -> tactic) -> local_theory -> nominal_info * local_theory |
16 (Proof.context -> tactic) -> local_theory -> nominal_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 -> Nominal_Function_Common.nominal_function_config -> |
19 Specification.multi_specs_cmd -> Nominal_Function_Common.nominal_function_config -> |
20 (Proof.context -> tactic) -> bool -> local_theory -> nominal_info * local_theory |
20 (Proof.context -> tactic) -> bool -> local_theory -> nominal_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 -> Nominal_Function_Common.nominal_function_config -> |
23 Specification.multi_specs -> 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 -> Nominal_Function_Common.nominal_function_config -> |
27 Specification.multi_specs_cmd -> Nominal_Function_Common.nominal_function_config -> |
28 bool -> local_theory -> Proof.state |
28 bool -> local_theory -> Proof.state |
29 |
29 |
30 val get_info : Proof.context -> term -> nominal_info |
30 val get_info : Proof.context -> term -> nominal_info |
31 end |
31 end |
32 |
32 |
100 |
100 |
101 |
101 |
102 |
102 |
103 val simp_attribs = map (Attrib.internal o K) |
103 val simp_attribs = map (Attrib.internal o K) |
104 [Simplifier.simp_add, |
104 [Simplifier.simp_add, |
105 Code.add_default_eqn_attribute, |
105 Code.add_default_eqn_attribute Code.Equation, |
106 Named_Theorems.add @{named_theorems nitpick_simp}] |
106 Named_Theorems.add @{named_theorems nitpick_simp}] |
107 |
107 |
108 val psimp_attribs = map (Attrib.internal o K) |
108 val psimp_attribs = map (Attrib.internal o K) |
109 [Named_Theorems.add @{named_theorems nitpick_psimp}] |
109 [Named_Theorems.add @{named_theorems nitpick_psimp}] |
110 |
110 |
201 lthy' |
201 lthy' |
202 |> afterqed [[pattern_thm]] |
202 |> afterqed [[pattern_thm]] |
203 end |
203 end |
204 |
204 |
205 val add_nominal_function = |
205 val add_nominal_function = |
206 gen_add_nominal_function false Specification.check_spec (Type_Infer.anyT @{sort type}) |
206 gen_add_nominal_function false Specification.check_multi_specs (Type_Infer.anyT @{sort type}) |
207 fun add_nominal_function_cmd a b c d int = |
207 fun add_nominal_function_cmd a b c d int = |
208 gen_add_nominal_function int Specification.read_spec "_::type" a b c d |
208 gen_add_nominal_function int Specification.read_multi_specs "_::type" a b c d |
209 |
209 |
210 fun gen_nominal_function do_print prep default_constraint fixspec eqns config lthy = |
210 fun gen_nominal_function do_print prep default_constraint fixspec eqns config lthy = |
211 let |
211 let |
212 val ((goal_state, afterqed), lthy') = |
212 val ((goal_state, afterqed), lthy') = |
213 prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy |
213 prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy |
216 |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (Thm.concl_of goal_state), [])]] |
216 |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (Thm.concl_of goal_state), [])]] |
217 |> Proof.refine_singleton (Method.primitive_text (K (K goal_state))) |
217 |> Proof.refine_singleton (Method.primitive_text (K (K goal_state))) |
218 end |
218 end |
219 |
219 |
220 val nominal_function = |
220 val nominal_function = |
221 gen_nominal_function false Specification.check_spec (Type_Infer.anyT @{sort type}) |
221 gen_nominal_function false Specification.check_multi_specs (Type_Infer.anyT @{sort type}) |
222 fun nominal_function_cmd a b c int = |
222 fun nominal_function_cmd a b c int = |
223 gen_nominal_function int Specification.read_spec "_::type" a b c |
223 gen_nominal_function int Specification.read_multi_specs "_::type" a b c |
224 |
224 |
225 fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t |
225 fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t |
226 |> the_single |> snd |
226 |> the_single |> snd |
227 |
227 |
228 |
228 |
239 fun config_parser default = |
239 fun config_parser default = |
240 (Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) []) |
240 (Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) []) |
241 >> (fn opts => fold apply_opt opts default) |
241 >> (fn opts => fold apply_opt opts default) |
242 in |
242 in |
243 fun nominal_function_parser default_cfg = |
243 fun nominal_function_parser default_cfg = |
244 config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs |
244 config_parser default_cfg -- Parse_Spec.specification |
245 end |
245 end |
246 |
246 |
247 |
|
248 (* nominal *) |
|
249 val _ = |
247 val _ = |
250 Outer_Syntax.local_theory_to_proof' @{command_keyword nominal_function} |
248 Outer_Syntax.local_theory_to_proof' @{command_keyword nominal_function} |
251 "define general recursive nominal functions" |
249 "define general recursive nominal functions" |
252 (nominal_function_parser nominal_default_config |
250 (nominal_function_parser nominal_default_config |
253 >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config)) |
251 >> (fn (config, (fixes, specs)) => nominal_function_cmd fixes specs config)) |
254 |
|
255 |
252 |
256 end |
253 end |