equal
deleted
inserted
replaced
9 |
9 |
10 signature NOMINAL_FUNCTION_CORE = |
10 signature NOMINAL_FUNCTION_CORE = |
11 sig |
11 sig |
12 val trace: bool Unsynchronized.ref |
12 val trace: bool Unsynchronized.ref |
13 |
13 |
14 val prepare_nominal_function : Function_Common.function_config |
14 val prepare_nominal_function : Nominal_Function_Common.nominal_function_config |
15 -> string (* defname *) |
15 -> string (* defname *) |
16 -> ((bstring * typ) * mixfix) list (* defined symbol *) |
16 -> ((bstring * typ) * mixfix) list (* defined symbol *) |
17 -> ((bstring * typ) list * term list * term * term) list (* specification *) |
17 -> ((bstring * typ) list * term list * term * term) list (* specification *) |
18 -> local_theory |
18 -> local_theory |
19 -> (term (* f *) |
19 -> (term (* f *) |
20 * thm (* goalstate *) |
20 * thm (* goalstate *) |
21 * (thm -> Function_Common.function_result) (* continuation *) |
21 * (thm -> Nominal_Function_Common.function_result) (* continuation *) |
22 ) * local_theory |
22 ) * local_theory |
23 |
23 |
24 end |
24 end |
25 |
25 |
26 structure Nominal_Function_Core : NOMINAL_FUNCTION_CORE = |
26 structure Nominal_Function_Core : NOMINAL_FUNCTION_CORE = |
31 |
31 |
32 val boolT = HOLogic.boolT |
32 val boolT = HOLogic.boolT |
33 val mk_eq = HOLogic.mk_eq |
33 val mk_eq = HOLogic.mk_eq |
34 |
34 |
35 open Function_Lib |
35 open Function_Lib |
36 open Function_Common |
36 open Nominal_Function_Common |
37 |
37 |
38 datatype globals = Globals of |
38 datatype globals = Globals of |
39 {fvar: term, |
39 {fvar: term, |
40 domT: typ, |
40 domT: typ, |
41 ranT: typ, |
41 ranT: typ, |
903 |
903 |
904 |
904 |
905 (* nominal *) |
905 (* nominal *) |
906 fun prepare_nominal_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy = |
906 fun prepare_nominal_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy = |
907 let |
907 let |
908 val FunctionConfig {domintros, default=default_opt, ...} = config |
908 val NominalFunctionConfig {domintros, default=default_opt, ...} = config |
909 |
909 |
910 val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*) |
910 val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*) |
911 val fvar = Free (fname, fT) |
911 val fvar = Free (fname, fT) |
912 val domT = domain_type fT |
912 val domT = domain_type fT |
913 val ranT = range_type fT |
913 val ranT = range_type fT |