--- 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}?
"}
--- 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}
--- 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)"
--- 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,[])
--- 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
--- 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,
--- 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;
--- 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,
--- 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;
--- 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
--- 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 =
--- 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)))*)
--- 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;
--- 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) =>