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