src/HOL/Nominal/nominal_primrec.ML
changeset 21541 ea881fbe0489
child 21618 1cbb1134cb6c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Mon Nov 27 12:10:51 2006 +0100
     1.3 @@ -0,0 +1,445 @@
     1.4 +(*  Title:      HOL/Nominal/nominal_primrec.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Stefan Berghofer, TU Muenchen and Norbert Voelker, FernUni Hagen
     1.7 +
     1.8 +Package for defining functions on nominal datatypes by primitive recursion.
     1.9 +Taken from HOL/Tools/primrec_package.ML
    1.10 +*)
    1.11 +
    1.12 +signature NOMINAL_PRIMREC =
    1.13 +sig
    1.14 +  val quiet_mode: bool ref
    1.15 +  val add_primrec: string -> string list option -> string option ->
    1.16 +    ((bstring * string) * Attrib.src list) list -> theory -> Proof.state
    1.17 +  val add_primrec_unchecked: string -> string list option -> string option ->
    1.18 +    ((bstring * string) * Attrib.src list) list -> theory -> Proof.state
    1.19 +  val add_primrec_i: string -> term list option -> term option ->
    1.20 +    ((bstring * term) * attribute list) list -> theory -> Proof.state
    1.21 +  val add_primrec_unchecked_i: string -> term list option -> term option ->
    1.22 +    ((bstring * term) * attribute list) list -> theory -> Proof.state
    1.23 +end;
    1.24 +
    1.25 +structure NominalPrimrec : NOMINAL_PRIMREC =
    1.26 +struct
    1.27 +
    1.28 +open DatatypeAux;
    1.29 +
    1.30 +exception RecError of string;
    1.31 +
    1.32 +fun primrec_err s = error ("Nominal primrec definition error:\n" ^ s);
    1.33 +fun primrec_eq_err thy s eq =
    1.34 +  primrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term thy eq));
    1.35 +
    1.36 +
    1.37 +(* messages *)
    1.38 +
    1.39 +val quiet_mode = ref false;
    1.40 +fun message s = if ! quiet_mode then () else writeln s;
    1.41 +
    1.42 +
    1.43 +(* preprocessing of equations *)
    1.44 +
    1.45 +fun process_eqn thy eq rec_fns = 
    1.46 +  let
    1.47 +    val (lhs, rhs) = 
    1.48 +      if null (term_vars eq) then
    1.49 +        HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq))
    1.50 +        handle TERM _ => raise RecError "not a proper equation"
    1.51 +      else raise RecError "illegal schematic variable(s)";
    1.52 +
    1.53 +    val (recfun, args) = strip_comb lhs;
    1.54 +    val fnameT = dest_Const recfun handle TERM _ => 
    1.55 +      raise RecError "function is not declared as constant in theory";
    1.56 +
    1.57 +    val (ls', rest)  = take_prefix is_Free args;
    1.58 +    val (middle, rs') = take_suffix is_Free rest;
    1.59 +    val rpos = length ls';
    1.60 +
    1.61 +    val (constr, cargs') = if null middle then raise RecError "constructor missing"
    1.62 +      else strip_comb (hd middle);
    1.63 +    val (cname, T) = dest_Const constr
    1.64 +      handle TERM _ => raise RecError "ill-formed constructor";
    1.65 +    val (tname, _) = dest_Type (body_type T) handle TYPE _ =>
    1.66 +      raise RecError "cannot determine datatype associated with function"
    1.67 +
    1.68 +    val (ls, cargs, rs) =
    1.69 +      (map dest_Free ls', map dest_Free cargs', map dest_Free rs')
    1.70 +      handle TERM _ => raise RecError "illegal argument in pattern";
    1.71 +    val lfrees = ls @ rs @ cargs;
    1.72 +
    1.73 +    fun check_vars _ [] = ()
    1.74 +      | check_vars s vars = raise RecError (s ^ commas_quote (map fst vars))
    1.75 +  in
    1.76 +    if length middle > 1 then 
    1.77 +      raise RecError "more than one non-variable in pattern"
    1.78 +    else
    1.79 +     (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
    1.80 +      check_vars "extra variables on rhs: "
    1.81 +        (map dest_Free (term_frees rhs) \\ lfrees);
    1.82 +      case AList.lookup (op =) rec_fns fnameT of
    1.83 +        NONE =>
    1.84 +          (fnameT, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns
    1.85 +      | SOME (_, rpos', eqns) =>
    1.86 +          if AList.defined (op =) eqns cname then
    1.87 +            raise RecError "constructor already occurred as pattern"
    1.88 +          else if rpos <> rpos' then
    1.89 +            raise RecError "position of recursive argument inconsistent"
    1.90 +          else
    1.91 +            AList.update (op =) (fnameT, (tname, rpos, (cname, (ls, cargs, rs, rhs, eq))::eqns))
    1.92 +              rec_fns)
    1.93 +  end
    1.94 +  handle RecError s => primrec_eq_err thy s eq;
    1.95 +
    1.96 +val param_err = "Parameters must be the same for all recursive functions";
    1.97 +
    1.98 +fun process_fun thy descr rec_eqns (i, fnameT as (fname, _)) (fnameTs, fnss) =
    1.99 +  let
   1.100 +    val (_, (tname, _, constrs)) = List.nth (descr, i);
   1.101 +
   1.102 +    (* substitute "fname ls x rs" by "y" for (x, (_, y)) in subs *)
   1.103 +
   1.104 +    fun subst [] t fs = (t, fs)
   1.105 +      | subst subs (Abs (a, T, t)) fs =
   1.106 +          fs
   1.107 +          |> subst subs t
   1.108 +          |-> (fn t' => pair (Abs (a, T, t')))
   1.109 +      | subst subs (t as (_ $ _)) fs =
   1.110 +          let
   1.111 +            val (f, ts) = strip_comb t;
   1.112 +          in
   1.113 +            if is_Const f andalso dest_Const f mem map fst rec_eqns then
   1.114 +              let
   1.115 +                val fnameT' as (fname', _) = dest_Const f;
   1.116 +                val (_, rpos, eqns) = the (AList.lookup (op =) rec_eqns fnameT');
   1.117 +                val ls = Library.take (rpos, ts);
   1.118 +                val rest = Library.drop (rpos, ts);
   1.119 +                val (x', rs) = (hd rest, tl rest)
   1.120 +                  handle Empty => raise RecError ("not enough arguments\
   1.121 +                   \ in recursive application\nof function " ^ quote fname' ^ " on rhs");
   1.122 +                val _ = (case eqns of
   1.123 +                    (_, (ls', _, rs', _, _)) :: _ =>
   1.124 +                      if ls = map Free ls' andalso rs = map Free rs' then ()
   1.125 +                      else raise RecError param_err
   1.126 +                  | _ => ());
   1.127 +                val (x, xs) = strip_comb x'
   1.128 +              in case AList.lookup (op =) subs x
   1.129 +               of NONE =>
   1.130 +                    fs
   1.131 +                    |> fold_map (subst subs) ts
   1.132 +                    |-> (fn ts' => pair (list_comb (f, ts')))
   1.133 +                | SOME (i', y) =>
   1.134 +                    fs
   1.135 +                    |> fold_map (subst subs) xs
   1.136 +                    ||> process_fun thy descr rec_eqns (i', fnameT')
   1.137 +                    |-> (fn ts' => pair (list_comb (y, ts')))
   1.138 +              end
   1.139 +            else
   1.140 +              fs
   1.141 +              |> fold_map (subst subs) (f :: ts)
   1.142 +              |-> (fn (f'::ts') => pair (list_comb (f', ts')))
   1.143 +          end
   1.144 +      | subst _ t fs = (t, fs);
   1.145 +
   1.146 +    (* translate rec equations into function arguments suitable for rec comb *)
   1.147 +
   1.148 +    fun trans eqns (cname, cargs) (fnameTs', fnss', fns) =
   1.149 +      (case AList.lookup (op =) eqns cname of
   1.150 +          NONE => (warning ("No equation for constructor " ^ quote cname ^
   1.151 +            "\nin definition of function " ^ quote fname);
   1.152 +              (fnameTs', fnss', (Const ("arbitrary", dummyT))::fns))
   1.153 +        | SOME (ls, cargs', rs, rhs, eq) =>
   1.154 +            let
   1.155 +              val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
   1.156 +              val rargs = map fst recs;
   1.157 +              val subs = map (rpair dummyT o fst) 
   1.158 +                (rev (rename_wrt_term rhs rargs));
   1.159 +              val (rhs', (fnameTs'', fnss'')) = 
   1.160 +                  (subst (map (fn ((x, y), z) =>
   1.161 +                               (Free x, (body_index y, Free z)))
   1.162 +                          (recs ~~ subs)) rhs (fnameTs', fnss'))
   1.163 +                  handle RecError s => primrec_eq_err thy s eq
   1.164 +            in (fnameTs'', fnss'', 
   1.165 +                (list_abs_free (cargs' @ subs, rhs'))::fns)
   1.166 +            end)
   1.167 +
   1.168 +  in (case AList.lookup (op =) fnameTs i of
   1.169 +      NONE =>
   1.170 +        if exists (equal fnameT o snd) fnameTs then
   1.171 +          raise RecError ("inconsistent functions for datatype " ^ quote tname)
   1.172 +        else
   1.173 +          let
   1.174 +            val SOME (_, _, eqns as (_, (ls, _, rs, _, _)) :: _) =
   1.175 +              AList.lookup (op =) rec_eqns fnameT;
   1.176 +            val (fnameTs', fnss', fns) = fold_rev (trans eqns) constrs
   1.177 +              ((i, fnameT)::fnameTs, fnss, []) 
   1.178 +          in
   1.179 +            (fnameTs', (i, (fname, ls, rs, fns))::fnss')
   1.180 +          end
   1.181 +    | SOME fnameT' =>
   1.182 +        if fnameT = fnameT' then (fnameTs, fnss)
   1.183 +        else raise RecError ("inconsistent functions for datatype " ^ quote tname))
   1.184 +  end;
   1.185 +
   1.186 +
   1.187 +(* prepare functions needed for definitions *)
   1.188 +
   1.189 +fun get_fns fns ((i : int, (tname, _, constrs)), rec_name) (fs, defs) =
   1.190 +  case AList.lookup (op =) fns i of
   1.191 +     NONE =>
   1.192 +       let
   1.193 +         val dummy_fns = map (fn (_, cargs) => Const ("arbitrary",
   1.194 +           replicate ((length cargs) + (length (List.filter is_rec_type cargs)))
   1.195 +             dummyT ---> HOLogic.unitT)) constrs;
   1.196 +         val _ = warning ("No function definition for datatype " ^ quote tname)
   1.197 +       in
   1.198 +         (dummy_fns @ fs, defs)
   1.199 +       end
   1.200 +   | SOME (fname, ls, rs, fs') => (fs' @ fs, (fname, ls, rs, rec_name, tname) :: defs);
   1.201 +
   1.202 +
   1.203 +(* make definition *)
   1.204 +
   1.205 +fun make_def thy fs (fname, ls, rs, rec_name, tname) =
   1.206 +  let
   1.207 +    val used = map fst (fold Term.add_frees fs []);
   1.208 +    val x = (Name.variant used "x", dummyT);
   1.209 +    val frees = ls @ x :: rs;
   1.210 +    val rhs = list_abs_free (frees,
   1.211 +      list_comb (Const (rec_name, dummyT), fs @ [Free x]))
   1.212 +    val defpair = (Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def",
   1.213 +                   Logic.mk_equals (Const (fname, dummyT), rhs));
   1.214 +    val defpair' as (_, _ $ _ $ t) = Theory.inferT_axm thy defpair
   1.215 +  in (defpair', subst_bounds (rev (map Free frees), strip_abs_body t)) end;
   1.216 +
   1.217 +
   1.218 +(* find datatypes which contain all datatypes in tnames' *)
   1.219 +
   1.220 +fun find_dts (dt_info : NominalPackage.nominal_datatype_info Symtab.table) _ [] = []
   1.221 +  | find_dts dt_info tnames' (tname::tnames) =
   1.222 +      (case Symtab.lookup dt_info tname of
   1.223 +          NONE => primrec_err (quote tname ^ " is not a nominal datatype")
   1.224 +        | SOME dt =>
   1.225 +            if tnames' subset (map (#1 o snd) (#descr dt)) then
   1.226 +              (tname, dt)::(find_dts dt_info tnames' tnames)
   1.227 +            else find_dts dt_info tnames' tnames);
   1.228 +
   1.229 +fun common_prefix eq ([], _) = []
   1.230 +  | common_prefix eq (_, []) = []
   1.231 +  | common_prefix eq (x :: xs, y :: ys) =
   1.232 +      if eq (x, y) then x :: common_prefix eq (xs, ys) else [];
   1.233 +
   1.234 +local
   1.235 +
   1.236 +fun gen_primrec_i note def alt_name invs fctxt eqns_atts thy =
   1.237 +  let
   1.238 +    val (eqns, atts) = split_list eqns_atts;
   1.239 +    val dt_info = NominalPackage.get_nominal_datatypes thy;
   1.240 +    val rec_eqns = fold_rev (process_eqn thy o snd) eqns [];
   1.241 +    val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
   1.242 +      map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) rec_eqns
   1.243 +    val _ =
   1.244 +      (if forall (curry eq_set lsrs) lsrss andalso forall
   1.245 +         (fn (_, (_, _, (_, (ls, _, rs, _, _)) :: eqns)) =>
   1.246 +               forall (fn (_, (ls', _, rs', _, _)) =>
   1.247 +                 ls = ls' andalso rs = rs') eqns
   1.248 +           | _ => true) rec_eqns
   1.249 +       then () else raise RecError param_err);
   1.250 +    val tnames = distinct (op =) (map (#1 o snd) rec_eqns);
   1.251 +    val dts = find_dts dt_info tnames tnames;
   1.252 +    val main_fns = 
   1.253 +      map (fn (tname, {index, ...}) =>
   1.254 +        (index, 
   1.255 +          (fst o the o find_first (fn f => (#1 o snd) f = tname)) rec_eqns))
   1.256 +      dts;
   1.257 +    val {descr, rec_names, rec_rewrites, ...} = 
   1.258 +      if null dts then
   1.259 +        primrec_err ("datatypes " ^ commas_quote tnames ^ "\nare not mutually recursive")
   1.260 +      else snd (hd dts);
   1.261 +    val (fnameTs, fnss) =
   1.262 +      fold_rev (process_fun thy descr rec_eqns) main_fns ([], []);
   1.263 +    val (fs, defs) = fold_rev (get_fns fnss) (descr ~~ rec_names) ([], []);
   1.264 +    val defs' = map (make_def thy fs) defs;
   1.265 +    val nameTs1 = map snd fnameTs;
   1.266 +    val nameTs2 = map fst rec_eqns;
   1.267 +    val _ = if gen_eq_set (op =) (nameTs1, nameTs2) then ()
   1.268 +            else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^
   1.269 +              "\nare not mutually recursive");
   1.270 +    val primrec_name =
   1.271 +      if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name;
   1.272 +    val (defs_thms', thy') =
   1.273 +      thy
   1.274 +      |> Theory.add_path primrec_name
   1.275 +      |> fold_map def (map (fn ((name, t), _) => ((name, []), t)) defs');
   1.276 +    val cert = cterm_of thy';
   1.277 +
   1.278 +    fun mk_idx eq =
   1.279 +      let
   1.280 +        val Const c = head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
   1.281 +          (Logic.strip_imp_concl eq))));
   1.282 +        val SOME i = AList.lookup op = (map swap fnameTs) c;
   1.283 +        val SOME (_, _, constrs) = AList.lookup op = descr i;
   1.284 +        val SOME (_, _, eqns) = AList.lookup op = rec_eqns c;
   1.285 +        val SOME (cname, (_, cargs, _, _, _)) = find_first
   1.286 +          (fn (_, (_, _, _, _, eq')) => eq = eq') eqns
   1.287 +      in (i, find_index (fn (cname', _) => cname = cname') constrs, cargs) end;
   1.288 +
   1.289 +    val rec_rewritess =
   1.290 +      unflat (map (fn (_, (_, _, constrs)) => constrs) descr) rec_rewrites;
   1.291 +    val fvars = rec_rewrites |> hd |> concl_of |> HOLogic.dest_Trueprop |>
   1.292 +      HOLogic.dest_eq |> fst |> strip_comb |> snd |> take_prefix is_Var |> fst;
   1.293 +    val (pvars, ctxtvars) = List.partition
   1.294 +      (equal HOLogic.boolT o body_type o snd)
   1.295 +      (fold Term.add_vars (map Logic.strip_assums_concl
   1.296 +        (prems_of (hd rec_rewrites))) [] \\ map dest_Var fvars);
   1.297 +    val cfs = defs' |> hd |> snd |> strip_comb |> snd |>
   1.298 +      curry (List.take o swap) (length fvars) |> map cert;
   1.299 +    val invs' = (case invs of
   1.300 +        NONE => map (fn (i, _) =>
   1.301 +          let
   1.302 +            val SOME (_, T) = AList.lookup op = fnameTs i
   1.303 +            val (Ts, U) = strip_type T
   1.304 +          in
   1.305 +            Abs ("x", List.drop (Ts, length lsrs + 1) ---> U, HOLogic.true_const)
   1.306 +          end) descr
   1.307 +      | SOME invs' => invs');
   1.308 +    val inst = (map cert fvars ~~ cfs) @
   1.309 +      (map (cert o Var) pvars ~~ map cert invs') @
   1.310 +      (case ctxtvars of
   1.311 +         [ctxtvar] => [(cert (Var ctxtvar), cert (the_default HOLogic.unit fctxt))]
   1.312 +       | _ => []);
   1.313 +    val rec_rewrites' = map (fn (_, eq) =>
   1.314 +      let
   1.315 +        val (i, j, cargs) = mk_idx eq
   1.316 +        val th = nth (nth rec_rewritess i) j;
   1.317 +        val cargs' = th |> concl_of |> HOLogic.dest_Trueprop |>
   1.318 +          HOLogic.dest_eq |> fst |> strip_comb |> snd |> split_last |> snd |>
   1.319 +          strip_comb |> snd
   1.320 +      in (cargs, Logic.strip_imp_prems eq,
   1.321 +        Drule.cterm_instantiate (inst @
   1.322 +          (map (cterm_of thy') cargs' ~~ map (cterm_of thy' o Free) cargs)) th)
   1.323 +      end) eqns;
   1.324 +
   1.325 +    val prems = foldr1 (common_prefix op aconv) (map (prems_of o #3) rec_rewrites');
   1.326 +    val cprems = map cert prems;
   1.327 +    val asms = map Thm.assume cprems;
   1.328 +    val premss = map (fn (cargs, eprems, eqn) =>
   1.329 +      map (fn t => list_all_free (cargs, Logic.list_implies (eprems, t)))
   1.330 +        (List.drop (prems_of eqn, length prems))) rec_rewrites';
   1.331 +    val cpremss = map (map cert) premss;
   1.332 +    val asmss = map (map Thm.assume) cpremss;
   1.333 +
   1.334 +    fun mk_eqn ((cargs, eprems, eqn), asms') =
   1.335 +      let
   1.336 +        val ceprems = map cert eprems;
   1.337 +        val asms'' = map Thm.assume ceprems;
   1.338 +        val ccargs = map (cert o Free) cargs;
   1.339 +        val asms''' = map (fn th => implies_elim_list
   1.340 +          (forall_elim_list ccargs th) asms'') asms'
   1.341 +      in
   1.342 +        implies_elim_list eqn (asms @ asms''') |>
   1.343 +        implies_intr_list ceprems |>
   1.344 +        forall_intr_list ccargs
   1.345 +      end;
   1.346 +
   1.347 +    val rule_prems = cprems @ flat cpremss;
   1.348 +    val rule = implies_intr_list rule_prems
   1.349 +      (foldr1 (uncurry Conjunction.intr) (map mk_eqn (rec_rewrites' ~~ asmss)));
   1.350 +
   1.351 +    val goals = map (fn ((cargs, _, _), (_, eqn)) =>
   1.352 +      (list_all_free (cargs, eqn), [])) (rec_rewrites' ~~ eqns);
   1.353 +
   1.354 +  in
   1.355 +    thy' |>
   1.356 +    ProofContext.init |>
   1.357 +    Proof.theorem_i NONE
   1.358 +      (fn thss => ProofContext.theory (fn thy =>
   1.359 +         let
   1.360 +           val simps = flat thss;
   1.361 +           val (simps', thy') =
   1.362 +             fold_map note ((map fst eqns ~~ atts) ~~ map single simps) thy;
   1.363 +           val simps'' = maps snd simps'
   1.364 +         in
   1.365 +           thy'
   1.366 +           |> note (("simps", [Simplifier.simp_add]), simps'')
   1.367 +           |> snd
   1.368 +           |> Theory.parent_path
   1.369 +         end))
   1.370 +      [goals] |>
   1.371 +    Proof.apply (Method.Basic (fn ctxt => Method.RAW_METHOD (fn ths =>
   1.372 +      rewrite_goals_tac (map snd defs_thms') THEN
   1.373 +      compose_tac (false, rule, length rule_prems) 1))) |>
   1.374 +    Seq.hd
   1.375 +  end;
   1.376 +
   1.377 +fun gen_primrec note def alt_name invs fctxt eqns thy =
   1.378 +  let
   1.379 +    fun readt T s = term_of (Thm.read_cterm thy (s, T));
   1.380 +    val ((names, strings), srcss) = apfst split_list (split_list eqns);
   1.381 +    val atts = map (map (Attrib.attribute thy)) srcss;
   1.382 +    val eqn_ts = map (fn s => readt propT s
   1.383 +      handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings;
   1.384 +    val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq
   1.385 +      (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq))))
   1.386 +      handle TERM _ => primrec_eq_err thy "not a proper equation" eq) eqn_ts;
   1.387 +    val (_, eqn_ts') = OldInductivePackage.unify_consts thy rec_ts eqn_ts
   1.388 +  in
   1.389 +    gen_primrec_i note def alt_name
   1.390 +      (Option.map (map (readt TypeInfer.logicT)) invs)
   1.391 +      (Option.map (readt TypeInfer.logicT) fctxt)
   1.392 +      (names ~~ eqn_ts' ~~ atts) thy
   1.393 +  end;
   1.394 +
   1.395 +fun thy_note ((name, atts), thms) =
   1.396 +  PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
   1.397 +fun thy_def false ((name, atts), t) =
   1.398 +      PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
   1.399 +  | thy_def true ((name, atts), t) =
   1.400 +      PureThy.add_defs_unchecked_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
   1.401 +
   1.402 +in
   1.403 +
   1.404 +val add_primrec = gen_primrec thy_note (thy_def false);
   1.405 +val add_primrec_unchecked = gen_primrec thy_note (thy_def true);
   1.406 +val add_primrec_i = gen_primrec_i thy_note (thy_def false);
   1.407 +val add_primrec_unchecked_i = gen_primrec_i thy_note (thy_def true);
   1.408 +
   1.409 +end; (*local*)
   1.410 +
   1.411 +
   1.412 +(* outer syntax *)
   1.413 +
   1.414 +local structure P = OuterParse and K = OuterKeyword in
   1.415 +
   1.416 +val parser1 = P.$$$ "freshness_context" |-- P.$$$ ":" |-- (P.term >> SOME);
   1.417 +val parser2 =
   1.418 +  P.$$$ "invariant" |-- P.$$$ ":" |--
   1.419 +    (Scan.repeat1 P.term >> SOME) -- Scan.optional parser1 NONE ||
   1.420 +  (parser1 >> pair NONE);
   1.421 +val parser3 =
   1.422 +  P.name -- Scan.optional parser2 (NONE, NONE) ||
   1.423 +  (parser2 >> pair "");
   1.424 +val parser4 =
   1.425 +  (P.$$$ "unchecked" >> K true) -- Scan.optional parser3 ("", (NONE, NONE)) ||
   1.426 +  (parser3 >> pair false);
   1.427 +val options =
   1.428 +  Scan.optional (P.$$$ "(" |-- P.!!!
   1.429 +    (parser4 --| P.$$$ ")")) (false, ("", (NONE, NONE)));
   1.430 +
   1.431 +val primrec_decl =
   1.432 +  options -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
   1.433 +
   1.434 +val primrecP =
   1.435 +  OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal
   1.436 +    (primrec_decl >> (fn ((unchecked, (alt_name, (invs, fctxt))), eqns) =>
   1.437 +      Toplevel.theory_to_proof
   1.438 +        ((if unchecked then add_primrec_unchecked else add_primrec) alt_name invs fctxt
   1.439 +          (map P.triple_swap eqns))));
   1.440 +
   1.441 +val _ = OuterSyntax.add_parsers [primrecP];
   1.442 +val _ = OuterSyntax.add_keywords ["invariant", "freshness_context"];
   1.443 +
   1.444 +end;
   1.445 +
   1.446 +
   1.447 +end;
   1.448 +