src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
changeset 56945 3d1ead21a055
parent 56857 aa2de99be748
child 57397 5004aca20821
equal deleted inserted replaced
56944:578dc6b4be89 56945:3d1ead21a055
   529              space_implode "\n  " (map (quote o Syntax.string_of_term lthy) eqns));
   529              space_implode "\n  " (map (quote o Syntax.string_of_term lthy) eqns));
   530 
   530 
   531 val add_primrec_simple = add_primrec_simple' [];
   531 val add_primrec_simple = add_primrec_simple' [];
   532 
   532 
   533 fun gen_primrec old_primrec prep_spec opts
   533 fun gen_primrec old_primrec prep_spec opts
   534     (raw_fixes : (binding * 'a option * mixfix) list) raw_spec lthy =
   534     (raw_fixes : (binding * 'a option * mixfix) list) raw_specs lthy =
   535   let
   535   let
   536     val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes)
   536     val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes)
   537     val _ = null d orelse raise PRIMREC ("duplicate function name(s): " ^ commas d, []);
   537     val _ = null d orelse raise PRIMREC ("duplicate function name(s): " ^ commas d, []);
   538 
   538 
   539     val (fixes, specs) = fst (prep_spec raw_fixes raw_spec lthy);
   539     val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy);
   540 
   540 
   541     val mk_notes =
   541     val mk_notes =
   542       flat ooo map3 (fn js => fn prefix => fn thms =>
   542       flat ooo map3 (fn js => fn prefix => fn thms =>
   543         let
   543         let
   544           val (bs, attrss) = map_split (fst o nth specs) js;
   544           val (bs, attrss) = map_split (fst o nth specs) js;
   556     |-> (fn (names, (ts, (jss, simpss))) =>
   556     |-> (fn (names, (ts, (jss, simpss))) =>
   557       Spec_Rules.add Spec_Rules.Equational (ts, flat simpss)
   557       Spec_Rules.add Spec_Rules.Equational (ts, flat simpss)
   558       #> Local_Theory.notes (mk_notes jss names simpss)
   558       #> Local_Theory.notes (mk_notes jss names simpss)
   559       #>> pair ts o map snd)
   559       #>> pair ts o map snd)
   560   end
   560   end
   561   handle OLD_PRIMREC () => old_primrec raw_fixes raw_spec lthy |>> apsnd single;
   561   handle OLD_PRIMREC () => old_primrec raw_fixes raw_specs lthy |>> apsnd single;
   562 
   562 
   563 val add_primrec = gen_primrec Primrec.add_primrec Specification.check_spec [];
   563 val add_primrec = gen_primrec Primrec.add_primrec Specification.check_spec [];
   564 val add_primrec_cmd = gen_primrec Primrec.add_primrec_cmd Specification.read_spec;
   564 val add_primrec_cmd = gen_primrec Primrec.add_primrec_cmd Specification.read_spec;
   565 
   565 
   566 fun add_primrec_global fixes specs =
   566 fun add_primrec_global fixes specs =
   579 val _ = Outer_Syntax.local_theory @{command_spec "primrec"}
   579 val _ = Outer_Syntax.local_theory @{command_spec "primrec"}
   580   "define primitive recursive functions"
   580   "define primitive recursive functions"
   581   ((Scan.optional (@{keyword "("} |--
   581   ((Scan.optional (@{keyword "("} |--
   582       Parse.!!! (Parse.list1 primrec_option_parser) --| @{keyword ")"}) []) --
   582       Parse.!!! (Parse.list1 primrec_option_parser) --| @{keyword ")"}) []) --
   583     (Parse.fixes -- Parse_Spec.where_alt_specs)
   583     (Parse.fixes -- Parse_Spec.where_alt_specs)
   584     >> (fn (opts, (fixes, spec)) => snd o add_primrec_cmd opts fixes spec));
   584     >> (fn (opts, (fixes, specs)) => snd o add_primrec_cmd opts fixes specs));
   585 
   585 
   586 end;
   586 end;