1.1 --- a/src/HOL/Nominal/nominal_datatype.ML Thu Dec 15 21:46:52 2011 +0100
1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML Fri Dec 16 10:38:38 2011 +0100
1.3 @@ -42,8 +42,8 @@
1.4 (* theory data *)
1.5
1.6 type descr =
1.7 - (int * (string * Datatype_Aux.dtyp list *
1.8 - (string * (Datatype_Aux.dtyp list * Datatype_Aux.dtyp) list) list)) list;
1.9 + (int * (string * Datatype.dtyp list *
1.10 + (string * (Datatype.dtyp list * Datatype.dtyp) list) list)) list;
1.11
1.12 type nominal_datatype_info =
1.13 {index : int,
1.14 @@ -200,7 +200,7 @@
1.15 val (full_new_type_names',thy1) = Datatype.add_datatype config dts'' thy;
1.16
1.17 val {descr, induct, ...} = Datatype.the_info thy1 (hd full_new_type_names');
1.18 - fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr (Datatype_Aux.DtRec i);
1.19 + fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr (Datatype.DtRec i);
1.20
1.21 val big_name = space_implode "_" new_type_names;
1.22
1.23 @@ -465,13 +465,13 @@
1.24 | (i, _) => SOME (Datatype_Aux.name_of_typ (nth_dtyp i))) descr)) ^ "_set";
1.25 val _ = warning ("big_rep_name: " ^ big_rep_name);
1.26
1.27 - fun strip_option (dtf as Datatype_Aux.DtType ("fun", [dt, Datatype_Aux.DtRec i])) =
1.28 + fun strip_option (dtf as Datatype.DtType ("fun", [dt, Datatype.DtRec i])) =
1.29 (case AList.lookup op = descr i of
1.30 SOME ("Nominal.noption", _, [(_, [dt']), _]) =>
1.31 apfst (cons dt) (strip_option dt')
1.32 | _ => ([], dtf))
1.33 - | strip_option (Datatype_Aux.DtType ("fun",
1.34 - [dt, Datatype_Aux.DtType ("Nominal.noption", [dt'])])) =
1.35 + | strip_option (Datatype.DtType ("fun",
1.36 + [dt, Datatype.DtType ("Nominal.noption", [dt'])])) =
1.37 apfst (cons dt) (strip_option dt')
1.38 | strip_option dt = ([], dt);
1.39
1.40 @@ -497,7 +497,7 @@
1.41 end
1.42 in (j + 1, j' + length Ts,
1.43 case dt'' of
1.44 - Datatype_Aux.DtRec k => list_all (map (pair "x") Us,
1.45 + Datatype.DtRec k => list_all (map (pair "x") Us,
1.46 HOLogic.mk_Trueprop (Free (nth rep_set_names k,
1.47 T --> HOLogic.boolT) $ free')) :: prems
1.48 | _ => prems,
1.49 @@ -676,8 +676,8 @@
1.50 (fn ((i, ("Nominal.noption", _, _)), p) => p
1.51 | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
1.52
1.53 - fun reindex (Datatype_Aux.DtType (s, dts)) = Datatype_Aux.DtType (s, map reindex dts)
1.54 - | reindex (Datatype_Aux.DtRec i) = Datatype_Aux.DtRec (the (AList.lookup op = ty_idxs i))
1.55 + fun reindex (Datatype.DtType (s, dts)) = Datatype.DtType (s, map reindex dts)
1.56 + | reindex (Datatype.DtRec i) = Datatype.DtRec (the (AList.lookup op = ty_idxs i))
1.57 | reindex dt = dt;
1.58
1.59 fun strip_suffix i s = implode (List.take (raw_explode s, size s - i)); (* FIXME Symbol.explode (?) *)
1.60 @@ -713,7 +713,7 @@
1.61 map (fn ((cname, cargs), idxs) => (cname, partition_cargs idxs cargs))
1.62 (constrs ~~ idxss)))) (descr'' ~~ ndescr);
1.63
1.64 - fun nth_dtyp' i = Datatype_Aux.typ_of_dtyp descr'' (Datatype_Aux.DtRec i);
1.65 + fun nth_dtyp' i = Datatype_Aux.typ_of_dtyp descr'' (Datatype.DtRec i);
1.66
1.67 val rep_names = map (fn s =>
1.68 Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names;
1.69 @@ -740,7 +740,7 @@
1.70 xs @ x :: l_args,
1.71 fold_rev mk_abs_fun xs
1.72 (case dt of
1.73 - Datatype_Aux.DtRec k => if k < length new_type_names then
1.74 + Datatype.DtRec k => if k < length new_type_names then
1.75 Const (nth rep_names k, Datatype_Aux.typ_of_dtyp descr'' dt -->
1.76 Datatype_Aux.typ_of_dtyp descr dt) $ x
1.77 else error "nested recursion not (yet) supported"
1.78 @@ -1435,7 +1435,7 @@
1.79 val binders = maps fst frees';
1.80 val atomTs = distinct op = (maps (map snd o fst) frees');
1.81 val recs = map_filter
1.82 - (fn ((_, Datatype_Aux.DtRec i), p) => SOME (i, p) | _ => NONE)
1.83 + (fn ((_, Datatype.DtRec i), p) => SOME (i, p) | _ => NONE)
1.84 (partition_cargs idxs cargs ~~ frees');
1.85 val frees'' = map (fn i => "y" ^ string_of_int i) (1 upto length recs) ~~
1.86 map (fn (i, _) => nth rec_result_Ts i) recs;
2.1 --- a/src/HOL/Tools/ATP/atp_util.ML Thu Dec 15 21:46:52 2011 +0100
2.2 +++ b/src/HOL/Tools/ATP/atp_util.ML Fri Dec 16 10:38:38 2011 +0100
2.3 @@ -23,9 +23,7 @@
2.4 val varify_type : Proof.context -> typ -> typ
2.5 val instantiate_type : theory -> typ -> typ -> typ -> typ
2.6 val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
2.7 - val typ_of_dtyp :
2.8 - Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
2.9 - -> typ
2.10 + val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
2.11 val is_type_surely_finite : Proof.context -> typ -> bool
2.12 val is_type_surely_infinite : Proof.context -> bool -> typ list -> typ -> bool
2.13 val s_not : term -> term
2.14 @@ -148,11 +146,11 @@
2.15 instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2)
2.16 end
2.17
2.18 -fun typ_of_dtyp _ typ_assoc (Datatype_Aux.DtTFree a) =
2.19 - the (AList.lookup (op =) typ_assoc (Datatype_Aux.DtTFree a))
2.20 - | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtType (s, Us)) =
2.21 +fun typ_of_dtyp _ typ_assoc (Datatype.DtTFree a) =
2.22 + the (AList.lookup (op =) typ_assoc (Datatype.DtTFree a))
2.23 + | typ_of_dtyp descr typ_assoc (Datatype.DtType (s, Us)) =
2.24 Type (s, map (typ_of_dtyp descr typ_assoc) Us)
2.25 - | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) =
2.26 + | typ_of_dtyp descr typ_assoc (Datatype.DtRec i) =
2.27 let val (s, ds, _) = the (AList.lookup (op =) descr i) in
2.28 Type (s, map (typ_of_dtyp descr typ_assoc) ds)
2.29 end
3.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Dec 15 21:46:52 2011 +0100
3.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Fri Dec 16 10:38:38 2011 +0100
3.3 @@ -8,7 +8,8 @@
3.4
3.5 signature DATATYPE_ABS_PROOFS =
3.6 sig
3.7 - include DATATYPE_COMMON
3.8 + type config = Datatype_Aux.config
3.9 + type descr = Datatype_Aux.descr
3.10 val prove_casedist_thms : config -> string list -> descr list -> thm ->
3.11 attribute list -> theory -> thm list * theory
3.12 val prove_primrec_thms : config -> string list -> descr list ->
3.13 @@ -29,10 +30,13 @@
3.14 structure Datatype_Abs_Proofs: DATATYPE_ABS_PROOFS =
3.15 struct
3.16
3.17 +type config = Datatype_Aux.config;
3.18 +type descr = Datatype_Aux.descr;
3.19 +
3.20 +
3.21 (************************ case distinction theorems ***************************)
3.22
3.23 -fun prove_casedist_thms (config : Datatype_Aux.config)
3.24 - new_type_names descr induct case_names_exhausts thy =
3.25 +fun prove_casedist_thms (config : config) new_type_names descr induct case_names_exhausts thy =
3.26 let
3.27 val _ = Datatype_Aux.message config "Proving case distinction theorems ...";
3.28
3.29 @@ -79,7 +83,7 @@
3.30
3.31 (*************************** primrec combinators ******************************)
3.32
3.33 -fun prove_primrec_thms (config : Datatype_Aux.config) new_type_names descr
3.34 +fun prove_primrec_thms (config : config) new_type_names descr
3.35 injects_of constr_inject (dist_rewrites, other_dist_rewrites) induct thy =
3.36 let
3.37 val _ = Datatype_Aux.message config "Constructing primrec combinators ...";
3.38 @@ -275,8 +279,7 @@
3.39
3.40 (***************************** case combinators *******************************)
3.41
3.42 -fun prove_case_thms (config : Datatype_Aux.config)
3.43 - new_type_names descr reccomb_names primrec_thms thy =
3.44 +fun prove_case_thms (config : config) new_type_names descr reccomb_names primrec_thms thy =
3.45 let
3.46 val _ = Datatype_Aux.message config "Proving characteristic theorems for case combinators ...";
3.47
3.48 @@ -350,7 +353,7 @@
3.49
3.50 (******************************* case splitting *******************************)
3.51
3.52 -fun prove_split_thms (config : Datatype_Aux.config)
3.53 +fun prove_split_thms (config : config)
3.54 new_type_names case_names descr constr_inject dist_rewrites casedist_thms case_thms thy =
3.55 let
3.56 val _ = Datatype_Aux.message config "Proving equations for case splitting ...";
3.57 @@ -399,7 +402,7 @@
3.58
3.59 (************************* additional theorems for TFL ************************)
3.60
3.61 -fun prove_nchotomys (config : Datatype_Aux.config) new_type_names descr casedist_thms thy =
3.62 +fun prove_nchotomys (config : config) new_type_names descr casedist_thms thy =
3.63 let
3.64 val _ = Datatype_Aux.message config "Proving additional theorems for TFL ...";
3.65
3.66 @@ -449,7 +452,4 @@
3.67
3.68 in thy |> Datatype_Aux.store_thms "case_cong" new_type_names case_congs end;
3.69
3.70 -
3.71 -open Datatype_Aux;
3.72 -
3.73 end;
4.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML Thu Dec 15 21:46:52 2011 +0100
4.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML Fri Dec 16 10:38:38 2011 +0100
4.3 @@ -6,7 +6,7 @@
4.4
4.5 signature DATATYPE_PROP =
4.6 sig
4.7 - include DATATYPE_COMMON
4.8 + type descr = Datatype_Aux.descr
4.9 val indexify_names: string list -> string list
4.10 val make_tnames: typ list -> string list
4.11 val make_injs : descr list -> term list list
4.12 @@ -26,6 +26,9 @@
4.13 structure Datatype_Prop : DATATYPE_PROP =
4.14 struct
4.15
4.16 +type descr = Datatype_Aux.descr;
4.17 +
4.18 +
4.19 fun indexify_names names =
4.20 let
4.21 fun index (x :: xs) tab =
4.22 @@ -429,7 +432,4 @@
4.23 (hd descr ~~ newTs)
4.24 end;
4.25
4.26 -
4.27 -open Datatype_Aux;
4.28 -
4.29 end;
5.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Thu Dec 15 21:46:52 2011 +0100
5.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Fri Dec 16 10:38:38 2011 +0100
5.3 @@ -25,7 +25,7 @@
5.4 fun tname_of (Type (s, _)) = s
5.5 | tname_of _ = "";
5.6
5.7 -fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Datatype_Aux.info) is thy =
5.8 +fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Datatype.info) is thy =
5.9 let
5.10 val recTs = Datatype_Aux.get_rec_types descr;
5.11 val pnames =
5.12 @@ -157,7 +157,7 @@
5.13 in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
5.14
5.15
5.16 -fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Datatype_Aux.info) thy =
5.17 +fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Datatype.info) thy =
5.18 let
5.19 val cert = cterm_of thy;
5.20 val rT = TFree ("'P", HOLogic.typeS);
6.1 --- a/src/HOL/Tools/Function/size.ML Thu Dec 15 21:46:52 2011 +0100
6.2 +++ b/src/HOL/Tools/Function/size.ML Fri Dec 16 10:38:38 2011 +0100
6.3 @@ -40,7 +40,7 @@
6.4 NONE => Abs ("x", T, HOLogic.zero)
6.5 | SOME t => t);
6.6
6.7 -fun is_poly thy (Datatype_Aux.DtType (name, dts)) =
6.8 +fun is_poly thy (Datatype.DtType (name, dts)) =
6.9 (case Datatype.get_info thy name of
6.10 NONE => false
6.11 | SOME _ => exists (is_poly thy) dts)
7.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Dec 15 21:46:52 2011 +0100
7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Dec 16 10:38:38 2011 +0100
7.3 @@ -61,9 +61,7 @@
7.4 val int_T : typ
7.5 val simple_string_of_typ : typ -> string
7.6 val is_real_constr : theory -> string * typ -> bool
7.7 - val typ_of_dtyp :
7.8 - Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
7.9 - -> typ
7.10 + val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
7.11 val varify_type : Proof.context -> typ -> typ
7.12 val instantiate_type : theory -> typ -> typ -> typ -> typ
7.13 val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
8.1 --- a/src/HOL/Tools/refute.ML Thu Dec 15 21:46:52 2011 +0100
8.2 +++ b/src/HOL/Tools/refute.ML Fri Dec 16 10:38:38 2011 +0100
8.3 @@ -862,7 +862,7 @@
8.4 (* sanity check: every element in 'dtyps' must be a *)
8.5 (* 'DtTFree' *)
8.6 val _ = if Library.exists (fn d =>
8.7 - case d of Datatype_Aux.DtTFree _ => false | _ => true) typs then
8.8 + case d of Datatype.DtTFree _ => false | _ => true) typs then
8.9 raise REFUTE ("ground_types", "datatype argument (for type "
8.10 ^ Syntax.string_of_typ ctxt T ^ ") is not a variable")
8.11 else ()
8.12 @@ -874,11 +874,11 @@
8.13 val dT = typ_of_dtyp descr typ_assoc d
8.14 in
8.15 case d of
8.16 - Datatype_Aux.DtTFree _ =>
8.17 + Datatype.DtTFree _ =>
8.18 collect_types dT acc
8.19 - | Datatype_Aux.DtType (_, ds) =>
8.20 + | Datatype.DtType (_, ds) =>
8.21 collect_types dT (fold_rev collect_dtyp ds acc)
8.22 - | Datatype_Aux.DtRec i =>
8.23 + | Datatype.DtRec i =>
8.24 if member (op =) acc dT then
8.25 acc (* prevent infinite recursion *)
8.26 else
8.27 @@ -901,7 +901,7 @@
8.28 in
8.29 (* argument types 'Ts' could be added here, but they are also *)
8.30 (* added by 'collect_dtyp' automatically *)
8.31 - collect_dtyp (Datatype_Aux.DtRec index) acc
8.32 + collect_dtyp (Datatype.DtRec index) acc
8.33 end
8.34 | NONE =>
8.35 (* not an inductive datatype, e.g. defined via "typedef" or *)
8.36 @@ -1853,7 +1853,7 @@
8.37 (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
8.38 val _ =
8.39 if Library.exists (fn d =>
8.40 - case d of Datatype_Aux.DtTFree _ => false | _ => true) dtyps
8.41 + case d of Datatype.DtTFree _ => false | _ => true) dtyps
8.42 then
8.43 raise REFUTE ("IDT_interpreter",
8.44 "datatype argument (for type "
8.45 @@ -1975,7 +1975,7 @@
8.46 (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
8.47 val _ =
8.48 if Library.exists (fn d =>
8.49 - case d of Datatype_Aux.DtTFree _ => false | _ => true) dtyps
8.50 + case d of Datatype.DtTFree _ => false | _ => true) dtyps
8.51 then
8.52 raise REFUTE ("IDT_constructor_interpreter",
8.53 "datatype argument (for type "
8.54 @@ -2035,7 +2035,7 @@
8.55 val typ_assoc = dtyps ~~ Ts'
8.56 (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
8.57 val _ = if Library.exists (fn d =>
8.58 - case d of Datatype_Aux.DtTFree _ => false | _ => true) dtyps
8.59 + case d of Datatype.DtTFree _ => false | _ => true) dtyps
8.60 then
8.61 raise REFUTE ("IDT_constructor_interpreter",
8.62 "datatype argument (for type "
8.63 @@ -2250,7 +2250,7 @@
8.64 (* 'DtTFree' *)
8.65 val _ =
8.66 if Library.exists (fn d =>
8.67 - case d of Datatype_Aux.DtTFree _ => false
8.68 + case d of Datatype.DtTFree _ => false
8.69 | _ => true) dtyps
8.70 then
8.71 raise REFUTE ("IDT_recursion_interpreter",
8.72 @@ -2271,10 +2271,10 @@
8.73 (case AList.lookup op= acc d of
8.74 NONE =>
8.75 (case d of
8.76 - Datatype_Aux.DtTFree _ =>
8.77 + Datatype.DtTFree _ =>
8.78 (* add the association, proceed *)
8.79 rec_typ_assoc ((d, T)::acc) xs
8.80 - | Datatype_Aux.DtType (s, ds) =>
8.81 + | Datatype.DtType (s, ds) =>
8.82 let
8.83 val (s', Ts) = dest_Type T
8.84 in
8.85 @@ -2284,7 +2284,7 @@
8.86 raise REFUTE ("IDT_recursion_interpreter",
8.87 "DtType/Type mismatch")
8.88 end
8.89 - | Datatype_Aux.DtRec i =>
8.90 + | Datatype.DtRec i =>
8.91 let
8.92 val (_, ds, _) = the (AList.lookup (op =) descr i)
8.93 val (_, Ts) = dest_Type T
8.94 @@ -2300,7 +2300,7 @@
8.95 raise REFUTE ("IDT_recursion_interpreter",
8.96 "different type associations for the same dtyp"))
8.97 val typ_assoc = filter
8.98 - (fn (Datatype_Aux.DtTFree _, _) => true | (_, _) => false)
8.99 + (fn (Datatype.DtTFree _, _) => true | (_, _) => false)
8.100 (rec_typ_assoc []
8.101 (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT))
8.102 (* sanity check: typ_assoc must associate types to the *)
8.103 @@ -2317,7 +2317,7 @@
8.104 val mc_intrs = map (fn (idx, (_, _, cs)) =>
8.105 let
8.106 val c_return_typ = typ_of_dtyp descr typ_assoc
8.107 - (Datatype_Aux.DtRec idx)
8.108 + (Datatype.DtRec idx)
8.109 in
8.110 (idx, map (fn (cname, cargs) =>
8.111 (#1 o interpret ctxt (typs, []) {maxvars=0,
8.112 @@ -2371,7 +2371,7 @@
8.113 val _ = map (fn (idx, intrs) =>
8.114 let
8.115 val T = typ_of_dtyp descr typ_assoc
8.116 - (Datatype_Aux.DtRec idx)
8.117 + (Datatype.DtRec idx)
8.118 in
8.119 if length intrs <> size_of_type ctxt (typs, []) T then
8.120 raise REFUTE ("IDT_recursion_interpreter",
8.121 @@ -2465,17 +2465,17 @@
8.122 (* takes the dtyp and interpretation of an element, *)
8.123 (* and computes the interpretation for the *)
8.124 (* corresponding recursive argument *)
8.125 - fun rec_intr (Datatype_Aux.DtRec i) (Leaf xs) =
8.126 + fun rec_intr (Datatype.DtRec i) (Leaf xs) =
8.127 (* recursive argument is "rec_i params elem" *)
8.128 compute_array_entry i (find_index (fn x => x = True) xs)
8.129 - | rec_intr (Datatype_Aux.DtRec _) (Node _) =
8.130 + | rec_intr (Datatype.DtRec _) (Node _) =
8.131 raise REFUTE ("IDT_recursion_interpreter",
8.132 "interpretation for IDT is a node")
8.133 - | rec_intr (Datatype_Aux.DtType ("fun", [dt1, dt2])) (Node xs) =
8.134 + | rec_intr (Datatype.DtType ("fun", [dt1, dt2])) (Node xs) =
8.135 (* recursive argument is something like *)
8.136 (* "\<lambda>x::dt1. rec_? params (elem x)" *)
8.137 Node (map (rec_intr dt2) xs)
8.138 - | rec_intr (Datatype_Aux.DtType ("fun", [_, _])) (Leaf _) =
8.139 + | rec_intr (Datatype.DtType ("fun", [_, _])) (Leaf _) =
8.140 raise REFUTE ("IDT_recursion_interpreter",
8.141 "interpretation for function dtyp is a leaf")
8.142 | rec_intr _ _ =
8.143 @@ -3024,7 +3024,7 @@
8.144 (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
8.145 val _ =
8.146 if Library.exists (fn d =>
8.147 - case d of Datatype_Aux.DtTFree _ => false | _ => true) dtyps
8.148 + case d of Datatype.DtTFree _ => false | _ => true) dtyps
8.149 then
8.150 raise REFUTE ("IDT_printer", "datatype argument (for type " ^
8.151 Syntax.string_of_typ ctxt (Type (s, Ts)) ^ ") is not a variable")