Implemented new "nominal_primrec" command for defining
authorberghofe
Mon Nov 27 12:10:51 2006 +0100 (2006-11-27)
changeset 21541ea881fbe0489
parent 21540 f3faed8276e6
child 21542 4462ee172ef0
Implemented new "nominal_primrec" command for defining
functions on nominal datatypes.
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_primrec.ML
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Mon Nov 27 12:09:55 2006 +0100
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Mon Nov 27 12:10:51 2006 +0100
     1.3 @@ -7,6 +7,7 @@
     1.4    ("nominal_package.ML")
     1.5    ("nominal_induct.ML") 
     1.6    ("nominal_permeq.ML")
     1.7 +  ("nominal_primrec.ML")
     1.8  begin 
     1.9  
    1.10  section {* Permutations *}
    1.11 @@ -3009,6 +3010,10 @@
    1.12  use "nominal_permeq.ML";
    1.13  use "nominal_package.ML"
    1.14  setup "NominalAtoms.setup"
    1.15 +setup "NominalPackage.setup"
    1.16 +
    1.17 +(** primitive recursive functions on nominal datatypes **)
    1.18 +use "nominal_primrec.ML"
    1.19  
    1.20  (*****************************************)
    1.21  (* setup for induction principles method *)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Mon Nov 27 12:10:51 2006 +0100
     2.3 @@ -0,0 +1,445 @@
     2.4 +(*  Title:      HOL/Nominal/nominal_primrec.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Stefan Berghofer, TU Muenchen and Norbert Voelker, FernUni Hagen
     2.7 +
     2.8 +Package for defining functions on nominal datatypes by primitive recursion.
     2.9 +Taken from HOL/Tools/primrec_package.ML
    2.10 +*)
    2.11 +
    2.12 +signature NOMINAL_PRIMREC =
    2.13 +sig
    2.14 +  val quiet_mode: bool ref
    2.15 +  val add_primrec: string -> string list option -> string option ->
    2.16 +    ((bstring * string) * Attrib.src list) list -> theory -> Proof.state
    2.17 +  val add_primrec_unchecked: string -> string list option -> string option ->
    2.18 +    ((bstring * string) * Attrib.src list) list -> theory -> Proof.state
    2.19 +  val add_primrec_i: string -> term list option -> term option ->
    2.20 +    ((bstring * term) * attribute list) list -> theory -> Proof.state
    2.21 +  val add_primrec_unchecked_i: string -> term list option -> term option ->
    2.22 +    ((bstring * term) * attribute list) list -> theory -> Proof.state
    2.23 +end;
    2.24 +
    2.25 +structure NominalPrimrec : NOMINAL_PRIMREC =
    2.26 +struct
    2.27 +
    2.28 +open DatatypeAux;
    2.29 +
    2.30 +exception RecError of string;
    2.31 +
    2.32 +fun primrec_err s = error ("Nominal primrec definition error:\n" ^ s);
    2.33 +fun primrec_eq_err thy s eq =
    2.34 +  primrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term thy eq));
    2.35 +
    2.36 +
    2.37 +(* messages *)
    2.38 +
    2.39 +val quiet_mode = ref false;
    2.40 +fun message s = if ! quiet_mode then () else writeln s;
    2.41 +
    2.42 +
    2.43 +(* preprocessing of equations *)
    2.44 +
    2.45 +fun process_eqn thy eq rec_fns = 
    2.46 +  let
    2.47 +    val (lhs, rhs) = 
    2.48 +      if null (term_vars eq) then
    2.49 +        HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq))
    2.50 +        handle TERM _ => raise RecError "not a proper equation"
    2.51 +      else raise RecError "illegal schematic variable(s)";
    2.52 +
    2.53 +    val (recfun, args) = strip_comb lhs;
    2.54 +    val fnameT = dest_Const recfun handle TERM _ => 
    2.55 +      raise RecError "function is not declared as constant in theory";
    2.56 +
    2.57 +    val (ls', rest)  = take_prefix is_Free args;
    2.58 +    val (middle, rs') = take_suffix is_Free rest;
    2.59 +    val rpos = length ls';
    2.60 +
    2.61 +    val (constr, cargs') = if null middle then raise RecError "constructor missing"
    2.62 +      else strip_comb (hd middle);
    2.63 +    val (cname, T) = dest_Const constr
    2.64 +      handle TERM _ => raise RecError "ill-formed constructor";
    2.65 +    val (tname, _) = dest_Type (body_type T) handle TYPE _ =>
    2.66 +      raise RecError "cannot determine datatype associated with function"
    2.67 +
    2.68 +    val (ls, cargs, rs) =
    2.69 +      (map dest_Free ls', map dest_Free cargs', map dest_Free rs')
    2.70 +      handle TERM _ => raise RecError "illegal argument in pattern";
    2.71 +    val lfrees = ls @ rs @ cargs;
    2.72 +
    2.73 +    fun check_vars _ [] = ()
    2.74 +      | check_vars s vars = raise RecError (s ^ commas_quote (map fst vars))
    2.75 +  in
    2.76 +    if length middle > 1 then 
    2.77 +      raise RecError "more than one non-variable in pattern"
    2.78 +    else
    2.79 +     (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
    2.80 +      check_vars "extra variables on rhs: "
    2.81 +        (map dest_Free (term_frees rhs) \\ lfrees);
    2.82 +      case AList.lookup (op =) rec_fns fnameT of
    2.83 +        NONE =>
    2.84 +          (fnameT, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns
    2.85 +      | SOME (_, rpos', eqns) =>
    2.86 +          if AList.defined (op =) eqns cname then
    2.87 +            raise RecError "constructor already occurred as pattern"
    2.88 +          else if rpos <> rpos' then
    2.89 +            raise RecError "position of recursive argument inconsistent"
    2.90 +          else
    2.91 +            AList.update (op =) (fnameT, (tname, rpos, (cname, (ls, cargs, rs, rhs, eq))::eqns))
    2.92 +              rec_fns)
    2.93 +  end
    2.94 +  handle RecError s => primrec_eq_err thy s eq;
    2.95 +
    2.96 +val param_err = "Parameters must be the same for all recursive functions";
    2.97 +
    2.98 +fun process_fun thy descr rec_eqns (i, fnameT as (fname, _)) (fnameTs, fnss) =
    2.99 +  let
   2.100 +    val (_, (tname, _, constrs)) = List.nth (descr, i);
   2.101 +
   2.102 +    (* substitute "fname ls x rs" by "y" for (x, (_, y)) in subs *)
   2.103 +
   2.104 +    fun subst [] t fs = (t, fs)
   2.105 +      | subst subs (Abs (a, T, t)) fs =
   2.106 +          fs
   2.107 +          |> subst subs t
   2.108 +          |-> (fn t' => pair (Abs (a, T, t')))
   2.109 +      | subst subs (t as (_ $ _)) fs =
   2.110 +          let
   2.111 +            val (f, ts) = strip_comb t;
   2.112 +          in
   2.113 +            if is_Const f andalso dest_Const f mem map fst rec_eqns then
   2.114 +              let
   2.115 +                val fnameT' as (fname', _) = dest_Const f;
   2.116 +                val (_, rpos, eqns) = the (AList.lookup (op =) rec_eqns fnameT');
   2.117 +                val ls = Library.take (rpos, ts);
   2.118 +                val rest = Library.drop (rpos, ts);
   2.119 +                val (x', rs) = (hd rest, tl rest)
   2.120 +                  handle Empty => raise RecError ("not enough arguments\
   2.121 +                   \ in recursive application\nof function " ^ quote fname' ^ " on rhs");
   2.122 +                val _ = (case eqns of
   2.123 +                    (_, (ls', _, rs', _, _)) :: _ =>
   2.124 +                      if ls = map Free ls' andalso rs = map Free rs' then ()
   2.125 +                      else raise RecError param_err
   2.126 +                  | _ => ());
   2.127 +                val (x, xs) = strip_comb x'
   2.128 +              in case AList.lookup (op =) subs x
   2.129 +               of NONE =>
   2.130 +                    fs
   2.131 +                    |> fold_map (subst subs) ts
   2.132 +                    |-> (fn ts' => pair (list_comb (f, ts')))
   2.133 +                | SOME (i', y) =>
   2.134 +                    fs
   2.135 +                    |> fold_map (subst subs) xs
   2.136 +                    ||> process_fun thy descr rec_eqns (i', fnameT')
   2.137 +                    |-> (fn ts' => pair (list_comb (y, ts')))
   2.138 +              end
   2.139 +            else
   2.140 +              fs
   2.141 +              |> fold_map (subst subs) (f :: ts)
   2.142 +              |-> (fn (f'::ts') => pair (list_comb (f', ts')))
   2.143 +          end
   2.144 +      | subst _ t fs = (t, fs);
   2.145 +
   2.146 +    (* translate rec equations into function arguments suitable for rec comb *)
   2.147 +
   2.148 +    fun trans eqns (cname, cargs) (fnameTs', fnss', fns) =
   2.149 +      (case AList.lookup (op =) eqns cname of
   2.150 +          NONE => (warning ("No equation for constructor " ^ quote cname ^
   2.151 +            "\nin definition of function " ^ quote fname);
   2.152 +              (fnameTs', fnss', (Const ("arbitrary", dummyT))::fns))
   2.153 +        | SOME (ls, cargs', rs, rhs, eq) =>
   2.154 +            let
   2.155 +              val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
   2.156 +              val rargs = map fst recs;
   2.157 +              val subs = map (rpair dummyT o fst) 
   2.158 +                (rev (rename_wrt_term rhs rargs));
   2.159 +              val (rhs', (fnameTs'', fnss'')) = 
   2.160 +                  (subst (map (fn ((x, y), z) =>
   2.161 +                               (Free x, (body_index y, Free z)))
   2.162 +                          (recs ~~ subs)) rhs (fnameTs', fnss'))
   2.163 +                  handle RecError s => primrec_eq_err thy s eq
   2.164 +            in (fnameTs'', fnss'', 
   2.165 +                (list_abs_free (cargs' @ subs, rhs'))::fns)
   2.166 +            end)
   2.167 +
   2.168 +  in (case AList.lookup (op =) fnameTs i of
   2.169 +      NONE =>
   2.170 +        if exists (equal fnameT o snd) fnameTs then
   2.171 +          raise RecError ("inconsistent functions for datatype " ^ quote tname)
   2.172 +        else
   2.173 +          let
   2.174 +            val SOME (_, _, eqns as (_, (ls, _, rs, _, _)) :: _) =
   2.175 +              AList.lookup (op =) rec_eqns fnameT;
   2.176 +            val (fnameTs', fnss', fns) = fold_rev (trans eqns) constrs
   2.177 +              ((i, fnameT)::fnameTs, fnss, []) 
   2.178 +          in
   2.179 +            (fnameTs', (i, (fname, ls, rs, fns))::fnss')
   2.180 +          end
   2.181 +    | SOME fnameT' =>
   2.182 +        if fnameT = fnameT' then (fnameTs, fnss)
   2.183 +        else raise RecError ("inconsistent functions for datatype " ^ quote tname))
   2.184 +  end;
   2.185 +
   2.186 +
   2.187 +(* prepare functions needed for definitions *)
   2.188 +
   2.189 +fun get_fns fns ((i : int, (tname, _, constrs)), rec_name) (fs, defs) =
   2.190 +  case AList.lookup (op =) fns i of
   2.191 +     NONE =>
   2.192 +       let
   2.193 +         val dummy_fns = map (fn (_, cargs) => Const ("arbitrary",
   2.194 +           replicate ((length cargs) + (length (List.filter is_rec_type cargs)))
   2.195 +             dummyT ---> HOLogic.unitT)) constrs;
   2.196 +         val _ = warning ("No function definition for datatype " ^ quote tname)
   2.197 +       in
   2.198 +         (dummy_fns @ fs, defs)
   2.199 +       end
   2.200 +   | SOME (fname, ls, rs, fs') => (fs' @ fs, (fname, ls, rs, rec_name, tname) :: defs);
   2.201 +
   2.202 +
   2.203 +(* make definition *)
   2.204 +
   2.205 +fun make_def thy fs (fname, ls, rs, rec_name, tname) =
   2.206 +  let
   2.207 +    val used = map fst (fold Term.add_frees fs []);
   2.208 +    val x = (Name.variant used "x", dummyT);
   2.209 +    val frees = ls @ x :: rs;
   2.210 +    val rhs = list_abs_free (frees,
   2.211 +      list_comb (Const (rec_name, dummyT), fs @ [Free x]))
   2.212 +    val defpair = (Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def",
   2.213 +                   Logic.mk_equals (Const (fname, dummyT), rhs));
   2.214 +    val defpair' as (_, _ $ _ $ t) = Theory.inferT_axm thy defpair
   2.215 +  in (defpair', subst_bounds (rev (map Free frees), strip_abs_body t)) end;
   2.216 +
   2.217 +
   2.218 +(* find datatypes which contain all datatypes in tnames' *)
   2.219 +
   2.220 +fun find_dts (dt_info : NominalPackage.nominal_datatype_info Symtab.table) _ [] = []
   2.221 +  | find_dts dt_info tnames' (tname::tnames) =
   2.222 +      (case Symtab.lookup dt_info tname of
   2.223 +          NONE => primrec_err (quote tname ^ " is not a nominal datatype")
   2.224 +        | SOME dt =>
   2.225 +            if tnames' subset (map (#1 o snd) (#descr dt)) then
   2.226 +              (tname, dt)::(find_dts dt_info tnames' tnames)
   2.227 +            else find_dts dt_info tnames' tnames);
   2.228 +
   2.229 +fun common_prefix eq ([], _) = []
   2.230 +  | common_prefix eq (_, []) = []
   2.231 +  | common_prefix eq (x :: xs, y :: ys) =
   2.232 +      if eq (x, y) then x :: common_prefix eq (xs, ys) else [];
   2.233 +
   2.234 +local
   2.235 +
   2.236 +fun gen_primrec_i note def alt_name invs fctxt eqns_atts thy =
   2.237 +  let
   2.238 +    val (eqns, atts) = split_list eqns_atts;
   2.239 +    val dt_info = NominalPackage.get_nominal_datatypes thy;
   2.240 +    val rec_eqns = fold_rev (process_eqn thy o snd) eqns [];
   2.241 +    val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
   2.242 +      map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) rec_eqns
   2.243 +    val _ =
   2.244 +      (if forall (curry eq_set lsrs) lsrss andalso forall
   2.245 +         (fn (_, (_, _, (_, (ls, _, rs, _, _)) :: eqns)) =>
   2.246 +               forall (fn (_, (ls', _, rs', _, _)) =>
   2.247 +                 ls = ls' andalso rs = rs') eqns
   2.248 +           | _ => true) rec_eqns
   2.249 +       then () else raise RecError param_err);
   2.250 +    val tnames = distinct (op =) (map (#1 o snd) rec_eqns);
   2.251 +    val dts = find_dts dt_info tnames tnames;
   2.252 +    val main_fns = 
   2.253 +      map (fn (tname, {index, ...}) =>
   2.254 +        (index, 
   2.255 +          (fst o the o find_first (fn f => (#1 o snd) f = tname)) rec_eqns))
   2.256 +      dts;
   2.257 +    val {descr, rec_names, rec_rewrites, ...} = 
   2.258 +      if null dts then
   2.259 +        primrec_err ("datatypes " ^ commas_quote tnames ^ "\nare not mutually recursive")
   2.260 +      else snd (hd dts);
   2.261 +    val (fnameTs, fnss) =
   2.262 +      fold_rev (process_fun thy descr rec_eqns) main_fns ([], []);
   2.263 +    val (fs, defs) = fold_rev (get_fns fnss) (descr ~~ rec_names) ([], []);
   2.264 +    val defs' = map (make_def thy fs) defs;
   2.265 +    val nameTs1 = map snd fnameTs;
   2.266 +    val nameTs2 = map fst rec_eqns;
   2.267 +    val _ = if gen_eq_set (op =) (nameTs1, nameTs2) then ()
   2.268 +            else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^
   2.269 +              "\nare not mutually recursive");
   2.270 +    val primrec_name =
   2.271 +      if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name;
   2.272 +    val (defs_thms', thy') =
   2.273 +      thy
   2.274 +      |> Theory.add_path primrec_name
   2.275 +      |> fold_map def (map (fn ((name, t), _) => ((name, []), t)) defs');
   2.276 +    val cert = cterm_of thy';
   2.277 +
   2.278 +    fun mk_idx eq =
   2.279 +      let
   2.280 +        val Const c = head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
   2.281 +          (Logic.strip_imp_concl eq))));
   2.282 +        val SOME i = AList.lookup op = (map swap fnameTs) c;
   2.283 +        val SOME (_, _, constrs) = AList.lookup op = descr i;
   2.284 +        val SOME (_, _, eqns) = AList.lookup op = rec_eqns c;
   2.285 +        val SOME (cname, (_, cargs, _, _, _)) = find_first
   2.286 +          (fn (_, (_, _, _, _, eq')) => eq = eq') eqns
   2.287 +      in (i, find_index (fn (cname', _) => cname = cname') constrs, cargs) end;
   2.288 +
   2.289 +    val rec_rewritess =
   2.290 +      unflat (map (fn (_, (_, _, constrs)) => constrs) descr) rec_rewrites;
   2.291 +    val fvars = rec_rewrites |> hd |> concl_of |> HOLogic.dest_Trueprop |>
   2.292 +      HOLogic.dest_eq |> fst |> strip_comb |> snd |> take_prefix is_Var |> fst;
   2.293 +    val (pvars, ctxtvars) = List.partition
   2.294 +      (equal HOLogic.boolT o body_type o snd)
   2.295 +      (fold Term.add_vars (map Logic.strip_assums_concl
   2.296 +        (prems_of (hd rec_rewrites))) [] \\ map dest_Var fvars);
   2.297 +    val cfs = defs' |> hd |> snd |> strip_comb |> snd |>
   2.298 +      curry (List.take o swap) (length fvars) |> map cert;
   2.299 +    val invs' = (case invs of
   2.300 +        NONE => map (fn (i, _) =>
   2.301 +          let
   2.302 +            val SOME (_, T) = AList.lookup op = fnameTs i
   2.303 +            val (Ts, U) = strip_type T
   2.304 +          in
   2.305 +            Abs ("x", List.drop (Ts, length lsrs + 1) ---> U, HOLogic.true_const)
   2.306 +          end) descr
   2.307 +      | SOME invs' => invs');
   2.308 +    val inst = (map cert fvars ~~ cfs) @
   2.309 +      (map (cert o Var) pvars ~~ map cert invs') @
   2.310 +      (case ctxtvars of
   2.311 +         [ctxtvar] => [(cert (Var ctxtvar), cert (the_default HOLogic.unit fctxt))]
   2.312 +       | _ => []);
   2.313 +    val rec_rewrites' = map (fn (_, eq) =>
   2.314 +      let
   2.315 +        val (i, j, cargs) = mk_idx eq
   2.316 +        val th = nth (nth rec_rewritess i) j;
   2.317 +        val cargs' = th |> concl_of |> HOLogic.dest_Trueprop |>
   2.318 +          HOLogic.dest_eq |> fst |> strip_comb |> snd |> split_last |> snd |>
   2.319 +          strip_comb |> snd
   2.320 +      in (cargs, Logic.strip_imp_prems eq,
   2.321 +        Drule.cterm_instantiate (inst @
   2.322 +          (map (cterm_of thy') cargs' ~~ map (cterm_of thy' o Free) cargs)) th)
   2.323 +      end) eqns;
   2.324 +
   2.325 +    val prems = foldr1 (common_prefix op aconv) (map (prems_of o #3) rec_rewrites');
   2.326 +    val cprems = map cert prems;
   2.327 +    val asms = map Thm.assume cprems;
   2.328 +    val premss = map (fn (cargs, eprems, eqn) =>
   2.329 +      map (fn t => list_all_free (cargs, Logic.list_implies (eprems, t)))
   2.330 +        (List.drop (prems_of eqn, length prems))) rec_rewrites';
   2.331 +    val cpremss = map (map cert) premss;
   2.332 +    val asmss = map (map Thm.assume) cpremss;
   2.333 +
   2.334 +    fun mk_eqn ((cargs, eprems, eqn), asms') =
   2.335 +      let
   2.336 +        val ceprems = map cert eprems;
   2.337 +        val asms'' = map Thm.assume ceprems;
   2.338 +        val ccargs = map (cert o Free) cargs;
   2.339 +        val asms''' = map (fn th => implies_elim_list
   2.340 +          (forall_elim_list ccargs th) asms'') asms'
   2.341 +      in
   2.342 +        implies_elim_list eqn (asms @ asms''') |>
   2.343 +        implies_intr_list ceprems |>
   2.344 +        forall_intr_list ccargs
   2.345 +      end;
   2.346 +
   2.347 +    val rule_prems = cprems @ flat cpremss;
   2.348 +    val rule = implies_intr_list rule_prems
   2.349 +      (foldr1 (uncurry Conjunction.intr) (map mk_eqn (rec_rewrites' ~~ asmss)));
   2.350 +
   2.351 +    val goals = map (fn ((cargs, _, _), (_, eqn)) =>
   2.352 +      (list_all_free (cargs, eqn), [])) (rec_rewrites' ~~ eqns);
   2.353 +
   2.354 +  in
   2.355 +    thy' |>
   2.356 +    ProofContext.init |>
   2.357 +    Proof.theorem_i NONE
   2.358 +      (fn thss => ProofContext.theory (fn thy =>
   2.359 +         let
   2.360 +           val simps = flat thss;
   2.361 +           val (simps', thy') =
   2.362 +             fold_map note ((map fst eqns ~~ atts) ~~ map single simps) thy;
   2.363 +           val simps'' = maps snd simps'
   2.364 +         in
   2.365 +           thy'
   2.366 +           |> note (("simps", [Simplifier.simp_add]), simps'')
   2.367 +           |> snd
   2.368 +           |> Theory.parent_path
   2.369 +         end))
   2.370 +      [goals] |>
   2.371 +    Proof.apply (Method.Basic (fn ctxt => Method.RAW_METHOD (fn ths =>
   2.372 +      rewrite_goals_tac (map snd defs_thms') THEN
   2.373 +      compose_tac (false, rule, length rule_prems) 1))) |>
   2.374 +    Seq.hd
   2.375 +  end;
   2.376 +
   2.377 +fun gen_primrec note def alt_name invs fctxt eqns thy =
   2.378 +  let
   2.379 +    fun readt T s = term_of (Thm.read_cterm thy (s, T));
   2.380 +    val ((names, strings), srcss) = apfst split_list (split_list eqns);
   2.381 +    val atts = map (map (Attrib.attribute thy)) srcss;
   2.382 +    val eqn_ts = map (fn s => readt propT s
   2.383 +      handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings;
   2.384 +    val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq
   2.385 +      (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq))))
   2.386 +      handle TERM _ => primrec_eq_err thy "not a proper equation" eq) eqn_ts;
   2.387 +    val (_, eqn_ts') = OldInductivePackage.unify_consts thy rec_ts eqn_ts
   2.388 +  in
   2.389 +    gen_primrec_i note def alt_name
   2.390 +      (Option.map (map (readt TypeInfer.logicT)) invs)
   2.391 +      (Option.map (readt TypeInfer.logicT) fctxt)
   2.392 +      (names ~~ eqn_ts' ~~ atts) thy
   2.393 +  end;
   2.394 +
   2.395 +fun thy_note ((name, atts), thms) =
   2.396 +  PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
   2.397 +fun thy_def false ((name, atts), t) =
   2.398 +      PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
   2.399 +  | thy_def true ((name, atts), t) =
   2.400 +      PureThy.add_defs_unchecked_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
   2.401 +
   2.402 +in
   2.403 +
   2.404 +val add_primrec = gen_primrec thy_note (thy_def false);
   2.405 +val add_primrec_unchecked = gen_primrec thy_note (thy_def true);
   2.406 +val add_primrec_i = gen_primrec_i thy_note (thy_def false);
   2.407 +val add_primrec_unchecked_i = gen_primrec_i thy_note (thy_def true);
   2.408 +
   2.409 +end; (*local*)
   2.410 +
   2.411 +
   2.412 +(* outer syntax *)
   2.413 +
   2.414 +local structure P = OuterParse and K = OuterKeyword in
   2.415 +
   2.416 +val parser1 = P.$$$ "freshness_context" |-- P.$$$ ":" |-- (P.term >> SOME);
   2.417 +val parser2 =
   2.418 +  P.$$$ "invariant" |-- P.$$$ ":" |--
   2.419 +    (Scan.repeat1 P.term >> SOME) -- Scan.optional parser1 NONE ||
   2.420 +  (parser1 >> pair NONE);
   2.421 +val parser3 =
   2.422 +  P.name -- Scan.optional parser2 (NONE, NONE) ||
   2.423 +  (parser2 >> pair "");
   2.424 +val parser4 =
   2.425 +  (P.$$$ "unchecked" >> K true) -- Scan.optional parser3 ("", (NONE, NONE)) ||
   2.426 +  (parser3 >> pair false);
   2.427 +val options =
   2.428 +  Scan.optional (P.$$$ "(" |-- P.!!!
   2.429 +    (parser4 --| P.$$$ ")")) (false, ("", (NONE, NONE)));
   2.430 +
   2.431 +val primrec_decl =
   2.432 +  options -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
   2.433 +
   2.434 +val primrecP =
   2.435 +  OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal
   2.436 +    (primrec_decl >> (fn ((unchecked, (alt_name, (invs, fctxt))), eqns) =>
   2.437 +      Toplevel.theory_to_proof
   2.438 +        ((if unchecked then add_primrec_unchecked else add_primrec) alt_name invs fctxt
   2.439 +          (map P.triple_swap eqns))));
   2.440 +
   2.441 +val _ = OuterSyntax.add_parsers [primrecP];
   2.442 +val _ = OuterSyntax.add_keywords ["invariant", "freshness_context"];
   2.443 +
   2.444 +end;
   2.445 +
   2.446 +
   2.447 +end;
   2.448 +