# HG changeset patch # User wenzelm # Date 1322692208 -3600 # Node ID 615da8b8d758fd2c3d18be0aceaf3ed68d1a61ee # Parent 9dcbf6a1829cc818bf3fc36b6aadfe255333e3d7 discontinued obsolete datatype "alt_names"; diff -r 9dcbf6a1829c -r 615da8b8d758 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Nov 30 21:14:01 2011 +0100 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Nov 30 23:30:08 2011 +0100 @@ -693,7 +693,7 @@ @@{command (HOL) rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +) ; - spec: @{syntax parname}? @{syntax typespec} @{syntax mixfix}? '=' (cons + '|') + spec: @{syntax typespec} @{syntax mixfix}? '=' (cons + '|') ; cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}? "} diff -r 9dcbf6a1829c -r 615da8b8d758 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Nov 30 21:14:01 2011 +0100 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Nov 30 23:30:08 2011 +0100 @@ -1036,10 +1036,6 @@ \rail@endplus \rail@end \rail@begin{2}{\isa{spec}} -\rail@bar -\rail@nextbar{1} -\rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[] -\rail@endbar \rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[] \rail@bar \rail@nextbar{1} diff -r 9dcbf6a1829c -r 615da8b8d758 src/HOL/Library/Bit.thy --- a/src/HOL/Library/Bit.thy Wed Nov 30 21:14:01 2011 +0100 +++ b/src/HOL/Library/Bit.thy Wed Nov 30 23:30:08 2011 +0100 @@ -25,7 +25,7 @@ end -rep_datatype (bit) "0::bit" "1::bit" +rep_datatype "0::bit" "1::bit" proof - fix P and x :: bit assume "P (0::bit)" and "P (1::bit)" diff -r 9dcbf6a1829c -r 615da8b8d758 src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Wed Nov 30 21:14:01 2011 +0100 +++ b/src/HOL/Nominal/nominal_atoms.ML Wed Nov 30 23:30:08 2011 +0100 @@ -100,8 +100,7 @@ val (_,thy1) = fold_map (fn ak => fn thy => let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)]) - val (dt_names, thy1) = Datatype.add_datatype - Datatype.default_config [ak] [dt] thy; + val (dt_names, thy1) = Datatype.add_datatype Datatype.default_config [dt] thy; val injects = maps (#inject o Datatype.the_info thy1) dt_names; val ak_type = Type (Sign.intern_type thy1 ak,[]) diff -r 9dcbf6a1829c -r 615da8b8d758 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Wed Nov 30 21:14:01 2011 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Wed Nov 30 23:30:08 2011 +0100 @@ -6,9 +6,9 @@ signature NOMINAL_DATATYPE = sig - val add_nominal_datatype : Datatype.config -> string list -> - (string list * bstring * mixfix * - (bstring * string list * mixfix) list) list -> theory -> theory + val add_nominal_datatype : Datatype.config -> + (string list * binding * mixfix * (binding * string list * mixfix) list) list -> + theory -> theory type descr type nominal_datatype_info val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table @@ -188,14 +188,16 @@ fun fresh_star_const T U = Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT); -fun gen_add_nominal_datatype prep_typ config new_type_names dts thy = +fun gen_add_nominal_datatype prep_typ config dts thy = let + val new_type_names = map (Binding.name_of o #2) dts; + + (* this theory is used just for parsing *) val tmp_thy = thy |> Theory.copy |> - Sign.add_types_global (map (fn (tvs, tname, mx, _) => - (Binding.name tname, length tvs, mx)) dts); + Sign.add_types_global (map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dts); val atoms = atoms_of thy; @@ -224,7 +226,7 @@ map (fn (cname, cargs, mx) => (cname, mx)) constrs) dts'; val ps = map (fn (_, n, _, _) => - (Sign.full_bname tmp_thy n, Sign.full_bname tmp_thy (n ^ "_Rep"))) dts; + (Sign.full_name tmp_thy n, Sign.full_name tmp_thy (Binding.suffix_name "_Rep" n))) dts; val rps = map Library.swap ps; fun replace_types (Type ("Nominal.ABS", [T, U])) = @@ -233,17 +235,16 @@ Type (the_default s (AList.lookup op = ps s), map replace_types Ts) | replace_types T = T; - val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, Binding.name (tname ^ "_Rep"), NoSyn, - map (fn (cname, cargs, mx) => (Binding.name (cname ^ "_Rep"), - map replace_types cargs, NoSyn)) constrs)) dts'; + val dts'' = map (fn (tvs, tname, mx, constrs) => + (tvs, Binding.suffix_name "_Rep" tname, NoSyn, + map (fn (cname, cargs, mx) => (Binding.suffix_name "_Rep" cname, + map replace_types cargs, NoSyn)) constrs)) dts'; val new_type_names' = map (fn n => n ^ "_Rep") new_type_names; - val (full_new_type_names',thy1) = - Datatype.add_datatype config new_type_names' dts'' thy; + val (full_new_type_names',thy1) = Datatype.add_datatype config dts'' thy; - val {descr, induct, ...} = - Datatype.the_info thy1 (hd full_new_type_names'); + val {descr, induct, ...} = Datatype.the_info thy1 (hd full_new_type_names'); fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); val big_name = space_implode "_" new_type_names; @@ -612,9 +613,9 @@ val (typedefs, thy6) = thy4 - |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy => - Typedef.add_typedef_global false (SOME (Binding.name name')) - (Binding.name name, map (fn (v, _) => (v, dummyS)) tvs, mx) (* FIXME keep constraints!? *) + |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy => + Typedef.add_typedef_global false NONE + (name, map (fn (v, _) => (v, dummyS)) tvs, mx) (* FIXME keep constraints!? *) (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $ Const (cname, U --> HOLogic.boolT)) NONE (rtac exI 1 THEN rtac CollectI 1 THEN @@ -624,18 +625,17 @@ val permT = mk_permT (TFree (singleton (Name.variant_list (map fst tvs)) "'a", HOLogic.typeS)); val pi = Free ("pi", permT); - val T = Type (Sign.intern_type thy name, map TFree tvs); + val T = Type (Sign.full_name thy name, map TFree tvs); in apfst (pair r o hd) - (Global_Theory.add_defs_unchecked true [((Binding.name ("prm_" ^ name ^ "_def"), Logic.mk_equals - (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T), - Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $ - (Const ("Nominal.perm", permT --> U --> U) $ pi $ - (Const (Sign.intern_const thy ("Rep_" ^ name), T --> U) $ - Free ("x", T))))), [])] thy) + (Global_Theory.add_defs_unchecked true + [((Binding.map_name (fn n => "prm_" ^ n ^ "_def") name, Logic.mk_equals + (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T), + Const (Sign.intern_const thy ("Abs_" ^ Binding.name_of name), U --> T) $ + (Const ("Nominal.perm", permT --> U --> U) $ pi $ + (Const (Sign.intern_const thy ("Rep_" ^ Binding.name_of name), T --> U) $ + Free ("x", T))))), [])] thy) end)) - (types_syntax ~~ tyvars ~~ - List.take (rep_set_names'' ~~ recTs', length new_type_names) ~~ - new_type_names); + (types_syntax ~~ tyvars ~~ List.take (rep_set_names'' ~~ recTs', length new_type_names)); val perm_defs = map snd typedefs; val Abs_inverse_thms = map (collect_simp o #Abs_inverse o snd o fst) typedefs; @@ -800,7 +800,7 @@ (Const (rep_name, T --> T') $ lhs, rhs)); val def_name = (Long_Name.base_name cname) ^ "_def"; val ([def_thm], thy') = thy |> - Sign.add_consts_i [(Binding.name cname', constrT, mx)] |> + Sign.add_consts_i [(cname', constrT, mx)] |> (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)] in (thy', defs @ [def_thm], eqns @ [eqn]) end; @@ -2002,7 +2002,7 @@ (* define primrec combinators *) - val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec"; + val big_reccomb_name = space_implode "_" new_type_names ^ "_rec"; val reccomb_names = map (Sign.full_bname thy11) (if length descr'' = 1 then [big_reccomb_name] else (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int) @@ -2069,23 +2069,9 @@ val add_nominal_datatype = gen_add_nominal_datatype Datatype.read_typ; - -(* FIXME: The following stuff should be exported by Datatype *) - -val datatype_decl = - Scan.option (Parse.$$$ "(" |-- Parse.name --| Parse.$$$ ")") -- - Parse.type_args -- Parse.name -- Parse.opt_mixfix -- - (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.name -- Scan.repeat Parse.typ -- Parse.opt_mixfix)); - -fun mk_datatype args = - let - val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args; - val specs = map (fn ((((_, vs), t), mx), cons) => - (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args; - in add_nominal_datatype Datatype.default_config names specs end; - val _ = Outer_Syntax.command "nominal_datatype" "define inductive datatypes" Keyword.thy_decl - (Parse.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype)); + (Parse.and_list1 Datatype.parse_decl + >> (Toplevel.theory o add_nominal_datatype Datatype.default_config)); end diff -r 9dcbf6a1829c -r 615da8b8d758 src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Wed Nov 30 21:14:01 2011 +0100 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Wed Nov 30 23:30:08 2011 +0100 @@ -305,7 +305,7 @@ val tyname = Sign.full_name thy tyb in (thy |> - Datatype.add_datatype {strict = true, quiet = true} [s] + Datatype.add_datatype {strict = true, quiet = true} [([], tyb, NoSyn, map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |> add_enum_type s tyname, diff -r 9dcbf6a1829c -r 615da8b8d758 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Wed Nov 30 21:14:01 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype.ML Wed Nov 30 23:30:08 2011 +0100 @@ -10,10 +10,13 @@ signature DATATYPE = sig include DATATYPE_DATA - val add_datatype : config -> string list -> (string list * binding * mixfix * - (binding * typ list * mixfix) list) list -> theory -> string list * theory - val datatype_cmd : string list -> (string list * binding * mixfix * - (binding * string list * mixfix) list) list -> theory -> theory + val add_datatype: config -> + (string list * binding * mixfix * (binding * typ list * mixfix) list) list -> + theory -> string list * theory + val add_datatype_cmd: + (string list * binding * mixfix * (binding * string list * mixfix) list) list -> + theory -> theory + val parse_decl: (string list * binding * mixfix * (binding * string list * mixfix) list) parser end; structure Datatype : DATATYPE = @@ -58,9 +61,10 @@ (** proof of characteristic theorems **) fun representation_proofs (config : Datatype_Aux.config) (dt_info : Datatype_Aux.info Symtab.table) - new_type_names descr sorts types_syntax constr_syntax case_names_induct thy = + descr sorts types_syntax constr_syntax case_names_induct thy = let val descr' = flat descr; + val new_type_names = map (Binding.name_of o fst) types_syntax; val big_name = space_implode "_" new_type_names; val thy1 = Sign.add_path big_name thy; val big_rec_name = big_name ^ "_rep_set"; @@ -189,26 +193,26 @@ (********************************* typedef ********************************) - val (typedefs, thy3) = thy2 |> - Sign.parent_path |> - fold_map (fn ((((name, mx), tvs), c), name') => - Typedef.add_typedef_global false (SOME (Binding.name name')) + val (typedefs, thy3) = thy2 + |> Sign.parent_path + |> fold_map + (fn (((name, mx), tvs), c) => + Typedef.add_typedef_global false NONE (name, map (rpair dummyS) tvs, mx) (Collect $ Const (c, UnivT')) NONE (rtac exI 1 THEN rtac CollectI 1 THEN QUIET_BREADTH_FIRST (has_fewer_prems 1) (resolve_tac rep_intrs 1))) - (types_syntax ~~ tyvars ~~ - (take (length newTs) rep_set_names) ~~ new_type_names) ||> - Sign.add_path big_name; + (types_syntax ~~ tyvars ~~ (take (length newTs) rep_set_names)) + ||> Sign.add_path big_name; (*********************** definition of constructors ***********************) val big_rep_name = space_implode "_" new_type_names ^ "_Rep_"; val rep_names = map (prefix "Rep_") new_type_names; - val rep_names' = map (fn i => big_rep_name ^ (string_of_int i)) - (1 upto (length (flat (tl descr)))); - val all_rep_names = map (Sign.intern_const thy3) rep_names @ + val rep_names' = map (fn i => big_rep_name ^ string_of_int i) (1 upto length (flat (tl descr))); + val all_rep_names = + map (Sign.intern_const thy3) rep_names @ map (Sign.full_bname thy3) rep_names'; (* isomorphism declarations *) @@ -669,9 +673,9 @@ -(** definitional introduction of datatypes **) +(** datatype definition **) -fun gen_add_datatype prep_typ config new_type_names dts thy = +fun gen_add_datatype prep_typ config dts thy = let val _ = Theory.requires thy "Datatype" "datatype definitions"; @@ -694,11 +698,11 @@ val dt_names = map fst new_dts; val _ = - (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of + (case duplicates (op =) (map fst new_dts) of [] => () | dups => error ("Duplicate datatypes: " ^ commas dups)); - fun prep_dt_spec (tvs, tname, mx, constrs) tname' (dts', constr_syntax, sorts, i) = + fun prep_dt_spec (tvs, tname, mx, constrs) (dts', constr_syntax, sorts, i) = let fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') = let @@ -707,7 +711,7 @@ (case subtract (op =) tvs (fold (curry Misc_Legacy.add_typ_tfree_names) cargs' []) of [] => () | vs => error ("Extra type variables on rhs: " ^ commas vs)); - val c = Sign.full_name_path tmp_thy tname' cname; + val c = Sign.full_name_path tmp_thy (Binding.name_of tname) cname; in (constrs @ [(c, map (Datatype_Aux.dtyp_of_typ new_dts) cargs')], constr_syntax' @ [(cname, mx')], sorts'') @@ -725,7 +729,7 @@ error ("Duplicate constructors " ^ commas dups ^ " in datatype " ^ Binding.print tname)) end; - val (dts', constr_syntax, sorts', i) = fold2 prep_dt_spec dts new_type_names ([], [], [], 0); + val (dts', constr_syntax, sorts', i) = fold prep_dt_spec dts ([], [], [], 0); val sorts = sorts' @ map (rpair (Sign.defaultS tmp_thy)) (subtract (op =) (map fst sorts') tyvars); val dt_info = Datatype_Data.get_all thy; @@ -736,45 +740,31 @@ if #strict config then error ("Nonemptiness check failed for datatype " ^ s) else reraise exn; - val _ = Datatype_Aux.message config ("Constructing datatype(s) " ^ commas_quote new_type_names); - + val _ = + Datatype_Aux.message config + ("Constructing datatype(s) " ^ commas_quote (map (Binding.name_of o #2) dts)); in thy - |> representation_proofs config dt_info new_type_names descr sorts - types_syntax constr_syntax (Datatype_Data.mk_case_names_induct (flat descr)) + |> representation_proofs config dt_info descr sorts types_syntax constr_syntax + (Datatype_Data.mk_case_names_induct (flat descr)) |-> (fn (inject, distinct, induct) => - Datatype_Data.derive_datatype_props - config dt_names (SOME new_type_names) descr sorts - induct inject distinct) + Datatype_Data.derive_datatype_props config dt_names descr sorts induct inject distinct) end; val add_datatype = gen_add_datatype Datatype_Data.cert_typ; -val datatype_cmd = snd ooo gen_add_datatype Datatype_Data.read_typ Datatype_Aux.default_config; +val add_datatype_cmd = snd oo gen_add_datatype Datatype_Data.read_typ Datatype_Aux.default_config; -local + +(* concrete syntax *) -fun prep_datatype_decls args = - let - val names = map - (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args; - val specs = map (fn ((((_, vs), t), mx), cons) => - (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args; - in (names, specs) end; - -val parse_datatype_decl = - (Scan.option (Parse.$$$ "(" |-- Parse.name --| Parse.$$$ ")") -- - Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- - (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix))); - -val parse_datatype_decls = Parse.and_list1 parse_datatype_decl >> prep_datatype_decls; - -in +val parse_decl = + Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- + (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix)) + >> (fn (((vs, t), mx), cons) => (vs, t, mx, map Parse.triple1 cons)); val _ = Outer_Syntax.command "datatype" "define inductive datatypes" Keyword.thy_decl - (parse_datatype_decls >> (fn (names, specs) => Toplevel.theory (datatype_cmd names specs))); - -end; + (Parse.and_list1 parse_decl >> (Toplevel.theory o add_datatype_cmd)); open Datatype_Data; diff -r 9dcbf6a1829c -r 615da8b8d758 src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Wed Nov 30 21:14:01 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Wed Nov 30 23:30:08 2011 +0100 @@ -15,7 +15,6 @@ type descr = (int * (string * dtyp list * (string * dtyp list) list)) list type info = {index : int, - alt_names : string list option, descr : descr, sorts : (string * sort) list, inject : thm list, @@ -188,7 +187,6 @@ type info = {index : int, - alt_names : string list option, descr : descr, sorts : (string * sort) list, inject : thm list, diff -r 9dcbf6a1829c -r 615da8b8d758 src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Wed Nov 30 21:14:01 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Wed Nov 30 23:30:08 2011 +0100 @@ -7,17 +7,16 @@ signature DATATYPE_DATA = sig include DATATYPE_COMMON - val derive_datatype_props : config -> string list -> string list option - -> descr list -> (string * sort) list -> thm -> thm list list -> thm list list - -> theory -> string list * theory - val rep_datatype : config -> (string list -> Proof.context -> Proof.context) - -> string list option -> term list -> theory -> Proof.state - val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state + val derive_datatype_props : config -> string list -> descr list -> (string * sort) list -> + thm -> thm list list -> thm list list -> theory -> string list * theory + val rep_datatype : config -> (string list -> Proof.context -> Proof.context) -> + term list -> theory -> Proof.state + val rep_datatype_cmd : string list -> theory -> Proof.state val get_info : theory -> string -> info option val the_info : theory -> string -> info - val the_descr : theory -> string list - -> descr * (string * sort) list * string list - * string * (string list * string list) * (typ list * typ list) + val the_descr : theory -> string list -> + descr * (string * sort) list * string list * string * + (string list * string list) * (typ list * typ list) val the_spec : theory -> string -> (string * sort) list * (string * typ list) list val all_distincts : theory -> typ list -> thm list list val get_constrs : theory -> string -> (string * typ) list option @@ -144,7 +143,7 @@ val (Ts, Us) = (pairself o map) Type protoTs; - val names = map Long_Name.base_name (the_default tycos (#alt_names info)); + val names = map Long_Name.base_name tycos; val (auxnames, _) = Name.make_context names |> fold_map (Name.variant o Datatype_Aux.name_of_typ) Us; @@ -284,13 +283,12 @@ ); fun interpretation f = Datatype_Interpretation.interpretation (uncurry f); -fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites +fun make_dt_info descr sorts induct inducts rec_names rec_rewrites (index, (((((((((((_, (tname, _, _))), inject), distinct), exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong), (split, split_asm))) = (tname, {index = index, - alt_names = alt_names, descr = descr, sorts = sorts, inject = inject, @@ -308,12 +306,12 @@ split = split, split_asm = split_asm}); -fun derive_datatype_props config dt_names alt_names descr sorts +fun derive_datatype_props config dt_names descr sorts induct inject distinct thy1 = let val thy2 = thy1 |> Theory.checkpoint; val flat_descr = flat descr; - val new_type_names = map Long_Name.base_name (the_default dt_names alt_names); + val new_type_names = map Long_Name.base_name dt_names; val _ = Datatype_Aux.message config ("Deriving properties for datatype(s) " ^ commas_quote new_type_names); @@ -343,7 +341,7 @@ val inducts = Project_Rule.projections (Proof_Context.init_global thy2) induct; val dt_infos = map_index - (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites) + (make_dt_info flat_descr sorts induct inducts rec_names rec_rewrites) (hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~ case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits); val dt_names = map fst dt_infos; @@ -380,11 +378,10 @@ (** declare existing type as datatype **) -fun prove_rep_datatype config dt_names alt_names descr sorts - raw_inject half_distinct raw_induct thy1 = +fun prove_rep_datatype config dt_names descr sorts raw_inject half_distinct raw_induct thy1 = let val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct; - val new_type_names = map Long_Name.base_name (the_default dt_names alt_names); + val new_type_names = map Long_Name.base_name dt_names; val prfx = Binding.qualify true (space_implode "_" new_type_names); val (((inject, distinct), [induct]), thy2) = thy1 @@ -395,11 +392,10 @@ [mk_case_names_induct descr])]; in thy2 - |> derive_datatype_props config dt_names alt_names [descr] sorts - induct inject distinct + |> derive_datatype_props config dt_names [descr] sorts induct inject distinct end; -fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy = +fun gen_rep_datatype prep_term config after_qed raw_ts thy = let val ctxt = Proof_Context.init_global thy; @@ -461,8 +457,7 @@ (*FIXME somehow dubious*) in Proof_Context.background_theory_result (* FIXME !? *) - (prove_rep_datatype config dt_names alt_names descr vs - raw_inject half_distinct raw_induct) + (prove_rep_datatype config dt_names descr vs raw_inject half_distinct raw_induct) #-> after_qed end; in @@ -489,10 +484,8 @@ val _ = Outer_Syntax.command "rep_datatype" "represent existing types inductively" Keyword.thy_goal - (Scan.option (Parse.$$$ "(" |-- Scan.repeat1 Parse.name --| Parse.$$$ ")") -- - Scan.repeat1 Parse.term - >> (fn (alt_names, ts) => - Toplevel.print o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts))); + (Scan.repeat1 Parse.term >> (fn ts => + Toplevel.print o Toplevel.theory_to_proof (rep_datatype_cmd ts))); open Datatype_Aux; diff -r 9dcbf6a1829c -r 615da8b8d758 src/HOL/Tools/Function/size.ML --- a/src/HOL/Tools/Function/size.ML Wed Nov 30 21:14:01 2011 +0100 +++ b/src/HOL/Tools/Function/size.ML Wed Nov 30 23:30:08 2011 +0100 @@ -58,10 +58,8 @@ fun prove_size_thms (info : info) new_type_names thy = let - val {descr, alt_names, sorts, rec_names, rec_rewrites, induct, ...} = info; + val {descr, sorts, rec_names, rec_rewrites, induct, ...} = info; val l = length new_type_names; - val alt_names' = (case alt_names of - NONE => replicate l NONE | SOME names => map SOME names); val descr' = List.take (descr, l); val (rec_names1, rec_names2) = chop l rec_names; val recTs = get_rec_types descr sorts; @@ -83,11 +81,10 @@ val extra_size = Option.map fst o lookup_size thy; val (((size_names, size_fns), def_names), def_names') = - recTs1 ~~ alt_names' |> - map (fn (T as Type (s, _), optname) => + recTs1 |> map (fn T as Type (s, _) => let - val s' = the_default (Long_Name.base_name s) optname ^ "_size"; - val s'' = Sign.full_bname thy s' + val s' = Long_Name.base_name s ^ "_size"; + val s'' = Sign.full_bname thy s'; in (s'', (list_comb (Const (s'', param_size_fTs @ [T] ---> HOLogic.natT), @@ -221,12 +218,13 @@ fun add_size_thms config (new_type_names as name :: _) thy = let - val info as {descr, alt_names, ...} = Datatype.the_info thy name; - val prefix = Long_Name.map_base_name (K (space_implode "_" - (the_default (map Long_Name.base_name new_type_names) alt_names))) name; + val info as {descr, ...} = Datatype.the_info thy name; + val prefix = + Long_Name.map_base_name (K (space_implode "_" (map Long_Name.base_name new_type_names))) name; val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt => is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs) descr - in if no_size then thy + in + if no_size then thy else thy |> Sign.root_path diff -r 9dcbf6a1829c -r 615da8b8d758 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Nov 30 21:14:01 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Nov 30 23:30:08 2011 +0100 @@ -932,13 +932,10 @@ fun case_rewrites thy Tcon = let - val info = Datatype.the_info thy Tcon - val descr = #descr info - val sorts = #sorts info - val typ_names = the_default [Tcon] (#alt_names info) + val {descr, sorts, ...} = Datatype.the_info thy Tcon in map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop) - (make_case_distribs typ_names [descr] sorts thy) + (make_case_distribs [Tcon] [descr] sorts thy) end fun instantiated_case_rewrites thy Tcon = diff -r 9dcbf6a1829c -r 615da8b8d758 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Nov 30 21:14:01 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Nov 30 23:30:08 2011 +0100 @@ -159,10 +159,12 @@ val eval_if_P = @{lemma "P ==> Predicate.eval x z ==> Predicate.eval (if P then x else y) z" by simp} fun get_case_rewrite t = - if (is_constructor thy t) then let - val case_rewrites = (#case_rewrites (Datatype.the_info thy - ((fst o dest_Type o fastype_of) t))) - in fold (union Thm.eq_thm) (case_rewrites :: map get_case_rewrite (snd (strip_comb t))) [] end + if (is_constructor thy t) then + let + val {case_rewrites, ...} = Datatype.the_info thy (fst (dest_Type (fastype_of t))) + in + fold (union Thm.eq_thm) (case_rewrites :: map get_case_rewrite (snd (strip_comb t))) [] + end else [] val simprules = insert Thm.eq_thm @{thm "unit.cases"} (insert Thm.eq_thm @{thm "prod.cases"} (fold (union Thm.eq_thm) (map get_case_rewrite out_ts) [])) @@ -327,13 +329,14 @@ | split_term_tac t = if (is_constructor thy t) then let - val info = Datatype.the_info thy ((fst o dest_Type o fastype_of) t) - val num_of_constrs = length (#case_rewrites info) + val {case_rewrites, split_asm, ...} = + Datatype.the_info thy (fst (dest_Type (fastype_of t))) + val num_of_constrs = length case_rewrites val (_, ts) = strip_comb t in print_tac options ("Term " ^ (Syntax.string_of_term ctxt t) ^ - "splitting with rules \n" ^ Display.string_of_thm ctxt (#split_asm info)) - THEN TRY ((Splitter.split_asm_tac [#split_asm info] 1) + "splitting with rules \n" ^ Display.string_of_thm ctxt split_asm) + THEN TRY (Splitter.split_asm_tac [split_asm] 1 THEN (print_tac options "after splitting with split_asm rules") (* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1) THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*) diff -r 9dcbf6a1829c -r 615da8b8d758 src/HOL/Tools/TFL/casesplit.ML --- a/src/HOL/Tools/TFL/casesplit.ML Wed Nov 30 21:14:01 2011 +0100 +++ b/src/HOL/Tools/TFL/casesplit.ML Wed Nov 30 23:30:08 2011 +0100 @@ -36,9 +36,9 @@ Type(ty_str, _) => ty_str | TFree(s,_) => error ("Free type: " ^ s) | TVar((s,i),_) => error ("Free variable: " ^ s) - val dt = Datatype.the_info thy ty_str + val {induct, ...} = Datatype.the_info thy ty_str in - cases_thm_of_induct_thm (#induct dt) + cases_thm_of_induct_thm induct end; diff -r 9dcbf6a1829c -r 615da8b8d758 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Wed Nov 30 21:14:01 2011 +0100 +++ b/src/HOL/Tools/inductive_realizer.ML Wed Nov 30 23:30:08 2011 +0100 @@ -305,15 +305,15 @@ val ((dummies, some_dt_names), thy2) = thy1 - |> add_dummies (Datatype.add_datatype - { strict = false, quiet = false } (map (Binding.name_of o #2) dts)) - (map (pair false) dts) [] + |> add_dummies (Datatype.add_datatype {strict = false, quiet = false}) + (map (pair false) dts) [] ||> Extraction.add_typeof_eqns_i ty_eqs ||> Extraction.add_realizes_eqns_i rlz_eqs; val dt_names = these some_dt_names; val case_thms = map (#case_rewrites o Datatype.the_info thy2) dt_names; - val rec_thms = if null dt_names then [] - else (#rec_rewrites o Datatype.the_info thy2) (hd dt_names); + val rec_thms = + if null dt_names then [] + else #rec_rewrites (Datatype.the_info thy2 (hd dt_names)); val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms); val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>