--- a/src/HOL/Nominal/nominal_datatype.ML Mon Dec 12 20:55:57 2011 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Mon Dec 12 23:05:21 2011 +0100
@@ -77,7 +77,6 @@
type nominal_datatype_info =
{index : int,
descr : descr,
- sorts : (string * sort) list,
rec_names : string list,
rec_rewrites : thm list,
induction : thm,
@@ -100,12 +99,11 @@
(**** make datatype info ****)
-fun make_dt_info descr sorts induct reccomb_names rec_thms
+fun make_dt_info descr induct reccomb_names rec_thms
(i, (((_, (tname, _, _)), distinct), inject)) =
(tname,
{index = i,
descr = descr,
- sorts = sorts,
rec_names = reccomb_names,
rec_rewrites = rec_thms,
induction = induct,
@@ -245,7 +243,7 @@
val (full_new_type_names',thy1) = Datatype.add_datatype config dts'' thy;
val {descr, induct, ...} = Datatype.the_info thy1 (hd full_new_type_names');
- fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
+ fun nth_dtyp i = typ_of_dtyp descr (DtRec i);
val big_name = space_implode "_" new_type_names;
@@ -268,7 +266,7 @@
let val T = nth_dtyp i
in map (fn (cname, dts) =>
let
- val Ts = map (typ_of_dtyp descr sorts) dts;
+ val Ts = map (typ_of_dtyp descr) dts;
val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
val args = map Free (names ~~ Ts);
val c = Const (cname, Ts ---> T);
@@ -518,7 +516,7 @@
apfst (cons dt) (strip_option dt')
| strip_option dt = ([], dt);
- val dt_atomTs = distinct op = (map (typ_of_dtyp descr sorts)
+ val dt_atomTs = distinct op = (map (typ_of_dtyp descr)
(maps (fn (_, (_, _, cs)) => maps (maps (fst o strip_option) o snd) cs) descr));
val dt_atoms = map (fst o dest_Type) dt_atomTs;
@@ -528,9 +526,9 @@
let
val (dts, dt') = strip_option dt;
val (dts', dt'') = strip_dtyp dt';
- val Ts = map (typ_of_dtyp descr sorts) dts;
- val Us = map (typ_of_dtyp descr sorts) dts';
- val T = typ_of_dtyp descr sorts dt'';
+ val Ts = map (typ_of_dtyp descr) dts;
+ val Us = map (typ_of_dtyp descr) dts';
+ val T = typ_of_dtyp descr dt'';
val free = mk_Free "x" (Us ---> T) j;
val free' = app_bnds free (length Us);
fun mk_abs_fun T (i, t) =
@@ -756,14 +754,14 @@
map (fn ((cname, cargs), idxs) => (cname, partition_cargs idxs cargs))
(constrs ~~ idxss)))) (descr'' ~~ ndescr);
- fun nth_dtyp' i = typ_of_dtyp descr'' sorts (DtRec i);
+ fun nth_dtyp' i = typ_of_dtyp descr'' (DtRec i);
val rep_names = map (fn s =>
Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names;
val abs_names = map (fn s =>
Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
- val recTs = get_rec_types descr'' sorts;
+ val recTs = get_rec_types descr'';
val newTs' = take (length new_type_names) recTs';
val newTs = take (length new_type_names) recTs;
@@ -774,17 +772,17 @@
let
fun constr_arg (dts, dt) (j, l_args, r_args) =
let
- val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp descr'' sorts dt) i)
+ val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp descr'' dt) i)
(dts ~~ (j upto j + length dts - 1))
- val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
+ val x = mk_Free "x" (typ_of_dtyp descr'' dt) (j + length dts)
in
(j + length dts + 1,
xs @ x :: l_args,
fold_rev mk_abs_fun xs
(case dt of
DtRec k => if k < length new_type_names then
- Const (nth rep_names k, typ_of_dtyp descr'' sorts dt -->
- typ_of_dtyp descr sorts dt) $ x
+ Const (nth rep_names k, typ_of_dtyp descr'' dt -->
+ typ_of_dtyp descr dt) $ x
else error "nested recursion not (yet) supported"
| _ => x) :: r_args)
end
@@ -866,7 +864,7 @@
(* prove distinctness theorems *)
- val distinct_props = Datatype_Prop.make_distincts descr' sorts;
+ val distinct_props = Datatype_Prop.make_distincts descr';
val dist_rewrites = map2 (fn rep_thms => fn dist_lemma =>
dist_lemma :: rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0])
constr_rep_thmss dist_lemmas;
@@ -902,10 +900,10 @@
fun constr_arg (dts, dt) (j, l_args, r_args) =
let
- val Ts = map (typ_of_dtyp descr'' sorts) dts;
+ val Ts = map (typ_of_dtyp descr'') dts;
val xs = map (fn (T, i) => mk_Free "x" T i)
(Ts ~~ (j upto j + length dts - 1))
- val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
+ val x = mk_Free "x" (typ_of_dtyp descr'' dt) (j + length dts)
in
(j + length dts + 1,
xs @ x :: l_args,
@@ -952,11 +950,11 @@
fun make_inj (dts, dt) (j, args1, args2, eqs) =
let
- val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
+ val Ts_idx = map (typ_of_dtyp descr'') dts ~~ (j upto j + length dts - 1);
val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
val ys = map (fn (T, i) => mk_Free "y" T i) Ts_idx;
- val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts);
- val y = mk_Free "y" (typ_of_dtyp descr'' sorts dt) (j + length dts)
+ val x = mk_Free "x" (typ_of_dtyp descr'' dt) (j + length dts);
+ val y = mk_Free "y" (typ_of_dtyp descr'' dt) (j + length dts);
in
(j + length dts + 1,
xs @ (x :: args1), ys @ (y :: args2),
@@ -995,9 +993,9 @@
fun process_constr (dts, dt) (j, args1, args2) =
let
- val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
+ val Ts_idx = map (typ_of_dtyp descr'') dts ~~ (j upto j + length dts - 1);
val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
- val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
+ val x = mk_Free "x" (typ_of_dtyp descr'' dt) (j + length dts);
in
(j + length dts + 1,
xs @ (x :: args1), fold_rev mk_abs_fun xs x :: args2)
@@ -1066,7 +1064,7 @@
val Abs_inverse_thms' = map (fn r => r RS subst) Abs_inverse_thms;
- val dt_induct_prop = Datatype_Prop.make_ind descr' sorts;
+ val dt_induct_prop = Datatype_Prop.make_ind descr';
val dt_induct = Goal.prove_global thy8 []
(Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
(fn {prems, ...} => EVERY
@@ -1163,8 +1161,8 @@
fun make_ind_prem fsT f k T ((cname, cargs), idxs) =
let
val recs = filter is_rec_type cargs;
- val Ts = map (typ_of_dtyp descr'' sorts) cargs;
- val recTs' = map (typ_of_dtyp descr'' sorts) recs;
+ val Ts = map (typ_of_dtyp descr'') cargs;
+ val recTs' = map (typ_of_dtyp descr'') recs;
val tnames = Name.variant_list pnames (Datatype_Prop.make_tnames Ts);
val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
val frees = tnames ~~ Ts;
@@ -1416,7 +1414,7 @@
val used = fold Term.add_tfree_namesT recTs [];
- val (rec_result_Ts', rec_fn_Ts') = Datatype_Prop.make_primrec_Ts descr' sorts used;
+ val (rec_result_Ts', rec_fn_Ts') = Datatype_Prop.make_primrec_Ts descr' used;
val rec_sort = if null dt_atomTs then HOLogic.typeS else
Sign.minimize_sort thy10 (Sign.certify_sort thy10 pt_cp_sort);
@@ -1459,7 +1457,7 @@
fun make_rec_intr T p rec_set ((cname, cargs), idxs)
(rec_intr_ts, rec_prems, rec_prems', rec_eq_prems, l) =
let
- val Ts = map (typ_of_dtyp descr'' sorts) cargs;
+ val Ts = map (typ_of_dtyp descr'') cargs;
val frees = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) ~~ Ts;
val frees' = partition_cargs idxs frees;
val binders = maps fst frees';
@@ -2046,9 +2044,9 @@
resolve_tac rec_intrs 1,
REPEAT (solve (prems @ rec_total_thms) prems 1)])
end) (rec_eq_prems ~~
- Datatype_Prop.make_primrecs new_type_names descr' sorts thy12);
+ Datatype_Prop.make_primrecs new_type_names descr' thy12);
- val dt_infos = map_index (make_dt_info pdescr sorts induct reccomb_names rec_thms)
+ val dt_infos = map_index (make_dt_info pdescr induct reccomb_names rec_thms)
(descr1 ~~ distinct_thms ~~ inject_thms);
(* FIXME: theorems are stored in database for testing only *)
--- a/src/HOL/Tools/Datatype/datatype.ML Mon Dec 12 20:55:57 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Mon Dec 12 23:05:21 2011 +0100
@@ -61,7 +61,7 @@
(** proof of characteristic theorems **)
fun representation_proofs (config : Datatype_Aux.config) (dt_info : Datatype_Aux.info Symtab.table)
- descr sorts types_syntax constr_syntax case_names_induct thy =
+ descr 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;
@@ -74,17 +74,16 @@
val rep_set_names = map (Sign.full_bname thy1) rep_set_names';
val tyvars = map (fn (_, (_, Ts, _)) => map Datatype_Aux.dest_DtTFree Ts) (hd descr);
- val leafTs' = Datatype_Aux.get_nonrec_types descr' sorts;
- val branchTs = Datatype_Aux.get_branching_types descr' sorts;
+ val leafTs' = Datatype_Aux.get_nonrec_types descr';
+ val branchTs = Datatype_Aux.get_branching_types descr';
val branchT =
if null branchTs then HOLogic.unitT
else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) branchTs;
val arities = remove (op =) 0 (Datatype_Aux.get_arities descr');
val unneeded_vars =
- subtract (op =) (fold Term.add_tfree_namesT (leafTs' @ branchTs) []) (hd tyvars);
- val leafTs =
- leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
- val recTs = Datatype_Aux.get_rec_types descr' sorts;
+ subtract (op =) (fold Term.add_tfreesT (leafTs' @ branchTs) []) (hd tyvars);
+ val leafTs = leafTs' @ map TFree unneeded_vars;
+ val recTs = Datatype_Aux.get_rec_types descr';
val (newTs, oldTs) = chop (length (hd descr)) recTs;
val sumT =
if null leafTs then HOLogic.unitT
@@ -156,7 +155,7 @@
(case Datatype_Aux.strip_dtyp dt of
(dts, Datatype_Aux.DtRec k) =>
let
- val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) dts;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr') dts;
val free_t =
Datatype_Aux.app_bnds (Datatype_Aux.mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
in
@@ -166,7 +165,7 @@
mk_lim free_t Ts :: ts)
end
| _ =>
- let val T = Datatype_Aux.typ_of_dtyp descr' sorts dt
+ let val T = Datatype_Aux.typ_of_dtyp descr' dt
in (j + 1, prems, (Leaf $ mk_inj T (Datatype_Aux.mk_Free "x" T j)) :: ts) end);
val (_, prems, ts) = fold_rev mk_prem cargs (1, [], []);
@@ -194,8 +193,7 @@
|> Sign.parent_path
|> fold_map
(fn (((name, mx), tvs), c) =>
- Typedef.add_typedef_global false NONE
- (name, map (rpair dummyS) tvs, mx)
+ Typedef.add_typedef_global false NONE (name, tvs, mx)
(Collect $ Const (c, UnivT')) NONE
(rtac exI 1 THEN rtac CollectI 1 THEN
QUIET_BREADTH_FIRST (has_fewer_prems 1)
@@ -223,7 +221,7 @@
let
fun constr_arg dt (j, l_args, r_args) =
let
- val T = Datatype_Aux.typ_of_dtyp descr' sorts dt;
+ val T = Datatype_Aux.typ_of_dtyp descr' dt;
val free_t = Datatype_Aux.mk_Free "x" T j;
in
(case (Datatype_Aux.strip_dtyp dt, strip_type T) of
@@ -235,7 +233,7 @@
end;
val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);
- val constrT = (map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs) ---> T;
+ val constrT = map (Datatype_Aux.typ_of_dtyp descr') cargs ---> T;
val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
val lhs = list_comb (Const (cname, constrT), l_args);
@@ -305,7 +303,7 @@
fun make_iso_def k ks n (cname, cargs) (fs, eqns, i) =
let
- val argTs = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+ val argTs = map (Datatype_Aux.typ_of_dtyp descr') cargs;
val T = nth recTs k;
val rep_name = nth all_rep_names k;
val rep_const = Const (rep_name, T --> Univ_elT);
@@ -313,7 +311,7 @@
fun process_arg ks' dt (i2, i2', ts, Ts) =
let
- val T' = Datatype_Aux.typ_of_dtyp descr' sorts dt;
+ val T' = Datatype_Aux.typ_of_dtyp descr' dt;
val (Us, U) = strip_type T'
in
(case Datatype_Aux.strip_dtyp dt of
@@ -556,7 +554,7 @@
in prove ts end;
val distinct_thms =
- map2 (prove_distinct_thms) dist_rewrites (Datatype_Prop.make_distincts descr sorts);
+ map2 (prove_distinct_thms) dist_rewrites (Datatype_Prop.make_distincts descr);
(* prove injectivity of constructors *)
@@ -582,7 +580,7 @@
val constr_inject =
map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
- ((Datatype_Prop.make_injs descr sorts) ~~ constr_rep_thms);
+ (Datatype_Prop.make_injs descr ~~ constr_rep_thms);
val ((constr_inject', distinct_thms'), thy6) =
thy5
@@ -642,7 +640,7 @@
else map (Free o apfst fst o dest_Var) Ps;
val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
- val dt_induct_prop = Datatype_Prop.make_ind descr sorts;
+ val dt_induct_prop = Datatype_Prop.make_ind descr;
val dt_induct =
Skip_Proof.prove_global thy6 []
(Logic.strip_imp_prems dt_induct_prop)
@@ -698,7 +696,7 @@
val _ =
(case duplicates (op =) (map fst new_dts) of
[] => ()
- | dups => error ("Duplicate datatypes: " ^ commas dups));
+ | dups => error ("Duplicate datatypes: " ^ commas_quote dups));
fun prep_dt_spec (tvs, tname, mx, constrs) (dts', constr_syntax, sorts, i) =
let
@@ -721,21 +719,28 @@
in
(case duplicates (op =) (map fst constrs') of
[] =>
- (dts' @ [(i, (Sign.full_name tmp_thy tname, map Datatype_Aux.DtTFree tvs, constrs'))],
+ (dts' @ [(i, (Sign.full_name tmp_thy tname, tvs, constrs'))],
constr_syntax @ [constr_syntax'], sorts', i + 1)
| dups =>
- error ("Duplicate constructors " ^ commas dups ^ " in datatype " ^ Binding.print tname))
+ error ("Duplicate constructors " ^ commas_quote dups ^
+ " in datatype " ^ Binding.print tname))
end;
- 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 (dts0, constr_syntax, sorts', i) = fold prep_dt_spec dts ([], [], [], 0);
+ val tmp_ctxt' = tmp_ctxt |> fold (Variable.declare_typ o TFree) sorts';
+
+ val dts' = dts0 |> map (fn (i, (name, tvs, cs)) =>
+ let
+ val args = tvs |>
+ map (fn a => Datatype_Aux.DtTFree (a, Proof_Context.default_sort tmp_ctxt' (a, ~1)));
+ in (i, (name, args, cs)) end);
+
val dt_info = Datatype_Data.get_all thy;
- val (descr, _) = Datatype_Aux.unfold_datatypes tmp_ctxt dts' sorts dt_info dts' i;
+ val (descr, _) = Datatype_Aux.unfold_datatypes tmp_ctxt dts' dt_info dts' i;
val _ =
Datatype_Aux.check_nonempty descr
handle (exn as Datatype_Aux.Datatype_Empty s) =>
- if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
+ if #strict config then error ("Nonemptiness check failed for datatype " ^ quote s)
else reraise exn;
val _ =
@@ -743,10 +748,10 @@
("Constructing datatype(s) " ^ commas_quote (map (Binding.name_of o #2) dts));
in
thy
- |> representation_proofs config dt_info descr sorts types_syntax constr_syntax
+ |> representation_proofs config dt_info descr types_syntax constr_syntax
(Datatype_Data.mk_case_names_induct (flat descr))
|-> (fn (inject, distinct, induct) =>
- Datatype_Data.derive_datatype_props config dt_names descr sorts induct inject distinct)
+ Datatype_Data.derive_datatype_props config dt_names descr induct inject distinct)
end;
val add_datatype = gen_add_datatype Datatype_Data.cert_typ;
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Dec 12 20:55:57 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Dec 12 23:05:21 2011 +0100
@@ -9,27 +9,21 @@
signature DATATYPE_ABS_PROOFS =
sig
include DATATYPE_COMMON
- val prove_casedist_thms : config -> string list ->
- descr list -> (string * sort) list -> thm ->
+ val prove_casedist_thms : config -> string list -> descr list -> thm ->
attribute list -> theory -> thm list * theory
- val prove_primrec_thms : config -> string list ->
- descr list -> (string * sort) list ->
- (string -> thm list) -> thm list list -> thm list list * thm list list ->
- thm -> theory -> (string list * thm list) * theory
- val prove_case_thms : config -> string list ->
- descr list -> (string * sort) list ->
- string list -> thm list -> theory -> (thm list list * string list) * theory
- val prove_split_thms : config -> string list ->
- descr list -> (string * sort) list ->
- thm list list -> thm list list -> thm list -> thm list list -> theory ->
- (thm * thm) list * theory
+ val prove_primrec_thms : config -> string list -> descr list ->
+ (string -> thm list) -> thm list list -> thm list list * thm list list ->
+ thm -> theory -> (string list * thm list) * theory
+ val prove_case_thms : config -> string list -> descr list ->
+ string list -> thm list -> theory -> (thm list list * string list) * theory
+ val prove_split_thms : config -> string list -> descr list ->
+ thm list list -> thm list list -> thm list -> thm list list -> theory ->
+ (thm * thm) list * theory
val prove_nchotomys : config -> string list -> descr list ->
- (string * sort) list -> thm list -> theory -> thm list * theory
- val prove_weak_case_congs : string list -> descr list ->
- (string * sort) list -> theory -> thm list * theory
- val prove_case_congs : string list ->
- descr list -> (string * sort) list ->
- thm list -> thm list list -> theory -> thm list * theory
+ thm list -> theory -> thm list * theory
+ val prove_weak_case_congs : string list -> descr list -> theory -> thm list * theory
+ val prove_case_congs : string list -> descr list ->
+ thm list -> thm list list -> theory -> thm list * theory
end;
structure Datatype_Abs_Proofs: DATATYPE_ABS_PROOFS =
@@ -38,12 +32,12 @@
(************************ case distinction theorems ***************************)
fun prove_casedist_thms (config : Datatype_Aux.config)
- new_type_names descr sorts induct case_names_exhausts thy =
+ new_type_names descr induct case_names_exhausts thy =
let
val _ = Datatype_Aux.message config "Proving case distinction theorems ...";
val descr' = flat descr;
- val recTs = Datatype_Aux.get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr';
val newTs = take (length (hd descr)) recTs;
val maxidx = Thm.maxidx_of induct;
@@ -75,7 +69,7 @@
end;
val casedist_thms =
- map_index prove_casedist_thm (newTs ~~ Datatype_Prop.make_casedists descr sorts);
+ map_index prove_casedist_thm (newTs ~~ Datatype_Prop.make_casedists descr);
in
thy
|> Datatype_Aux.store_thms_atts "exhaust" new_type_names
@@ -85,7 +79,7 @@
(*************************** primrec combinators ******************************)
-fun prove_primrec_thms (config : Datatype_Aux.config) new_type_names descr sorts
+fun prove_primrec_thms (config : Datatype_Aux.config) new_type_names descr
injects_of constr_inject (dist_rewrites, other_dist_rewrites) induct thy =
let
val _ = Datatype_Aux.message config "Constructing primrec combinators ...";
@@ -94,7 +88,7 @@
val thy0 = Sign.add_path big_name thy;
val descr' = flat descr;
- val recTs = Datatype_Aux.get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr';
val used = fold Term.add_tfree_namesT recTs [];
val newTs = take (length (hd descr)) recTs;
@@ -106,7 +100,7 @@
else map (prefix (big_rec_name' ^ "_") o string_of_int) (1 upto length descr');
val rec_set_names = map (Sign.full_bname thy0) rec_set_names';
- val (rec_result_Ts, reccomb_fn_Ts) = Datatype_Prop.make_primrec_Ts descr sorts used;
+ val (rec_result_Ts, reccomb_fn_Ts) = Datatype_Prop.make_primrec_Ts descr used;
val rec_set_Ts =
map (fn (T1, T2) => (reccomb_fn_Ts @ [T1, T2]) ---> HOLogic.boolT) (recTs ~~ rec_result_Ts);
@@ -139,7 +133,7 @@
| _ => (j + 1, k, prems, free1 :: t1s, t2s))
end;
- val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
val (_, _, prems, t1s, t2s) = fold_rev mk_prem (cargs ~~ Ts) (1, 1, [], [], []);
in
@@ -268,7 +262,7 @@
resolve_tac rec_unique_thms 1,
resolve_tac rec_intrs 1,
REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
- (Datatype_Prop.make_primrecs new_type_names descr sorts thy2);
+ (Datatype_Prop.make_primrecs new_type_names descr thy2);
in
thy2
|> Sign.add_path (space_implode "_" new_type_names)
@@ -282,24 +276,24 @@
(***************************** case combinators *******************************)
fun prove_case_thms (config : Datatype_Aux.config)
- new_type_names descr sorts reccomb_names primrec_thms thy =
+ new_type_names descr reccomb_names primrec_thms thy =
let
val _ = Datatype_Aux.message config "Proving characteristic theorems for case combinators ...";
val thy1 = Sign.add_path (space_implode "_" new_type_names) thy;
val descr' = flat descr;
- val recTs = Datatype_Aux.get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr';
val used = fold Term.add_tfree_namesT recTs [];
val newTs = take (length (hd descr)) recTs;
val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
- fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' sorts dt) ---> T';
+ fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' dt) ---> T';
val case_dummy_fns =
map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
let
- val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
val Ts' = map mk_dummyT (filter Datatype_Aux.is_rec_type cargs)
in Const (@{const_name undefined}, Ts @ Ts' ---> T') end) constrs) descr';
@@ -312,7 +306,7 @@
let
val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
let
- val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
val Ts' = Ts @ map mk_dummyT (filter Datatype_Aux.is_rec_type cargs);
val frees' = map2 (Datatype_Aux.mk_Free "x") Ts' (1 upto length Ts');
val frees = take (length cargs) frees';
@@ -344,7 +338,7 @@
Skip_Proof.prove_global thy2 [] [] t
(fn _ =>
EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]))
- (Datatype_Prop.make_cases new_type_names descr sorts thy2);
+ (Datatype_Prop.make_cases new_type_names descr thy2);
in
thy2
|> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)
@@ -357,12 +351,12 @@
(******************************* case splitting *******************************)
fun prove_split_thms (config : Datatype_Aux.config)
- new_type_names descr sorts constr_inject dist_rewrites casedist_thms case_thms thy =
+ new_type_names descr constr_inject dist_rewrites casedist_thms case_thms thy =
let
val _ = Datatype_Aux.message config "Proving equations for case splitting ...";
val descr' = flat descr;
- val recTs = Datatype_Aux.get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr';
val newTs = take (length (hd descr)) recTs;
fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'), exhaustion), case_thms'), T) =
@@ -380,7 +374,7 @@
val split_thm_pairs =
map prove_split_thms
- ((Datatype_Prop.make_splits new_type_names descr sorts thy) ~~ constr_inject ~~
+ (Datatype_Prop.make_splits new_type_names descr thy ~~ constr_inject ~~
dist_rewrites ~~ casedist_thms ~~ case_thms ~~ newTs);
val (split_thms, split_asm_thms) = ListPair.unzip split_thm_pairs
@@ -392,21 +386,20 @@
|-> (fn (thms1, thms2) => pair (thms1 ~~ thms2))
end;
-fun prove_weak_case_congs new_type_names descr sorts thy =
+fun prove_weak_case_congs new_type_names descr thy =
let
fun prove_weak_case_cong t =
Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
(fn {prems, ...} => EVERY [rtac ((hd prems) RS arg_cong) 1]);
val weak_case_congs =
- map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs new_type_names descr sorts thy);
+ map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs new_type_names descr thy);
in thy |> Datatype_Aux.store_thms "weak_case_cong" new_type_names weak_case_congs end;
(************************* additional theorems for TFL ************************)
-fun prove_nchotomys (config : Datatype_Aux.config)
- new_type_names descr sorts casedist_thms thy =
+fun prove_nchotomys (config : Datatype_Aux.config) new_type_names descr casedist_thms thy =
let
val _ = Datatype_Aux.message config "Proving additional theorems for TFL ...";
@@ -424,11 +417,11 @@
end;
val nchotomys =
- map prove_nchotomy (Datatype_Prop.make_nchotomys descr sorts ~~ casedist_thms);
+ map prove_nchotomy (Datatype_Prop.make_nchotomys descr ~~ casedist_thms);
in thy |> Datatype_Aux.store_thms "nchotomy" new_type_names nchotomys end;
-fun prove_case_congs new_type_names descr sorts nchotomys case_thms thy =
+fun prove_case_congs new_type_names descr nchotomys case_thms thy =
let
fun prove_case_cong ((t, nchotomy), case_rewrites) =
let
@@ -452,7 +445,7 @@
val case_congs =
map prove_case_cong (Datatype_Prop.make_case_congs
- new_type_names descr sorts thy ~~ nchotomys ~~ case_thms);
+ new_type_names descr thy ~~ nchotomys ~~ case_thms);
in thy |> Datatype_Aux.store_thms "case_cong" new_type_names case_congs end;
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Mon Dec 12 20:55:57 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Mon Dec 12 23:05:21 2011 +0100
@@ -9,14 +9,13 @@
type config = {strict : bool, quiet : bool}
val default_config : config
datatype dtyp =
- DtTFree of string
+ DtTFree of string * sort
| DtType of string * dtyp list
| DtRec of int
type descr = (int * (string * dtyp list * (string * dtyp list) list)) list
type info =
{index : int,
descr : descr,
- sorts : (string * sort) list,
inject : thm list,
distinct : thm list,
induct : thm,
@@ -61,23 +60,22 @@
val dtyp_of_typ : (string * string list) list -> typ -> dtyp
val mk_Free : string -> typ -> int -> term
val is_rec_type : dtyp -> bool
- val typ_of_dtyp : descr -> (string * sort) list -> dtyp -> typ
- val dest_DtTFree : dtyp -> string
+ val typ_of_dtyp : descr -> dtyp -> typ
+ val dest_DtTFree : dtyp -> string * sort
val dest_DtRec : dtyp -> int
val strip_dtyp : dtyp -> dtyp list * dtyp
val body_index : dtyp -> int
val mk_fun_dtyp : dtyp list -> dtyp -> dtyp
- val get_nonrec_types : descr -> (string * sort) list -> typ list
- val get_branching_types : descr -> (string * sort) list -> typ list
+ val get_nonrec_types : descr -> typ list
+ val get_branching_types : descr -> typ list
val get_arities : descr -> int list
- val get_rec_types : descr -> (string * sort) list -> typ list
- val interpret_construction : descr -> (string * sort) list
- -> { atyp: typ -> 'a, dtyp: typ list -> int * bool -> string * typ list -> 'a }
- -> ((string * typ list) * (string * 'a list) list) list
+ val get_rec_types : descr -> typ list
+ val interpret_construction : descr -> (string * sort) list ->
+ {atyp: typ -> 'a, dtyp: typ list -> int * bool -> string * typ list -> 'a} ->
+ ((string * typ list) * (string * 'a list) list) list
val check_nonempty : descr list -> unit
- val unfold_datatypes :
- Proof.context -> descr -> (string * sort) list -> info Symtab.table ->
- descr -> int -> descr list * int
+ val unfold_datatypes : Proof.context -> descr -> info Symtab.table ->
+ descr -> int -> descr list * int
val find_shortest_path : descr -> int -> (string * int) option
end;
@@ -176,7 +174,7 @@
(********************** Internal description of datatypes *********************)
datatype dtyp =
- DtTFree of string
+ DtTFree of string * sort
| DtType of string * dtyp list
| DtRec of int;
@@ -188,7 +186,6 @@
type info =
{index : int,
descr : descr,
- sorts : (string * sort) list,
inject : thm list,
distinct : thm list,
induct : thm,
@@ -206,7 +203,7 @@
fun mk_Free s T i = Free (s ^ string_of_int i, T);
-fun subst_DtTFree _ substs (T as DtTFree name) = the_default T (AList.lookup (op =) substs name)
+fun subst_DtTFree _ substs (T as DtTFree a) = the_default T (AList.lookup (op =) substs a)
| subst_DtTFree i substs (DtType (name, ts)) = DtType (name, map (subst_DtTFree i substs) ts)
| subst_DtTFree i _ (DtRec j) = DtRec (i + j);
@@ -239,7 +236,7 @@
end
| name_of_typ _ = "";
-fun dtyp_of_typ _ (TFree (n, _)) = DtTFree n
+fun dtyp_of_typ _ (TFree a) = DtTFree a
| dtyp_of_typ _ (TVar _) = error "Illegal schematic type variable(s)"
| dtyp_of_typ new_dts (Type (tname, Ts)) =
(case AList.lookup (op =) new_dts tname of
@@ -247,29 +244,29 @@
| SOME vs =>
if map (try (fst o dest_TFree)) Ts = map SOME vs then
DtRec (find_index (curry op = tname o fst) new_dts)
- else error ("Illegal occurrence of recursive type " ^ tname));
+ else error ("Illegal occurrence of recursive type " ^ quote tname));
-fun typ_of_dtyp descr sorts (DtTFree a) = TFree (a, (the o AList.lookup (op =) sorts) a)
- | typ_of_dtyp descr sorts (DtRec i) =
+fun typ_of_dtyp descr (DtTFree a) = TFree a
+ | typ_of_dtyp descr (DtRec i) =
let val (s, ds, _) = the (AList.lookup (op =) descr i)
- in Type (s, map (typ_of_dtyp descr sorts) ds) end
- | typ_of_dtyp descr sorts (DtType (s, ds)) = Type (s, map (typ_of_dtyp descr sorts) ds);
+ in Type (s, map (typ_of_dtyp descr) ds) end
+ | typ_of_dtyp descr (DtType (s, ds)) = Type (s, map (typ_of_dtyp descr) ds);
(* find all non-recursive types in datatype description *)
-fun get_nonrec_types descr sorts =
- map (typ_of_dtyp descr sorts) (fold (fn (_, (_, _, constrs)) =>
+fun get_nonrec_types descr =
+ map (typ_of_dtyp descr) (fold (fn (_, (_, _, constrs)) =>
fold (fn (_, cargs) => union (op =) (filter_out is_rec_type cargs)) constrs) descr []);
(* get all recursive types in datatype description *)
-fun get_rec_types descr sorts = map (fn (_ , (s, ds, _)) =>
- Type (s, map (typ_of_dtyp descr sorts) ds)) descr;
+fun get_rec_types descr = map (fn (_ , (s, ds, _)) =>
+ Type (s, map (typ_of_dtyp descr) ds)) descr;
(* get all branching types *)
-fun get_branching_types descr sorts =
- map (typ_of_dtyp descr sorts)
+fun get_branching_types descr =
+ map (typ_of_dtyp descr)
(fold
(fn (_, (_, _, constrs)) =>
fold (fn (_, cargs) => fold (strip_dtyp #> fst #> fold (insert op =)) cargs) constrs)
@@ -286,19 +283,21 @@
fun interpret_construction descr vs {atyp, dtyp} =
let
- val typ_of_dtyp = typ_of_dtyp descr vs;
+ val typ_of =
+ typ_of_dtyp descr #>
+ map_atyps (fn TFree (a, _) => TFree (a, the (AList.lookup (op =) vs a)) | T => T);
fun interpT dT =
(case strip_dtyp dT of
(dTs, DtRec l) =>
let
val (tyco, dTs', _) = the (AList.lookup (op =) descr l);
- val Ts = map typ_of_dtyp dTs;
- val Ts' = map typ_of_dtyp dTs';
+ val Ts = map typ_of dTs;
+ val Ts' = map typ_of dTs';
val is_proper = forall (can dest_TFree) Ts';
in dtyp Ts (l, is_proper) (tyco, Ts') end
- | _ => atyp (typ_of_dtyp dT));
+ | _ => atyp (typ_of dT));
fun interpC (c, dTs) = (c, map interpT dTs);
- fun interpD (_, (tyco, dTs, cs)) = ((tyco, map typ_of_dtyp dTs), map interpC cs);
+ fun interpD (_, (tyco, dTs, cs)) = ((tyco, map typ_of dTs), map interpC cs);
in map interpD descr end;
(* nonemptiness check for datatypes *)
@@ -323,22 +322,23 @@
(* all types of the form DtType (dt_name, [..., DtRec _, ...]) *)
(* need to be unfolded *)
-fun unfold_datatypes ctxt orig_descr sorts (dt_info : info Symtab.table) descr i =
+fun unfold_datatypes ctxt orig_descr (dt_info : info Symtab.table) descr i =
let
fun typ_error T msg =
error ("Non-admissible type expression\n" ^
- Syntax.string_of_typ ctxt (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
+ Syntax.string_of_typ ctxt (typ_of_dtyp (orig_descr @ descr) T) ^ "\n" ^ msg);
fun get_dt_descr T i tname dts =
(case Symtab.lookup dt_info tname of
NONE =>
- typ_error T (tname ^ " is not a datatype - can't use it in nested recursion")
+ typ_error T (quote tname ^ " is not a datatype - can't use it in nested recursion")
| SOME {index, descr, ...} =>
let
val (_, vars, _) = the (AList.lookup (op =) descr index);
val subst = map dest_DtTFree vars ~~ dts
handle ListPair.UnequalLengths =>
- typ_error T ("Type constructor " ^ tname ^ " used with wrong number of arguments");
+ typ_error T ("Type constructor " ^ quote tname ^
+ " used with wrong number of arguments");
in
(i + index,
map (fn (j, (tn, args, cs)) =>
@@ -359,7 +359,7 @@
let
val (index, descr) = get_dt_descr T i tname dts;
val (descr', i') =
- unfold_datatypes ctxt orig_descr sorts dt_info descr (i + length descr);
+ unfold_datatypes ctxt orig_descr dt_info descr (i + length descr);
in (i', Ts @ [mk_fun_dtyp Us (DtRec index)], descrs @ descr') end
| _ => (i, Ts @ [T], descrs))
end
--- a/src/HOL/Tools/Datatype/datatype_case.ML Mon Dec 12 20:55:57 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Mon Dec 12 23:05:21 2011 +0100
@@ -36,10 +36,10 @@
fun ty_info tab sT =
(case tab sT of
- SOME ({descr, case_name, index, sorts, ...} : info) =>
+ SOME ({descr, case_name, index, ...} : info) =>
let
val (_, (tname, dts, constrs)) = nth descr index;
- val mk_ty = Datatype_Aux.typ_of_dtyp descr sorts;
+ val mk_ty = Datatype_Aux.typ_of_dtyp descr;
val T = Type (tname, map mk_ty dts);
in
SOME {case_name = case_name,
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Dec 12 20:55:57 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Dec 12 23:05:21 2011 +0100
@@ -76,11 +76,11 @@
| _ => NONE) cos;
fun prep_inject (trueprop $ (equiv $ (_ $ t1 $ t2) $ rhs)) =
trueprop $ (equiv $ mk_eq (t1, t2) $ rhs);
- val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr] vs) index);
+ val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr]) index);
fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) =
[trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
val distincts =
- maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
+ maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr]) index));
val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
val simpset =
Simplifier.global_context thy
--- a/src/HOL/Tools/Datatype/datatype_data.ML Mon Dec 12 20:55:57 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Mon Dec 12 23:05:21 2011 +0100
@@ -7,7 +7,7 @@
signature DATATYPE_DATA =
sig
include DATATYPE_COMMON
- val derive_datatype_props : config -> string list -> descr list -> (string * sort) list ->
+ val derive_datatype_props : config -> string list -> descr 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
@@ -109,22 +109,19 @@
fun the_spec thy dtco =
let
- val {descr, index, sorts = raw_sorts, ...} = the_info thy dtco;
+ val {descr, index, ...} = the_info thy dtco;
val (_, dtys, raw_cos) = the (AList.lookup (op =) descr index);
- val sorts =
- map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v)) o Datatype_Aux.dest_DtTFree) dtys;
- val cos = map (fn (co, tys) => (co, map (Datatype_Aux.typ_of_dtyp descr sorts) tys)) raw_cos;
- in (sorts, cos) end;
+ val args = map Datatype_Aux.dest_DtTFree dtys;
+ val cos = map (fn (co, tys) => (co, map (Datatype_Aux.typ_of_dtyp descr) tys)) raw_cos;
+ in (args, cos) end;
fun the_descr thy (raw_tycos as raw_tyco :: _) =
let
val info = the_info thy raw_tyco;
val descr = #descr info;
- val SOME (_, dtys, _) = AList.lookup (op =) descr (#index info);
- val vs =
- map ((fn v => (v, the (AList.lookup (op =) (#sorts info) v))) o Datatype_Aux.dest_DtTFree)
- dtys;
+ val (_, dtys, _) = the (AList.lookup (op =) descr (#index info));
+ val vs = map Datatype_Aux.dest_DtTFree dtys;
fun is_DtTFree (Datatype_Aux.DtTFree _) = true
| is_DtTFree _ = false;
@@ -132,7 +129,7 @@
val protoTs as (dataTs, _) =
chop k descr
|> (pairself o map)
- (fn (_, (tyco, dTs, _)) => (tyco, map (Datatype_Aux.typ_of_dtyp descr vs) dTs));
+ (fn (_, (tyco, dTs, _)) => (tyco, map (Datatype_Aux.typ_of_dtyp descr) dTs));
val tycos = map fst dataTs;
val _ =
@@ -160,12 +157,12 @@
fun get_constrs thy dtco =
(case try (the_spec thy) dtco of
- SOME (sorts, cos) =>
+ SOME (args, cos) =>
let
fun subst (v, sort) = TVar ((v, 0), sort);
fun subst_ty (TFree v) = subst v
| subst_ty ty = ty;
- val dty = Type (dtco, map subst sorts);
+ val dty = Type (dtco, map subst args);
fun mk_co (co, tys) = (co, map (Term.map_atyps subst_ty) tys ---> dty);
in SOME (map mk_co cos) end
| NONE => NONE);
@@ -283,14 +280,13 @@
);
fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
-fun make_dt_info descr sorts induct inducts rec_names rec_rewrites
+fun make_dt_info descr 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,
descr = descr,
- sorts = sorts,
inject = inject,
distinct = distinct,
induct = induct,
@@ -306,8 +302,7 @@
split = split,
split_asm = split_asm});
-fun derive_datatype_props config dt_names descr sorts
- induct inject distinct thy1 =
+fun derive_datatype_props config dt_names descr induct inject distinct thy1 =
let
val thy2 = thy1 |> Theory.checkpoint;
val flat_descr = flat descr;
@@ -316,32 +311,28 @@
Datatype_Aux.message config
("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
- val (exhaust, thy3) =
- Datatype_Abs_Proofs.prove_casedist_thms config new_type_names
- descr sorts induct (mk_case_names_exhausts flat_descr dt_names) thy2;
- val (nchotomys, thy4) =
- Datatype_Abs_Proofs.prove_nchotomys config new_type_names
- descr sorts exhaust thy3;
- val ((rec_names, rec_rewrites), thy5) =
- Datatype_Abs_Proofs.prove_primrec_thms
- config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4))
- inject (distinct, all_distincts thy2 (Datatype_Aux.get_rec_types flat_descr sorts))
- induct thy4;
- val ((case_rewrites, case_names), thy6) =
- Datatype_Abs_Proofs.prove_case_thms
- config new_type_names descr sorts rec_names rec_rewrites thy5;
- val (case_congs, thy7) =
- Datatype_Abs_Proofs.prove_case_congs new_type_names
- descr sorts nchotomys case_rewrites thy6;
- val (weak_case_congs, thy8) =
- Datatype_Abs_Proofs.prove_weak_case_congs new_type_names descr sorts thy7;
- val (splits, thy9) =
- Datatype_Abs_Proofs.prove_split_thms
- config new_type_names descr sorts inject distinct exhaust case_rewrites thy8;
+ val (exhaust, thy3) = thy2
+ |> Datatype_Abs_Proofs.prove_casedist_thms config new_type_names
+ descr induct (mk_case_names_exhausts flat_descr dt_names);
+ val (nchotomys, thy4) = thy3
+ |> Datatype_Abs_Proofs.prove_nchotomys config new_type_names descr exhaust;
+ val ((rec_names, rec_rewrites), thy5) = thy4
+ |> Datatype_Abs_Proofs.prove_primrec_thms
+ config new_type_names descr (#inject o the o Symtab.lookup (get_all thy4))
+ inject (distinct, all_distincts thy2 (Datatype_Aux.get_rec_types flat_descr)) induct;
+ val ((case_rewrites, case_names), thy6) = thy5
+ |> Datatype_Abs_Proofs.prove_case_thms config new_type_names descr rec_names rec_rewrites;
+ val (case_congs, thy7) = thy6
+ |> Datatype_Abs_Proofs.prove_case_congs new_type_names descr nchotomys case_rewrites;
+ val (weak_case_congs, thy8) = thy7
+ |> Datatype_Abs_Proofs.prove_weak_case_congs new_type_names descr;
+ val (splits, thy9) = thy8
+ |> Datatype_Abs_Proofs.prove_split_thms
+ config new_type_names descr inject distinct exhaust case_rewrites;
val inducts = Project_Rule.projections (Proof_Context.init_global thy2) induct;
val dt_infos = map_index
- (make_dt_info flat_descr sorts induct inducts rec_names rec_rewrites)
+ (make_dt_info flat_descr 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;
@@ -378,7 +369,7 @@
(** declare existing type as datatype **)
-fun prove_rep_datatype config dt_names descr sorts raw_inject half_distinct raw_induct thy1 =
+fun prove_rep_datatype config dt_names descr 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 dt_names;
@@ -392,7 +383,7 @@
[mk_case_names_induct descr])];
in
thy2
- |> derive_datatype_props config dt_names [descr] sorts induct inject distinct
+ |> derive_datatype_props config dt_names [descr] induct inject distinct
end;
fun gen_rep_datatype prep_term config after_qed raw_ts thy =
@@ -441,13 +432,11 @@
val dt_names = map fst cs;
fun mk_spec (i, (tyco, constr)) =
- (i, (tyco,
- map (Datatype_Aux.DtTFree o fst) vs,
- (map o apsnd) dtyps_of_typ constr));
+ (i, (tyco, map Datatype_Aux.DtTFree vs, (map o apsnd) dtyps_of_typ constr));
val descr = map_index mk_spec cs;
- val injs = Datatype_Prop.make_injs [descr] vs;
- val half_distincts = map snd (Datatype_Prop.make_distincts [descr] vs);
- val ind = Datatype_Prop.make_ind [descr] vs;
+ val injs = Datatype_Prop.make_injs [descr];
+ val half_distincts = map snd (Datatype_Prop.make_distincts [descr]);
+ val ind = Datatype_Prop.make_ind [descr];
val rules = (map o map o map) Logic.close_form [[[ind]], injs, half_distincts];
fun after_qed' raw_thms =
@@ -457,7 +446,7 @@
(*FIXME somehow dubious*)
in
Proof_Context.background_theory_result (* FIXME !? *)
- (prove_rep_datatype config dt_names descr vs raw_inject half_distinct raw_induct)
+ (prove_rep_datatype config dt_names descr raw_inject half_distinct raw_induct)
#-> after_qed
end;
in
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Mon Dec 12 20:55:57 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Mon Dec 12 23:05:21 2011 +0100
@@ -9,27 +9,18 @@
include DATATYPE_COMMON
val indexify_names: string list -> string list
val make_tnames: typ list -> string list
- val make_injs : descr list -> (string * sort) list -> term list list
- val make_distincts : descr list ->
- (string * sort) list -> (int * term list) list (*no symmetric inequalities*)
- val make_ind : descr list -> (string * sort) list -> term
- val make_casedists : descr list -> (string * sort) list -> term list
- val make_primrec_Ts : descr list -> (string * sort) list ->
- string list -> typ list * typ list
- val make_primrecs : string list -> descr list ->
- (string * sort) list -> theory -> term list
- val make_cases : string list -> descr list ->
- (string * sort) list -> theory -> term list list
- val make_splits : string list -> descr list ->
- (string * sort) list -> theory -> (term * term) list
- val make_case_combs : string list -> descr list ->
- (string * sort) list -> theory -> string -> term list
- val make_weak_case_congs : string list -> descr list ->
- (string * sort) list -> theory -> term list
- val make_case_congs : string list -> descr list ->
- (string * sort) list -> theory -> term list
- val make_nchotomys : descr list ->
- (string * sort) list -> term list
+ val make_injs : descr list -> term list list
+ val make_distincts : descr list -> (int * term list) list (*no symmetric inequalities*)
+ val make_ind : descr list -> term
+ val make_casedists : descr list -> term list
+ val make_primrec_Ts : descr list -> string list -> typ list * typ list
+ val make_primrecs : string list -> descr list -> theory -> term list
+ val make_cases : string list -> descr list -> theory -> term list list
+ val make_splits : string list -> descr list -> theory -> (term * term) list
+ val make_case_combs : string list -> descr list -> theory -> string -> term list
+ val make_weak_case_congs : string list -> descr list -> theory -> term list
+ val make_case_congs : string list -> descr list -> theory -> term list
+ val make_nchotomys : descr list -> term list
end;
structure Datatype_Prop : DATATYPE_PROP =
@@ -58,14 +49,14 @@
(************************* injectivity of constructors ************************)
-fun make_injs descr sorts =
+fun make_injs descr =
let
val descr' = flat descr;
fun make_inj T (cname, cargs) =
if null cargs then I
else
let
- val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
val constr_t = Const (cname, Ts ---> T);
val tnames = make_tnames Ts;
val frees = map Free (tnames ~~ Ts);
@@ -78,20 +69,19 @@
end;
in
map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
- (hd descr) (take (length (hd descr)) (Datatype_Aux.get_rec_types descr' sorts))
+ (hd descr) (take (length (hd descr)) (Datatype_Aux.get_rec_types descr'))
end;
(************************* distinctness of constructors ***********************)
-fun make_distincts descr sorts =
+fun make_distincts descr =
let
val descr' = flat descr;
- val recTs = Datatype_Aux.get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr';
val newTs = take (length (hd descr)) recTs;
- fun prep_constr (cname, cargs) =
- (cname, map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs);
+ fun prep_constr (cname, cargs) = (cname, map (Datatype_Aux.typ_of_dtyp descr') cargs);
fun make_distincts' _ [] = []
| make_distincts' T ((cname, cargs) :: constrs) =
@@ -115,10 +105,10 @@
(********************************* induction **********************************)
-fun make_ind descr sorts =
+fun make_ind descr =
let
val descr' = flat descr;
- val recTs = Datatype_Aux.get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr';
val pnames =
if length descr' = 1 then ["P"]
else map (fn i => "P" ^ string_of_int i) (1 upto length descr');
@@ -139,8 +129,8 @@
end;
val recs = filter Datatype_Aux.is_rec_type cargs;
- val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
- val recTs' = map (Datatype_Aux.typ_of_dtyp descr' sorts) recs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
+ val recTs' = map (Datatype_Aux.typ_of_dtyp descr') recs;
val tnames = Name.variant_list pnames (make_tnames Ts);
val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
val frees = tnames ~~ Ts;
@@ -164,13 +154,13 @@
(******************************* case distinction *****************************)
-fun make_casedists descr sorts =
+fun make_casedists descr =
let
val descr' = flat descr;
fun make_casedist_prem T (cname, cargs) =
let
- val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
val frees = Name.variant_list ["P", "y"] (make_tnames Ts) ~~ Ts;
val free_ts = map Free frees;
in
@@ -186,12 +176,12 @@
in
map2 make_casedist (hd descr)
- (take (length (hd descr)) (Datatype_Aux.get_rec_types descr' sorts))
+ (take (length (hd descr)) (Datatype_Aux.get_rec_types descr'))
end;
(*************** characteristic equations for primrec combinator **************)
-fun make_primrec_Ts descr sorts used =
+fun make_primrec_Ts descr used =
let
val descr' = flat descr;
@@ -203,7 +193,7 @@
val reccomb_fn_Ts = maps (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
let
- val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
val recs = filter (Datatype_Aux.is_rec_type o fst) (cargs ~~ Ts);
fun mk_argT (dt, T) =
@@ -214,13 +204,13 @@
in (rec_result_Ts, reccomb_fn_Ts) end;
-fun make_primrecs new_type_names descr sorts thy =
+fun make_primrecs new_type_names descr thy =
let
val descr' = flat descr;
- val recTs = Datatype_Aux.get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr';
val used = fold Term.add_tfree_namesT recTs [];
- val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
+ val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr used;
val rec_fns =
map (uncurry (Datatype_Aux.mk_Free "f"))
@@ -238,8 +228,8 @@
fun make_primrec T comb_t (cname, cargs) (ts, f :: fs) =
let
val recs = filter Datatype_Aux.is_rec_type cargs;
- val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
- val recTs' = map (Datatype_Aux.typ_of_dtyp descr' sorts) recs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
+ val recTs' = map (Datatype_Aux.typ_of_dtyp descr') recs;
val tnames = make_tnames Ts;
val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
val frees = map Free (tnames ~~ Ts);
@@ -266,17 +256,17 @@
(****************** make terms of form t_case f1 ... fn *********************)
-fun make_case_combs new_type_names descr sorts thy fname =
+fun make_case_combs new_type_names descr thy fname =
let
val descr' = flat descr;
- val recTs = Datatype_Aux.get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr';
val used = fold Term.add_tfree_namesT recTs [];
val newTs = take (length (hd descr)) recTs;
val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
- let val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs
+ let val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs
in Ts ---> T' end) constrs) (hd descr);
val case_names = map (fn s => Sign.intern_const thy (s ^ "_case")) new_type_names;
@@ -289,15 +279,15 @@
(**************** characteristic equations for case combinator ****************)
-fun make_cases new_type_names descr sorts thy =
+fun make_cases new_type_names descr thy =
let
val descr' = flat descr;
- val recTs = Datatype_Aux.get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr';
val newTs = take (length (hd descr)) recTs;
fun make_case T comb_t ((cname, cargs), f) =
let
- val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
val frees = map Free ((make_tnames Ts) ~~ Ts);
in
HOLogic.mk_Trueprop
@@ -307,16 +297,16 @@
in
map (fn (((_, (_, _, constrs)), T), comb_t) =>
map (make_case T comb_t) (constrs ~~ (snd (strip_comb comb_t))))
- ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr sorts thy "f"))
+ ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr thy "f"))
end;
(*************************** the "split" - equations **************************)
-fun make_splits new_type_names descr sorts thy =
+fun make_splits new_type_names descr thy =
let
val descr' = flat descr;
- val recTs = Datatype_Aux.get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr';
val used' = fold Term.add_tfree_namesT recTs [];
val newTs = take (length (hd descr)) recTs;
val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS);
@@ -329,7 +319,7 @@
fun process_constr ((cname, cargs), f) (t1s, t2s) =
let
- val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
val frees = map Free (Name.variant_list used (make_tnames Ts) ~~ Ts);
val eqn = HOLogic.mk_eq (Free ("x", T), list_comb (Const (cname, Ts ---> T), frees));
val P' = P $ list_comb (f, frees);
@@ -348,14 +338,14 @@
end
in
- map make_split (hd descr ~~ newTs ~~ make_case_combs new_type_names descr sorts thy "f")
+ map make_split (hd descr ~~ newTs ~~ make_case_combs new_type_names descr thy "f")
end;
(************************* additional rules for TFL ***************************)
-fun make_weak_case_congs new_type_names descr sorts thy =
+fun make_weak_case_congs new_type_names descr thy =
let
- val case_combs = make_case_combs new_type_names descr sorts thy "f";
+ val case_combs = make_case_combs new_type_names descr thy "f";
fun mk_case_cong comb =
let
@@ -382,10 +372,10 @@
* (ty_case f1..fn M = ty_case g1..gn M')
*---------------------------------------------------------------------------*)
-fun make_case_congs new_type_names descr sorts thy =
+fun make_case_congs new_type_names descr thy =
let
- val case_combs = make_case_combs new_type_names descr sorts thy "f";
- val case_combs' = make_case_combs new_type_names descr sorts thy "g";
+ val case_combs = make_case_combs new_type_names descr thy "f";
+ val case_combs' = make_case_combs new_type_names descr thy "g";
fun mk_case_cong ((comb, comb'), (_, (_, _, constrs))) =
let
@@ -423,15 +413,15 @@
* !v. (? y1..yi. v = C1 y1..yi) | ... | (? y1..yj. v = Cn y1..yj)
*---------------------------------------------------------------------------*)
-fun make_nchotomys descr sorts =
+fun make_nchotomys descr =
let
val descr' = flat descr;
- val recTs = Datatype_Aux.get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr';
val newTs = take (length (hd descr)) recTs;
fun mk_eqn T (cname, cargs) =
let
- val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
val tnames = Name.variant_list ["v"] (make_tnames Ts);
val frees = tnames ~~ Ts;
in
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Dec 12 20:55:57 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Dec 12 23:05:21 2011 +0100
@@ -25,9 +25,9 @@
fun tname_of (Type (s, _)) = s
| tname_of _ = "";
-fun make_ind sorts ({descr, rec_names, rec_rewrites, induct, ...} : Datatype_Aux.info) is thy =
+fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Datatype_Aux.info) is thy =
let
- val recTs = Datatype_Aux.get_rec_types descr sorts;
+ val recTs = Datatype_Aux.get_rec_types descr;
val pnames =
if length descr = 1 then ["P"]
else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
@@ -47,7 +47,7 @@
val (prems, rec_fns) = split_list (flat (fst (fold_map
(fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
let
- val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs;
val tnames = Name.variant_list pnames (Datatype_Prop.make_tnames Ts);
val recs = filter (Datatype_Aux.is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
val frees = tnames ~~ Ts;
@@ -128,7 +128,7 @@
(Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
||> Sign.restore_naming thy;
- val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr] sorts)) []);
+ val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr])) []);
val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
val ivs1 = map Var (filter_out (fn (_, T) => @{type_name bool} = tname_of (body_type T)) ivs);
val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
@@ -157,8 +157,7 @@
in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
-fun make_casedists sorts
- ({index, descr, case_name, case_rewrites, exhaust, ...} : Datatype_Aux.info) thy =
+fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Datatype_Aux.info) thy =
let
val cert = cterm_of thy;
val rT = TFree ("'P", HOLogic.typeS);
@@ -166,7 +165,7 @@
fun make_casedist_prem T (cname, cargs) =
let
- val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs;
val frees = Name.variant_list ["P", "y"] (Datatype_Prop.make_tnames Ts) ~~ Ts;
val free_ts = map Free frees;
val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
@@ -178,7 +177,7 @@
end;
val SOME (_, _, constrs) = AList.lookup (op =) descr index;
- val T = nth (Datatype_Aux.get_rec_types descr sorts) index;
+ val T = nth (Datatype_Aux.get_rec_types descr) index;
val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
val r = Const (case_name, map fastype_of rs ---> T --> rT);
@@ -233,8 +232,8 @@
val info :: _ = infos;
in
thy
- |> fold_rev (make_ind (#sorts info) info) (subsets 0 (length (#descr info) - 1))
- |> fold_rev (make_casedists (#sorts info)) infos
+ |> fold_rev (make_ind info) (subsets 0 (length (#descr info) - 1))
+ |> fold_rev make_casedists infos
end;
val setup = Datatype.interpretation add_dt_realizers;
--- a/src/HOL/Tools/Function/size.ML Mon Dec 12 20:55:57 2011 +0100
+++ b/src/HOL/Tools/Function/size.ML Mon Dec 12 23:05:21 2011 +0100
@@ -56,14 +56,14 @@
fun prove_size_thms (info : Datatype.info) new_type_names thy =
let
- val {descr, sorts, rec_names, rec_rewrites, induct, ...} = info;
+ val {descr, rec_names, rec_rewrites, induct, ...} = info;
val l = length new_type_names;
val descr' = List.take (descr, l);
val (rec_names1, rec_names2) = chop l rec_names;
- val recTs = Datatype_Aux.get_rec_types descr sorts;
+ val recTs = Datatype_Aux.get_rec_types descr;
val (recTs1, recTs2) = chop l recTs;
val (_, (_, paramdts, _)) :: _ = descr;
- val paramTs = map (Datatype_Aux.typ_of_dtyp descr sorts) paramdts;
+ val paramTs = map (Datatype_Aux.typ_of_dtyp descr) paramdts;
val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
map (fn T as TFree (s, _) =>
let
@@ -94,7 +94,7 @@
(* instantiation for primrec combinator *)
fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) =
let
- val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs;
val k = length (filter Datatype_Aux.is_rec_type cargs);
val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) =>
if Datatype_Aux.is_rec_type dt then (Bound i :: us, i + 1, j + 1)
@@ -172,7 +172,7 @@
(* characteristic equations for size functions *)
fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) =
let
- val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs;
val tnames = Name.variant_list f_names (Datatype_Prop.make_tnames Ts);
val ts = map_filter (fn (sT as (s, T), dt) =>
Option.map (fn sz => sz $ Free sT)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Dec 12 20:55:57 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Dec 12 23:05:21 2011 +0100
@@ -903,9 +903,9 @@
fun datatype_names_of_case_name thy case_name =
map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name)))
-fun make_case_distribs new_type_names descr sorts thy =
+fun make_case_distribs new_type_names descr thy =
let
- val case_combs = Datatype_Prop.make_case_combs new_type_names descr sorts thy "f";
+ val case_combs = Datatype_Prop.make_case_combs new_type_names descr thy "f";
fun make comb =
let
val Type ("fun", [T, T']) = fastype_of comb;
@@ -932,10 +932,10 @@
fun case_rewrites thy Tcon =
let
- val {descr, sorts, ...} = Datatype.the_info thy Tcon
+ val {descr, ...} = Datatype.the_info thy Tcon
in
map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
- (make_case_distribs [Tcon] [descr] sorts thy)
+ (make_case_distribs [Tcon] [descr] thy)
end
fun instantiated_case_rewrites thy Tcon =