--- a/src/HOL/Tools/Datatype/datatype.ML Mon Oct 12 12:19:19 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Mon Oct 12 14:22:54 2009 +0200
@@ -321,7 +321,7 @@
split_asm = split_asm});
fun derive_datatype_props config dt_names alt_names descr sorts
- induct inject (distinct_rules, distinct_rewrites, distinct_entry) thy1 =
+ induct inject distinct thy1 =
let
val thy2 = thy1 |> Theory.checkpoint;
val flat_descr = flat descr;
@@ -334,7 +334,7 @@
descr sorts exhaust thy3;
val ((rec_names, rec_rewrites), thy5) = DatatypeAbsProofs.prove_primrec_thms
config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4))
- inject distinct_rewrites (Simplifier.theory_context thy4 dist_ss) induct thy4;
+ inject distinct (Simplifier.theory_context thy4 dist_ss) induct thy4;
val ((case_rewrites, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
config new_type_names descr sorts rec_names rec_rewrites thy5;
val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
@@ -342,15 +342,15 @@
val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
descr sorts thy7;
val (splits, thy9) = DatatypeAbsProofs.prove_split_thms
- config new_type_names descr sorts inject distinct_rewrites exhaust case_rewrites thy8;
+ config new_type_names descr sorts inject distinct exhaust case_rewrites thy8;
val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
val dt_infos = map_index (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
- (hd descr ~~ inject ~~ distinct_entry ~~ exhaust ~~ nchotomys ~~
+ (hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~
case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
val dt_names = map fst dt_infos;
val prfx = Binding.qualify true (space_implode "_" new_type_names);
- val simps = flat (inject @ distinct_rules @ case_rewrites) @ rec_rewrites;
+ val simps = flat (inject @ distinct @ case_rewrites) @ rec_rewrites;
val named_rules = flat (map_index (fn (index, tname) =>
[((Binding.empty, [nth inducts index]), [Induct.induct_type tname]),
((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
@@ -362,11 +362,11 @@
|> PureThy.add_thmss ([((prfx (Binding.name "simps"), simps), []),
((prfx (Binding.name "inducts"), inducts), []),
((prfx (Binding.name "splits"), maps (fn (x, y) => [x, y]) splits), []),
- ((Binding.empty, flat case_rewrites @ flat distinct_rules @ rec_rewrites),
+ ((Binding.empty, flat case_rewrites @ flat distinct @ rec_rewrites),
[Simplifier.simp_add]),
((Binding.empty, rec_rewrites), [Code.add_default_eqn_attribute]),
((Binding.empty, flat inject), [iff_add]),
- ((Binding.empty, map (fn th => th RS notE) (flat distinct_rules)),
+ ((Binding.empty, map (fn th => th RS notE) (flat distinct)),
[Classical.safe_elim NONE]),
((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)])]
@ named_rules @ unnamed_rules)
@@ -394,7 +394,7 @@
in
thy2
|> derive_datatype_props config dt_names alt_names [descr] sorts
- induct inject (distinct, distinct, distinct)
+ induct inject distinct
end;
fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
@@ -531,12 +531,12 @@
else raise exn;
val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
- val ((inject, (distinct_rules, distinct_rewrites, distinct_entry), induct), thy') = thy |>
+ val ((inject, distinct, induct), thy') = thy |>
DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
types_syntax constr_syntax (mk_case_names_induct (flat descr));
in
derive_datatype_props config dt_names (SOME new_type_names) descr sorts
- induct inject (distinct_rules, distinct_rewrites, distinct_entry) thy'
+ induct inject distinct thy'
end;
val add_datatype = gen_add_datatype cert_typ;
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Oct 12 12:19:19 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Oct 12 14:22:54 2009 +0200
@@ -65,8 +65,8 @@
val insts = Library.take (i, dummyPs) @ (P::(Library.drop (i + 1, dummyPs)));
val cert = cterm_of thy;
val insts' = (map cert induct_Ps) ~~ (map cert insts);
- val induct' = refl RS ((List.nth
- (split_conj_thm (cterm_instantiate insts' induct), i)) RSN (2, rev_mp))
+ val induct' = refl RS ((nth
+ (split_conj_thm (cterm_instantiate insts' induct)) i) RSN (2, rev_mp))
in
SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
@@ -123,17 +123,17 @@
(* introduction rules for graph of primrec function *)
- fun make_rec_intr T rec_set ((rec_intr_ts, l), (cname, cargs)) =
+ 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 free2 = mk_Free "y" (Us ---> List.nth (rec_result_Ts, m)) k;
+ val free2 = 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, List.nth (rec_sets', m) $
+ (map (pair "x") Us, nth rec_sets' m $
app_bnds free1 i $ app_bnds free2 i)) :: prems,
free1::t1s, free2::t2s)
end
@@ -145,12 +145,12 @@
in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop
(rec_set $ list_comb (Const (cname, Ts ---> T), t1s) $
- list_comb (List.nth (rec_fns, l), t1s @ t2s)))], l + 1)
+ list_comb (nth rec_fns l, t1s @ t2s)))], l + 1)
end;
- val (rec_intr_ts, _) = Library.foldl (fn (x, ((d, T), set_name)) =>
- Library.foldl (make_rec_intr T set_name) (x, #3 (snd d)))
- (([], 0), descr' ~~ recTs ~~ rec_sets');
+ val (rec_intr_ts, _) = fold (fn ((d, T), set_name) =>
+ fold (make_rec_intr T set_name) (#3 (snd d)))
+ (descr' ~~ recTs ~~ rec_sets') ([], 0);
val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
Inductive.add_inductive_global (serial_string ())
@@ -165,18 +165,18 @@
val _ = message config "Proving termination and uniqueness of primrec functions ...";
- fun mk_unique_tac ((tac, intrs), ((((i, (tname, _, constrs)), elim), T), T')) =
+ fun mk_unique_tac ((((i, (tname, _, constrs)), elim), T), T') (tac, intrs) =
let
val distinct_tac =
(if i < length newTs then
- full_simp_tac (HOL_ss addsimps (List.nth (dist_rewrites, i))) 1
+ full_simp_tac (HOL_ss addsimps (nth dist_rewrites i)) 1
else full_simp_tac dist_ss 1);
val inject = map (fn r => r RS iffD1)
- (if i < length newTs then List.nth (constr_inject, i)
+ (if i < length newTs then nth constr_inject i
else injects_of tname);
- fun mk_unique_constr_tac n ((tac, intr::intrs, j), (cname, cargs)) =
+ fun mk_unique_constr_tac n (cname, cargs) (tac, intr::intrs, j) =
let
val k = length (filter is_rec_type cargs)
@@ -195,8 +195,8 @@
intrs, j + 1)
end;
- val (tac', intrs', _) = Library.foldl (mk_unique_constr_tac (length constrs))
- ((tac, intrs, 0), constrs);
+ val (tac', intrs', _) = fold (mk_unique_constr_tac (length constrs))
+ constrs (tac, intrs, 0);
in (tac', intrs') end;
@@ -211,10 +211,9 @@
((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
val induct' = cterm_instantiate ((map cert induct_Ps) ~~
(map cert insts)) induct;
- val (tac, _) = Library.foldl mk_unique_tac
- (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
- THEN rewrite_goals_tac [mk_meta_eq choice_eq], rec_intrs),
- descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
+ val (tac, _) = fold mk_unique_tac (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
+ (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
+ THEN rewrite_goals_tac [mk_meta_eq choice_eq], rec_intrs));
in split_conj_thm (SkipProof.prove_global thy1 [] []
(HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))
@@ -267,7 +266,7 @@
[Nitpick_Const_Simps.add])]
||> Sign.parent_path
||> Theory.checkpoint
- |-> (fn thms => pair (reccomb_names, Library.flat thms))
+ |-> (fn thms => pair (reccomb_names, flat thms))
end;
@@ -298,10 +297,9 @@
(* define case combinators via primrec combinators *)
- val (case_defs, thy2) = Library.foldl (fn ((defs, thy),
- ((((i, (_, _, constrs)), T), name), recname)) =>
+ val (case_defs, thy2) = fold (fn ((((i, (_, _, constrs)), T), name), recname) => fn (defs, thy) =>
let
- val (fns1, fns2) = ListPair.unzip (map (fn ((_, cargs), j) =>
+ 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 (List.filter is_rec_type cargs);
@@ -328,8 +326,8 @@
|> (PureThy.add_defs false o map Thm.no_attributes) [def];
in (defs @ [def_thm], thy')
- end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
- (Library.take (length newTs, reccomb_names)))
+ end) (hd descr ~~ newTs ~~ case_names ~~
+ Library.take (length newTs, reccomb_names)) ([], thy1)
||> Theory.checkpoint;
val case_thms = map (map (fn t => SkipProof.prove_global thy2 [] [] t