# HG changeset patch # User wenzelm # Date 1005342790 -3600 # Node ID 673bc8469a0863e2adb94f6208a02f2de9440a62 # Parent 30d9143aff7e2dd53eaabcd911b87ed99040adee adapted to add_inductive_x; diff -r 30d9143aff7e -r 673bc8469a08 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Fri Nov 09 22:52:38 2001 +0100 +++ b/src/ZF/Tools/datatype_package.ML Fri Nov 09 22:53:10 2001 +0100 @@ -23,7 +23,7 @@ signature DATATYPE_ARG = - sig + sig val intrs : thm list val elims : thm list end; @@ -31,37 +31,37 @@ (*Functor's result signature*) signature DATATYPE_PACKAGE = - sig +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 * + 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 * + 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; +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 +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 = +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?*) @@ -77,12 +77,12 @@ 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 intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists); - val dummy = - writeln ((if (#1 (dest_Const Fp.oper) = "Fixedpt.lfp") then "Datatype" - else "Codatatype") - ^ " definition " ^ big_rec_name) + val dummy = + writeln ((if (#1 (dest_Const Fp.oper) = "Fixedpt.lfp") then "Datatype" + else "Codatatype") + ^ " definition " ^ big_rec_name) val case_varname = "f"; (*name for case variables*) @@ -99,27 +99,27 @@ val full_name = Sign.full_name sign; - (*Make constructor definition; + (*Make constructor definition; kpart is the number of this mutually recursive part*) - fun mk_con_defs (kpart, con_ty_list) = + 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))) + 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 = + 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 + | call_f (free,args) = + CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args)) + Ind_Syntax.iT + free in fold_bal (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list) end; (** Generating function variables for the case definition @@ -130,7 +130,7 @@ 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) + (opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args) :: cases); (*Treatment of a list of constructors, for one part @@ -151,7 +151,7 @@ (*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_const = Const (case_name, case_typ); val case_tm = list_comb (case_const, case_args); val case_def = Logic.mk_defpair @@ -164,37 +164,37 @@ (*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 + (*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; + "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)) = + 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)) + 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)) + 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 a mem_string rec_names - then arg :: rec_args prems - else rec_args prems - | _ => rec_args prems) - | rec_args (_::prems) = rec_args prems; + Const(a,_) => (*recursive occurrence?*) + if a mem_string rec_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 @@ -204,19 +204,19 @@ (*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) + 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); + 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); + ---> (iT-->iT); val recursor_base_name = big_rec_base_name ^ "_rec"; val recursor_name = full_name recursor_base_name; @@ -225,126 +225,126 @@ val recursor_args = flat (map (map #1) recursor_lists); val recursor_tm = - list_comb (Const (recursor_name, recursor_typ), recursor_args); + list_comb (Const (recursor_name, recursor_typ), recursor_args); - val recursor_cases = map call_recursor - (flat case_lists ~~ flat recursor_lists) + val recursor_cases = map call_recursor + (flat case_lists ~~ flat recursor_lists) - val recursor_def = + val recursor_def = Logic.mk_defpair - (recursor_tm, - Ind_Syntax.Vrecursor_const $ - absfree ("rec", iT, list_comb (case_const, recursor_cases))); + (recursor_tm, + Ind_Syntax.Vrecursor_const $ + absfree ("rec", iT, list_comb (case_const, recursor_cases))); (* Build the new theory *) - val need_recursor = + val need_recursor = (#1 (dest_Const Fp.oper) = "Fixedpt.lfp" andalso recursor_typ <> case_typ); - fun add_recursor thy = + fun add_recursor thy = if need_recursor then - thy |> Theory.add_consts_i - [(recursor_base_name, recursor_typ, NoSyn)] - |> (#1 o PureThy.add_defs_i false [Thm.no_attributes recursor_def]) + thy |> Theory.add_consts_i + [(recursor_base_name, recursor_typ, NoSyn)] + |> (#1 o PureThy.add_defs_i false [Thm.no_attributes recursor_def]) else thy; val (thy0, con_defs) = thy_path - |> Theory.add_consts_i - ((case_base_name, case_typ, NoSyn) :: - map #1 (flat con_ty_lists)) - |> PureThy.add_defs_i false - (map Thm.no_attributes - (case_def :: - flat (ListPair.map mk_con_defs - (1 upto npart, con_ty_lists)))) - |>> add_recursor - |>> Theory.parent_path + |> Theory.add_consts_i + ((case_base_name, case_typ, NoSyn) :: + map #1 (flat con_ty_lists)) + |> PureThy.add_defs_i false + (map Thm.no_attributes + (case_def :: + flat (ListPair.map mk_con_defs + (1 upto npart, con_ty_lists)))) + |>> add_recursor + |>> Theory.parent_path - val (thy1, ind_result) = + 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) + false (rec_tms, dom_sum) (map (fn tm => (("", tm), [])) 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 + (*Each equation has the form case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *) - fun mk_case_eqn (((_,T,_), name, args, _), case_free) = + 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))); + (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 _ = + 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)]; + 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); + prove_goalw_cterm [] + (Ind_Syntax.traceIt "next case equation = " + (cterm_of (sign_of thy1) (mk_case_eqn arg))) + (case_tacsf con_def); val free_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); + 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 => + []) + | 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; + (*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)))); + (*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; + 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)]; + (*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 + 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) + map prove_recursor_eqn (flat con_ty_lists ~~ recursor_cases) end val constructors = @@ -359,27 +359,27 @@ 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 @ Su.free_SEs) 1]); + (fn prems => [cut_facts_tac prems 1, + fast_tac (ZF_cs addSEs free_SEs @ Su.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}; + {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, + constructors = constructors, (*let primrec handle definition by cases*) - free_iffs = free_iffs, - rec_rewrites = (case recursor_eqns of - [] => case_eqns | _ => recursor_eqns)}; + free_iffs = free_iffs, + 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 @@ -387,18 +387,18 @@ in (*Updating theory components: simprules and datatype info*) (thy1 |> Theory.add_path big_rec_base_name - |> (#1 o PureThy.add_thmss [(("simps", simps), - [Simplifier.simp_add_global])]) - |> (#1 o PureThy.add_thmss [(("", intrs), + |> (#1 o PureThy.add_thmss [(("simps", simps), + [Simplifier.simp_add_global])]) + |> (#1 o PureThy.add_thmss [(("", intrs), (*not "intrs" to avoid the warning that they - are already stored by the inductive package*) - [Classical.safe_intro_global])]) - |> DatatypesData.put - (Symtab.update - ((big_rec_name, dt_info), DatatypesData.get thy1)) + are already stored by the inductive package*) + [Classical.safe_intro_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, + (foldr Symtab.update (con_pairs, ConstructorsData.get thy1)) + |> Theory.parent_path, ind_result, {con_defs = con_defs, case_eqns = case_eqns, @@ -409,20 +409,20 @@ end; -fun add_datatype (sdom, srec_tms, scon_ty_lists, - monos, type_intrs, type_elims) thy = +fun add_datatype (sdom, srec_tms, scon_ty_lists, + monos, type_intrs, type_elims) thy = let val sign = sign_of thy val read_i = Sign.simple_read_term sign Ind_Syntax.iT val rec_tms = map read_i srec_tms val con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists - val dom_sum = + val dom_sum = if sdom = "" then - Ind_Syntax.data_domain (#1(dest_Const Fp.oper) <> "Fixedpt.lfp") - (rec_tms, con_ty_lists) + Ind_Syntax.data_domain (#1(dest_Const Fp.oper) <> "Fixedpt.lfp") + (rec_tms, con_ty_lists) else read_i sdom - in - add_datatype_i (dom_sum, rec_tms, con_ty_lists, - monos, type_intrs, type_elims) thy - end + in + add_datatype_i (dom_sum, rec_tms, con_ty_lists, + monos, type_intrs, type_elims) thy + end end;