src/HOL/Tools/Datatype/datatype_data.ML
changeset 33963 977b94b64905
parent 33959 2afc55e8ed27
equal deleted inserted replaced
33962:abf9fa17452a 33963:977b94b64905
       
     1 (*  Title:      HOL/Tools/datatype.ML
       
     2     Author:     Stefan Berghofer, TU Muenchen
       
     3 
       
     4 Datatype package for Isabelle/HOL.
       
     5 *)
       
     6 
       
     7 signature DATATYPE_DATA =
       
     8 sig
       
     9   include DATATYPE_COMMON
       
    10   val derive_datatype_props : config -> string list -> string list option
       
    11     -> descr list -> (string * sort) list -> thm -> thm list list -> thm list list
       
    12     -> theory -> string list * theory
       
    13   val rep_datatype : config -> (string list -> Proof.context -> Proof.context)
       
    14     -> string list option -> term list -> theory -> Proof.state
       
    15   val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
       
    16   val get_info : theory -> string -> info option
       
    17   val the_info : theory -> string -> info
       
    18   val the_descr : theory -> string list
       
    19     -> descr * (string * sort) list * string list
       
    20       * string * (string list * string list) * (typ list * typ list)
       
    21   val the_spec : theory -> string -> (string * sort) list * (string * typ list) list
       
    22   val all_distincts : theory -> typ list -> thm list list
       
    23   val get_constrs : theory -> string -> (string * typ) list option
       
    24   val get_all : theory -> info Symtab.table
       
    25   val info_of_constr : theory -> string * typ -> info option
       
    26   val info_of_case : theory -> string -> info option
       
    27   val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
       
    28   val make_case :  Proof.context -> DatatypeCase.config -> string list -> term ->
       
    29     (term * term) list -> term * (term * (int * bool)) list
       
    30   val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
       
    31   val read_typ: theory -> string -> (string * sort) list -> typ * (string * sort) list
       
    32   val cert_typ: theory -> typ -> (string * sort) list -> typ * (string * sort) list
       
    33   val mk_case_names_induct: descr -> attribute
       
    34   val setup: theory -> theory
       
    35 end;
       
    36 
       
    37 structure Datatype_Data: DATATYPE_DATA =
       
    38 struct
       
    39 
       
    40 open DatatypeAux;
       
    41 
       
    42 (** theory data **)
       
    43 
       
    44 (* data management *)
       
    45 
       
    46 structure DatatypesData = Theory_Data
       
    47 (
       
    48   type T =
       
    49     {types: info Symtab.table,
       
    50      constrs: (string * info) list Symtab.table,
       
    51      cases: info Symtab.table};
       
    52 
       
    53   val empty =
       
    54     {types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
       
    55   val extend = I;
       
    56   fun merge
       
    57     ({types = types1, constrs = constrs1, cases = cases1},
       
    58      {types = types2, constrs = constrs2, cases = cases2}) : T =
       
    59     {types = Symtab.merge (K true) (types1, types2),
       
    60      constrs = Symtab.join (K (AList.merge (op =) (K true))) (constrs1, constrs2),
       
    61      cases = Symtab.merge (K true) (cases1, cases2)};
       
    62 );
       
    63 
       
    64 val get_all = #types o DatatypesData.get;
       
    65 val get_info = Symtab.lookup o get_all;
       
    66 
       
    67 fun the_info thy name =
       
    68   (case get_info thy name of
       
    69     SOME info => info
       
    70   | NONE => error ("Unknown datatype " ^ quote name));
       
    71 
       
    72 fun info_of_constr thy (c, T) =
       
    73   let
       
    74     val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c;
       
    75     val hint = case strip_type T of (_, Type (tyco, _)) => SOME tyco | _ => NONE;
       
    76     val default = if null tab then NONE
       
    77       else SOME (snd (Library.last_elem tab))
       
    78         (*conservative wrt. overloaded constructors*);
       
    79   in case hint
       
    80    of NONE => default
       
    81     | SOME tyco => case AList.lookup (op =) tab tyco
       
    82        of NONE => default (*permissive*)
       
    83         | SOME info => SOME info
       
    84   end;
       
    85 
       
    86 val info_of_case = Symtab.lookup o #cases o DatatypesData.get;
       
    87 
       
    88 fun register (dt_infos : (string * info) list) =
       
    89   DatatypesData.map (fn {types, constrs, cases} =>
       
    90     {types = types |> fold Symtab.update dt_infos,
       
    91      constrs = constrs |> fold (fn (constr, dtname_info) =>
       
    92          Symtab.map_default (constr, []) (cons dtname_info))
       
    93        (maps (fn (dtname, info as {descr, index, ...}) =>
       
    94           map (rpair (dtname, info) o fst)
       
    95             (#3 (the (AList.lookup op = descr index)))) dt_infos),
       
    96      cases = cases |> fold Symtab.update
       
    97        (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)});
       
    98 
       
    99 
       
   100 (* complex queries *)
       
   101 
       
   102 fun the_spec thy dtco =
       
   103   let
       
   104     val info as { descr, index, sorts = raw_sorts, ... } = the_info thy dtco;
       
   105     val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr index;
       
   106     val sorts = map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v))
       
   107       o DatatypeAux.dest_DtTFree) dtys;
       
   108     val cos = map
       
   109       (fn (co, tys) => (co, map (DatatypeAux.typ_of_dtyp descr sorts) tys)) raw_cos;
       
   110   in (sorts, cos) end;
       
   111 
       
   112 fun the_descr thy (raw_tycos as raw_tyco :: _) =
       
   113   let
       
   114     val info = the_info thy raw_tyco;
       
   115     val descr = #descr info;
       
   116 
       
   117     val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr (#index info);
       
   118     val vs = map ((fn v => (v, (the o AList.lookup (op =) (#sorts info)) v))
       
   119       o dest_DtTFree) dtys;
       
   120 
       
   121     fun is_DtTFree (DtTFree _) = true
       
   122       | is_DtTFree _ = false
       
   123     val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr;
       
   124     val protoTs as (dataTs, _) = chop k descr
       
   125       |> (pairself o map) (fn (_, (tyco, dTs, _)) => (tyco, map (typ_of_dtyp descr vs) dTs));
       
   126     
       
   127     val tycos = map fst dataTs;
       
   128     val _ = if eq_set (op =) (tycos, raw_tycos) then ()
       
   129       else error ("Type constructors " ^ commas (map quote raw_tycos)
       
   130         ^ " do not belong exhaustively to one mutual recursive datatype");
       
   131 
       
   132     val (Ts, Us) = (pairself o map) Type protoTs;
       
   133 
       
   134     val names = map Long_Name.base_name (the_default tycos (#alt_names info));
       
   135     val (auxnames, _) = Name.make_context names
       
   136       |> fold_map (yield_singleton Name.variants o name_of_typ) Us;
       
   137     val prefix = space_implode "_" names;
       
   138 
       
   139   in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end;
       
   140 
       
   141 fun all_distincts thy Ts =
       
   142   let
       
   143     fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
       
   144       | add_tycos _ = I;
       
   145     val tycos = fold add_tycos Ts [];
       
   146   in map_filter (Option.map #distinct o get_info thy) tycos end;
       
   147 
       
   148 fun get_constrs thy dtco =
       
   149   case try (the_spec thy) dtco
       
   150    of SOME (sorts, cos) =>
       
   151         let
       
   152           fun subst (v, sort) = TVar ((v, 0), sort);
       
   153           fun subst_ty (TFree v) = subst v
       
   154             | subst_ty ty = ty;
       
   155           val dty = Type (dtco, map subst sorts);
       
   156           fun mk_co (co, tys) = (co, map (Term.map_atyps subst_ty) tys ---> dty);
       
   157         in SOME (map mk_co cos) end
       
   158     | NONE => NONE;
       
   159 
       
   160 
       
   161 
       
   162 (** various auxiliary **)
       
   163 
       
   164 (* prepare datatype specifications *)
       
   165 
       
   166 fun read_typ thy str sorts =
       
   167   let
       
   168     val ctxt = ProofContext.init thy
       
   169       |> fold (Variable.declare_typ o TFree) sorts;
       
   170     val T = Syntax.read_typ ctxt str;
       
   171   in (T, Term.add_tfreesT T sorts) end;
       
   172 
       
   173 fun cert_typ sign raw_T sorts =
       
   174   let
       
   175     val T = Type.no_tvars (Sign.certify_typ sign raw_T)
       
   176       handle TYPE (msg, _, _) => error msg;
       
   177     val sorts' = Term.add_tfreesT T sorts;
       
   178     val _ =
       
   179       case duplicates (op =) (map fst sorts') of
       
   180         [] => ()
       
   181       | dups => error ("Inconsistent sort constraints for " ^ commas dups)
       
   182   in (T, sorts') end;
       
   183 
       
   184 
       
   185 (* case names *)
       
   186 
       
   187 local
       
   188 
       
   189 fun dt_recs (DtTFree _) = []
       
   190   | dt_recs (DtType (_, dts)) = maps dt_recs dts
       
   191   | dt_recs (DtRec i) = [i];
       
   192 
       
   193 fun dt_cases (descr: descr) (_, args, constrs) =
       
   194   let
       
   195     fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
       
   196     val bnames = map the_bname (distinct (op =) (maps dt_recs args));
       
   197   in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
       
   198 
       
   199 fun induct_cases descr =
       
   200   DatatypeProp.indexify_names (maps (dt_cases descr) (map #2 descr));
       
   201 
       
   202 fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i));
       
   203 
       
   204 in
       
   205 
       
   206 fun mk_case_names_induct descr = Rule_Cases.case_names (induct_cases descr);
       
   207 
       
   208 fun mk_case_names_exhausts descr new =
       
   209   map (Rule_Cases.case_names o exhaust_cases descr o #1)
       
   210     (filter (fn ((_, (name, _, _))) => member (op =) new name) descr);
       
   211 
       
   212 end;
       
   213 
       
   214 
       
   215 (* translation rules for case *)
       
   216 
       
   217 fun make_case ctxt = DatatypeCase.make_case
       
   218   (info_of_constr (ProofContext.theory_of ctxt)) ctxt;
       
   219 
       
   220 fun strip_case ctxt = DatatypeCase.strip_case
       
   221   (info_of_case (ProofContext.theory_of ctxt));
       
   222 
       
   223 fun add_case_tr' case_names thy =
       
   224   Sign.add_advanced_trfuns ([], [],
       
   225     map (fn case_name =>
       
   226       let val case_name' = Sign.const_syntax_name thy case_name
       
   227       in (case_name', DatatypeCase.case_tr' info_of_case case_name')
       
   228       end) case_names, []) thy;
       
   229 
       
   230 val trfun_setup =
       
   231   Sign.add_advanced_trfuns ([],
       
   232     [("_case_syntax", DatatypeCase.case_tr true info_of_constr)],
       
   233     [], []);
       
   234 
       
   235 
       
   236 
       
   237 (** document antiquotation **)
       
   238 
       
   239 val _ = ThyOutput.antiquotation "datatype" Args.tyname
       
   240   (fn {source = src, context = ctxt, ...} => fn dtco =>
       
   241     let
       
   242       val thy = ProofContext.theory_of ctxt;
       
   243       val (vs, cos) = the_spec thy dtco;
       
   244       val ty = Type (dtco, map TFree vs);
       
   245       fun pretty_typ_bracket (ty as Type (_, _ :: _)) =
       
   246             Pretty.enclose "(" ")" [Syntax.pretty_typ ctxt ty]
       
   247         | pretty_typ_bracket ty =
       
   248             Syntax.pretty_typ ctxt ty;
       
   249       fun pretty_constr (co, tys) =
       
   250         (Pretty.block o Pretty.breaks)
       
   251           (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
       
   252             map pretty_typ_bracket tys);
       
   253       val pretty_datatype =
       
   254         Pretty.block
       
   255           (Pretty.command "datatype" :: Pretty.brk 1 ::
       
   256            Syntax.pretty_typ ctxt ty ::
       
   257            Pretty.str " =" :: Pretty.brk 1 ::
       
   258            flat (separate [Pretty.brk 1, Pretty.str "| "]
       
   259              (map (single o pretty_constr) cos)));
       
   260     in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end);
       
   261 
       
   262 
       
   263 
       
   264 (** abstract theory extensions relative to a datatype characterisation **)
       
   265 
       
   266 structure Datatype_Interpretation = Interpretation
       
   267   (type T = config * string list val eq: T * T -> bool = eq_snd op =);
       
   268 fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
       
   269 
       
   270 fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites
       
   271     (index, (((((((((((_, (tname, _, _))), inject), distinct),
       
   272       exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong),
       
   273         (split, split_asm))) =
       
   274   (tname,
       
   275    {index = index,
       
   276     alt_names = alt_names,
       
   277     descr = descr,
       
   278     sorts = sorts,
       
   279     inject = inject,
       
   280     distinct = distinct,
       
   281     induct = induct,
       
   282     inducts = inducts,
       
   283     exhaust = exhaust,
       
   284     nchotomy = nchotomy,
       
   285     rec_names = rec_names,
       
   286     rec_rewrites = rec_rewrites,
       
   287     case_name = case_name,
       
   288     case_rewrites = case_rewrites,
       
   289     case_cong = case_cong,
       
   290     weak_case_cong = weak_case_cong,
       
   291     split = split,
       
   292     split_asm = split_asm});
       
   293 
       
   294 fun derive_datatype_props config dt_names alt_names descr sorts
       
   295     induct inject distinct thy1 =
       
   296   let
       
   297     val thy2 = thy1 |> Theory.checkpoint;
       
   298     val flat_descr = flat descr;
       
   299     val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
       
   300     val _ = message config ("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
       
   301 
       
   302     val (exhaust, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names
       
   303       descr sorts induct (mk_case_names_exhausts flat_descr dt_names) thy2;
       
   304     val (nchotomys, thy4) = DatatypeAbsProofs.prove_nchotomys config new_type_names
       
   305       descr sorts exhaust thy3;
       
   306     val ((rec_names, rec_rewrites), thy5) = DatatypeAbsProofs.prove_primrec_thms
       
   307       config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4))
       
   308       inject (distinct, all_distincts thy2 (get_rec_types flat_descr sorts))
       
   309       induct thy4;
       
   310     val ((case_rewrites, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
       
   311       config new_type_names descr sorts rec_names rec_rewrites thy5;
       
   312     val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
       
   313       descr sorts nchotomys case_rewrites thy6;
       
   314     val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
       
   315       descr sorts thy7;
       
   316     val (splits, thy9) = DatatypeAbsProofs.prove_split_thms
       
   317       config new_type_names descr sorts inject distinct exhaust case_rewrites thy8;
       
   318 
       
   319     val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
       
   320     val dt_infos = map_index
       
   321       (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
       
   322       (hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~
       
   323         case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
       
   324     val dt_names = map fst dt_infos;
       
   325     val prfx = Binding.qualify true (space_implode "_" new_type_names);
       
   326     val simps = flat (inject @ distinct @ case_rewrites) @ rec_rewrites;
       
   327     val named_rules = flat (map_index (fn (index, tname) =>
       
   328       [((Binding.empty, [nth inducts index]), [Induct.induct_type tname]),
       
   329        ((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
       
   330     val unnamed_rules = map (fn induct =>
       
   331       ((Binding.empty, [induct]), [Rule_Cases.inner_rule, Induct.induct_type ""]))
       
   332         (drop (length dt_names) inducts);
       
   333   in
       
   334     thy9
       
   335     |> PureThy.add_thmss ([((prfx (Binding.name "simps"), simps), []),
       
   336         ((prfx (Binding.name "inducts"), inducts), []),
       
   337         ((prfx (Binding.name "splits"), maps (fn (x, y) => [x, y]) splits), []),
       
   338         ((Binding.empty, flat case_rewrites @ flat distinct @ rec_rewrites),
       
   339           [Simplifier.simp_add]),
       
   340         ((Binding.empty, rec_rewrites), [Code.add_default_eqn_attribute]),
       
   341         ((Binding.empty, flat inject), [iff_add]),
       
   342         ((Binding.empty, map (fn th => th RS notE) (flat distinct)),
       
   343           [Classical.safe_elim NONE]),
       
   344         ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)])]
       
   345         @ named_rules @ unnamed_rules)
       
   346     |> snd
       
   347     |> add_case_tr' case_names
       
   348     |> register dt_infos
       
   349     |> Datatype_Interpretation.data (config, dt_names)
       
   350     |> pair dt_names
       
   351   end;
       
   352 
       
   353 
       
   354 
       
   355 (** declare existing type as datatype **)
       
   356 
       
   357 fun prove_rep_datatype config dt_names alt_names descr sorts
       
   358     raw_inject half_distinct raw_induct thy1 =
       
   359   let
       
   360     val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
       
   361     val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
       
   362     val (((inject, distinct), [induct]), thy2) =
       
   363       thy1
       
   364       |> store_thmss "inject" new_type_names raw_inject
       
   365       ||>> store_thmss "distinct" new_type_names raw_distinct
       
   366       ||> Sign.add_path (space_implode "_" new_type_names)
       
   367       ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])]
       
   368       ||> Sign.restore_naming thy1;
       
   369   in
       
   370     thy2
       
   371     |> derive_datatype_props config dt_names alt_names [descr] sorts
       
   372          induct inject distinct
       
   373  end;
       
   374 
       
   375 fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
       
   376   let
       
   377     fun constr_of_term (Const (c, T)) = (c, T)
       
   378       | constr_of_term t =
       
   379           error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
       
   380     fun no_constr (c, T) = error ("Bad constructor: "
       
   381       ^ Sign.extern_const thy c ^ "::"
       
   382       ^ Syntax.string_of_typ_global thy T);
       
   383     fun type_of_constr (cT as (_, T)) =
       
   384       let
       
   385         val frees = OldTerm.typ_tfrees T;
       
   386         val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) T
       
   387           handle TYPE _ => no_constr cT
       
   388         val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();
       
   389         val _ = if length frees <> length vs then no_constr cT else ();
       
   390       in (tyco, (vs, cT)) end;
       
   391 
       
   392     val raw_cs = AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts);
       
   393     val _ = case map_filter (fn (tyco, _) =>
       
   394         if Symtab.defined (get_all thy) tyco then SOME tyco else NONE) raw_cs
       
   395      of [] => ()
       
   396       | tycos => error ("Type(s) " ^ commas (map quote tycos)
       
   397           ^ " already represented inductivly");
       
   398     val raw_vss = maps (map (map snd o fst) o snd) raw_cs;
       
   399     val ms = case distinct (op =) (map length raw_vss)
       
   400      of [n] => 0 upto n - 1
       
   401       | _ => error ("Different types in given constructors");
       
   402     fun inter_sort m = map (fn xs => nth xs m) raw_vss
       
   403       |> Library.foldr1 (Sorts.inter_sort (Sign.classes_of thy))
       
   404     val sorts = map inter_sort ms;
       
   405     val vs = Name.names Name.context Name.aT sorts;
       
   406 
       
   407     fun norm_constr (raw_vs, (c, T)) = (c, map_atyps
       
   408       (TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T);
       
   409 
       
   410     val cs = map (apsnd (map norm_constr)) raw_cs;
       
   411     val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
       
   412       o fst o strip_type;
       
   413     val dt_names = map fst cs;
       
   414 
       
   415     fun mk_spec (i, (tyco, constr)) = (i, (tyco,
       
   416       map (DtTFree o fst) vs,
       
   417       (map o apsnd) dtyps_of_typ constr))
       
   418     val descr = map_index mk_spec cs;
       
   419     val injs = DatatypeProp.make_injs [descr] vs;
       
   420     val half_distincts = map snd (DatatypeProp.make_distincts [descr] vs);
       
   421     val ind = DatatypeProp.make_ind [descr] vs;
       
   422     val rules = (map o map o map) Logic.close_form [[[ind]], injs, half_distincts];
       
   423 
       
   424     fun after_qed' raw_thms =
       
   425       let
       
   426         val [[[raw_induct]], raw_inject, half_distinct] =
       
   427           unflat rules (map Drule.zero_var_indexes_list raw_thms);
       
   428             (*FIXME somehow dubious*)
       
   429       in
       
   430         ProofContext.theory_result
       
   431           (prove_rep_datatype config dt_names alt_names descr vs
       
   432             raw_inject half_distinct raw_induct)
       
   433         #-> after_qed
       
   434       end;
       
   435   in
       
   436     thy
       
   437     |> ProofContext.init
       
   438     |> Proof.theorem_i NONE after_qed' ((map o map) (rpair []) (flat rules))
       
   439   end;
       
   440 
       
   441 val rep_datatype = gen_rep_datatype Sign.cert_term;
       
   442 val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I);
       
   443 
       
   444 
       
   445 
       
   446 (** package setup **)
       
   447 
       
   448 (* setup theory *)
       
   449 
       
   450 val setup =
       
   451   trfun_setup #>
       
   452   Datatype_Interpretation.init;
       
   453 
       
   454 
       
   455 (* outer syntax *)
       
   456 
       
   457 local
       
   458 
       
   459 structure P = OuterParse and K = OuterKeyword
       
   460 
       
   461 in
       
   462 
       
   463 val _ =
       
   464   OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal
       
   465     (Scan.option (P.$$$ "(" |-- Scan.repeat1 P.name --| P.$$$ ")") -- Scan.repeat1 P.term
       
   466       >> (fn (alt_names, ts) => Toplevel.print
       
   467            o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
       
   468 
       
   469 end;
       
   470 
       
   471 end;