1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Nov 30 21:14:01 2011 +0100
1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Nov 30 23:30:08 2011 +0100
1.3 @@ -693,7 +693,7 @@
1.4 @@{command (HOL) rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)
1.5 ;
1.6
1.7 - spec: @{syntax parname}? @{syntax typespec} @{syntax mixfix}? '=' (cons + '|')
1.8 + spec: @{syntax typespec} @{syntax mixfix}? '=' (cons + '|')
1.9 ;
1.10 cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?
1.11 "}
2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Nov 30 21:14:01 2011 +0100
2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Nov 30 23:30:08 2011 +0100
2.3 @@ -1036,10 +1036,6 @@
2.4 \rail@endplus
2.5 \rail@end
2.6 \rail@begin{2}{\isa{spec}}
2.7 -\rail@bar
2.8 -\rail@nextbar{1}
2.9 -\rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[]
2.10 -\rail@endbar
2.11 \rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
2.12 \rail@bar
2.13 \rail@nextbar{1}
3.1 --- a/src/HOL/Library/Bit.thy Wed Nov 30 21:14:01 2011 +0100
3.2 +++ b/src/HOL/Library/Bit.thy Wed Nov 30 23:30:08 2011 +0100
3.3 @@ -25,7 +25,7 @@
3.4
3.5 end
3.6
3.7 -rep_datatype (bit) "0::bit" "1::bit"
3.8 +rep_datatype "0::bit" "1::bit"
3.9 proof -
3.10 fix P and x :: bit
3.11 assume "P (0::bit)" and "P (1::bit)"
4.1 --- a/src/HOL/Nominal/nominal_atoms.ML Wed Nov 30 21:14:01 2011 +0100
4.2 +++ b/src/HOL/Nominal/nominal_atoms.ML Wed Nov 30 23:30:08 2011 +0100
4.3 @@ -100,8 +100,7 @@
4.4 val (_,thy1) =
4.5 fold_map (fn ak => fn thy =>
4.6 let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
4.7 - val (dt_names, thy1) = Datatype.add_datatype
4.8 - Datatype.default_config [ak] [dt] thy;
4.9 + val (dt_names, thy1) = Datatype.add_datatype Datatype.default_config [dt] thy;
4.10
4.11 val injects = maps (#inject o Datatype.the_info thy1) dt_names;
4.12 val ak_type = Type (Sign.intern_type thy1 ak,[])
5.1 --- a/src/HOL/Nominal/nominal_datatype.ML Wed Nov 30 21:14:01 2011 +0100
5.2 +++ b/src/HOL/Nominal/nominal_datatype.ML Wed Nov 30 23:30:08 2011 +0100
5.3 @@ -6,9 +6,9 @@
5.4
5.5 signature NOMINAL_DATATYPE =
5.6 sig
5.7 - val add_nominal_datatype : Datatype.config -> string list ->
5.8 - (string list * bstring * mixfix *
5.9 - (bstring * string list * mixfix) list) list -> theory -> theory
5.10 + val add_nominal_datatype : Datatype.config ->
5.11 + (string list * binding * mixfix * (binding * string list * mixfix) list) list ->
5.12 + theory -> theory
5.13 type descr
5.14 type nominal_datatype_info
5.15 val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table
5.16 @@ -188,14 +188,16 @@
5.17 fun fresh_star_const T U =
5.18 Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT);
5.19
5.20 -fun gen_add_nominal_datatype prep_typ config new_type_names dts thy =
5.21 +fun gen_add_nominal_datatype prep_typ config dts thy =
5.22 let
5.23 + val new_type_names = map (Binding.name_of o #2) dts;
5.24 +
5.25 +
5.26 (* this theory is used just for parsing *)
5.27
5.28 val tmp_thy = thy |>
5.29 Theory.copy |>
5.30 - Sign.add_types_global (map (fn (tvs, tname, mx, _) =>
5.31 - (Binding.name tname, length tvs, mx)) dts);
5.32 + Sign.add_types_global (map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dts);
5.33
5.34 val atoms = atoms_of thy;
5.35
5.36 @@ -224,7 +226,7 @@
5.37 map (fn (cname, cargs, mx) => (cname, mx)) constrs) dts';
5.38
5.39 val ps = map (fn (_, n, _, _) =>
5.40 - (Sign.full_bname tmp_thy n, Sign.full_bname tmp_thy (n ^ "_Rep"))) dts;
5.41 + (Sign.full_name tmp_thy n, Sign.full_name tmp_thy (Binding.suffix_name "_Rep" n))) dts;
5.42 val rps = map Library.swap ps;
5.43
5.44 fun replace_types (Type ("Nominal.ABS", [T, U])) =
5.45 @@ -233,17 +235,16 @@
5.46 Type (the_default s (AList.lookup op = ps s), map replace_types Ts)
5.47 | replace_types T = T;
5.48
5.49 - val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, Binding.name (tname ^ "_Rep"), NoSyn,
5.50 - map (fn (cname, cargs, mx) => (Binding.name (cname ^ "_Rep"),
5.51 - map replace_types cargs, NoSyn)) constrs)) dts';
5.52 + val dts'' = map (fn (tvs, tname, mx, constrs) =>
5.53 + (tvs, Binding.suffix_name "_Rep" tname, NoSyn,
5.54 + map (fn (cname, cargs, mx) => (Binding.suffix_name "_Rep" cname,
5.55 + map replace_types cargs, NoSyn)) constrs)) dts';
5.56
5.57 val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
5.58
5.59 - val (full_new_type_names',thy1) =
5.60 - Datatype.add_datatype config new_type_names' dts'' thy;
5.61 + val (full_new_type_names',thy1) = Datatype.add_datatype config dts'' thy;
5.62
5.63 - val {descr, induct, ...} =
5.64 - Datatype.the_info thy1 (hd full_new_type_names');
5.65 + val {descr, induct, ...} = Datatype.the_info thy1 (hd full_new_type_names');
5.66 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
5.67
5.68 val big_name = space_implode "_" new_type_names;
5.69 @@ -612,9 +613,9 @@
5.70
5.71 val (typedefs, thy6) =
5.72 thy4
5.73 - |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
5.74 - Typedef.add_typedef_global false (SOME (Binding.name name'))
5.75 - (Binding.name name, map (fn (v, _) => (v, dummyS)) tvs, mx) (* FIXME keep constraints!? *)
5.76 + |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy =>
5.77 + Typedef.add_typedef_global false NONE
5.78 + (name, map (fn (v, _) => (v, dummyS)) tvs, mx) (* FIXME keep constraints!? *)
5.79 (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
5.80 Const (cname, U --> HOLogic.boolT)) NONE
5.81 (rtac exI 1 THEN rtac CollectI 1 THEN
5.82 @@ -624,18 +625,17 @@
5.83 val permT = mk_permT
5.84 (TFree (singleton (Name.variant_list (map fst tvs)) "'a", HOLogic.typeS));
5.85 val pi = Free ("pi", permT);
5.86 - val T = Type (Sign.intern_type thy name, map TFree tvs);
5.87 + val T = Type (Sign.full_name thy name, map TFree tvs);
5.88 in apfst (pair r o hd)
5.89 - (Global_Theory.add_defs_unchecked true [((Binding.name ("prm_" ^ name ^ "_def"), Logic.mk_equals
5.90 - (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
5.91 - Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
5.92 - (Const ("Nominal.perm", permT --> U --> U) $ pi $
5.93 - (Const (Sign.intern_const thy ("Rep_" ^ name), T --> U) $
5.94 - Free ("x", T))))), [])] thy)
5.95 + (Global_Theory.add_defs_unchecked true
5.96 + [((Binding.map_name (fn n => "prm_" ^ n ^ "_def") name, Logic.mk_equals
5.97 + (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
5.98 + Const (Sign.intern_const thy ("Abs_" ^ Binding.name_of name), U --> T) $
5.99 + (Const ("Nominal.perm", permT --> U --> U) $ pi $
5.100 + (Const (Sign.intern_const thy ("Rep_" ^ Binding.name_of name), T --> U) $
5.101 + Free ("x", T))))), [])] thy)
5.102 end))
5.103 - (types_syntax ~~ tyvars ~~
5.104 - List.take (rep_set_names'' ~~ recTs', length new_type_names) ~~
5.105 - new_type_names);
5.106 + (types_syntax ~~ tyvars ~~ List.take (rep_set_names'' ~~ recTs', length new_type_names));
5.107
5.108 val perm_defs = map snd typedefs;
5.109 val Abs_inverse_thms = map (collect_simp o #Abs_inverse o snd o fst) typedefs;
5.110 @@ -800,7 +800,7 @@
5.111 (Const (rep_name, T --> T') $ lhs, rhs));
5.112 val def_name = (Long_Name.base_name cname) ^ "_def";
5.113 val ([def_thm], thy') = thy |>
5.114 - Sign.add_consts_i [(Binding.name cname', constrT, mx)] |>
5.115 + Sign.add_consts_i [(cname', constrT, mx)] |>
5.116 (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
5.117 in (thy', defs @ [def_thm], eqns @ [eqn]) end;
5.118
5.119 @@ -2002,7 +2002,7 @@
5.120
5.121 (* define primrec combinators *)
5.122
5.123 - val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
5.124 + val big_reccomb_name = space_implode "_" new_type_names ^ "_rec";
5.125 val reccomb_names = map (Sign.full_bname thy11)
5.126 (if length descr'' = 1 then [big_reccomb_name] else
5.127 (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
5.128 @@ -2069,23 +2069,9 @@
5.129
5.130 val add_nominal_datatype = gen_add_nominal_datatype Datatype.read_typ;
5.131
5.132 -
5.133 -(* FIXME: The following stuff should be exported by Datatype *)
5.134 -
5.135 -val datatype_decl =
5.136 - Scan.option (Parse.$$$ "(" |-- Parse.name --| Parse.$$$ ")") --
5.137 - Parse.type_args -- Parse.name -- Parse.opt_mixfix --
5.138 - (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.name -- Scan.repeat Parse.typ -- Parse.opt_mixfix));
5.139 -
5.140 -fun mk_datatype args =
5.141 - let
5.142 - val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
5.143 - val specs = map (fn ((((_, vs), t), mx), cons) =>
5.144 - (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
5.145 - in add_nominal_datatype Datatype.default_config names specs end;
5.146 -
5.147 val _ =
5.148 Outer_Syntax.command "nominal_datatype" "define inductive datatypes" Keyword.thy_decl
5.149 - (Parse.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
5.150 + (Parse.and_list1 Datatype.parse_decl
5.151 + >> (Toplevel.theory o add_nominal_datatype Datatype.default_config));
5.152
5.153 end
6.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML Wed Nov 30 21:14:01 2011 +0100
6.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Wed Nov 30 23:30:08 2011 +0100
6.3 @@ -305,7 +305,7 @@
6.4 val tyname = Sign.full_name thy tyb
6.5 in
6.6 (thy |>
6.7 - Datatype.add_datatype {strict = true, quiet = true} [s]
6.8 + Datatype.add_datatype {strict = true, quiet = true}
6.9 [([], tyb, NoSyn,
6.10 map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
6.11 add_enum_type s tyname,
7.1 --- a/src/HOL/Tools/Datatype/datatype.ML Wed Nov 30 21:14:01 2011 +0100
7.2 +++ b/src/HOL/Tools/Datatype/datatype.ML Wed Nov 30 23:30:08 2011 +0100
7.3 @@ -10,10 +10,13 @@
7.4 signature DATATYPE =
7.5 sig
7.6 include DATATYPE_DATA
7.7 - val add_datatype : config -> string list -> (string list * binding * mixfix *
7.8 - (binding * typ list * mixfix) list) list -> theory -> string list * theory
7.9 - val datatype_cmd : string list -> (string list * binding * mixfix *
7.10 - (binding * string list * mixfix) list) list -> theory -> theory
7.11 + val add_datatype: config ->
7.12 + (string list * binding * mixfix * (binding * typ list * mixfix) list) list ->
7.13 + theory -> string list * theory
7.14 + val add_datatype_cmd:
7.15 + (string list * binding * mixfix * (binding * string list * mixfix) list) list ->
7.16 + theory -> theory
7.17 + val parse_decl: (string list * binding * mixfix * (binding * string list * mixfix) list) parser
7.18 end;
7.19
7.20 structure Datatype : DATATYPE =
7.21 @@ -58,9 +61,10 @@
7.22 (** proof of characteristic theorems **)
7.23
7.24 fun representation_proofs (config : Datatype_Aux.config) (dt_info : Datatype_Aux.info Symtab.table)
7.25 - new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
7.26 + descr sorts types_syntax constr_syntax case_names_induct thy =
7.27 let
7.28 val descr' = flat descr;
7.29 + val new_type_names = map (Binding.name_of o fst) types_syntax;
7.30 val big_name = space_implode "_" new_type_names;
7.31 val thy1 = Sign.add_path big_name thy;
7.32 val big_rec_name = big_name ^ "_rep_set";
7.33 @@ -189,26 +193,26 @@
7.34
7.35 (********************************* typedef ********************************)
7.36
7.37 - val (typedefs, thy3) = thy2 |>
7.38 - Sign.parent_path |>
7.39 - fold_map (fn ((((name, mx), tvs), c), name') =>
7.40 - Typedef.add_typedef_global false (SOME (Binding.name name'))
7.41 + val (typedefs, thy3) = thy2
7.42 + |> Sign.parent_path
7.43 + |> fold_map
7.44 + (fn (((name, mx), tvs), c) =>
7.45 + Typedef.add_typedef_global false NONE
7.46 (name, map (rpair dummyS) tvs, mx)
7.47 (Collect $ Const (c, UnivT')) NONE
7.48 (rtac exI 1 THEN rtac CollectI 1 THEN
7.49 QUIET_BREADTH_FIRST (has_fewer_prems 1)
7.50 (resolve_tac rep_intrs 1)))
7.51 - (types_syntax ~~ tyvars ~~
7.52 - (take (length newTs) rep_set_names) ~~ new_type_names) ||>
7.53 - Sign.add_path big_name;
7.54 + (types_syntax ~~ tyvars ~~ (take (length newTs) rep_set_names))
7.55 + ||> Sign.add_path big_name;
7.56
7.57 (*********************** definition of constructors ***********************)
7.58
7.59 val big_rep_name = space_implode "_" new_type_names ^ "_Rep_";
7.60 val rep_names = map (prefix "Rep_") new_type_names;
7.61 - val rep_names' = map (fn i => big_rep_name ^ (string_of_int i))
7.62 - (1 upto (length (flat (tl descr))));
7.63 - val all_rep_names = map (Sign.intern_const thy3) rep_names @
7.64 + val rep_names' = map (fn i => big_rep_name ^ string_of_int i) (1 upto length (flat (tl descr)));
7.65 + val all_rep_names =
7.66 + map (Sign.intern_const thy3) rep_names @
7.67 map (Sign.full_bname thy3) rep_names';
7.68
7.69 (* isomorphism declarations *)
7.70 @@ -669,9 +673,9 @@
7.71
7.72
7.73
7.74 -(** definitional introduction of datatypes **)
7.75 +(** datatype definition **)
7.76
7.77 -fun gen_add_datatype prep_typ config new_type_names dts thy =
7.78 +fun gen_add_datatype prep_typ config dts thy =
7.79 let
7.80 val _ = Theory.requires thy "Datatype" "datatype definitions";
7.81
7.82 @@ -694,11 +698,11 @@
7.83 val dt_names = map fst new_dts;
7.84
7.85 val _ =
7.86 - (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
7.87 + (case duplicates (op =) (map fst new_dts) of
7.88 [] => ()
7.89 | dups => error ("Duplicate datatypes: " ^ commas dups));
7.90
7.91 - fun prep_dt_spec (tvs, tname, mx, constrs) tname' (dts', constr_syntax, sorts, i) =
7.92 + fun prep_dt_spec (tvs, tname, mx, constrs) (dts', constr_syntax, sorts, i) =
7.93 let
7.94 fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
7.95 let
7.96 @@ -707,7 +711,7 @@
7.97 (case subtract (op =) tvs (fold (curry Misc_Legacy.add_typ_tfree_names) cargs' []) of
7.98 [] => ()
7.99 | vs => error ("Extra type variables on rhs: " ^ commas vs));
7.100 - val c = Sign.full_name_path tmp_thy tname' cname;
7.101 + val c = Sign.full_name_path tmp_thy (Binding.name_of tname) cname;
7.102 in
7.103 (constrs @ [(c, map (Datatype_Aux.dtyp_of_typ new_dts) cargs')],
7.104 constr_syntax' @ [(cname, mx')], sorts'')
7.105 @@ -725,7 +729,7 @@
7.106 error ("Duplicate constructors " ^ commas dups ^ " in datatype " ^ Binding.print tname))
7.107 end;
7.108
7.109 - val (dts', constr_syntax, sorts', i) = fold2 prep_dt_spec dts new_type_names ([], [], [], 0);
7.110 + val (dts', constr_syntax, sorts', i) = fold prep_dt_spec dts ([], [], [], 0);
7.111 val sorts =
7.112 sorts' @ map (rpair (Sign.defaultS tmp_thy)) (subtract (op =) (map fst sorts') tyvars);
7.113 val dt_info = Datatype_Data.get_all thy;
7.114 @@ -736,45 +740,31 @@
7.115 if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
7.116 else reraise exn;
7.117
7.118 - val _ = Datatype_Aux.message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
7.119 -
7.120 + val _ =
7.121 + Datatype_Aux.message config
7.122 + ("Constructing datatype(s) " ^ commas_quote (map (Binding.name_of o #2) dts));
7.123 in
7.124 thy
7.125 - |> representation_proofs config dt_info new_type_names descr sorts
7.126 - types_syntax constr_syntax (Datatype_Data.mk_case_names_induct (flat descr))
7.127 + |> representation_proofs config dt_info descr sorts types_syntax constr_syntax
7.128 + (Datatype_Data.mk_case_names_induct (flat descr))
7.129 |-> (fn (inject, distinct, induct) =>
7.130 - Datatype_Data.derive_datatype_props
7.131 - config dt_names (SOME new_type_names) descr sorts
7.132 - induct inject distinct)
7.133 + Datatype_Data.derive_datatype_props config dt_names descr sorts induct inject distinct)
7.134 end;
7.135
7.136 val add_datatype = gen_add_datatype Datatype_Data.cert_typ;
7.137 -val datatype_cmd = snd ooo gen_add_datatype Datatype_Data.read_typ Datatype_Aux.default_config;
7.138 +val add_datatype_cmd = snd oo gen_add_datatype Datatype_Data.read_typ Datatype_Aux.default_config;
7.139
7.140 -local
7.141
7.142 -fun prep_datatype_decls args =
7.143 - let
7.144 - val names = map
7.145 - (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args;
7.146 - val specs = map (fn ((((_, vs), t), mx), cons) =>
7.147 - (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
7.148 - in (names, specs) end;
7.149 +(* concrete syntax *)
7.150
7.151 -val parse_datatype_decl =
7.152 - (Scan.option (Parse.$$$ "(" |-- Parse.name --| Parse.$$$ ")") --
7.153 - Parse.type_args -- Parse.binding -- Parse.opt_mixfix --
7.154 - (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix)));
7.155 -
7.156 -val parse_datatype_decls = Parse.and_list1 parse_datatype_decl >> prep_datatype_decls;
7.157 -
7.158 -in
7.159 +val parse_decl =
7.160 + Parse.type_args -- Parse.binding -- Parse.opt_mixfix --
7.161 + (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix))
7.162 + >> (fn (((vs, t), mx), cons) => (vs, t, mx, map Parse.triple1 cons));
7.163
7.164 val _ =
7.165 Outer_Syntax.command "datatype" "define inductive datatypes" Keyword.thy_decl
7.166 - (parse_datatype_decls >> (fn (names, specs) => Toplevel.theory (datatype_cmd names specs)));
7.167 -
7.168 -end;
7.169 + (Parse.and_list1 parse_decl >> (Toplevel.theory o add_datatype_cmd));
7.170
7.171
7.172 open Datatype_Data;
8.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML Wed Nov 30 21:14:01 2011 +0100
8.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Wed Nov 30 23:30:08 2011 +0100
8.3 @@ -15,7 +15,6 @@
8.4 type descr = (int * (string * dtyp list * (string * dtyp list) list)) list
8.5 type info =
8.6 {index : int,
8.7 - alt_names : string list option,
8.8 descr : descr,
8.9 sorts : (string * sort) list,
8.10 inject : thm list,
8.11 @@ -188,7 +187,6 @@
8.12
8.13 type info =
8.14 {index : int,
8.15 - alt_names : string list option,
8.16 descr : descr,
8.17 sorts : (string * sort) list,
8.18 inject : thm list,
9.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML Wed Nov 30 21:14:01 2011 +0100
9.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Wed Nov 30 23:30:08 2011 +0100
9.3 @@ -7,17 +7,16 @@
9.4 signature DATATYPE_DATA =
9.5 sig
9.6 include DATATYPE_COMMON
9.7 - val derive_datatype_props : config -> string list -> string list option
9.8 - -> descr list -> (string * sort) list -> thm -> thm list list -> thm list list
9.9 - -> theory -> string list * theory
9.10 - val rep_datatype : config -> (string list -> Proof.context -> Proof.context)
9.11 - -> string list option -> term list -> theory -> Proof.state
9.12 - val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
9.13 + val derive_datatype_props : config -> string list -> descr list -> (string * sort) list ->
9.14 + thm -> thm list list -> thm list list -> theory -> string list * theory
9.15 + val rep_datatype : config -> (string list -> Proof.context -> Proof.context) ->
9.16 + term list -> theory -> Proof.state
9.17 + val rep_datatype_cmd : string list -> theory -> Proof.state
9.18 val get_info : theory -> string -> info option
9.19 val the_info : theory -> string -> info
9.20 - val the_descr : theory -> string list
9.21 - -> descr * (string * sort) list * string list
9.22 - * string * (string list * string list) * (typ list * typ list)
9.23 + val the_descr : theory -> string list ->
9.24 + descr * (string * sort) list * string list * string *
9.25 + (string list * string list) * (typ list * typ list)
9.26 val the_spec : theory -> string -> (string * sort) list * (string * typ list) list
9.27 val all_distincts : theory -> typ list -> thm list list
9.28 val get_constrs : theory -> string -> (string * typ) list option
9.29 @@ -144,7 +143,7 @@
9.30
9.31 val (Ts, Us) = (pairself o map) Type protoTs;
9.32
9.33 - val names = map Long_Name.base_name (the_default tycos (#alt_names info));
9.34 + val names = map Long_Name.base_name tycos;
9.35 val (auxnames, _) =
9.36 Name.make_context names
9.37 |> fold_map (Name.variant o Datatype_Aux.name_of_typ) Us;
9.38 @@ -284,13 +283,12 @@
9.39 );
9.40 fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
9.41
9.42 -fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites
9.43 +fun make_dt_info descr sorts induct inducts rec_names rec_rewrites
9.44 (index, (((((((((((_, (tname, _, _))), inject), distinct),
9.45 exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong),
9.46 (split, split_asm))) =
9.47 (tname,
9.48 {index = index,
9.49 - alt_names = alt_names,
9.50 descr = descr,
9.51 sorts = sorts,
9.52 inject = inject,
9.53 @@ -308,12 +306,12 @@
9.54 split = split,
9.55 split_asm = split_asm});
9.56
9.57 -fun derive_datatype_props config dt_names alt_names descr sorts
9.58 +fun derive_datatype_props config dt_names descr sorts
9.59 induct inject distinct thy1 =
9.60 let
9.61 val thy2 = thy1 |> Theory.checkpoint;
9.62 val flat_descr = flat descr;
9.63 - val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
9.64 + val new_type_names = map Long_Name.base_name dt_names;
9.65 val _ =
9.66 Datatype_Aux.message config
9.67 ("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
9.68 @@ -343,7 +341,7 @@
9.69
9.70 val inducts = Project_Rule.projections (Proof_Context.init_global thy2) induct;
9.71 val dt_infos = map_index
9.72 - (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
9.73 + (make_dt_info flat_descr sorts induct inducts rec_names rec_rewrites)
9.74 (hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~
9.75 case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
9.76 val dt_names = map fst dt_infos;
9.77 @@ -380,11 +378,10 @@
9.78
9.79 (** declare existing type as datatype **)
9.80
9.81 -fun prove_rep_datatype config dt_names alt_names descr sorts
9.82 - raw_inject half_distinct raw_induct thy1 =
9.83 +fun prove_rep_datatype config dt_names descr sorts raw_inject half_distinct raw_induct thy1 =
9.84 let
9.85 val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
9.86 - val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
9.87 + val new_type_names = map Long_Name.base_name dt_names;
9.88 val prfx = Binding.qualify true (space_implode "_" new_type_names);
9.89 val (((inject, distinct), [induct]), thy2) =
9.90 thy1
9.91 @@ -395,11 +392,10 @@
9.92 [mk_case_names_induct descr])];
9.93 in
9.94 thy2
9.95 - |> derive_datatype_props config dt_names alt_names [descr] sorts
9.96 - induct inject distinct
9.97 + |> derive_datatype_props config dt_names [descr] sorts induct inject distinct
9.98 end;
9.99
9.100 -fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
9.101 +fun gen_rep_datatype prep_term config after_qed raw_ts thy =
9.102 let
9.103 val ctxt = Proof_Context.init_global thy;
9.104
9.105 @@ -461,8 +457,7 @@
9.106 (*FIXME somehow dubious*)
9.107 in
9.108 Proof_Context.background_theory_result (* FIXME !? *)
9.109 - (prove_rep_datatype config dt_names alt_names descr vs
9.110 - raw_inject half_distinct raw_induct)
9.111 + (prove_rep_datatype config dt_names descr vs raw_inject half_distinct raw_induct)
9.112 #-> after_qed
9.113 end;
9.114 in
9.115 @@ -489,10 +484,8 @@
9.116
9.117 val _ =
9.118 Outer_Syntax.command "rep_datatype" "represent existing types inductively" Keyword.thy_goal
9.119 - (Scan.option (Parse.$$$ "(" |-- Scan.repeat1 Parse.name --| Parse.$$$ ")") --
9.120 - Scan.repeat1 Parse.term
9.121 - >> (fn (alt_names, ts) =>
9.122 - Toplevel.print o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
9.123 + (Scan.repeat1 Parse.term >> (fn ts =>
9.124 + Toplevel.print o Toplevel.theory_to_proof (rep_datatype_cmd ts)));
9.125
9.126
9.127 open Datatype_Aux;
10.1 --- a/src/HOL/Tools/Function/size.ML Wed Nov 30 21:14:01 2011 +0100
10.2 +++ b/src/HOL/Tools/Function/size.ML Wed Nov 30 23:30:08 2011 +0100
10.3 @@ -58,10 +58,8 @@
10.4
10.5 fun prove_size_thms (info : info) new_type_names thy =
10.6 let
10.7 - val {descr, alt_names, sorts, rec_names, rec_rewrites, induct, ...} = info;
10.8 + val {descr, sorts, rec_names, rec_rewrites, induct, ...} = info;
10.9 val l = length new_type_names;
10.10 - val alt_names' = (case alt_names of
10.11 - NONE => replicate l NONE | SOME names => map SOME names);
10.12 val descr' = List.take (descr, l);
10.13 val (rec_names1, rec_names2) = chop l rec_names;
10.14 val recTs = get_rec_types descr sorts;
10.15 @@ -83,11 +81,10 @@
10.16 val extra_size = Option.map fst o lookup_size thy;
10.17
10.18 val (((size_names, size_fns), def_names), def_names') =
10.19 - recTs1 ~~ alt_names' |>
10.20 - map (fn (T as Type (s, _), optname) =>
10.21 + recTs1 |> map (fn T as Type (s, _) =>
10.22 let
10.23 - val s' = the_default (Long_Name.base_name s) optname ^ "_size";
10.24 - val s'' = Sign.full_bname thy s'
10.25 + val s' = Long_Name.base_name s ^ "_size";
10.26 + val s'' = Sign.full_bname thy s';
10.27 in
10.28 (s'',
10.29 (list_comb (Const (s'', param_size_fTs @ [T] ---> HOLogic.natT),
10.30 @@ -221,12 +218,13 @@
10.31
10.32 fun add_size_thms config (new_type_names as name :: _) thy =
10.33 let
10.34 - val info as {descr, alt_names, ...} = Datatype.the_info thy name;
10.35 - val prefix = Long_Name.map_base_name (K (space_implode "_"
10.36 - (the_default (map Long_Name.base_name new_type_names) alt_names))) name;
10.37 + val info as {descr, ...} = Datatype.the_info thy name;
10.38 + val prefix =
10.39 + Long_Name.map_base_name (K (space_implode "_" (map Long_Name.base_name new_type_names))) name;
10.40 val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
10.41 is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs) descr
10.42 - in if no_size then thy
10.43 + in
10.44 + if no_size then thy
10.45 else
10.46 thy
10.47 |> Sign.root_path
11.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Nov 30 21:14:01 2011 +0100
11.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Nov 30 23:30:08 2011 +0100
11.3 @@ -932,13 +932,10 @@
11.4
11.5 fun case_rewrites thy Tcon =
11.6 let
11.7 - val info = Datatype.the_info thy Tcon
11.8 - val descr = #descr info
11.9 - val sorts = #sorts info
11.10 - val typ_names = the_default [Tcon] (#alt_names info)
11.11 + val {descr, sorts, ...} = Datatype.the_info thy Tcon
11.12 in
11.13 map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
11.14 - (make_case_distribs typ_names [descr] sorts thy)
11.15 + (make_case_distribs [Tcon] [descr] sorts thy)
11.16 end
11.17
11.18 fun instantiated_case_rewrites thy Tcon =
12.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Nov 30 21:14:01 2011 +0100
12.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Nov 30 23:30:08 2011 +0100
12.3 @@ -159,10 +159,12 @@
12.4 val eval_if_P =
12.5 @{lemma "P ==> Predicate.eval x z ==> Predicate.eval (if P then x else y) z" by simp}
12.6 fun get_case_rewrite t =
12.7 - if (is_constructor thy t) then let
12.8 - val case_rewrites = (#case_rewrites (Datatype.the_info thy
12.9 - ((fst o dest_Type o fastype_of) t)))
12.10 - in fold (union Thm.eq_thm) (case_rewrites :: map get_case_rewrite (snd (strip_comb t))) [] end
12.11 + if (is_constructor thy t) then
12.12 + let
12.13 + val {case_rewrites, ...} = Datatype.the_info thy (fst (dest_Type (fastype_of t)))
12.14 + in
12.15 + fold (union Thm.eq_thm) (case_rewrites :: map get_case_rewrite (snd (strip_comb t))) []
12.16 + end
12.17 else []
12.18 val simprules = insert Thm.eq_thm @{thm "unit.cases"} (insert Thm.eq_thm @{thm "prod.cases"}
12.19 (fold (union Thm.eq_thm) (map get_case_rewrite out_ts) []))
12.20 @@ -327,13 +329,14 @@
12.21 | split_term_tac t =
12.22 if (is_constructor thy t) then
12.23 let
12.24 - val info = Datatype.the_info thy ((fst o dest_Type o fastype_of) t)
12.25 - val num_of_constrs = length (#case_rewrites info)
12.26 + val {case_rewrites, split_asm, ...} =
12.27 + Datatype.the_info thy (fst (dest_Type (fastype_of t)))
12.28 + val num_of_constrs = length case_rewrites
12.29 val (_, ts) = strip_comb t
12.30 in
12.31 print_tac options ("Term " ^ (Syntax.string_of_term ctxt t) ^
12.32 - "splitting with rules \n" ^ Display.string_of_thm ctxt (#split_asm info))
12.33 - THEN TRY ((Splitter.split_asm_tac [#split_asm info] 1)
12.34 + "splitting with rules \n" ^ Display.string_of_thm ctxt split_asm)
12.35 + THEN TRY (Splitter.split_asm_tac [split_asm] 1
12.36 THEN (print_tac options "after splitting with split_asm rules")
12.37 (* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1)
12.38 THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
13.1 --- a/src/HOL/Tools/TFL/casesplit.ML Wed Nov 30 21:14:01 2011 +0100
13.2 +++ b/src/HOL/Tools/TFL/casesplit.ML Wed Nov 30 23:30:08 2011 +0100
13.3 @@ -36,9 +36,9 @@
13.4 Type(ty_str, _) => ty_str
13.5 | TFree(s,_) => error ("Free type: " ^ s)
13.6 | TVar((s,i),_) => error ("Free variable: " ^ s)
13.7 - val dt = Datatype.the_info thy ty_str
13.8 + val {induct, ...} = Datatype.the_info thy ty_str
13.9 in
13.10 - cases_thm_of_induct_thm (#induct dt)
13.11 + cases_thm_of_induct_thm induct
13.12 end;
13.13
13.14
14.1 --- a/src/HOL/Tools/inductive_realizer.ML Wed Nov 30 21:14:01 2011 +0100
14.2 +++ b/src/HOL/Tools/inductive_realizer.ML Wed Nov 30 23:30:08 2011 +0100
14.3 @@ -305,15 +305,15 @@
14.4
14.5 val ((dummies, some_dt_names), thy2) =
14.6 thy1
14.7 - |> add_dummies (Datatype.add_datatype
14.8 - { strict = false, quiet = false } (map (Binding.name_of o #2) dts))
14.9 - (map (pair false) dts) []
14.10 + |> add_dummies (Datatype.add_datatype {strict = false, quiet = false})
14.11 + (map (pair false) dts) []
14.12 ||> Extraction.add_typeof_eqns_i ty_eqs
14.13 ||> Extraction.add_realizes_eqns_i rlz_eqs;
14.14 val dt_names = these some_dt_names;
14.15 val case_thms = map (#case_rewrites o Datatype.the_info thy2) dt_names;
14.16 - val rec_thms = if null dt_names then []
14.17 - else (#rec_rewrites o Datatype.the_info thy2) (hd dt_names);
14.18 + val rec_thms =
14.19 + if null dt_names then []
14.20 + else #rec_rewrites (Datatype.the_info thy2 (hd dt_names));
14.21 val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
14.22 HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms);
14.23 val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>