Nominal/nominal_function.ML
changeset 2819 4bd584ff4fab
parent 2789 32979078bfe9
child 2821 c7d4bd9e89e0
equal deleted inserted replaced
2818:8fe80e9f796d 2819:4bd584ff4fab
    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 
    36 
    36 
    37 structure Nominal_Function : NOMINAL_FUNCTION =
    37 structure Nominal_Function : NOMINAL_FUNCTION =
    38 struct
    38 struct
    39 
    39 
    40 open Function_Lib
    40 open Function_Lib
    41 open Function_Common
    41 open Nominal_Function_Common
    42 
       
    43 
    42 
    44 
    43 
    45 (* Check for all sorts of errors in the input - nominal needs a different checking function *)
    44 (* Check for all sorts of errors in the input - nominal needs a different checking function *)
    46 fun nominal_check_defs ctxt fixes eqs =
    45 fun nominal_check_defs ctxt fixes eqs =
    47   let
    46   let
   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