--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Tools/datatype_package.ML Mon Dec 28 16:58:11 1998 +0100
@@ -0,0 +1,480 @@
+(* Title: ZF/datatype_package.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Fixedpoint definition module -- for Inductive/Codatatype Definitions
+
+The functor will be instantiated for normal sums/products (datatype defs)
+ and non-standard sums/products (codatatype defs)
+
+Sums are used only for mutual recursion;
+Products are used only to derive "streamlined" induction rules for relations
+*)
+
+
+(** Datatype information, e.g. associated theorems **)
+
+type datatype_info =
+ {inductive: bool, (*true if inductive, not coinductive*)
+ constructors : term list, (*the constructors, as Consts*)
+ rec_rewrites : thm list, (*recursor equations*)
+ case_rewrites : thm list, (*case equations*)
+ induct : thm,
+ mutual_induct : thm,
+ exhaustion : thm};
+
+structure DatatypesArgs =
+ struct
+ val name = "ZF/datatypes";
+ type T = datatype_info Symtab.table;
+
+ val empty = Symtab.empty;
+ val prep_ext = I;
+ val merge: T * T -> T = Symtab.merge (K true);
+
+ fun print sg tab =
+ Pretty.writeln (Pretty.strs ("datatypes:" ::
+ map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab)));
+ end;
+
+structure DatatypesData = TheoryDataFun(DatatypesArgs);
+
+
+(** Constructor information: needed to map constructors to datatypes **)
+
+type constructor_info =
+ {big_rec_name : string, (*name of the mutually recursive set*)
+ constructors : term list, (*the constructors, as Consts*)
+ rec_rewrites : thm list}; (*recursor equations*)
+
+
+structure ConstructorsArgs =
+struct
+ val name = "ZF/constructors"
+ type T = constructor_info Symtab.table
+
+ val empty = Symtab.empty
+ val prep_ext = I
+ val merge: T * T -> T = Symtab.merge (K true)
+
+ fun print sg tab = () (*nothing extra to print*)
+end;
+
+structure ConstructorsData = TheoryDataFun(ConstructorsArgs);
+
+val setup_datatypes = [DatatypesData.init, ConstructorsData.init];
+
+
+type datatype_result =
+ {con_defs : thm list, (*definitions made in thy*)
+ case_eqns : thm list, (*equations for case operator*)
+ recursor_eqns : thm list, (*equations for the recursor*)
+ free_iffs : thm list, (*freeness rewrite rules*)
+ free_SEs : thm list, (*freeness destruct rules*)
+ mk_free : string -> thm}; (*makes freeness theorems*)
+
+
+signature DATATYPE_ARG =
+ sig
+ val intrs : thm list
+ val elims : thm list
+ end;
+
+
+(*Functor's result signature*)
+signature DATATYPE_PACKAGE =
+ sig
+
+ (*Insert definitions for the recursive sets, which
+ must *already* be declared as constants in parent theory!*)
+ val add_datatype_i :
+ term * term list * Ind_Syntax.constructor_spec list list *
+ thm list * thm list * thm list
+ -> theory -> theory * inductive_result * datatype_result
+
+ val add_datatype :
+ string * string list *
+ (string * string list * mixfix) list list *
+ thm list * thm list * thm list
+ -> theory -> theory * inductive_result * datatype_result
+
+ end;
+
+
+(*Declares functions to add fixedpoint/constructor defs to a theory.
+ Recursive sets must *already* be declared as constants.*)
+functor Add_datatype_def_Fun
+ (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU
+ and Ind_Package : INDUCTIVE_PACKAGE
+ and Datatype_Arg : DATATYPE_ARG)
+ : DATATYPE_PACKAGE =
+struct
+
+
+(*con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
+fun add_datatype_i (dom_sum, rec_tms, con_ty_lists,
+ monos, type_intrs, type_elims) thy =
+ let
+ open BasisLibrary
+ val dummy = (*has essential ancestors?*)
+ Theory.requires thy "Datatype" "(co)datatype definitions";
+
+
+ val rec_names = map (#1 o dest_Const o head_of) rec_tms
+ val rec_base_names = map Sign.base_name rec_names
+ val big_rec_base_name = space_implode "_" rec_base_names
+
+ val thy_path = thy |> Theory.add_path big_rec_base_name
+ val sign = sign_of thy_path
+
+ val big_rec_name = Sign.intern_const sign big_rec_base_name;
+
+ val intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists)
+
+ val dummy =
+ writeln ((if (#1 (dest_Const Fp.oper) = "lfp") then "Datatype"
+ else "Codatatype")
+ ^ " definition " ^ big_rec_name)
+
+ val case_varname = "f"; (*name for case variables*)
+
+ (** Define the constructors **)
+
+ (*The empty tuple is 0*)
+ fun mk_tuple [] = Const("0",iT)
+ | mk_tuple args = foldr1 (app Pr.pair) args;
+
+ fun mk_inject n k u = access_bal (ap Su.inl, ap Su.inr, u) n k;
+
+ val npart = length rec_names; (*number of mutually recursive parts*)
+
+
+ val full_name = Sign.full_name sign;
+
+ (*Make constructor definition;
+ kpart is the number of this mutually recursive part*)
+ fun mk_con_defs (kpart, con_ty_list) =
+ let val ncon = length con_ty_list (*number of constructors*)
+ fun mk_def (((id,T,syn), name, args, prems), kcon) =
+ (*kcon is index of constructor*)
+ Logic.mk_defpair (list_comb (Const (full_name name, T), args),
+ mk_inject npart kpart
+ (mk_inject ncon kcon (mk_tuple args)))
+ in ListPair.map mk_def (con_ty_list, 1 upto ncon) end;
+
+
+ (*** Define the case operator ***)
+
+ (*Combine split terms using case; yields the case operator for one part*)
+ fun call_case case_list =
+ let fun call_f (free,[]) = Abs("null", iT, free)
+ | call_f (free,args) =
+ CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
+ Ind_Syntax.iT
+ free
+ in fold_bal (app Su.elim) (map call_f case_list) end;
+
+ (** Generating function variables for the case definition
+ Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
+
+ (*The function variable for a single constructor*)
+ fun add_case (((_, T, _), name, args, _), (opno, cases)) =
+ if Syntax.is_identifier name then
+ (opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases)
+ else
+ (opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args)
+ :: cases);
+
+ (*Treatment of a list of constructors, for one part
+ Result adds a list of terms, each a function variable with arguments*)
+ fun add_case_list (con_ty_list, (opno, case_lists)) =
+ let val (opno', case_list) = foldr add_case (con_ty_list, (opno, []))
+ in (opno', case_list :: case_lists) end;
+
+ (*Treatment of all parts*)
+ val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
+
+ (*extract the types of all the variables*)
+ val case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
+
+ val case_base_name = big_rec_base_name ^ "_case";
+ val case_name = full_name case_base_name;
+
+ (*The list of all the function variables*)
+ val case_args = flat (map (map #1) case_lists);
+
+ val case_const = Const (case_name, case_typ);
+ val case_tm = list_comb (case_const, case_args);
+
+ val case_def = Logic.mk_defpair
+ (case_tm, fold_bal (app Su.elim) (map call_case case_lists));
+
+
+ (** Generating function variables for the recursor definition
+ Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
+
+ (*a recursive call for x is the application rec`x *)
+ val rec_call = Ind_Syntax.apply_const $ Free ("rec", iT);
+
+ (*look back down the "case args" (which have been reversed) to
+ determine the de Bruijn index*)
+ fun make_rec_call ([], _) arg = error
+ "Internal error in datatype (variable name mismatch)"
+ | make_rec_call (a::args, i) arg =
+ if a = arg then rec_call $ Bound i
+ else make_rec_call (args, i+1) arg;
+
+ (*creates one case of the "X_case" definition of the recursor*)
+ fun call_recursor ((case_var, case_args), (recursor_var, recursor_args)) =
+ let fun add_abs (Free(a,T), u) = Abs(a,T,u)
+ val ncase_args = length case_args
+ val bound_args = map Bound ((ncase_args - 1) downto 0)
+ val rec_args = map (make_rec_call (rev case_args,0))
+ (List.drop(recursor_args, ncase_args))
+ in
+ foldr add_abs
+ (case_args, list_comb (recursor_var,
+ bound_args @ rec_args))
+ end
+
+ (*Find each recursive argument and add a recursive call for it*)
+ fun rec_args [] = []
+ | rec_args ((Const("op :",_)$arg$X)::prems) =
+ (case head_of X of
+ Const(a,_) => (*recursive occurrence?*)
+ if Sign.base_name a mem_string rec_base_names
+ then arg :: rec_args prems
+ else rec_args prems
+ | _ => rec_args prems)
+ | rec_args (_::prems) = rec_args prems;
+
+ (*Add an argument position for each occurrence of a recursive set.
+ Strictly speaking, the recursive arguments are the LAST of the function
+ variable, but they all have type "i" anyway*)
+ fun add_rec_args args' T = (map (fn _ => iT) args') ---> T
+
+ (*Plug in the function variable type needed for the recursor
+ as well as the new arguments (recursive calls)*)
+ fun rec_ty_elem ((id, T, syn), name, args, prems) =
+ let val args' = rec_args prems
+ in ((id, add_rec_args args' T, syn),
+ name, args @ args', prems)
+ end;
+
+ val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists);
+
+ (*Treatment of all parts*)
+ val (_, recursor_lists) = foldr add_case_list (rec_ty_lists, (1,[]));
+
+ (*extract the types of all the variables*)
+ val recursor_typ = flat (map (map (#2 o #1)) rec_ty_lists)
+ ---> (iT-->iT);
+
+ val recursor_base_name = big_rec_base_name ^ "_rec";
+ val recursor_name = full_name recursor_base_name;
+
+ (*The list of all the function variables*)
+ val recursor_args = flat (map (map #1) recursor_lists);
+
+ val recursor_tm =
+ list_comb (Const (recursor_name, recursor_typ), recursor_args);
+
+ val recursor_cases = map call_recursor
+ (flat case_lists ~~ flat recursor_lists)
+
+ val recursor_def =
+ Logic.mk_defpair
+ (recursor_tm,
+ Ind_Syntax.Vrecursor_const $
+ absfree ("rec", iT, list_comb (case_const, recursor_cases)));
+
+ (* Build the new theory *)
+
+ val need_recursor =
+ (#1 (dest_Const Fp.oper) = "lfp" andalso recursor_typ <> case_typ);
+
+ fun add_recursor thy =
+ if need_recursor then
+ thy |> Theory.add_consts_i
+ [(recursor_base_name, recursor_typ, NoSyn)]
+ |> PureThy.add_defs_i [Attribute.none recursor_def]
+ else thy;
+
+ val thy0 = thy_path
+ |> Theory.add_consts_i
+ ((case_base_name, case_typ, NoSyn) ::
+ map #1 (flat con_ty_lists))
+ |> PureThy.add_defs_i
+ (map Attribute.none
+ (case_def ::
+ flat (ListPair.map mk_con_defs
+ (1 upto npart, con_ty_lists))))
+ |> add_recursor
+ |> Theory.parent_path
+
+ val con_defs = get_def thy0 case_name ::
+ map (get_def thy0 o #2) (flat con_ty_lists);
+
+ val (thy1, ind_result) =
+ thy0 |> Ind_Package.add_inductive_i
+ false (rec_tms, dom_sum, intr_tms,
+ monos, con_defs,
+ type_intrs @ Datatype_Arg.intrs,
+ type_elims @ Datatype_Arg.elims)
+
+ (**** Now prove the datatype theorems in this theory ****)
+
+
+ (*** Prove the case theorems ***)
+
+ (*Each equation has the form
+ case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
+ fun mk_case_eqn (((_,T,_), name, args, _), case_free) =
+ FOLogic.mk_Trueprop
+ (FOLogic.mk_eq
+ (case_tm $
+ (list_comb (Const (Sign.intern_const (sign_of thy1) name,T),
+ args)),
+ list_comb (case_free, args)));
+
+ val case_trans = hd con_defs RS Ind_Syntax.def_trans
+ and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans;
+
+ (*Proves a single case equation. Could use simp_tac, but it's slower!*)
+ fun case_tacsf con_def _ =
+ [rewtac con_def,
+ rtac case_trans 1,
+ REPEAT (resolve_tac [refl, split_trans,
+ Su.case_inl RS trans,
+ Su.case_inr RS trans] 1)];
+
+ fun prove_case_eqn (arg,con_def) =
+ prove_goalw_cterm []
+ (Ind_Syntax.traceIt "next case equation = "
+ (cterm_of (sign_of thy1) (mk_case_eqn arg)))
+ (case_tacsf con_def);
+
+ val con_iffs = con_defs RL [Ind_Syntax.def_swap_iff];
+
+ val case_eqns =
+ map prove_case_eqn
+ (flat con_ty_lists ~~ case_args ~~ tl con_defs);
+
+ (*** Prove the recursor theorems ***)
+
+ val recursor_eqns = case try (get_def thy1) recursor_base_name of
+ None => (writeln " [ No recursion operator ]";
+ [])
+ | Some recursor_def =>
+ let
+ (*Replace subterms rec`x (where rec is a Free var) by recursor_tm(x) *)
+ fun subst_rec (Const("op `",_) $ Free _ $ arg) = recursor_tm $ arg
+ | subst_rec tm =
+ let val (head, args) = strip_comb tm
+ in list_comb (head, map subst_rec args) end;
+
+ (*Each equation has the form
+ REC(coni(args)) = f_coni(args, REC(rec_arg), ...)
+ where REC = recursor(f_con1,...,f_conn) and rec_arg is a recursive
+ constructor argument.*)
+ fun mk_recursor_eqn (((_,T,_), name, args, _), recursor_case) =
+ FOLogic.mk_Trueprop
+ (FOLogic.mk_eq
+ (recursor_tm $
+ (list_comb (Const (Sign.intern_const (sign_of thy1) name,T),
+ args)),
+ subst_rec (foldl betapply (recursor_case, args))));
+
+ val recursor_trans = recursor_def RS def_Vrecursor RS trans;
+
+ (*Proves a single recursor equation.*)
+ fun recursor_tacsf _ =
+ [rtac recursor_trans 1,
+ simp_tac (rank_ss addsimps case_eqns) 1,
+ IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)];
+
+ fun prove_recursor_eqn arg =
+ prove_goalw_cterm []
+ (Ind_Syntax.traceIt "next recursor equation = "
+ (cterm_of (sign_of thy1) (mk_recursor_eqn arg)))
+ recursor_tacsf
+ in
+ map prove_recursor_eqn (flat con_ty_lists ~~ recursor_cases)
+ end
+
+ val constructors =
+ map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);
+
+ val free_iffs = con_iffs @
+ [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff];
+
+ val free_SEs = Ind_Syntax.mk_free_SEs con_iffs @ Su.free_SEs;
+
+ val {elim, induct, mutual_induct, ...} = ind_result
+
+ (*Typical theorems have the form ~con1=con2, con1=con2==>False,
+ con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *)
+ fun mk_free s =
+ prove_goalw (theory_of_thm elim) (*Don't use thy1: it will be stale*)
+ con_defs s
+ (fn prems => [cut_facts_tac prems 1,
+ fast_tac (ZF_cs addSEs free_SEs) 1]);
+
+ val simps = case_eqns @ recursor_eqns;
+
+ val dt_info =
+ {inductive = true,
+ constructors = constructors,
+ rec_rewrites = recursor_eqns,
+ case_rewrites = case_eqns,
+ induct = induct,
+ mutual_induct = mutual_induct,
+ exhaustion = elim};
+
+ val con_info =
+ {big_rec_name = big_rec_name,
+ constructors = constructors,
+ (*let primrec handle definition by cases*)
+ rec_rewrites = (case recursor_eqns of
+ [] => case_eqns | _ => recursor_eqns)};
+
+ (*associate with each constructor the datatype name and rewrites*)
+ val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
+
+ in
+ (*Updating theory components: simprules and datatype info*)
+ (thy1 |> Theory.add_path big_rec_base_name
+ |> PureThy.add_tthmss [(("simps", Attribute.tthms_of simps),
+ [Simplifier.simp_add_global])]
+ |> DatatypesData.put
+ (Symtab.update
+ ((big_rec_name, dt_info), DatatypesData.get thy1))
+ |> ConstructorsData.put
+ (foldr Symtab.update (con_pairs, ConstructorsData.get thy1))
+ |> Theory.parent_path,
+ ind_result,
+ {con_defs = con_defs,
+ case_eqns = case_eqns,
+ recursor_eqns = recursor_eqns,
+ free_iffs = free_iffs,
+ free_SEs = free_SEs,
+ mk_free = mk_free})
+ end;
+
+
+fun add_datatype (sdom, srec_tms, scon_ty_lists,
+ monos, type_intrs, type_elims) thy =
+ let val sign = sign_of thy
+ val rec_tms = map (readtm sign Ind_Syntax.iT) srec_tms
+ val dom_sum =
+ if sdom = "" then
+ Ind_Syntax.data_domain (#1 (dest_Const Fp.oper) <> "lfp") rec_tms
+ else readtm sign Ind_Syntax.iT sdom
+ and con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists
+ in
+ add_datatype_i (dom_sum, rec_tms, con_ty_lists,
+ monos, type_intrs, type_elims) thy
+ end
+
+end;