6052

1 
(* Title: ZF/datatype_package.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1994 University of Cambridge


5 


6 
Fixedpoint definition module  for Inductive/Codatatype Definitions


7 


8 
The functor will be instantiated for normal sums/products (datatype defs)


9 
and nonstandard 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 
(** Datatype information, e.g. associated theorems **)


17 


18 
type datatype_info =


19 
{inductive: bool, (*true if inductive, not coinductive*)


20 
constructors : term list, (*the constructors, as Consts*)


21 
rec_rewrites : thm list, (*recursor equations*)


22 
case_rewrites : thm list, (*case equations*)


23 
induct : thm,


24 
mutual_induct : thm,


25 
exhaustion : thm};


26 


27 
structure DatatypesArgs =


28 
struct


29 
val name = "ZF/datatypes";


30 
type T = datatype_info Symtab.table;


31 


32 
val empty = Symtab.empty;


33 
val prep_ext = I;


34 
val merge: T * T > T = Symtab.merge (K true);


35 


36 
fun print sg tab =


37 
Pretty.writeln (Pretty.strs ("datatypes:" ::


38 
map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab)));


39 
end;


40 


41 
structure DatatypesData = TheoryDataFun(DatatypesArgs);


42 


43 


44 
(** Constructor information: needed to map constructors to datatypes **)


45 


46 
type constructor_info =


47 
{big_rec_name : string, (*name of the mutually recursive set*)


48 
constructors : term list, (*the constructors, as Consts*)


49 
rec_rewrites : thm list}; (*recursor equations*)


50 


51 


52 
structure ConstructorsArgs =


53 
struct


54 
val name = "ZF/constructors"


55 
type T = constructor_info Symtab.table


56 


57 
val empty = Symtab.empty


58 
val prep_ext = I


59 
val merge: T * T > T = Symtab.merge (K true)


60 


61 
fun print sg tab = () (*nothing extra to print*)


62 
end;


63 


64 
structure ConstructorsData = TheoryDataFun(ConstructorsArgs);


65 


66 
val setup_datatypes = [DatatypesData.init, ConstructorsData.init];


67 


68 


69 
type datatype_result =


70 
{con_defs : thm list, (*definitions made in thy*)


71 
case_eqns : thm list, (*equations for case operator*)


72 
recursor_eqns : thm list, (*equations for the recursor*)


73 
free_iffs : thm list, (*freeness rewrite rules*)


74 
free_SEs : thm list, (*freeness destruct rules*)


75 
mk_free : string > thm}; (*makes freeness theorems*)


76 


77 


78 
signature DATATYPE_ARG =


79 
sig


80 
val intrs : thm list


81 
val elims : thm list


82 
end;


83 


84 


85 
(*Functor's result signature*)


86 
signature DATATYPE_PACKAGE =


87 
sig


88 


89 
(*Insert definitions for the recursive sets, which


90 
must *already* be declared as constants in parent theory!*)


91 
val add_datatype_i :


92 
term * term list * Ind_Syntax.constructor_spec list list *


93 
thm list * thm list * thm list


94 
> theory > theory * inductive_result * datatype_result


95 


96 
val add_datatype :


97 
string * string list *


98 
(string * string list * mixfix) list list *


99 
thm list * thm list * thm list


100 
> theory > theory * inductive_result * datatype_result


101 


102 
end;


103 


104 


105 
(*Declares functions to add fixedpoint/constructor defs to a theory.


106 
Recursive sets must *already* be declared as constants.*)


107 
functor Add_datatype_def_Fun


108 
(structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU


109 
and Ind_Package : INDUCTIVE_PACKAGE


110 
and Datatype_Arg : DATATYPE_ARG)


111 
: DATATYPE_PACKAGE =


112 
struct


113 


114 


115 
(*con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)


116 
fun add_datatype_i (dom_sum, rec_tms, con_ty_lists,


117 
monos, type_intrs, type_elims) thy =


118 
let


119 
open BasisLibrary


120 
val dummy = (*has essential ancestors?*)


121 
Theory.requires thy "Datatype" "(co)datatype definitions";


122 


123 


124 
val rec_names = map (#1 o dest_Const o head_of) rec_tms


125 
val rec_base_names = map Sign.base_name rec_names


126 
val big_rec_base_name = space_implode "_" rec_base_names


127 


128 
val thy_path = thy > Theory.add_path big_rec_base_name


129 
val sign = sign_of thy_path


130 


131 
val big_rec_name = Sign.intern_const sign big_rec_base_name;


132 


133 
val intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists)


134 


135 
val dummy =


136 
writeln ((if (#1 (dest_Const Fp.oper) = "lfp") then "Datatype"


137 
else "Codatatype")


138 
^ " definition " ^ big_rec_name)


139 


140 
val case_varname = "f"; (*name for case variables*)


141 


142 
(** Define the constructors **)


143 


144 
(*The empty tuple is 0*)


145 
fun mk_tuple [] = Const("0",iT)


146 
 mk_tuple args = foldr1 (app Pr.pair) args;


147 


148 
fun mk_inject n k u = access_bal (ap Su.inl, ap Su.inr, u) n k;


149 


150 
val npart = length rec_names; (*number of mutually recursive parts*)


151 


152 


153 
val full_name = Sign.full_name sign;


154 


155 
(*Make constructor definition;


156 
kpart is the number of this mutually recursive part*)


157 
fun mk_con_defs (kpart, con_ty_list) =


158 
let val ncon = length con_ty_list (*number of constructors*)


159 
fun mk_def (((id,T,syn), name, args, prems), kcon) =


160 
(*kcon is index of constructor*)


161 
Logic.mk_defpair (list_comb (Const (full_name name, T), args),


162 
mk_inject npart kpart


163 
(mk_inject ncon kcon (mk_tuple args)))


164 
in ListPair.map mk_def (con_ty_list, 1 upto ncon) end;


165 


166 


167 
(*** Define the case operator ***)


168 


169 
(*Combine split terms using case; yields the case operator for one part*)


170 
fun call_case case_list =


171 
let fun call_f (free,[]) = Abs("null", iT, free)


172 
 call_f (free,args) =


173 
CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))


174 
Ind_Syntax.iT


175 
free


176 
in fold_bal (app Su.elim) (map call_f case_list) end;


177 


178 
(** Generating function variables for the case definition


179 
Nonidentifiers (e.g. infixes) get a name of the form f_op_nnn. **)


180 


181 
(*The function variable for a single constructor*)


182 
fun add_case (((_, T, _), name, args, _), (opno, cases)) =


183 
if Syntax.is_identifier name then


184 
(opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases)


185 
else


186 
(opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args)


187 
:: cases);


188 


189 
(*Treatment of a list of constructors, for one part


190 
Result adds a list of terms, each a function variable with arguments*)


191 
fun add_case_list (con_ty_list, (opno, case_lists)) =


192 
let val (opno', case_list) = foldr add_case (con_ty_list, (opno, []))


193 
in (opno', case_list :: case_lists) end;


194 


195 
(*Treatment of all parts*)


196 
val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));


197 


198 
(*extract the types of all the variables*)


199 
val case_typ = flat (map (map (#2 o #1)) con_ty_lists) > (iT>iT);


200 


201 
val case_base_name = big_rec_base_name ^ "_case";


202 
val case_name = full_name case_base_name;


203 


204 
(*The list of all the function variables*)


205 
val case_args = flat (map (map #1) case_lists);


206 


207 
val case_const = Const (case_name, case_typ);


208 
val case_tm = list_comb (case_const, case_args);


209 


210 
val case_def = Logic.mk_defpair


211 
(case_tm, fold_bal (app Su.elim) (map call_case case_lists));


212 


213 


214 
(** Generating function variables for the recursor definition


215 
Nonidentifiers (e.g. infixes) get a name of the form f_op_nnn. **)


216 


217 
(*a recursive call for x is the application rec`x *)


218 
val rec_call = Ind_Syntax.apply_const $ Free ("rec", iT);


219 


220 
(*look back down the "case args" (which have been reversed) to


221 
determine the de Bruijn index*)


222 
fun make_rec_call ([], _) arg = error


223 
"Internal error in datatype (variable name mismatch)"


224 
 make_rec_call (a::args, i) arg =


225 
if a = arg then rec_call $ Bound i


226 
else make_rec_call (args, i+1) arg;


227 


228 
(*creates one case of the "X_case" definition of the recursor*)


229 
fun call_recursor ((case_var, case_args), (recursor_var, recursor_args)) =


230 
let fun add_abs (Free(a,T), u) = Abs(a,T,u)


231 
val ncase_args = length case_args


232 
val bound_args = map Bound ((ncase_args  1) downto 0)


233 
val rec_args = map (make_rec_call (rev case_args,0))


234 
(List.drop(recursor_args, ncase_args))


235 
in


236 
foldr add_abs


237 
(case_args, list_comb (recursor_var,


238 
bound_args @ rec_args))


239 
end


240 


241 
(*Find each recursive argument and add a recursive call for it*)


242 
fun rec_args [] = []


243 
 rec_args ((Const("op :",_)$arg$X)::prems) =


244 
(case head_of X of


245 
Const(a,_) => (*recursive occurrence?*)


246 
if Sign.base_name a mem_string rec_base_names


247 
then arg :: rec_args prems


248 
else rec_args prems


249 
 _ => rec_args prems)


250 
 rec_args (_::prems) = rec_args prems;


251 


252 
(*Add an argument position for each occurrence of a recursive set.


253 
Strictly speaking, the recursive arguments are the LAST of the function


254 
variable, but they all have type "i" anyway*)


255 
fun add_rec_args args' T = (map (fn _ => iT) args') > T


256 


257 
(*Plug in the function variable type needed for the recursor


258 
as well as the new arguments (recursive calls)*)


259 
fun rec_ty_elem ((id, T, syn), name, args, prems) =


260 
let val args' = rec_args prems


261 
in ((id, add_rec_args args' T, syn),


262 
name, args @ args', prems)


263 
end;


264 


265 
val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists);


266 


267 
(*Treatment of all parts*)


268 
val (_, recursor_lists) = foldr add_case_list (rec_ty_lists, (1,[]));


269 


270 
(*extract the types of all the variables*)


271 
val recursor_typ = flat (map (map (#2 o #1)) rec_ty_lists)


272 
> (iT>iT);


273 


274 
val recursor_base_name = big_rec_base_name ^ "_rec";


275 
val recursor_name = full_name recursor_base_name;


276 


277 
(*The list of all the function variables*)


278 
val recursor_args = flat (map (map #1) recursor_lists);


279 


280 
val recursor_tm =


281 
list_comb (Const (recursor_name, recursor_typ), recursor_args);


282 


283 
val recursor_cases = map call_recursor


284 
(flat case_lists ~~ flat recursor_lists)


285 


286 
val recursor_def =


287 
Logic.mk_defpair


288 
(recursor_tm,


289 
Ind_Syntax.Vrecursor_const $


290 
absfree ("rec", iT, list_comb (case_const, recursor_cases)));


291 


292 
(* Build the new theory *)


293 


294 
val need_recursor =


295 
(#1 (dest_Const Fp.oper) = "lfp" andalso recursor_typ <> case_typ);


296 


297 
fun add_recursor thy =


298 
if need_recursor then


299 
thy > Theory.add_consts_i


300 
[(recursor_base_name, recursor_typ, NoSyn)]


301 
> PureThy.add_defs_i [Attribute.none recursor_def]


302 
else thy;


303 


304 
val thy0 = thy_path


305 
> Theory.add_consts_i


306 
((case_base_name, case_typ, NoSyn) ::


307 
map #1 (flat con_ty_lists))


308 
> PureThy.add_defs_i


309 
(map Attribute.none


310 
(case_def ::


311 
flat (ListPair.map mk_con_defs


312 
(1 upto npart, con_ty_lists))))


313 
> add_recursor


314 
> Theory.parent_path


315 


316 
val con_defs = get_def thy0 case_name ::


317 
map (get_def thy0 o #2) (flat con_ty_lists);


318 


319 
val (thy1, ind_result) =


320 
thy0 > Ind_Package.add_inductive_i


321 
false (rec_tms, dom_sum, intr_tms,


322 
monos, con_defs,


323 
type_intrs @ Datatype_Arg.intrs,


324 
type_elims @ Datatype_Arg.elims)


325 


326 
(**** Now prove the datatype theorems in this theory ****)


327 


328 


329 
(*** Prove the case theorems ***)


330 


331 
(*Each equation has the form


332 
case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)


333 
fun mk_case_eqn (((_,T,_), name, args, _), case_free) =


334 
FOLogic.mk_Trueprop


335 
(FOLogic.mk_eq


336 
(case_tm $


337 
(list_comb (Const (Sign.intern_const (sign_of thy1) name,T),


338 
args)),


339 
list_comb (case_free, args)));


340 


341 
val case_trans = hd con_defs RS Ind_Syntax.def_trans


342 
and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans;


343 


344 
(*Proves a single case equation. Could use simp_tac, but it's slower!*)


345 
fun case_tacsf con_def _ =


346 
[rewtac con_def,


347 
rtac case_trans 1,


348 
REPEAT (resolve_tac [refl, split_trans,


349 
Su.case_inl RS trans,


350 
Su.case_inr RS trans] 1)];


351 


352 
fun prove_case_eqn (arg,con_def) =


353 
prove_goalw_cterm []


354 
(Ind_Syntax.traceIt "next case equation = "


355 
(cterm_of (sign_of thy1) (mk_case_eqn arg)))


356 
(case_tacsf con_def);


357 


358 
val con_iffs = con_defs RL [Ind_Syntax.def_swap_iff];


359 


360 
val case_eqns =


361 
map prove_case_eqn


362 
(flat con_ty_lists ~~ case_args ~~ tl con_defs);


363 


364 
(*** Prove the recursor theorems ***)


365 


366 
val recursor_eqns = case try (get_def thy1) recursor_base_name of


367 
None => (writeln " [ No recursion operator ]";


368 
[])


369 
 Some recursor_def =>


370 
let


371 
(*Replace subterms rec`x (where rec is a Free var) by recursor_tm(x) *)


372 
fun subst_rec (Const("op `",_) $ Free _ $ arg) = recursor_tm $ arg


373 
 subst_rec tm =


374 
let val (head, args) = strip_comb tm


375 
in list_comb (head, map subst_rec args) end;


376 


377 
(*Each equation has the form


378 
REC(coni(args)) = f_coni(args, REC(rec_arg), ...)


379 
where REC = recursor(f_con1,...,f_conn) and rec_arg is a recursive


380 
constructor argument.*)


381 
fun mk_recursor_eqn (((_,T,_), name, args, _), recursor_case) =


382 
FOLogic.mk_Trueprop


383 
(FOLogic.mk_eq


384 
(recursor_tm $


385 
(list_comb (Const (Sign.intern_const (sign_of thy1) name,T),


386 
args)),


387 
subst_rec (foldl betapply (recursor_case, args))));


388 


389 
val recursor_trans = recursor_def RS def_Vrecursor RS trans;


390 


391 
(*Proves a single recursor equation.*)


392 
fun recursor_tacsf _ =


393 
[rtac recursor_trans 1,


394 
simp_tac (rank_ss addsimps case_eqns) 1,


395 
IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)];


396 


397 
fun prove_recursor_eqn arg =


398 
prove_goalw_cterm []


399 
(Ind_Syntax.traceIt "next recursor equation = "


400 
(cterm_of (sign_of thy1) (mk_recursor_eqn arg)))


401 
recursor_tacsf


402 
in


403 
map prove_recursor_eqn (flat con_ty_lists ~~ recursor_cases)


404 
end


405 


406 
val constructors =


407 
map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);


408 


409 
val free_iffs = con_iffs @


410 
[Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff];


411 


412 
val free_SEs = Ind_Syntax.mk_free_SEs con_iffs @ Su.free_SEs;


413 


414 
val {elim, induct, mutual_induct, ...} = ind_result


415 


416 
(*Typical theorems have the form ~con1=con2, con1=con2==>False,


417 
con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <> x=y, etc. *)


418 
fun mk_free s =


419 
prove_goalw (theory_of_thm elim) (*Don't use thy1: it will be stale*)


420 
con_defs s


421 
(fn prems => [cut_facts_tac prems 1,


422 
fast_tac (ZF_cs addSEs free_SEs) 1]);


423 


424 
val simps = case_eqns @ recursor_eqns;


425 


426 
val dt_info =


427 
{inductive = true,


428 
constructors = constructors,


429 
rec_rewrites = recursor_eqns,


430 
case_rewrites = case_eqns,


431 
induct = induct,


432 
mutual_induct = mutual_induct,


433 
exhaustion = elim};


434 


435 
val con_info =


436 
{big_rec_name = big_rec_name,


437 
constructors = constructors,


438 
(*let primrec handle definition by cases*)


439 
rec_rewrites = (case recursor_eqns of


440 
[] => case_eqns  _ => recursor_eqns)};


441 


442 
(*associate with each constructor the datatype name and rewrites*)


443 
val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors


444 


445 
in


446 
(*Updating theory components: simprules and datatype info*)


447 
(thy1 > Theory.add_path big_rec_base_name


448 
> PureThy.add_tthmss [(("simps", Attribute.tthms_of simps),


449 
[Simplifier.simp_add_global])]


450 
> DatatypesData.put


451 
(Symtab.update


452 
((big_rec_name, dt_info), DatatypesData.get thy1))


453 
> ConstructorsData.put


454 
(foldr Symtab.update (con_pairs, ConstructorsData.get thy1))


455 
> Theory.parent_path,


456 
ind_result,


457 
{con_defs = con_defs,


458 
case_eqns = case_eqns,


459 
recursor_eqns = recursor_eqns,


460 
free_iffs = free_iffs,


461 
free_SEs = free_SEs,


462 
mk_free = mk_free})


463 
end;


464 


465 


466 
fun add_datatype (sdom, srec_tms, scon_ty_lists,


467 
monos, type_intrs, type_elims) thy =


468 
let val sign = sign_of thy


469 
val rec_tms = map (readtm sign Ind_Syntax.iT) srec_tms


470 
val dom_sum =


471 
if sdom = "" then


472 
Ind_Syntax.data_domain (#1 (dest_Const Fp.oper) <> "lfp") rec_tms


473 
else readtm sign Ind_Syntax.iT sdom


474 
and con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists


475 
in


476 
add_datatype_i (dom_sum, rec_tms, con_ty_lists,


477 
monos, type_intrs, type_elims) thy


478 
end


479 


480 
end;
