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