--- a/src/HOL/Tools/Datatype/datatype.ML Thu Dec 30 22:34:53 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Thu Dec 30 23:42:06 2010 +0100
@@ -21,14 +21,11 @@
(** auxiliary **)
-open Datatype_Aux;
-open Datatype_Data;
-
val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
-fun exh_thm_of (dt_info : info Symtab.table) tname =
+fun exh_thm_of (dt_info : Datatype_Aux.info Symtab.table) tname =
#exhaust (the (Symtab.lookup dt_info tname));
val node_name = @{type_name "Datatype.node"};
@@ -60,7 +57,7 @@
(** proof of characteristic theorems **)
-fun representation_proofs (config : config) (dt_info : info Symtab.table)
+fun representation_proofs (config : Datatype_Aux.config) (dt_info : Datatype_Aux.info Symtab.table)
new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
let
val descr' = flat descr;
@@ -73,16 +70,16 @@
(1 upto (length descr'))));
val rep_set_names = map (Sign.full_bname thy1) rep_set_names';
- val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
- val leafTs' = get_nonrec_types descr' sorts;
- val branchTs = get_branching_types descr' sorts;
+ 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 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 (get_arities descr');
+ val arities = remove (op =) 0 (Datatype_Aux.get_arities descr');
val unneeded_vars =
subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
val leafTs = leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
- val recTs = get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr' sorts;
val (newTs, oldTs) = chop (length (hd descr)) recTs;
val sumT = if null leafTs then HOLogic.unitT
else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) leafTs;
@@ -143,27 +140,27 @@
(************** generate introduction rules for representing set **********)
- val _ = message config "Constructing representing sets ...";
+ val _ = Datatype_Aux.message config "Constructing representing sets ...";
(* make introduction rule for a single constructor *)
fun make_intr s n (i, (_, cargs)) =
let
fun mk_prem dt (j, prems, ts) =
- (case strip_dtyp dt of
- (dts, DtRec k) =>
+ (case Datatype_Aux.strip_dtyp dt of
+ (dts, Datatype_Aux.DtRec k) =>
let
- val Ts = map (typ_of_dtyp descr' sorts) dts;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) dts;
val free_t =
- app_bnds (mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
+ Datatype_Aux.app_bnds (Datatype_Aux.mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
in (j + 1, list_all (map (pair "x") Ts,
HOLogic.mk_Trueprop
(Free (nth rep_set_names' k, UnivT') $ free_t)) :: prems,
mk_lim free_t Ts :: ts)
end
| _ =>
- let val T = typ_of_dtyp descr' sorts dt
- in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
+ let val T = Datatype_Aux.typ_of_dtyp descr' sorts 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, [], []);
@@ -221,17 +218,18 @@
fun make_constr_def tname T n ((cname, cargs), (cname', mx)) (thy, defs, eqns, i) =
let
fun constr_arg dt (j, l_args, r_args) =
- let val T = typ_of_dtyp descr' sorts dt;
- val free_t = mk_Free "x" T j
- in (case (strip_dtyp dt, strip_type T) of
- ((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim
+ let
+ val T = Datatype_Aux.typ_of_dtyp descr' sorts dt;
+ val free_t = Datatype_Aux.mk_Free "x" T j;
+ in (case (Datatype_Aux.strip_dtyp dt, strip_type T) of
+ ((_, Datatype_Aux.DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim
(Const (nth all_rep_names m, U --> Univ_elT) $
- app_bnds free_t (length Us)) Us :: r_args)
+ Datatype_Aux.app_bnds free_t (length Us)) Us :: r_args)
| _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
end;
val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);
- val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T;
+ val constrT = (map (Datatype_Aux.typ_of_dtyp descr' sorts) 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);
@@ -276,7 +274,7 @@
(*********** isomorphisms for new types (introduced by typedef) ***********)
- val _ = message config "Proving isomorphism properties ...";
+ val _ = Datatype_Aux.message config "Proving isomorphism properties ...";
val newT_iso_axms = map (fn (_, (_, td)) =>
(collect_simp (#Abs_inverse td), #Rep_inverse td,
@@ -300,7 +298,7 @@
fun make_iso_def k ks n (cname, cargs) (fs, eqns, i) =
let
- val argTs = map (typ_of_dtyp descr' sorts) cargs;
+ val argTs = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
val T = nth recTs k;
val rep_name = nth all_rep_names k;
val rep_const = Const (rep_name, T --> Univ_elT);
@@ -308,23 +306,23 @@
fun process_arg ks' dt (i2, i2', ts, Ts) =
let
- val T' = typ_of_dtyp descr' sorts dt;
+ val T' = Datatype_Aux.typ_of_dtyp descr' sorts dt;
val (Us, U) = strip_type T'
- in (case strip_dtyp dt of
- (_, DtRec j) => if member (op =) ks' j then
- (i2 + 1, i2' + 1, ts @ [mk_lim (app_bnds
- (mk_Free "y" (Us ---> Univ_elT) i2') (length Us)) Us],
+ in (case Datatype_Aux.strip_dtyp dt of
+ (_, Datatype_Aux.DtRec j) => if member (op =) ks' j then
+ (i2 + 1, i2' + 1, ts @ [mk_lim (Datatype_Aux.app_bnds
+ (Datatype_Aux.mk_Free "y" (Us ---> Univ_elT) i2') (length Us)) Us],
Ts @ [Us ---> Univ_elT])
else
(i2 + 1, i2', ts @ [mk_lim
(Const (nth all_rep_names j, U --> Univ_elT) $
- app_bnds (mk_Free "x" T' i2) (length Us)) Us], Ts)
- | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts))
+ Datatype_Aux.app_bnds (Datatype_Aux.mk_Free "x" T' i2) (length Us)) Us], Ts)
+ | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (Datatype_Aux.mk_Free "x" T' i2)], Ts))
end;
val (i2, i2', ts, Ts) = fold (process_arg ks) cargs (1, 1, [], []);
- val xs = map (uncurry (mk_Free "x")) (argTs ~~ (1 upto (i2 - 1)));
- val ys = map (uncurry (mk_Free "y")) (Ts ~~ (1 upto (i2' - 1)));
+ val xs = map (uncurry (Datatype_Aux.mk_Free "x")) (argTs ~~ (1 upto (i2 - 1)));
+ val ys = map (uncurry (Datatype_Aux.mk_Free "y")) (Ts ~~ (1 upto (i2' - 1)));
val f = list_abs_free (map dest_Free (xs @ ys), mk_univ_inj ts n i);
val (_, _, ts', _) = fold (process_arg []) cargs (1, 1, [], []);
@@ -383,9 +381,9 @@
val f = Free ("f", Ts ---> U)
in Skip_Proof.prove_global thy [] [] (Logic.mk_implies
(HOLogic.mk_Trueprop (HOLogic.list_all
- (map (pair "x") Ts, S $ app_bnds f i)),
+ (map (pair "x") Ts, S $ Datatype_Aux.app_bnds f i)),
HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
- r $ (a $ app_bnds f i)), f))))
+ r $ (a $ Datatype_Aux.app_bnds f i)), f))))
(fn _ => EVERY [REPEAT_DETERM_N i (rtac ext 1),
REPEAT (etac allE 1), rtac thm 1, atac 1])
end
@@ -407,9 +405,9 @@
val Rep_t = Const (nth all_rep_names i, T --> Univ_elT);
val rep_set_name = nth rep_set_names i
in (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $
- HOLogic.mk_eq (Rep_t $ mk_Free "x" T i, Rep_t $ Bound 0) $
- HOLogic.mk_eq (mk_Free "x" T i, Bound 0)),
- Const (rep_set_name, UnivT') $ (Rep_t $ mk_Free "x" T i))
+ HOLogic.mk_eq (Rep_t $ Datatype_Aux.mk_Free "x" T i, Rep_t $ Bound 0) $
+ HOLogic.mk_eq (Datatype_Aux.mk_Free "x" T i, Bound 0)),
+ Const (rep_set_name, UnivT') $ (Rep_t $ Datatype_Aux.mk_Free "x" T i))
end;
val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
@@ -419,11 +417,11 @@
map (fn r => r RS @{thm injD}) inj_thms;
val inj_thm = Skip_Proof.prove_global thy5 [] []
- (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
- [(indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+ (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl1)) (fn _ => EVERY
+ [(Datatype_Aux.indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
REPEAT (EVERY
[rtac allI 1, rtac impI 1,
- exh_tac (exh_thm_of dt_info) 1,
+ Datatype_Aux.exh_tac (exh_thm_of dt_info) 1,
REPEAT (EVERY
[hyp_subst_tac 1,
rewrite_goals_tac rewrites,
@@ -440,17 +438,17 @@
Lim_inject :: inj_thms') @ fun_congs) 1),
atac 1]))])])])]);
- val inj_thms'' = map (fn r => r RS datatype_injI) (split_conj_thm inj_thm);
+ val inj_thms'' = map (fn r => r RS datatype_injI) (Datatype_Aux.split_conj_thm inj_thm);
val elem_thm =
- Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
- (fn _ =>
- EVERY [(indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
- rewrite_goals_tac rewrites,
- REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
- ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
+ Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl2))
+ (fn _ =>
+ EVERY [(Datatype_Aux.indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+ rewrite_goals_tac rewrites,
+ REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
+ ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
- in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
+ in (inj_thms'' @ inj_thms, elem_thms @ (Datatype_Aux.split_conj_thm elem_thm))
end;
val (iso_inj_thms_unfolded, iso_elem_thms) =
@@ -463,14 +461,14 @@
fun mk_iso_t (((set_name, iso_name), i), T) =
let val isoT = T --> Univ_elT
in HOLogic.imp $
- (Const (set_name, UnivT') $ mk_Free "x" Univ_elT i) $
+ (Const (set_name, UnivT') $ Datatype_Aux.mk_Free "x" Univ_elT i) $
(if i < length newTs then HOLogic.true_const
- else HOLogic.mk_mem (mk_Free "x" Univ_elT i,
+ else HOLogic.mk_mem (Datatype_Aux.mk_Free "x" Univ_elT i,
Const (@{const_name image}, isoT --> HOLogic.mk_setT T --> UnivT) $
Const (iso_name, isoT) $ Const (@{const_abbrev UNIV}, HOLogic.mk_setT T)))
end;
- val iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t
+ val iso_t = HOLogic.mk_Trueprop (Datatype_Aux.mk_conj (map mk_iso_t
(rep_set_names ~~ all_rep_names ~~ (0 upto (length descr' - 1)) ~~ recTs)));
(* all the theorems are proved by one single simultaneous induction *)
@@ -479,9 +477,9 @@
iso_inj_thms_unfolded;
val iso_thms = if length descr = 1 then [] else
- drop (length newTs) (split_conj_thm
+ drop (length newTs) (Datatype_Aux.split_conj_thm
(Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
- [(indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+ [(Datatype_Aux.indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
REPEAT (rtac TrueI 1),
rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
Thm.symmetric (mk_meta_eq @{thm fun_eq_iff}) :: range_eqs),
@@ -502,7 +500,7 @@
(******************* freeness theorems for constructors *******************)
- val _ = message config "Proving freeness of constructors ...";
+ val _ = Datatype_Aux.message config "Proving freeness of constructors ...";
(* prove theorem Rep_i (Constr_j ...) = Inj_j ... *)
@@ -566,12 +564,12 @@
val ((constr_inject', distinct_thms'), thy6) =
thy5
|> Sign.parent_path
- |> store_thmss "inject" new_type_names constr_inject
- ||>> store_thmss "distinct" new_type_names distinct_thms;
+ |> Datatype_Aux.store_thmss "inject" new_type_names constr_inject
+ ||>> Datatype_Aux.store_thmss "distinct" new_type_names distinct_thms;
(*************************** induction theorem ****************************)
- val _ = message config "Proving induction rule for datatypes ...";
+ val _ = Datatype_Aux.message config "Proving induction rule for datatypes ...";
val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
(map (fn r => r RS @{thm the_inv_f_f} RS subst) iso_inj_thms_unfolded);
@@ -580,7 +578,7 @@
fun mk_indrule_lemma ((i, _), T) (prems, concls) =
let
val Rep_t = Const (nth all_rep_names i, T --> Univ_elT) $
- mk_Free "x" T i;
+ Datatype_Aux.mk_Free "x" T i;
val Abs_t = if i < length newTs then
Const (Sign.intern_const thy6
@@ -589,10 +587,13 @@
[HOLogic.mk_setT T, T --> Univ_elT, Univ_elT] ---> T) $
HOLogic.mk_UNIV T $ Const (nth all_rep_names i, T --> Univ_elT)
- in (prems @ [HOLogic.imp $
+ in
+ (prems @
+ [HOLogic.imp $
(Const (nth rep_set_names i, UnivT') $ Rep_t) $
- (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
- concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i])
+ (Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
+ concls @
+ [Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ Datatype_Aux.mk_Free "x" T i])
end;
val (indrule_lemma_prems, indrule_lemma_concls) =
@@ -602,8 +603,8 @@
val indrule_lemma = Skip_Proof.prove_global thy6 [] []
(Logic.mk_implies
- (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
- HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
+ (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_prems),
+ HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_concls))) (fn _ => EVERY
[REPEAT (etac conjE 1),
REPEAT (EVERY
[TRY (rtac conjI 1), resolve_tac Rep_inverse_thms 1,
@@ -619,7 +620,7 @@
(Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
(fn {prems, ...} => EVERY
[rtac indrule_lemma' 1,
- (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+ (Datatype_Aux.indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
EVERY (map (fn (prem, r) => (EVERY
[REPEAT (eresolve_tac Abs_inverse_thms 1),
simp_tac (HOL_basic_ss addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
@@ -680,7 +681,7 @@
| vs => error ("Extra type variables on rhs: " ^ commas vs));
val c = Sign.full_name_path tmp_thy tname' cname;
in
- (constrs @ [(c, map (dtyp_of_typ new_dts) cargs')],
+ (constrs @ [(c, map (Datatype_Aux.dtyp_of_typ new_dts) cargs')],
constr_syntax' @ [(cname, mx')], sorts'')
end handle ERROR msg => cat_error msg
("The error above occurred in constructor " ^ quote (Binding.str_of cname) ^
@@ -691,7 +692,7 @@
in
case duplicates (op =) (map fst constrs') of
[] =>
- (dts' @ [(i, (Sign.full_name tmp_thy tname, map DtTFree tvs, constrs'))],
+ (dts' @ [(i, (Sign.full_name tmp_thy tname, map Datatype_Aux.DtTFree tvs, constrs'))],
constr_syntax @ [constr_syntax'], sorts', i + 1)
| dups => error ("Duplicate constructors " ^ commas dups ^
" in datatype " ^ quote (Binding.str_of tname))
@@ -701,12 +702,14 @@
fold2 prep_dt_spec dts new_type_names ([], [], [], 0);
val sorts = sorts' @ map (rpair (Sign.defaultS tmp_thy)) (subtract (op =) (map fst sorts') tyvars);
val dt_info = Datatype_Data.get_all thy;
- val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
- val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
- if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
- else reraise exn;
+ val (descr, _) = Datatype_Aux.unfold_datatypes tmp_thy dts' sorts 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)
+ else reraise exn;
- val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
+ val _ = Datatype_Aux.message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
in
thy
@@ -718,7 +721,7 @@
end;
val add_datatype = gen_add_datatype Datatype_Data.cert_typ;
-val datatype_cmd = snd ooo gen_add_datatype Datatype_Data.read_typ default_config;
+val datatype_cmd = snd ooo gen_add_datatype Datatype_Data.read_typ Datatype_Aux.default_config;
local
@@ -745,4 +748,7 @@
end;
+
+open Datatype_Data;
+
end;
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Dec 30 22:34:53 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Dec 30 23:42:06 2010 +0100
@@ -35,16 +35,15 @@
structure Datatype_Abs_Proofs: DATATYPE_ABS_PROOFS =
struct
-open Datatype_Aux;
-
(************************ case distinction theorems ***************************)
-fun prove_casedist_thms (config : config) new_type_names descr sorts induct case_names_exhausts thy =
+fun prove_casedist_thms (config : Datatype_Aux.config)
+ new_type_names descr sorts induct case_names_exhausts thy =
let
- val _ = message config "Proving case distinction theorems ...";
+ val _ = Datatype_Aux.message config "Proving case distinction theorems ...";
val descr' = flat descr;
- val recTs = get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr' sorts;
val newTs = take (length (hd descr)) recTs;
val {maxidx, ...} = rep_thm induct;
@@ -60,7 +59,7 @@
val cert = cterm_of thy;
val insts' = (map cert induct_Ps) ~~ (map cert insts);
val induct' = refl RS ((nth
- (split_conj_thm (cterm_instantiate insts' induct)) i) RSN (2, rev_mp))
+ (Datatype_Aux.split_conj_thm (cterm_instantiate insts' induct)) i) RSN (2, rev_mp))
in
Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
@@ -75,22 +74,23 @@
(newTs ~~ Datatype_Prop.make_casedists descr sorts)
in
thy
- |> store_thms_atts "exhaust" new_type_names (map single case_names_exhausts) casedist_thms
+ |> Datatype_Aux.store_thms_atts "exhaust" new_type_names
+ (map single case_names_exhausts) casedist_thms
end;
(*************************** primrec combinators ******************************)
-fun prove_primrec_thms (config : config) new_type_names descr sorts
+fun prove_primrec_thms (config : Datatype_Aux.config) new_type_names descr sorts
injects_of constr_inject (dist_rewrites, other_dist_rewrites) induct thy =
let
- val _ = message config "Constructing primrec combinators ...";
+ val _ = Datatype_Aux.message config "Constructing primrec combinators ...";
val big_name = space_implode "_" new_type_names;
val thy0 = Sign.add_path big_name thy;
val descr' = flat descr;
- val recTs = get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr' sorts;
val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
val newTs = take (length (hd descr)) recTs;
@@ -108,7 +108,7 @@
val rec_set_Ts = map (fn (T1, T2) =>
reccomb_fn_Ts @ [T1, T2] ---> HOLogic.boolT) (recTs ~~ rec_result_Ts);
- val rec_fns = map (uncurry (mk_Free "f"))
+ val rec_fns = map (uncurry (Datatype_Aux.mk_Free "f"))
(reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
val rec_sets' = map (fn c => list_comb (Free c, rec_fns))
(rec_set_names' ~~ rec_set_Ts);
@@ -120,21 +120,21 @@
fun make_rec_intr T rec_set (cname, cargs) (rec_intr_ts, l) =
let
fun mk_prem (dt, U) (j, k, prems, t1s, t2s) =
- let val free1 = mk_Free "x" U j
- in (case (strip_dtyp dt, strip_type U) of
- ((_, DtRec m), (Us, _)) =>
+ let val free1 = Datatype_Aux.mk_Free "x" U j
+ in (case (Datatype_Aux.strip_dtyp dt, strip_type U) of
+ ((_, Datatype_Aux.DtRec m), (Us, _)) =>
let
- val free2 = mk_Free "y" (Us ---> nth rec_result_Ts m) k;
+ val free2 = Datatype_Aux.mk_Free "y" (Us ---> nth rec_result_Ts m) k;
val i = length Us
in (j + 1, k + 1, HOLogic.mk_Trueprop (HOLogic.list_all
(map (pair "x") Us, nth rec_sets' m $
- app_bnds free1 i $ app_bnds free2 i)) :: prems,
+ Datatype_Aux.app_bnds free1 i $ Datatype_Aux.app_bnds free2 i)) :: prems,
free1::t1s, free2::t2s)
end
| _ => (j + 1, k, prems, free1::t1s, t2s))
end;
- val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
val (_, _, prems, t1s, t2s) = fold_rev mk_prem (cargs ~~ Ts) (1, 1, [], [], [])
in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop
@@ -160,7 +160,7 @@
(* prove uniqueness and termination of primrec combinators *)
- val _ = message config "Proving termination and uniqueness of primrec functions ...";
+ val _ = Datatype_Aux.message config "Proving termination and uniqueness of primrec functions ...";
fun mk_unique_tac ((((i, (tname, _, constrs)), elim), T), T') (tac, intrs) =
let
@@ -175,7 +175,7 @@
fun mk_unique_constr_tac n (cname, cargs) (tac, intr::intrs, j) =
let
- val k = length (filter is_rec_type cargs)
+ val k = length (filter Datatype_Aux.is_rec_type cargs)
in (EVERY [DETERM tac,
REPEAT (etac ex1E 1), rtac ex1I 1,
@@ -201,7 +201,7 @@
let
val rec_unique_ts = map (fn (((set_t, T1), T2), i) =>
Const (@{const_name Ex1}, (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
- absfree ("y", T2, set_t $ mk_Free "x" T1 i $ Free ("y", T2)))
+ absfree ("y", T2, set_t $ Datatype_Aux.mk_Free "x" T1 i $ Free ("y", T2)))
(rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
val cert = cterm_of thy1
val insts = map (fn ((i, T), t) => absfree ("x" ^ (string_of_int i), T, t))
@@ -212,8 +212,9 @@
(((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1
THEN rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs));
- in split_conj_thm (Skip_Proof.prove_global thy1 [] []
- (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))
+ in
+ Datatype_Aux.split_conj_thm (Skip_Proof.prove_global thy1 [] []
+ (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj rec_unique_ts)) (K tac))
end;
val rec_total_thms = map (fn r => r RS @{thm theI'}) rec_unique_thms;
@@ -247,7 +248,7 @@
(* prove characteristic equations for primrec combinators *)
- val _ = message config "Proving characteristic theorems for primrec combinators ..."
+ val _ = Datatype_Aux.message config "Proving characteristic theorems for primrec combinators ...";
val rec_thms = map (fn t => Skip_Proof.prove_global thy2 [] [] t
(fn _ => EVERY
@@ -256,8 +257,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 sorts thy2);
in
thy2
|> Sign.add_path (space_implode "_" new_type_names)
@@ -270,24 +270,25 @@
(***************************** case combinators *******************************)
-fun prove_case_thms (config : config) new_type_names descr sorts reccomb_names primrec_thms thy =
+fun prove_case_thms (config : Datatype_Aux.config)
+ new_type_names descr sorts reccomb_names primrec_thms thy =
let
- val _ = message config "Proving characteristic theorems for case combinators ...";
+ 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 = get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr' sorts;
val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
val newTs = take (length (hd descr)) recTs;
val T' = TFree (Name.variant used "'t", HOLogic.typeS);
- fun mk_dummyT dt = binder_types (typ_of_dtyp descr' sorts dt) ---> T';
+ fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' sorts dt) ---> T';
val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
let
- val Ts = map (typ_of_dtyp descr' sorts) cargs;
- val Ts' = map mk_dummyT (filter is_rec_type cargs)
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+ val Ts' = map mk_dummyT (filter Datatype_Aux.is_rec_type cargs)
in Const (@{const_name undefined}, Ts @ Ts' ---> T')
end) constrs) descr';
@@ -299,11 +300,11 @@
let
val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
let
- val Ts = map (typ_of_dtyp descr' sorts) cargs;
- val Ts' = Ts @ map mk_dummyT (filter is_rec_type cargs);
- val frees' = map2 (mk_Free "x") Ts' (1 upto length Ts');
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) 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';
- val free = mk_Free "f" (Ts ---> T') j
+ val free = Datatype_Aux.mk_Free "f" (Ts ---> T') j
in
(free, list_abs_free (map dest_Free frees',
list_comb (free, frees)))
@@ -335,20 +336,20 @@
thy2
|> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)
|> Sign.parent_path
- |> store_thmss "cases" new_type_names case_thms
+ |> Datatype_Aux.store_thmss "cases" new_type_names case_thms
|-> (fn thmss => pair (thmss, case_names))
end;
(******************************* case splitting *******************************)
-fun prove_split_thms (config : config) new_type_names descr sorts constr_inject dist_rewrites
- casedist_thms case_thms thy =
+fun prove_split_thms (config : Datatype_Aux.config)
+ new_type_names descr sorts constr_inject dist_rewrites casedist_thms case_thms thy =
let
- val _ = message config "Proving equations for case splitting ...";
+ val _ = Datatype_Aux.message config "Proving equations for case splitting ...";
val descr' = flat descr;
- val recTs = get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr' sorts;
val newTs = take (length (hd descr)) recTs;
fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'),
@@ -373,8 +374,8 @@
in
thy
- |> store_thms "split" new_type_names split_thms
- ||>> store_thms "split_asm" new_type_names split_asm_thms
+ |> Datatype_Aux.store_thms "split" new_type_names split_thms
+ ||>> Datatype_Aux.store_thms "split_asm" new_type_names split_asm_thms
|-> (fn (thms1, thms2) => pair (thms1 ~~ thms2))
end;
@@ -387,13 +388,14 @@
val weak_case_congs = map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs
new_type_names descr sorts thy)
- in thy |> store_thms "weak_case_cong" new_type_names weak_case_congs end;
+ in thy |> Datatype_Aux.store_thms "weak_case_cong" new_type_names weak_case_congs end;
(************************* additional theorems for TFL ************************)
-fun prove_nchotomys (config : config) new_type_names descr sorts casedist_thms thy =
+fun prove_nchotomys (config : Datatype_Aux.config)
+ new_type_names descr sorts casedist_thms thy =
let
- val _ = message config "Proving additional theorems for TFL ...";
+ val _ = Datatype_Aux.message config "Proving additional theorems for TFL ...";
fun prove_nchotomy (t, exhaustion) =
let
@@ -404,14 +406,14 @@
in
Skip_Proof.prove_global thy [] [] t (fn _ =>
EVERY [rtac allI 1,
- exh_tac (K exhaustion) 1,
+ Datatype_Aux.exh_tac (K exhaustion) 1,
ALLGOALS (fn i => tac i (i-1))])
end;
val nchotomys =
map prove_nchotomy (Datatype_Prop.make_nchotomys descr sorts ~~ casedist_thms)
- in thy |> store_thms "nchotomy" new_type_names nchotomys end;
+ 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 =
let
@@ -437,6 +439,9 @@
val case_congs = map prove_case_cong (Datatype_Prop.make_case_congs
new_type_names descr sorts thy ~~ nchotomys ~~ case_thms)
- in thy |> store_thms "case_cong" new_type_names case_congs end;
+ in thy |> Datatype_Aux.store_thms "case_cong" new_type_names case_congs end;
+
+
+open Datatype_Aux;
end;
--- a/src/HOL/Tools/Datatype/datatype_data.ML Thu Dec 30 22:34:53 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Thu Dec 30 23:42:06 2010 +0100
@@ -37,8 +37,6 @@
structure Datatype_Data: DATATYPE_DATA =
struct
-open Datatype_Aux;
-
(** theory data **)
(* data management *)
@@ -46,9 +44,9 @@
structure DatatypesData = Theory_Data
(
type T =
- {types: info Symtab.table,
- constrs: (string * info) list Symtab.table,
- cases: info Symtab.table};
+ {types: Datatype_Aux.info Symtab.table,
+ constrs: (string * Datatype_Aux.info) list Symtab.table,
+ cases: Datatype_Aux.info Symtab.table};
val empty =
{types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
@@ -85,7 +83,7 @@
val info_of_case = Symtab.lookup o #cases o DatatypesData.get;
-fun register (dt_infos : (string * info) list) =
+fun register (dt_infos : (string * Datatype_Aux.info) list) =
DatatypesData.map (fn {types, constrs, cases} =>
{types = types |> fold Symtab.update dt_infos,
constrs = constrs |> fold (fn (constr, dtname_info) =>
@@ -116,13 +114,15 @@
val SOME (_, dtys, _) = AList.lookup (op =) descr (#index info);
val vs = map ((fn v => (v, (the o AList.lookup (op =) (#sorts info)) v))
- o dest_DtTFree) dtys;
+ o Datatype_Aux.dest_DtTFree) dtys;
- fun is_DtTFree (DtTFree _) = true
+ fun is_DtTFree (Datatype_Aux.DtTFree _) = true
| is_DtTFree _ = false
val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr;
- val protoTs as (dataTs, _) = chop k descr
- |> (pairself o map) (fn (_, (tyco, dTs, _)) => (tyco, map (typ_of_dtyp descr vs) dTs));
+ val protoTs as (dataTs, _) =
+ chop k descr
+ |> (pairself o map)
+ (fn (_, (tyco, dTs, _)) => (tyco, map (Datatype_Aux.typ_of_dtyp descr vs) dTs));
val tycos = map fst dataTs;
val _ = if eq_set (op =) (tycos, raw_tycos) then ()
@@ -133,7 +133,7 @@
val names = map Long_Name.base_name (the_default tycos (#alt_names info));
val (auxnames, _) = Name.make_context names
- |> fold_map (yield_singleton Name.variants o name_of_typ) Us;
+ |> fold_map (yield_singleton Name.variants o Datatype_Aux.name_of_typ) Us;
val prefix = space_implode "_" names;
in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end;
@@ -186,11 +186,11 @@
local
-fun dt_recs (DtTFree _) = []
- | dt_recs (DtType (_, dts)) = maps dt_recs dts
- | dt_recs (DtRec i) = [i];
+fun dt_recs (Datatype_Aux.DtTFree _) = []
+ | dt_recs (Datatype_Aux.DtType (_, dts)) = maps dt_recs dts
+ | dt_recs (Datatype_Aux.DtRec i) = [i];
-fun dt_cases (descr: descr) (_, args, constrs) =
+fun dt_cases (descr: Datatype_Aux.descr) (_, args, constrs) =
let
fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
val bnames = map the_bname (distinct (op =) (maps dt_recs args));
@@ -264,7 +264,7 @@
(** abstract theory extensions relative to a datatype characterisation **)
structure Datatype_Interpretation = Interpretation
- (type T = config * string list val eq: T * T -> bool = eq_snd op =);
+ (type T = Datatype_Aux.config * string list val eq: T * T -> bool = eq_snd op =);
fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites
@@ -297,7 +297,9 @@
val thy2 = thy1 |> Theory.checkpoint;
val flat_descr = flat descr;
val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
- val _ = message config ("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
+ val _ =
+ 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;
@@ -305,7 +307,7 @@
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 (get_rec_types flat_descr sorts))
+ 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;
@@ -363,8 +365,8 @@
val prfx = Binding.qualify true (space_implode "_" new_type_names);
val (((inject, distinct), [induct]), thy2) =
thy1
- |> store_thmss "inject" new_type_names raw_inject
- ||>> store_thmss "distinct" new_type_names raw_distinct
+ |> Datatype_Aux.store_thmss "inject" new_type_names raw_inject
+ ||>> Datatype_Aux.store_thmss "distinct" new_type_names raw_distinct
||>> Global_Theory.add_thms
[((prfx (Binding.name "induct"), raw_induct),
[mk_case_names_induct descr])];
@@ -411,11 +413,11 @@
val cs = map (apsnd (map norm_constr)) raw_cs;
val dtyps_of_typ =
- map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs)) o binder_types;
+ map (Datatype_Aux.dtyp_of_typ (map (rpair (map fst vs) o fst) cs)) o binder_types;
val dt_names = map fst cs;
fun mk_spec (i, (tyco, constr)) = (i, (tyco,
- map (DtTFree o fst) vs,
+ map (Datatype_Aux.DtTFree o fst) vs,
(map o apsnd) dtyps_of_typ constr))
val descr = map_index mk_spec cs;
val injs = Datatype_Prop.make_injs [descr] vs;
@@ -441,7 +443,7 @@
end;
val rep_datatype = gen_rep_datatype Sign.cert_term;
-val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I);
+val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global Datatype_Aux.default_config (K I);
@@ -463,4 +465,7 @@
>> (fn (alt_names, ts) =>
Toplevel.print o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
+
+open Datatype_Aux;
+
end;
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Thu Dec 30 22:34:53 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Thu Dec 30 23:42:06 2010 +0100
@@ -35,8 +35,6 @@
structure Datatype_Prop : DATATYPE_PROP =
struct
-open Datatype_Aux;
-
fun indexify_names names =
let
fun index (x :: xs) tab =
@@ -63,7 +61,7 @@
fun make_inj T (cname, cargs) =
if null cargs then I else
let
- val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
val constr_t = Const (cname, Ts ---> T);
val tnames = make_tnames Ts;
val frees = map Free (tnames ~~ Ts);
@@ -75,7 +73,7 @@
end;
in
map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
- (hd descr) (take (length (hd descr)) (get_rec_types descr' sorts))
+ (hd descr) (take (length (hd descr)) (Datatype_Aux.get_rec_types descr' sorts))
end;
@@ -84,10 +82,10 @@
fun make_distincts descr sorts =
let
val descr' = flat descr;
- val recTs = get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr' sorts;
val newTs = take (length (hd descr)) recTs;
- fun prep_constr (cname, cargs) = (cname, map (typ_of_dtyp descr' sorts) cargs);
+ fun prep_constr (cname, cargs) = (cname, map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs);
fun make_distincts' _ [] = []
| make_distincts' T ((cname, cargs)::constrs) =
@@ -117,8 +115,9 @@
fun make_ind descr sorts =
let
val descr' = flat descr;
- val recTs = get_rec_types descr' sorts;
- val pnames = if length descr' = 1 then ["P"]
+ val recTs = Datatype_Aux.get_rec_types descr' sorts;
+ val pnames =
+ if length descr' = 1 then ["P"]
else map (fn i => "P" ^ string_of_int i) (1 upto length descr');
fun make_pred i T =
@@ -129,15 +128,18 @@
let
fun mk_prem ((dt, s), T) =
let val (Us, U) = strip_type T
- in list_all (map (pair "x") Us, HOLogic.mk_Trueprop
- (make_pred (body_index dt) U $ app_bnds (Free (s, T)) (length Us)))
+ in
+ list_all (map (pair "x") Us,
+ HOLogic.mk_Trueprop
+ (make_pred (Datatype_Aux.body_index dt) U $
+ Datatype_Aux.app_bnds (Free (s, T)) (length Us)))
end;
- 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 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 tnames = Name.variant_list pnames (make_tnames Ts);
- val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
+ val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
val frees = tnames ~~ Ts;
val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
@@ -163,7 +165,7 @@
fun make_casedist_prem T (cname, cargs) =
let
- val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
val frees = Name.variant_list ["P", "y"] (make_tnames Ts) ~~ Ts;
val free_ts = map Free frees
in list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
@@ -176,7 +178,10 @@
in Logic.list_implies (prems, HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)))
end
- in map2 make_casedist (hd descr) (take (length (hd descr)) (get_rec_types descr' sorts)) end;
+ in
+ map2 make_casedist (hd descr)
+ (take (length (hd descr)) (Datatype_Aux.get_rec_types descr' sorts))
+ end;
(*************** characteristic equations for primrec combinator **************)
@@ -190,11 +195,11 @@
val reccomb_fn_Ts = maps (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
let
- val Ts = map (typ_of_dtyp descr' sorts) cargs;
- val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+ val recs = filter (Datatype_Aux.is_rec_type o fst) (cargs ~~ Ts);
fun mk_argT (dt, T) =
- binder_types T ---> List.nth (rec_result_Ts, body_index dt);
+ binder_types T ---> List.nth (rec_result_Ts, Datatype_Aux.body_index dt);
val argTs = Ts @ map mk_argT recs
in argTs ---> List.nth (rec_result_Ts, i)
@@ -205,12 +210,12 @@
fun make_primrecs new_type_names descr sorts thy =
let
val descr' = flat descr;
- val recTs = get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr' sorts;
val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
- val rec_fns = map (uncurry (mk_Free "f"))
+ val rec_fns = map (uncurry (Datatype_Aux.mk_Free "f"))
(reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
@@ -224,18 +229,18 @@
fun make_primrec T comb_t (cname, cargs) (ts, f::fs) =
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 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 tnames = make_tnames Ts;
- val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
+ val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
val frees = map Free (tnames ~~ Ts);
val frees' = map Free (rec_tnames ~~ recTs');
fun mk_reccomb ((dt, T), t) =
let val (Us, U) = strip_type T
in list_abs (map (pair "x") Us,
- List.nth (reccombs, body_index dt) $ app_bnds t (length Us))
+ List.nth (reccombs, Datatype_Aux.body_index dt) $ Datatype_Aux.app_bnds t (length Us))
end;
val reccombs' = map mk_reccomb (recs ~~ recTs' ~~ frees')
@@ -256,14 +261,14 @@
fun make_case_combs new_type_names descr sorts thy fname =
let
val descr' = flat descr;
- val recTs = get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr' sorts;
val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
val newTs = take (length (hd descr)) recTs;
val T' = TFree (Name.variant used "'t", HOLogic.typeS);
val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
- let val Ts = map (typ_of_dtyp descr' sorts) cargs
+ let val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs
in Ts ---> T' end) constrs) (hd descr);
val case_names = map (fn s =>
@@ -271,7 +276,7 @@
in
map (fn ((name, Ts), T) => list_comb
(Const (name, Ts @ [T] ---> T'),
- map (uncurry (mk_Free fname)) (Ts ~~ (1 upto length Ts))))
+ map (uncurry (Datatype_Aux.mk_Free fname)) (Ts ~~ (1 upto length Ts))))
(case_names ~~ case_fn_Ts ~~ newTs)
end;
@@ -280,12 +285,12 @@
fun make_cases new_type_names descr sorts thy =
let
val descr' = flat descr;
- val recTs = get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr' sorts;
val newTs = take (length (hd descr)) recTs;
fun make_case T comb_t ((cname, cargs), f) =
let
- val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
val frees = map Free ((make_tnames Ts) ~~ Ts)
in HOLogic.mk_Trueprop (HOLogic.mk_eq
(comb_t $ list_comb (Const (cname, Ts ---> T), frees),
@@ -303,7 +308,7 @@
fun make_splits new_type_names descr sorts thy =
let
val descr' = flat descr;
- val recTs = get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr' sorts;
val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
val newTs = take (length (hd descr)) recTs;
val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
@@ -316,7 +321,7 @@
fun process_constr ((cname, cargs), f) (t1s, t2s) =
let
- val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) 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));
@@ -330,8 +335,8 @@
val (t1s, t2s) = fold_rev process_constr (constrs ~~ fs) ([], []);
val lhs = P $ (comb_t $ Free ("x", T))
in
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, mk_conj t1s)),
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, HOLogic.Not $ mk_disj t2s)))
+ (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, Datatype_Aux.mk_conj t1s)),
+ HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, HOLogic.Not $ Datatype_Aux.mk_disj t2s)))
end
in map make_split ((hd descr) ~~ newTs ~~
@@ -415,12 +420,12 @@
fun make_nchotomys descr sorts =
let
val descr' = flat descr;
- val recTs = get_rec_types descr' sorts;
+ val recTs = Datatype_Aux.get_rec_types descr' sorts;
val newTs = take (length (hd descr)) recTs;
fun mk_eqn T (cname, cargs) =
let
- val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
val tnames = Name.variant_list ["v"] (make_tnames Ts);
val frees = tnames ~~ Ts
in
@@ -430,8 +435,11 @@
end
in map (fn ((_, (_, _, constrs)), T) =>
- HOLogic.mk_Trueprop (HOLogic.mk_all ("v", T, mk_disj (map (mk_eqn T) constrs))))
+ HOLogic.mk_Trueprop (HOLogic.mk_all ("v", T, Datatype_Aux.mk_disj (map (mk_eqn T) constrs))))
(hd descr ~~ newTs)
end;
+
+open Datatype_Aux;
+
end;
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Thu Dec 30 22:34:53 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Thu Dec 30 23:42:06 2010 +0100
@@ -14,8 +14,6 @@
structure Datatype_Realizer : DATATYPE_REALIZER =
struct
-open Datatype_Aux;
-
fun subsets i j =
if i <= j then
let val is = subsets (i+1) j
@@ -30,9 +28,9 @@
fun tname_of (Type (s, _)) = s
| tname_of _ = "";
-fun make_ind sorts ({descr, rec_names, rec_rewrites, induct, ...} : info) is thy =
+fun make_ind sorts ({descr, rec_names, rec_rewrites, induct, ...} : Datatype_Aux.info) is thy =
let
- val recTs = get_rec_types descr sorts;
+ val recTs = Datatype_Aux.get_rec_types descr sorts;
val pnames = if length descr = 1 then ["P"]
else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
@@ -51,16 +49,16 @@
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 (typ_of_dtyp descr sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs;
val tnames = Name.variant_list pnames (Datatype_Prop.make_tnames Ts);
- val recs = filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
+ val recs = filter (Datatype_Aux.is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
val frees = tnames ~~ Ts;
fun mk_prems vs [] =
let
val rT = nth (rec_result_Ts) i;
val vs' = filter_out is_unit vs;
- val f = mk_Free "f" (map fastype_of vs' ---> rT) j;
+ val f = Datatype_Aux.mk_Free "f" (map fastype_of vs' ---> rT) j;
val f' = Envir.eta_contract (list_abs_free
(map dest_Free vs, if member (op =) is i then list_comb (f, vs')
else HOLogic.unit));
@@ -69,7 +67,7 @@
end
| mk_prems vs (((dt, s), T) :: ds) =
let
- val k = body_index dt;
+ val k = Datatype_Aux.body_index dt;
val (Us, U) = strip_type T;
val i = length Us;
val rT = nth (rec_result_Ts) k;
@@ -77,8 +75,8 @@
val (p, f) = mk_prems (vs @ [r]) ds
in (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
(list_all (map (pair "x") Us, HOLogic.mk_Trueprop
- (make_pred k rT U (app_bnds r i)
- (app_bnds (Free (s, T)) i))), p)), f)
+ (make_pred k rT U (Datatype_Aux.app_bnds r i)
+ (Datatype_Aux.app_bnds (Free (s, T)) i))), p)), f)
end
in (apfst (curry list_all_free frees) (mk_prems (map Free frees) recs), j + 1) end)
@@ -154,7 +152,8 @@
in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
-fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaust, ...} : info) thy =
+fun make_casedists sorts
+ ({index, descr, case_name, case_rewrites, exhaust, ...} : Datatype_Aux.info) thy =
let
val cert = cterm_of thy;
val rT = TFree ("'P", HOLogic.typeS);
@@ -162,7 +161,7 @@
fun make_casedist_prem T (cname, cargs) =
let
- val Ts = map (typ_of_dtyp descr sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) 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)
@@ -173,7 +172,7 @@
end;
val SOME (_, _, constrs) = AList.lookup (op =) descr index;
- val T = List.nth (get_rec_types descr sorts, index);
+ val T = List.nth (Datatype_Aux.get_rec_types descr sorts, index);
val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
val r = Const (case_name, map fastype_of rs ---> T --> rT);
@@ -218,7 +217,7 @@
if ! Proofterm.proofs < 2 then thy
else
let
- val _ = message config "Adding realizers for induction and case analysis ..."
+ val _ = Datatype_Aux.message config "Adding realizers for induction and case analysis ...";
val infos = map (Datatype.the_info thy) names;
val info :: _ = infos;
in
--- a/src/HOL/Tools/Function/size.ML Thu Dec 30 22:34:53 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML Thu Dec 30 23:42:06 2010 +0100
@@ -42,7 +42,7 @@
NONE => Abs ("x", T, HOLogic.zero)
| SOME t => t);
-fun is_poly thy (DtType (name, dts)) =
+fun is_poly thy (Datatype_Aux.DtType (name, dts)) =
(case Datatype.get_info thy name of
NONE => false
| SOME _ => exists (is_poly thy) dts)