equal
deleted
inserted
replaced
414 |
414 |
415 (* outer syntax *) |
415 (* outer syntax *) |
416 |
416 |
417 local structure P = OuterParse and K = OuterKeyword in |
417 local structure P = OuterParse and K = OuterKeyword in |
418 |
418 |
|
419 val _ = OuterSyntax.keywords ["invariant", "freshness_context"]; |
|
420 |
419 val parser1 = P.$$$ "freshness_context" |-- P.$$$ ":" |-- (P.term >> SOME); |
421 val parser1 = P.$$$ "freshness_context" |-- P.$$$ ":" |-- (P.term >> SOME); |
420 val parser2 = |
422 val parser2 = |
421 P.$$$ "invariant" |-- P.$$$ ":" |-- |
423 P.$$$ "invariant" |-- P.$$$ ":" |-- |
422 (Scan.repeat1 P.term >> SOME) -- Scan.optional parser1 NONE || |
424 (Scan.repeat1 P.term >> SOME) -- Scan.optional parser1 NONE || |
423 (parser1 >> pair NONE); |
425 (parser1 >> pair NONE); |
432 (parser4 --| P.$$$ ")")) (false, ("", (NONE, NONE))); |
434 (parser4 --| P.$$$ ")")) (false, ("", (NONE, NONE))); |
433 |
435 |
434 val primrec_decl = |
436 val primrec_decl = |
435 options -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop); |
437 options -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop); |
436 |
438 |
437 val primrecP = |
439 val _ = |
438 OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal |
440 OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal |
439 (primrec_decl >> (fn ((unchecked, (alt_name, (invs, fctxt))), eqns) => |
441 (primrec_decl >> (fn ((unchecked, (alt_name, (invs, fctxt))), eqns) => |
440 Toplevel.print o Toplevel.theory_to_proof |
442 Toplevel.print o Toplevel.theory_to_proof |
441 ((if unchecked then add_primrec_unchecked else add_primrec) alt_name invs fctxt |
443 ((if unchecked then add_primrec_unchecked else add_primrec) alt_name invs fctxt |
442 (map P.triple_swap eqns)))); |
444 (map P.triple_swap eqns)))); |
443 |
445 |
444 val _ = OuterSyntax.add_parsers [primrecP]; |
|
445 val _ = OuterSyntax.add_keywords ["invariant", "freshness_context"]; |
|
446 |
|
447 end; |
446 end; |
448 |
447 |
449 |
448 |
450 end; |
449 end; |
451 |
450 |