(* Title: ZF/Tools/datatype_package.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Datatype/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 *) 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}; (*function to make freeness theorems*) signature DATATYPE_ARG = sig val intrs : thm list val elims : thm list end; 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 -> (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list -> theory -> theory * inductive_result * datatype_result end; 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 val coind : bool): DATATYPE_PACKAGE = struct (*con_ty_lists specifies the constructors in the form (name, prems, mixfix) *) (*univ or quniv constitutes the sum domain for mutual recursion; it is applied to the datatype parameters and to Consts occurring in the definition other than Nat.nat and the datatype sets themselves. FIXME: could insert all constant set expressions, e.g. nat->nat.*) fun data_domain co (rec_tms, con_ty_lists) = let val rec_hds = map head_of rec_tms val dummy = assert_all is_Const rec_hds (fn t => "Datatype set not previously declared as constant: " ^ Syntax.string_of_term_global @{theory IFOL} t); val rec_names = (*nat doesn't have to be added*) @{const_name nat} :: map (#1 o dest_Const) rec_hds val u = if co then @{const QUniv.quniv} else @{const Univ.univ} val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms) (fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t | _ => I)) con_ty_lists []; in u $ Ind_Syntax.union_params (hd rec_tms, cs) end; fun add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy = let val dummy = (*has essential ancestors?*) Theory.requires thy "Datatype_ZF" "(co)datatype definitions"; val rec_hds = map head_of rec_tms; val dummy = assert_all is_Const rec_hds (fn t => "Datatype set not previously declared as constant: " ^ Syntax.string_of_term_global thy t); val rec_names = map (#1 o dest_Const) rec_hds val rec_base_names = map Long_Name.base_name rec_names val big_rec_base_name = space_implode "_" rec_base_names val thy_path = thy |> Sign.add_path big_rec_base_name val big_rec_name = Sign.intern_const thy_path big_rec_base_name; val intr_tms = Ind_Syntax.mk_all_intr_tms thy_path (rec_tms, con_ty_lists); val dummy = writeln ((if coind then "Codatatype" else "Datatype") ^ " definition " ^ quote big_rec_name); val case_varname = "f"; (*name for case variables*) (** Define the constructors **) (*The empty tuple is 0*) fun mk_tuple [] = @{const "0"} | mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args; fun mk_inject n k u = BalancedTree.access {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = u} n k; val npart = length rec_names; (*number of mutually recursive parts*) val full_name = Sign.full_bname thy_path; (*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*) PrimitiveDefs.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", @{typ i}, free) | call_f (free,args) = CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args)) @{typ i} free in BalancedTree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (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) = List.foldr add_case (opno, []) con_ty_list in (opno', case_list :: case_lists) end; (*Treatment of all parts*) val (_, case_lists) = List.foldr add_case_list (1,[]) con_ty_lists; (*extract the types of all the variables*) val case_typ = List.concat (map (map (#2 o #1)) con_ty_lists) ---> @{typ "i => i"}; 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 = List.concat (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 = PrimitiveDefs.mk_defpair (case_tm, BalancedTree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (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 = @{const apply} $ Free ("rec", @{typ i}); (*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 List.foldr add_abs (list_comb (recursor_var, bound_args @ rec_args)) case_args end (*Find each recursive argument and add a recursive call for it*) fun rec_args [] = [] | rec_args ((Const(@{const_name mem},_)$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; (*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 _ => @{typ i}) 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) = List.foldr add_case_list (1,[]) rec_ty_lists; (*extract the types of all the variables*) val recursor_typ = List.concat (map (map (#2 o #1)) rec_ty_lists) ---> @{typ "i => i"}; 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 = List.concat (map (map #1) recursor_lists); val recursor_tm = list_comb (Const (recursor_name, recursor_typ), recursor_args); val recursor_cases = map call_recursor (List.concat case_lists ~~ List.concat recursor_lists) val recursor_def = PrimitiveDefs.mk_defpair (recursor_tm, @{const Univ.Vrecursor} $ absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases))); (* Build the new theory *) val need_recursor = (not coind andalso recursor_typ <> case_typ); fun add_recursor thy = if need_recursor then thy |> Sign.add_consts_i [(Binding.name recursor_base_name, recursor_typ, NoSyn)] |> (snd o PureThy.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def]) else thy; val (con_defs, thy0) = thy_path |> Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) ((case_base_name, case_typ, NoSyn) :: map #1 (List.concat con_ty_lists))) |> PureThy.add_defs false (map (Thm.no_attributes o apfst Binding.name) (case_def :: List.concat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists)))) ||> add_recursor ||> Sign.parent_path val intr_names = map (Binding.name o #2) (List.concat con_ty_lists); val (thy1, ind_result) = thy0 |> Ind_Package.add_inductive_i false (rec_tms, dom_sum) (map Thm.no_attributes (intr_names ~~ 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 thy1 name,T), args)), list_comb (case_free, args))); val case_trans = hd con_defs RS @{thm def_trans} and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS @{thm trans}; fun prove_case_eqn (arg, con_def) = Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next case equation = " thy1 (mk_case_eqn arg)) (*Proves a single case equation. Could use simp_tac, but it's slower!*) (fn _ => EVERY [rewrite_goals_tac [con_def], rtac case_trans 1, REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)]); val free_iffs = map standard (con_defs RL [@{thm def_swap_iff}]); val case_eqns = map prove_case_eqn (List.concat con_ty_lists ~~ case_args ~~ tl con_defs); (*** Prove the recursor theorems ***) val recursor_eqns = case try (Drule.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(@{const_name apply},_) $ 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 thy1 name,T), args)), subst_rec (Term.betapplys (recursor_case, args)))); val recursor_trans = recursor_def RS @{thm def_Vrecursor} RS trans; fun prove_recursor_eqn arg = Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next recursor equation = " thy1 (mk_recursor_eqn arg)) (*Proves a single recursor equation.*) (fn _ => EVERY [rtac recursor_trans 1, simp_tac (rank_ss addsimps case_eqns) 1, IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)]); in map prove_recursor_eqn (List.concat 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_SEs = map standard (Ind_Syntax.mk_free_SEs free_iffs); val {intrs, 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 = let val thy = theory_of_thm elim in (*Don't use thy1: it will be stale*) Goal.prove_global thy [] [] (Syntax.read_prop_global thy s) (fn _ => EVERY [rewrite_goals_tac con_defs, fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1]) end; 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*) 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 in (*Updating theory components: simprules and datatype info*) (thy1 |> Sign.add_path big_rec_base_name |> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add]), ((Binding.empty , intrs), [Classical.safe_intro NONE]), ((Binding.name "con_defs", con_defs), []), ((Binding.name "case_eqns", case_eqns), []), ((Binding.name "recursor_eqns", recursor_eqns), []), ((Binding.name "free_iffs", free_iffs), []), ((Binding.name "free_elims", free_SEs), [])] |> snd |> DatatypesData.map (Symtab.update (big_rec_name, dt_info)) |> ConstructorsData.map (fold Symtab.update con_pairs) |> Sign.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 (raw_monos, raw_type_intrs, raw_type_elims) thy = let val ctxt = ProofContext.init thy; fun read_is strs = map (Syntax.parse_term ctxt #> TypeInfer.constrain @{typ i}) strs |> Syntax.check_terms ctxt; val rec_tms = read_is srec_tms; val con_ty_lists = Ind_Syntax.read_constructs ctxt scon_ty_lists; val dom_sum = if sdom = "" then data_domain coind (rec_tms, con_ty_lists) else singleton read_is sdom; val monos = Attrib.eval_thms ctxt raw_monos; val type_intrs = Attrib.eval_thms ctxt raw_type_intrs; val type_elims = Attrib.eval_thms ctxt raw_type_elims; in add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy end; (* outer syntax *) local structure P = OuterParse and K = OuterKeyword in fun mk_datatype ((((dom, dts), monos), type_intrs), type_elims) = #1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims); val con_decl = P.name -- Scan.optional (P.$$$ "(" |-- P.list1 P.term --| P.$$$ ")") [] -- P.opt_mixfix >> P.triple1; val datatype_decl = (Scan.optional ((P.$$$ "⊆" || P.$$$ "<=") |-- P.!!! P.term) "") -- P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) -- Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] -- Scan.optional (P.$$$ "type_intros" |-- P.!!! SpecParse.xthms1) [] -- Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) [] >> (Toplevel.theory o mk_datatype); val coind_prefix = if coind then "co" else ""; val _ = OuterSyntax.command (coind_prefix ^ "datatype") ("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl; end; end;