src/ZF/Tools/datatype_package.ML
author wenzelm
Thu Sep 15 17:16:56 2005 +0200 (2005-09-15)
changeset 17412 e26cb20ef0cc
parent 17261 193b84a70ca4
child 17936 308b19d78764
permissions -rw-r--r--
TableFun/Symtab: curried lookup and update;
     1 (*  Title:      ZF/Tools/datatype_package.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Datatype/Codatatype Definitions
     7 
     8 The functor will be instantiated for normal sums/products (datatype defs)
     9                          and non-standard sums/products (codatatype defs)
    10 
    11 Sums are used only for mutual recursion;
    12 Products are used only to derive "streamlined" induction rules for relations
    13 *)
    14 
    15 type datatype_result =
    16    {con_defs   : thm list,             (*definitions made in thy*)
    17     case_eqns  : thm list,             (*equations for case operator*)
    18     recursor_eqns : thm list,          (*equations for the recursor*)
    19     free_iffs  : thm list,             (*freeness rewrite rules*)
    20     free_SEs   : thm list,             (*freeness destruct rules*)
    21     mk_free    : string -> thm};       (*function to make freeness theorems*)
    22 
    23 signature DATATYPE_ARG =
    24 sig
    25   val intrs : thm list
    26   val elims : thm list
    27 end;
    28 
    29 (*Functor's result signature*)
    30 signature DATATYPE_PACKAGE =
    31 sig
    32   (*Insert definitions for the recursive sets, which
    33      must *already* be declared as constants in parent theory!*)
    34   val add_datatype_i: term * term list -> Ind_Syntax.constructor_spec list list ->
    35     thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
    36   val add_datatype_x: string * string list -> (string * string list * mixfix) list list ->
    37     thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
    38   val add_datatype: string * string list -> (string * string list * mixfix) list list ->
    39     (thmref * Attrib.src list) list * (thmref * Attrib.src list) list *
    40     (thmref * Attrib.src list) list -> theory -> theory * inductive_result * datatype_result
    41 end;
    42 
    43 functor Add_datatype_def_Fun
    44  (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU
    45   and Ind_Package : INDUCTIVE_PACKAGE
    46   and Datatype_Arg : DATATYPE_ARG
    47   val coind : bool): DATATYPE_PACKAGE =
    48 struct
    49 
    50 (*con_ty_lists specifies the constructors in the form (name, prems, mixfix) *)
    51 
    52 fun add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy =
    53  let
    54   val dummy = (*has essential ancestors?*)
    55     Theory.requires thy "Datatype" "(co)datatype definitions";
    56 
    57   val rec_hds = map head_of rec_tms;
    58 
    59   val dummy = assert_all is_Const rec_hds
    60           (fn t => "Datatype set not previously declared as constant: " ^
    61                    Sign.string_of_term (sign_of thy) t);
    62 
    63   val rec_names = map (#1 o dest_Const) rec_hds
    64   val rec_base_names = map Sign.base_name rec_names
    65   val big_rec_base_name = space_implode "_" rec_base_names
    66 
    67   val thy_path = thy |> Theory.add_path big_rec_base_name
    68   val sign = sign_of thy_path
    69 
    70   val big_rec_name = Sign.intern_const sign big_rec_base_name;
    71 
    72   val intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists);
    73 
    74   val dummy =
    75     writeln ((if coind then "Codatatype" else "Datatype") ^ " definition " ^ quote big_rec_name);
    76 
    77   val case_varname = "f";                (*name for case variables*)
    78 
    79   (** Define the constructors **)
    80 
    81   (*The empty tuple is 0*)
    82   fun mk_tuple [] = Const("0",iT)
    83     | mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args;
    84 
    85   fun mk_inject n k u = access_bal (fn t => Su.inl $ t, fn t => Su.inr $ t, u) n k;
    86 
    87   val npart = length rec_names;  (*number of mutually recursive parts*)
    88 
    89 
    90   val full_name = Sign.full_name sign;
    91 
    92   (*Make constructor definition;
    93     kpart is the number of this mutually recursive part*)
    94   fun mk_con_defs (kpart, con_ty_list) =
    95     let val ncon = length con_ty_list    (*number of constructors*)
    96         fun mk_def (((id,T,syn), name, args, prems), kcon) =
    97               (*kcon is index of constructor*)
    98             Logic.mk_defpair (list_comb (Const (full_name name, T), args),
    99                         mk_inject npart kpart
   100                         (mk_inject ncon kcon (mk_tuple args)))
   101     in  ListPair.map mk_def (con_ty_list, 1 upto ncon)  end;
   102 
   103 
   104   (*** Define the case operator ***)
   105 
   106   (*Combine split terms using case; yields the case operator for one part*)
   107   fun call_case case_list =
   108     let fun call_f (free,[]) = Abs("null", iT, free)
   109           | call_f (free,args) =
   110                 CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
   111                             Ind_Syntax.iT
   112                             free
   113     in  fold_bal (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list)  end;
   114 
   115   (** Generating function variables for the case definition
   116       Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
   117 
   118   (*The function variable for a single constructor*)
   119   fun add_case (((_, T, _), name, args, _), (opno, cases)) =
   120     if Syntax.is_identifier name then
   121       (opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases)
   122     else
   123       (opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args)
   124        :: cases);
   125 
   126   (*Treatment of a list of constructors, for one part
   127     Result adds a list of terms, each a function variable with arguments*)
   128   fun add_case_list (con_ty_list, (opno, case_lists)) =
   129     let val (opno', case_list) = foldr add_case (opno, []) con_ty_list
   130     in (opno', case_list :: case_lists) end;
   131 
   132   (*Treatment of all parts*)
   133   val (_, case_lists) = foldr add_case_list (1,[]) con_ty_lists;
   134 
   135   (*extract the types of all the variables*)
   136   val case_typ = List.concat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
   137 
   138   val case_base_name = big_rec_base_name ^ "_case";
   139   val case_name = full_name case_base_name;
   140 
   141   (*The list of all the function variables*)
   142   val case_args = List.concat (map (map #1) case_lists);
   143 
   144   val case_const = Const (case_name, case_typ);
   145   val case_tm = list_comb (case_const, case_args);
   146 
   147   val case_def = Logic.mk_defpair
   148            (case_tm, fold_bal (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
   149 
   150 
   151   (** Generating function variables for the recursor definition
   152       Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
   153 
   154   (*a recursive call for x is the application rec`x  *)
   155   val rec_call = Ind_Syntax.apply_const $ Free ("rec", iT);
   156 
   157   (*look back down the "case args" (which have been reversed) to
   158     determine the de Bruijn index*)
   159   fun make_rec_call ([], _) arg = error
   160           "Internal error in datatype (variable name mismatch)"
   161     | make_rec_call (a::args, i) arg =
   162            if a = arg then rec_call $ Bound i
   163            else make_rec_call (args, i+1) arg;
   164 
   165   (*creates one case of the "X_case" definition of the recursor*)
   166   fun call_recursor ((case_var, case_args), (recursor_var, recursor_args)) =
   167       let fun add_abs (Free(a,T), u) = Abs(a,T,u)
   168           val ncase_args = length case_args
   169           val bound_args = map Bound ((ncase_args - 1) downto 0)
   170           val rec_args = map (make_rec_call (rev case_args,0))
   171                          (List.drop(recursor_args, ncase_args))
   172       in
   173           foldr add_abs
   174             (list_comb (recursor_var,
   175                         bound_args @ rec_args)) case_args
   176       end
   177 
   178   (*Find each recursive argument and add a recursive call for it*)
   179   fun rec_args [] = []
   180     | rec_args ((Const("op :",_)$arg$X)::prems) =
   181        (case head_of X of
   182             Const(a,_) => (*recursive occurrence?*)
   183                           if a mem_string rec_names
   184                               then arg :: rec_args prems
   185                           else rec_args prems
   186           | _ => rec_args prems)
   187     | rec_args (_::prems) = rec_args prems;
   188 
   189   (*Add an argument position for each occurrence of a recursive set.
   190     Strictly speaking, the recursive arguments are the LAST of the function
   191     variable, but they all have type "i" anyway*)
   192   fun add_rec_args args' T = (map (fn _ => iT) args') ---> T
   193 
   194   (*Plug in the function variable type needed for the recursor
   195     as well as the new arguments (recursive calls)*)
   196   fun rec_ty_elem ((id, T, syn), name, args, prems) =
   197       let val args' = rec_args prems
   198       in ((id, add_rec_args args' T, syn),
   199           name, args @ args', prems)
   200       end;
   201 
   202   val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists);
   203 
   204   (*Treatment of all parts*)
   205   val (_, recursor_lists) = foldr add_case_list (1,[]) rec_ty_lists;
   206 
   207   (*extract the types of all the variables*)
   208   val recursor_typ = List.concat (map (map (#2 o #1)) rec_ty_lists)
   209                          ---> (iT-->iT);
   210 
   211   val recursor_base_name = big_rec_base_name ^ "_rec";
   212   val recursor_name = full_name recursor_base_name;
   213 
   214   (*The list of all the function variables*)
   215   val recursor_args = List.concat (map (map #1) recursor_lists);
   216 
   217   val recursor_tm =
   218     list_comb (Const (recursor_name, recursor_typ), recursor_args);
   219 
   220   val recursor_cases = map call_recursor
   221                          (List.concat case_lists ~~ List.concat recursor_lists)
   222 
   223   val recursor_def =
   224       Logic.mk_defpair
   225         (recursor_tm,
   226          Ind_Syntax.Vrecursor_const $
   227            absfree ("rec", iT, list_comb (case_const, recursor_cases)));
   228 
   229   (* Build the new theory *)
   230 
   231   val need_recursor = (not coind andalso recursor_typ <> case_typ);
   232 
   233   fun add_recursor thy =
   234       if need_recursor then
   235            thy |> Theory.add_consts_i
   236                     [(recursor_base_name, recursor_typ, NoSyn)]
   237                |> (#1 o PureThy.add_defs_i false [Thm.no_attributes recursor_def])
   238       else thy;
   239 
   240   val (thy0, con_defs) = thy_path
   241              |> Theory.add_consts_i
   242                  ((case_base_name, case_typ, NoSyn) ::
   243                   map #1 (List.concat con_ty_lists))
   244              |> PureThy.add_defs_i false
   245                  (map Thm.no_attributes
   246                   (case_def ::
   247                    List.concat (ListPair.map mk_con_defs
   248                          (1 upto npart, con_ty_lists))))
   249              |>> add_recursor
   250              |>> Theory.parent_path
   251 
   252   val intr_names = map #2 (List.concat con_ty_lists);
   253   val (thy1, ind_result) =
   254     thy0 |> Ind_Package.add_inductive_i
   255       false (rec_tms, dom_sum) (map Thm.no_attributes (intr_names ~~ intr_tms))
   256       (monos, con_defs, type_intrs @ Datatype_Arg.intrs, type_elims @ Datatype_Arg.elims);
   257 
   258   (**** Now prove the datatype theorems in this theory ****)
   259 
   260 
   261   (*** Prove the case theorems ***)
   262 
   263   (*Each equation has the form
   264     case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
   265   fun mk_case_eqn (((_,T,_), name, args, _), case_free) =
   266     FOLogic.mk_Trueprop
   267       (FOLogic.mk_eq
   268        (case_tm $
   269          (list_comb (Const (Sign.intern_const (sign_of thy1) name,T),
   270                      args)),
   271         list_comb (case_free, args)));
   272 
   273   val case_trans = hd con_defs RS Ind_Syntax.def_trans
   274   and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans;
   275 
   276   (*Proves a single case equation.  Could use simp_tac, but it's slower!*)
   277   fun case_tacsf con_def _ =
   278     [rewtac con_def,
   279      rtac case_trans 1,
   280      REPEAT (resolve_tac [refl, split_trans,
   281                           Su.case_inl RS trans,
   282                           Su.case_inr RS trans] 1)];
   283 
   284   fun prove_case_eqn (arg,con_def) =
   285       prove_goalw_cterm []
   286         (Ind_Syntax.traceIt "next case equation = "
   287            (cterm_of (sign_of thy1) (mk_case_eqn arg)))
   288         (case_tacsf con_def);
   289 
   290   val free_iffs = map standard (con_defs RL [Ind_Syntax.def_swap_iff]);
   291 
   292   val case_eqns =
   293       map prove_case_eqn
   294          (List.concat con_ty_lists ~~ case_args ~~ tl con_defs);
   295 
   296   (*** Prove the recursor theorems ***)
   297 
   298   val recursor_eqns = case try (get_def thy1) recursor_base_name of
   299      NONE => (writeln "  [ No recursion operator ]";
   300               [])
   301    | SOME recursor_def =>
   302       let
   303         (*Replace subterms rec`x (where rec is a Free var) by recursor_tm(x) *)
   304         fun subst_rec (Const("op `",_) $ Free _ $ arg) = recursor_tm $ arg
   305           | subst_rec tm =
   306               let val (head, args) = strip_comb tm
   307               in  list_comb (head, map subst_rec args)  end;
   308 
   309         (*Each equation has the form
   310           REC(coni(args)) = f_coni(args, REC(rec_arg), ...)
   311           where REC = recursor(f_con1,...,f_conn) and rec_arg is a recursive
   312           constructor argument.*)
   313         fun mk_recursor_eqn (((_,T,_), name, args, _), recursor_case) =
   314           FOLogic.mk_Trueprop
   315            (FOLogic.mk_eq
   316             (recursor_tm $
   317              (list_comb (Const (Sign.intern_const (sign_of thy1) name,T),
   318                          args)),
   319              subst_rec (Library.foldl betapply (recursor_case, args))));
   320 
   321         val recursor_trans = recursor_def RS def_Vrecursor RS trans;
   322 
   323         (*Proves a single recursor equation.*)
   324         fun recursor_tacsf _ =
   325           [rtac recursor_trans 1,
   326            simp_tac (rank_ss addsimps case_eqns) 1,
   327            IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)];
   328 
   329         fun prove_recursor_eqn arg =
   330             prove_goalw_cterm []
   331               (Ind_Syntax.traceIt "next recursor equation = "
   332                 (cterm_of (sign_of thy1) (mk_recursor_eqn arg)))
   333               recursor_tacsf
   334       in
   335          map prove_recursor_eqn (List.concat con_ty_lists ~~ recursor_cases)
   336       end
   337 
   338   val constructors =
   339       map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);
   340 
   341   val free_SEs = map standard (Ind_Syntax.mk_free_SEs free_iffs);
   342 
   343   val {intrs, elim, induct, mutual_induct, ...} = ind_result
   344 
   345   (*Typical theorems have the form ~con1=con2, con1=con2==>False,
   346     con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc.  *)
   347   fun mk_free s =
   348       prove_goalw (theory_of_thm elim)   (*Don't use thy1: it will be stale*)
   349                   con_defs s
   350         (fn prems => [cut_facts_tac prems 1,
   351                       fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1]);
   352 
   353   val simps = case_eqns @ recursor_eqns;
   354 
   355   val dt_info =
   356         {inductive = true,
   357          constructors = constructors,
   358          rec_rewrites = recursor_eqns,
   359          case_rewrites = case_eqns,
   360          induct = induct,
   361          mutual_induct = mutual_induct,
   362          exhaustion = elim};
   363 
   364   val con_info =
   365         {big_rec_name = big_rec_name,
   366          constructors = constructors,
   367             (*let primrec handle definition by cases*)
   368          free_iffs = free_iffs,
   369          rec_rewrites = (case recursor_eqns of
   370                              [] => case_eqns | _ => recursor_eqns)};
   371 
   372   (*associate with each constructor the datatype name and rewrites*)
   373   val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
   374 
   375  in
   376   (*Updating theory components: simprules and datatype info*)
   377   (thy1 |> Theory.add_path big_rec_base_name
   378         |> (#1 o PureThy.add_thmss
   379          [(("simps", simps), [Simplifier.simp_add_global]),
   380           (("", intrs), [Classical.safe_intro_global]),
   381           (("con_defs", con_defs), []),
   382           (("case_eqns", case_eqns), []),
   383           (("recursor_eqns", recursor_eqns), []),
   384           (("free_iffs", free_iffs), []),
   385           (("free_elims", free_SEs), [])])
   386         |> DatatypesData.map (Symtab.update (big_rec_name, dt_info))
   387         |> ConstructorsData.map (fold Symtab.update con_pairs)
   388         |> Theory.parent_path,
   389    ind_result,
   390    {con_defs = con_defs,
   391     case_eqns = case_eqns,
   392     recursor_eqns = recursor_eqns,
   393     free_iffs = free_iffs,
   394     free_SEs = free_SEs,
   395     mk_free = mk_free})
   396   end;
   397 
   398 
   399 fun add_datatype_x (sdom, srec_tms) scon_ty_lists (monos, type_intrs, type_elims) thy =
   400   let
   401     val sign = sign_of thy;
   402     val read_i = Sign.simple_read_term sign Ind_Syntax.iT;
   403     val rec_tms = map read_i srec_tms;
   404     val con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists
   405     val dom_sum =
   406       if sdom = "" then Ind_Syntax.data_domain coind (rec_tms, con_ty_lists)
   407       else read_i sdom;
   408   in add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy end;
   409 
   410 fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy =
   411   let
   412     val (thy', ((monos, type_intrs), type_elims)) = thy
   413       |> IsarThy.apply_theorems raw_monos
   414       |>>> IsarThy.apply_theorems raw_type_intrs
   415       |>>> IsarThy.apply_theorems raw_type_elims;
   416   in add_datatype_x (sdom, srec_tms) scon_ty_lists (monos, type_intrs, type_elims) thy' end;
   417 
   418 
   419 (* outer syntax *)
   420 
   421 local structure P = OuterParse and K = OuterKeyword in
   422 
   423 fun mk_datatype ((((dom, dts), monos), type_intrs), type_elims) =
   424   #1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims);
   425 
   426 val con_decl =
   427   P.name -- Scan.optional (P.$$$ "(" |-- P.list1 P.term --| P.$$$ ")") [] -- P.opt_mixfix
   428   >> P.triple1;
   429 
   430 val datatype_decl =
   431   (Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
   432   P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) --
   433   Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] --
   434   Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1) [] --
   435   Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1) []
   436   >> (Toplevel.theory o mk_datatype);
   437 
   438 val coind_prefix = if coind then "co" else "";
   439 
   440 val inductiveP = OuterSyntax.command (coind_prefix ^ "datatype")
   441   ("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl;
   442 
   443 val _ = OuterSyntax.add_parsers [inductiveP];
   444 
   445 end;
   446 
   447 end;
   448