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