--- a/src/HOL/Nitpick.thy Mon Feb 17 18:18:27 2014 +0100
+++ b/src/HOL/Nitpick.thy Mon Feb 17 22:54:38 2014 +0100
@@ -9,7 +9,9 @@
theory Nitpick
imports BNF_FP_Base Map Record Sledgehammer
-keywords "nitpick" :: diag and "nitpick_params" :: thy_decl
+keywords
+ "nitpick" :: diag and
+ "nitpick_params" :: thy_decl
begin
typedecl bisim_iterator
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Feb 17 18:18:27 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Feb 17 22:54:38 2014 +0100
@@ -10,22 +10,21 @@
type fp_sugar =
{T: typ,
fp: BNF_FP_Util.fp_kind,
- index: int,
- pre_bnfs: BNF_Def.bnf list,
+ fp_res_index: int,
+ fp_res: BNF_FP_Util.fp_result,
+ pre_bnf: BNF_Def.bnf,
nested_bnfs: BNF_Def.bnf list,
nesting_bnfs: BNF_Def.bnf list,
- fp_res: BNF_FP_Util.fp_result,
- ctr_defss: thm list list,
- ctr_sugars: Ctr_Sugar.ctr_sugar list,
- co_iterss: term list list,
- mapss: thm list list,
+ ctr_defs: thm list,
+ ctr_sugar: Ctr_Sugar.ctr_sugar,
+ co_iters: term list,
+ maps: thm list,
+ common_co_inducts: thm list,
co_inducts: thm list,
- co_inductss: thm list list,
- co_iter_thmsss: thm list list list,
- disc_co_itersss: thm list list list,
- sel_co_iterssss: thm list list list list};
+ co_iter_thmss: thm list list,
+ disc_co_iterss: thm list list,
+ sel_co_itersss: thm list list list};
- val of_fp_sugar: (fp_sugar -> 'a list) -> fp_sugar -> 'a
val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar
val fp_sugar_of: Proof.context -> string -> fp_sugar option
@@ -122,38 +121,40 @@
type fp_sugar =
{T: typ,
fp: fp_kind,
- index: int,
- pre_bnfs: bnf list,
+ fp_res_index: int,
+ fp_res: fp_result,
+ pre_bnf: bnf,
nested_bnfs: bnf list,
nesting_bnfs: bnf list,
- fp_res: fp_result,
- ctr_defss: thm list list,
- ctr_sugars: ctr_sugar list,
- co_iterss: term list list,
- mapss: thm list list,
+ ctr_defs: thm list,
+ ctr_sugar: Ctr_Sugar.ctr_sugar,
+ co_iters: term list,
+ maps: thm list,
+ common_co_inducts: thm list,
co_inducts: thm list,
- co_inductss: thm list list,
- co_iter_thmsss: thm list list list,
- disc_co_itersss: thm list list list,
- sel_co_iterssss: thm list list list list};
-
-fun of_fp_sugar f (fp_sugar as ({index, ...}: fp_sugar)) = nth (f fp_sugar) index;
+ co_iter_thmss: thm list list,
+ disc_co_iterss: thm list list,
+ sel_co_itersss: thm list list list};
-fun morph_fp_sugar phi ({T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
- ctr_sugars, co_iterss, mapss, co_inducts, co_inductss, co_iter_thmsss, disc_co_itersss,
- sel_co_iterssss} : fp_sugar) =
- {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
- nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
+fun morph_fp_sugar phi ({T, fp, fp_res, fp_res_index, pre_bnf, nested_bnfs, nesting_bnfs, ctr_defs,
+ ctr_sugar, co_iters, maps, common_co_inducts, co_inducts, co_iter_thmss, disc_co_iterss,
+ sel_co_itersss} : fp_sugar) =
+ {T = Morphism.typ phi T,
+ fp = fp,
fp_res = morph_fp_result phi fp_res,
- ctr_defss = map (map (Morphism.thm phi)) ctr_defss,
- ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars,
- co_iterss = map (map (Morphism.term phi)) co_iterss,
- mapss = map (map (Morphism.thm phi)) mapss,
+ fp_res_index = fp_res_index,
+ pre_bnf = morph_bnf phi pre_bnf,
+ nested_bnfs = map (morph_bnf phi) nested_bnfs,
+ nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
+ ctr_defs = map (Morphism.thm phi) ctr_defs,
+ ctr_sugar = morph_ctr_sugar phi ctr_sugar,
+ co_iters = map (Morphism.term phi) co_iters,
+ maps = map (Morphism.thm phi) maps,
+ common_co_inducts = map (Morphism.thm phi) common_co_inducts,
co_inducts = map (Morphism.thm phi) co_inducts,
- co_inductss = map (map (Morphism.thm phi)) co_inductss,
- co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss,
- disc_co_itersss = map (map (map (Morphism.thm phi))) disc_co_itersss,
- sel_co_iterssss = map (map (map (map (Morphism.thm phi)))) sel_co_iterssss};
+ co_iter_thmss = map (map (Morphism.thm phi)) co_iter_thmss,
+ disc_co_iterss = map (map (Morphism.thm phi)) disc_co_iterss,
+ sel_co_itersss = map (map (map (Morphism.thm phi))) sel_co_itersss};
val transfer_fp_sugar =
morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
@@ -183,15 +184,16 @@
(fn phi => Data.map (Symtab.update (key, morph_fp_sugar phi fp_sugar)));
fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss
- ctr_sugars co_iterss mapss co_inducts co_inductss co_iter_thmsss disc_co_itersss
+ ctr_sugars co_iterss mapss common_co_inducts co_inductss co_iter_thmsss disc_co_itersss
sel_co_iterssss lthy =
(0, lthy)
|> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
- register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
- nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
- ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
- co_inductss = co_inductss, co_iter_thmsss = co_iter_thmsss,
- disc_co_itersss = disc_co_itersss, sel_co_iterssss = sel_co_iterssss}
+ register_fp_sugar s {T = T, fp = fp, fp_res = fp_res, fp_res_index = kk,
+ pre_bnf = nth pre_bnfs kk, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs,
+ ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk, co_iters = nth co_iterss kk,
+ maps = nth mapss kk, common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk,
+ co_iter_thmss = nth co_iter_thmsss kk, disc_co_iterss = nth disc_co_itersss kk,
+ sel_co_itersss = nth sel_co_iterssss kk}
lthy)) Ts
|> snd;
@@ -1407,8 +1409,8 @@
|> Spec_Rules.add Spec_Rules.Equational (map co_rec_of iterss, flat rec_thmss)
|> Local_Theory.notes (common_notes @ notes) |> snd
|> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars
- iterss mapss [induct_thm] (transpose [induct_thms]) (transpose [fold_thmss, rec_thmss])
- [] []
+ iterss mapss [induct_thm] (map single induct_thms) (transpose [fold_thmss, rec_thmss])
+ (replicate nn []) (replicate nn [])
end;
fun derive_note_coinduct_coiters_thms_for_types
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Feb 17 18:18:27 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Feb 17 22:54:38 2014 +0100
@@ -47,7 +47,8 @@
fun construct_mutualized_fp fp fpTs fp_sugars bs resBs (resDs, Dss) bnfs lthy =
let
- fun steal get = map (of_fp_sugar (get o #fp_res)) fp_sugars;
+ fun steal_fp_res get =
+ map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars;
val n = length bnfs;
val deads = fold (union (op =)) Dss resDs;
@@ -77,8 +78,8 @@
val ((ctors, dtors), (xtor's, xtors)) =
let
- val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (steal #ctors);
- val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (steal #dtors);
+ val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (steal_fp_res #ctors);
+ val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (steal_fp_res #dtors);
in
((ctors, dtors), `(map (Term.subst_atomic_types theta)) (fp_case fp ctors dtors))
end;
@@ -92,9 +93,8 @@
||>> mk_Frees "x" xTs
||>> mk_Frees "y" yTs;
- val fp_bnfs = steal #bnfs;
- val pre_bnfs = map (of_fp_sugar #pre_bnfs) fp_sugars;
- val pre_bnfss = map #pre_bnfs fp_sugars;
+ val fp_bnfs = steal_fp_res #bnfs;
+ val pre_bnfs = map #pre_bnf fp_sugars;
val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
val fp_nesty_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_nesty_bnfss);
@@ -126,9 +126,9 @@
val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;
- val rel_unfoldss = map (maps (fn bnf => no_refl [rel_def_of_bnf bnf])) pre_bnfss;
- val rel_xtor_co_inducts = steal (split_conj_thm o #rel_xtor_co_induct_thm)
- |> map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) rel_unfoldss;
+ val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) pre_bnfs;
+ val rel_xtor_co_inducts = steal_fp_res (split_conj_thm o #rel_xtor_co_induct_thm)
+ |> map (unfold_thms lthy (id_apply :: rel_unfolds));
val rel_defs = map rel_def_of_bnf bnfs;
val rel_monos = map rel_mono_of_bnf bnfs;
@@ -185,11 +185,13 @@
|> mk_Frees' "s" fold_strTs
||>> mk_Frees' "s" rec_strTs;
- val co_iters = steal #xtor_co_iterss;
- val ns = map (length o #pre_bnfs) fp_sugars;
+ val co_iters = steal_fp_res #xtor_co_iterss;
+ val ns = map (length o #Ts o #fp_res) fp_sugars;
+
fun substT rho (Type (@{type_name "fun"}, [T, U])) = substT rho T --> substT rho U
| substT rho (Type (s, Ts)) = Type (s, map (typ_subst_nonatomic rho) Ts)
| substT _ T = T;
+
fun force_iter is_rec i TU TU_rec raw_iters =
let
val approx_fold = un_fold_of raw_iters
@@ -325,14 +327,14 @@
val pre_map_defs = no_refl (map map_def_of_bnf bnfs);
val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs);
- val map_unfoldss = map (maps (fn bnf => no_refl [map_def_of_bnf bnf])) pre_bnfss;
- val unfold_map = map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) map_unfoldss;
+ val map_unfolds = maps (fn bnf => no_refl [map_def_of_bnf bnf]) pre_bnfs;
+ val unfold_map = map (unfold_thms lthy (id_apply :: map_unfolds));
- val fp_xtor_co_iterss = steal #xtor_co_iter_thmss;
+ val fp_xtor_co_iterss = steal_fp_res #xtor_co_iter_thmss;
val fp_xtor_un_folds = map (mk_pointfree lthy o un_fold_of) fp_xtor_co_iterss |> unfold_map;
val fp_xtor_co_recs = map (mk_pointfree lthy o co_rec_of) fp_xtor_co_iterss |> unfold_map;
- val fp_co_iter_o_mapss = steal #xtor_co_iter_o_map_thmss;
+ val fp_co_iter_o_mapss = steal_fp_res #xtor_co_iter_o_map_thmss;
val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss |> unfold_map;
val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss |> unfold_map;
val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} :: @{thms id_apply
@@ -358,20 +360,21 @@
used by "primrec", "primcorecursive", and "datatype_compat". *)
val fp_res =
({Ts = fpTs,
- bnfs = steal #bnfs,
+ bnfs = steal_fp_res #bnfs,
dtors = dtors,
ctors = ctors,
xtor_co_iterss = transpose [un_folds, co_recs],
xtor_co_induct = xtor_co_induct_thm,
- dtor_ctors = steal #dtor_ctors (*too general types*),
- ctor_dtors = steal #ctor_dtors (*too general types*),
- ctor_injects = steal #ctor_injects (*too general types*),
- dtor_injects = steal #dtor_injects (*too general types*),
- xtor_map_thms = steal #xtor_map_thms (*too general types and terms*),
- xtor_set_thmss = steal #xtor_set_thmss (*too general types and terms*),
- xtor_rel_thms = steal #xtor_rel_thms (*too general types and terms*),
+ dtor_ctors = steal_fp_res #dtor_ctors (*too general types*),
+ ctor_dtors = steal_fp_res #ctor_dtors (*too general types*),
+ ctor_injects = steal_fp_res #ctor_injects (*too general types*),
+ dtor_injects = steal_fp_res #dtor_injects (*too general types*),
+ xtor_map_thms = steal_fp_res #xtor_map_thms (*too general types and terms*),
+ xtor_set_thmss = steal_fp_res #xtor_set_thmss (*too general types and terms*),
+ xtor_rel_thms = steal_fp_res #xtor_rel_thms (*too general types and terms*),
xtor_co_iter_thmss = transpose [xtor_un_fold_thms, xtor_co_rec_thms],
- xtor_co_iter_o_map_thmss = steal #xtor_co_iter_o_map_thmss (*theorem about old constant*),
+ xtor_co_iter_o_map_thmss = steal_fp_res #xtor_co_iter_o_map_thmss
+ (*theorem about old constant*),
rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
|> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
in
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Feb 17 18:18:27 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Feb 17 22:54:38 2014 +0100
@@ -119,17 +119,18 @@
val fp_b_names = map base_name_of_typ fpTs;
val nn = length fpTs;
+ val kks = 0 upto nn - 1;
- fun target_ctr_sugar_of_fp_sugar fpT ({T, index, ctr_sugars, ...} : fp_sugar) =
+ fun target_ctr_sugar_of_fp_sugar fpT ({T, ctr_sugar, ...} : fp_sugar) =
let
val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) [];
val phi = Morphism.term_morphism "BNF" (Term.subst_TVars rho);
in
- morph_ctr_sugar phi (nth ctr_sugars index)
+ morph_ctr_sugar phi ctr_sugar
end;
- val ctr_defss = map (of_fp_sugar #ctr_defss) fp_sugars0;
- val mapss = map (of_fp_sugar #mapss) fp_sugars0;
+ val ctr_defss = map #ctr_defs fp_sugars0;
+ val mapss = map #maps fp_sugars0;
val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
val ctrss = map #ctrs ctr_sugars;
@@ -215,14 +216,15 @@
(mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
|>> split_list;
- val ((co_inducts, co_inductss, un_fold_thmss, co_rec_thmss, disc_unfold_thmss,
+ val ((common_co_inducts, co_inductss, un_fold_thmss, co_rec_thmss, disc_unfold_thmss,
disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
if fp = Least_FP then
derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
co_iterss co_iter_defss lthy
|> `(fn ((inducts, induct, _), (fold_thmss, rec_thmss, _)) =>
- ([induct], [inducts], fold_thmss, rec_thmss, [], [], [], []))
+ ([induct], [inducts], fold_thmss, rec_thmss, replicate nn [],
+ replicate nn [], replicate nn [], replicate nn []))
||> (fn info => (SOME info, NONE))
else
derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
@@ -232,32 +234,38 @@
|> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
(disc_unfold_thmss, disc_corec_thmss, _), _,
(sel_unfold_thmsss, sel_corec_thmsss, _)) =>
- (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, unfold_thmss, corec_thmss,
- disc_unfold_thmss, disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss))
+ (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, unfold_thmss,
+ corec_thmss, disc_unfold_thmss, disc_corec_thmss, sel_unfold_thmsss,
+ sel_corec_thmsss))
||> (fn info => (NONE, SOME info));
val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
- fun mk_target_fp_sugar (kk, T) =
- {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
- nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
- ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
- co_inductss = transpose co_inductss,
- co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss],
- disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss],
- sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}
+ fun mk_target_fp_sugar T kk pre_bnf ctr_defs ctr_sugar co_iters maps co_inducts un_fold_thms
+ co_rec_thms disc_unfold_thms disc_corec_thms sel_unfold_thmss sel_corec_thmss =
+ {T = T, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf,
+ nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, ctr_defs = ctr_defs,
+ ctr_sugar = ctr_sugar, co_iters = co_iters, maps = maps,
+ common_co_inducts = common_co_inducts, co_inducts = co_inducts,
+ co_iter_thmss = [un_fold_thms, co_rec_thms],
+ disc_co_iterss = [disc_unfold_thms, disc_corec_thms],
+ sel_co_itersss = [sel_unfold_thmss, sel_corec_thmss]}
|> morph_fp_sugar phi;
- val n2m_sugar = (map_index mk_target_fp_sugar fpTs, fp_sugar_thms);
+ val target_fp_sugars =
+ map14 mk_target_fp_sugar fpTs kks pre_bnfs ctr_defss ctr_sugars co_iterss mapss
+ (transpose co_inductss) un_fold_thmss co_rec_thmss disc_unfold_thmss disc_corec_thmss
+ sel_unfold_thmsss sel_corec_thmsss;
+
+ val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
in
(n2m_sugar, lthy |> register_n2m_sugar key n2m_sugar)
end)
end;
(* TODO: needed? *)
-fun indexify_callsss fp_sugar callsss =
+fun indexify_callsss (fp_sugar as {ctr_sugar = {ctrs, ...}, ...} : fp_sugar) callsss =
let
- val {ctrs, ...} = of_fp_sugar #ctr_sugars fp_sugar;
fun indexify_ctr ctr =
(case AList.lookup Term.aconv_untyped callsss ctr of
NONE => replicate (num_binder_types (fastype_of ctr)) []
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Feb 17 18:18:27 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Feb 17 22:54:38 2014 +0100
@@ -367,9 +367,7 @@
| _ => not_codatatype ctxt res_T);
fun map_thms_of_typ ctxt (Type (s, _)) =
- (case fp_sugar_of ctxt s of
- SOME {index, mapss, ...} => nth mapss index
- | NONE => [])
+ (case fp_sugar_of ctxt s of SOME {maps, ...} => maps | NONE => [])
| map_thms_of_typ _ _ = [];
fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 =
@@ -378,15 +376,15 @@
val ((missing_res_Ts, perm0_kks,
fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
- co_inducts = coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
+ common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
nested_to_mutual_fps Greatest_FP bs res_Ts get_indices callssss0 lthy0;
- val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
+ val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars;
- val indices = map #index fp_sugars;
- val perm_indices = map #index perm_fp_sugars;
+ val indices = map #fp_res_index fp_sugars;
+ val perm_indices = map #fp_res_index perm_fp_sugars;
- val perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars;
+ val perm_ctrss = map (#ctrs o #ctr_sugar) perm_fp_sugars;
val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
val perm_gfpTs = map (body_type o fastype_of o hd) perm_ctrss;
@@ -395,8 +393,8 @@
val kks = 0 upto nn - 1;
val perm_ns = map length perm_ctr_Tsss;
- val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o
- of_fp_sugar (#xtor_co_iterss o #fp_res)) perm_fp_sugars;
+ val perm_Cs = map (fn {fp_res, fp_res_index, ...} => domain_type (body_fun_type (fastype_of
+ (co_rec_of (nth (#xtor_co_iterss fp_res) fp_res_index))))) perm_fp_sugars;
val (perm_p_Tss, (perm_q_Tssss, _, perm_f_Tssss, _)) =
mk_coiter_fun_arg_types perm_ctr_Tsss perm_Cs perm_ns (co_rec_of dtor_coiters1);
@@ -410,7 +408,7 @@
fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs;
fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs;
- val coinduct_thmss = map (unpermute0 o conj_dests nn) coinduct_thms;
+ val coinduct_thmss = map (unpermute0 o conj_dests nn) common_coinduct_thms;
val p_iss = map (map (find_index_eq fun_arg_hs)) (unpermute perm_p_hss);
val q_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_q_hssss);
@@ -444,35 +442,32 @@
disc_corec = disc_corec, sel_corecs = sel_corecs}
end;
- fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss
- sel_coiterssss =
+ fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...}
+ : ctr_sugar) p_is q_isss f_isss f_Tsss coiter_thmss disc_coiterss sel_coitersss =
let
- val {ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...} : ctr_sugar =
- nth ctr_sugars index;
val p_ios = map SOME p_is @ [NONE];
- val discIs = #discIs (nth ctr_sugars index);
- val corec_thms = co_rec_of (nth coiter_thmsss index);
- val disc_corecs = co_rec_of (nth disc_coitersss index);
- val sel_corecss = co_rec_of (nth sel_coiterssss index);
+ val corec_thms = co_rec_of coiter_thmss;
+ val disc_corecs = co_rec_of disc_coiterss;
+ val sel_corecss = co_rec_of sel_coitersss;
in
map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss
disc_excludesss collapses corec_thms disc_corecs sel_corecss
end;
- fun mk_spec ({T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss,
- disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...} : fp_sugar)
- p_is q_isss f_isss f_Tsss =
- {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)),
- disc_exhausts = #disc_exhausts (nth ctr_sugars index),
+ fun mk_spec ({T, ctr_sugar as {disc_exhausts, ...}, co_iters = coiters,
+ co_iter_thmss = coiter_thmss, disc_co_iterss = disc_coiterss,
+ sel_co_itersss = sel_coitersss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
+ {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of coiters),
+ disc_exhausts = disc_exhausts,
nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs,
nested_map_comps = map map_comp_of_bnf nested_bnfs,
- ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss
- disc_coitersss sel_coiterssss};
+ ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss coiter_thmss disc_coiterss
+ sel_coitersss};
in
((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
- co_induct_of coinduct_thms, strong_co_induct_of coinduct_thms, co_induct_of coinduct_thmss,
- strong_co_induct_of coinduct_thmss), lthy)
+ co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms,
+ co_induct_of coinduct_thmss, strong_co_induct_of coinduct_thmss), lthy)
end;
val undef_const = Const (@{const_name undefined}, dummyT);
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Feb 17 18:18:27 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Feb 17 22:54:38 2014 +0100
@@ -2,7 +2,7 @@
Author: Jasmin Blanchette, TU Muenchen
Copyright 2013
-Compatibility layer with the old datatype package.
+Compatibility layer with the old datatype package ("datatype_compat").
*)
signature BNF_LFP_COMPAT =
@@ -32,7 +32,7 @@
fun not_mutually_recursive ss =
error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes");
- val (fpT_names as fpT_name1 :: _) =
+ val fpT_names =
map (fst o dest_Type o Proof_Context.read_type_name_proper lthy false) raw_fpT_names;
fun lfp_sugar_of s =
@@ -40,7 +40,7 @@
SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
| _ => not_datatype s);
- val {ctr_sugars = fp_ctr_sugars, ...} = lfp_sugar_of fpT_name1;
+ val fp_ctr_sugars = map (#ctr_sugar o lfp_sugar_of) fpT_names;
val fpTs0 as Type (_, var_As) :: _ = map (body_type o fastype_of o hd o #ctrs) fp_ctr_sugars;
val fpT_names' = map (fst o dest_Type) fpTs0;
@@ -52,7 +52,7 @@
fun nested_Tparentss_indicessss_of parent_Tkks (T as Type (s, _)) kk =
(case try lfp_sugar_of s of
- SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ctr_sugars, ...}) =>
+ SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ...}) =>
let
val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T0, T) Vartab.empty) [];
val substT = Term.typ_subst_TVars rho;
@@ -88,7 +88,7 @@
#>> pair parent_Tkks'
end;
- val ctrss = map #ctrs ctr_sugars;
+ val ctrss = map (#ctrs o #ctr_sugar o lfp_sugar_of o fst o dest_Type) mutual_Ts;
val ctr_Tsss = map (map (binder_types o substT o fastype_of)) ctrss;
in
([], kk + mutual_nn)
@@ -107,7 +107,7 @@
val kkssss = map snd Tparentss_kkssss;
val fp_sugars0 = map (lfp_sugar_of o fst o dest_Type) Ts;
- val ctrss0 = map (#ctrs o of_fp_sugar #ctr_sugars) fp_sugars0;
+ val ctrss0 = map (#ctrs o #ctr_sugar) fp_sugars0;
val ctr_Tsss0 = map (map (binder_types o fastype_of)) ctrss0;
fun apply_comps n kk =
@@ -132,9 +132,8 @@
else
((fp_sugars0, (NONE, NONE)), lthy);
- val {ctr_sugars, co_inducts = [induct], co_inductss = inductss, co_iterss,
- co_iter_thmsss = iter_thmsss, ...} :: _ = fp_sugars;
- val inducts = map the_single inductss;
+ val {co_inducts = [induct], ...} :: _ = fp_sugars;
+ val inducts = map (the_single o #co_inducts) fp_sugars;
fun mk_dtyp [] (TFree a) = Datatype_Aux.DtTFree a
| mk_dtyp [] (Type (s, Ts)) = Datatype_Aux.DtType (s, map (mk_dtyp []) Ts)
@@ -148,23 +147,19 @@
(kk, (T_name, map (mk_dtyp (map snd (take 1 parents))) Ts, map2 (mk_ctr_descr Ts) kksss ctrs0));
val descr = map3 mk_typ_descr kkssss Tparentss ctrss0;
- val recs = map (fst o dest_Const o co_rec_of) co_iterss;
- val rec_thms = flat (map co_rec_of iter_thmsss);
+ val recs = map (fst o dest_Const o co_rec_of o #co_iters) fp_sugars;
+ val rec_thms = maps (co_rec_of o #co_iter_thmss) fp_sugars;
- fun mk_info ({T = Type (T_name0, _), index, ...} : fp_sugar) =
- let
- val {casex, exhaust, nchotomy, injects, distincts, case_thms, case_cong, weak_case_cong,
- split, split_asm, ...} = nth ctr_sugars index;
- in
- (T_name0,
- {index = index, descr = descr, inject = injects, distinct = distincts, induct = induct,
- inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
- rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
- case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,
- split_asm = split_asm})
- end;
+ fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar as {casex, exhaust, nchotomy, injects,
+ distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) =
+ (T_name0,
+ {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct,
+ inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
+ rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
+ case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,
+ split_asm = split_asm});
- val infos = map mk_info (take nn_fp fp_sugars);
+ val infos = map_index mk_info (take nn_fp fp_sugars);
val all_notes =
(case lfp_sugar_thms of
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Feb 17 18:18:27 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Feb 17 22:54:38 2014 +0100
@@ -136,20 +136,17 @@
type basic_lfp_sugar =
{T: typ,
- index: int,
- ctor_iterss: term list list,
- ctr_defss: thm list list,
- ctr_sugars: Ctr_Sugar.ctr_sugar list,
- iterss: term list list,
- iter_thmsss: thm list list list};
+ fp_res_index: int,
+ ctor_iters: term list,
+ ctr_defs: thm list,
+ ctr_sugar: ctr_sugar,
+ iters: term list,
+ iter_thmss: thm list list};
-fun basic_lfp_sugar_of ({T, index, fp_res = {xtor_co_iterss = ctor_iterss, ...}, ctr_defss,
- ctr_sugars, co_iterss = iterss, co_iter_thmsss = iter_thmsss, ...} : fp_sugar) =
- {T = T, index = index, ctor_iterss = ctor_iterss, ctr_defss = ctr_defss,
- ctr_sugars = ctr_sugars, iterss = iterss, iter_thmsss = iter_thmsss};
-
-fun of_basic_lfp_sugar f (basic_lfp_sugar as ({index, ...} : basic_lfp_sugar)) =
- nth (f basic_lfp_sugar) index;
+fun basic_lfp_sugar_of ({T, fp_res = {xtor_co_iterss = ctor_iterss, ...}, fp_res_index, ctr_defs,
+ ctr_sugar, co_iters = iters, co_iter_thmss = iter_thmss, ...} : fp_sugar) =
+ {T = T, fp_res_index = fp_res_index, ctor_iters = nth ctor_iterss fp_res_index,
+ ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, iters = iters, iter_thmss = iter_thmss};
fun get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0 =
let
@@ -172,23 +169,24 @@
ctor_iters1, induct_thm, lfp_sugar_thms, lthy) =
get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0;
- val perm_basic_lfp_sugars = sort (int_ord o pairself #index) basic_lfp_sugars;
+ val perm_basic_lfp_sugars = sort (int_ord o pairself #fp_res_index) basic_lfp_sugars;
- val indices = map #index basic_lfp_sugars;
- val perm_indices = map #index perm_basic_lfp_sugars;
+ val indices = map #fp_res_index basic_lfp_sugars;
+ val perm_indices = map #fp_res_index perm_basic_lfp_sugars;
- val perm_ctrss = map (#ctrs o of_basic_lfp_sugar #ctr_sugars) perm_basic_lfp_sugars;
+ val perm_ctrss = map (#ctrs o #ctr_sugar) perm_basic_lfp_sugars;
val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
- val perm_lfpTs = map (body_type o fastype_of o hd) perm_ctrss;
val nn0 = length arg_Ts;
- val nn = length perm_lfpTs;
+ val nn = length perm_ctrss;
val kks = 0 upto nn - 1;
+
val perm_ns = map length perm_ctr_Tsss;
val perm_mss = map (map length) perm_ctr_Tsss;
+ val perm_ctr_offsets = map (fn kk => Integer.sum (map length (take kk perm_ctrss))) kks;
- val perm_Cs = map (body_type o fastype_of o co_rec_of o of_basic_lfp_sugar #ctor_iterss)
- perm_basic_lfp_sugars;
+ val perm_lfpTs = map (body_type o fastype_of o hd) perm_ctrss;
+ val perm_Cs = map (body_type o fastype_of o co_rec_of o #ctor_iters) perm_basic_lfp_sugars;
val perm_fun_arg_Tssss =
mk_iter_fun_arg_types perm_ctr_Tsss perm_ns perm_mss (co_rec_of ctor_iters1);
@@ -199,6 +197,7 @@
val lfpTs = unpermute perm_lfpTs;
val Cs = unpermute perm_Cs;
+ val ctr_offsets = unpermute perm_ctr_offsets;
val As_rho = tvar_subst thy (take nn0 lfpTs) arg_Ts;
val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn res_Ts;
@@ -210,10 +209,6 @@
val perm_Cs' = map substCT perm_Cs;
- fun offset_of_ctr 0 _ = 0
- | offset_of_ctr n (({ctrs, ...} : ctr_sugar) :: ctr_sugars) =
- length ctrs + offset_of_ctr (n - 1) ctr_sugars;
-
fun call_of [i] [T] = (if exists_subtype_in Cs T then Nested_Rec else No_Rec) (i, substACT T)
| call_of [i, i'] [T, T'] = Mutual_Rec ((i, substACT T), (i', substACT T'));
@@ -227,22 +222,17 @@
rec_thm = rec_thm}
end;
- fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) iter_thmsss =
- let
- val ctrs = #ctrs (nth ctr_sugars index);
- val rec_thms = co_rec_of (nth iter_thmsss index);
- val k = offset_of_ctr index ctr_sugars;
- val n = length ctrs;
- in
- map4 mk_ctr_spec ctrs (k upto k + n - 1) (nth perm_fun_arg_Tssss index) rec_thms
- end;
+ fun mk_ctr_specs fp_res_index k ctrs rec_thms =
+ map4 mk_ctr_spec ctrs (k upto k + length ctrs - 1) (nth perm_fun_arg_Tssss fp_res_index)
+ rec_thms;
- fun mk_spec ({T, index, ctr_sugars, iterss, iter_thmsss, ...} : basic_lfp_sugar) =
- {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of (nth iterss index)),
+ fun mk_spec ctr_offset
+ ({T, fp_res_index, ctr_sugar = {ctrs, ...}, iters, iter_thmss, ...} : basic_lfp_sugar) =
+ {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of iters),
nested_map_idents = nested_map_idents, nested_map_comps = nested_map_comps,
- ctr_specs = mk_ctr_specs index ctr_sugars iter_thmsss};
+ ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs (co_rec_of iter_thmss)};
in
- ((is_some lfp_sugar_thms, map mk_spec basic_lfp_sugars, missing_arg_Ts, induct_thm,
+ ((is_some lfp_sugar_thms, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, induct_thm,
induct_thms), lthy)
end;
@@ -529,10 +519,11 @@
val actual_nn = length funs_data;
- val _ = let val ctrs = (maps (map #ctr o #ctr_specs) rec_specs) in
+ val ctrs = maps (map #ctr o #ctr_specs) rec_specs;
+ val _ =
map (fn {ctr, user_eqn, ...} => member (op =) ctrs ctr orelse
primrec_error_eqn ("argument " ^ quote (Syntax.string_of_term lthy ctr) ^
- " is not a constructor in left-hand side") user_eqn) eqns_data end;
+ " is not a constructor in left-hand side") user_eqn) eqns_data;
val defs = build_defs lthy bs mxs funs_data rec_specs has_call;
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Feb 17 18:18:27 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Feb 17 22:54:38 2014 +0100
@@ -1059,8 +1059,8 @@
(* Give the inner timeout a chance. *)
val timeout_bonus = seconds 1.0
-fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) mode i n
- step subst def_assm_ts nondef_assm_ts orig_t =
+fun pick_nits_in_term state (params as {timeout, expect, ...}) mode i n step
+ subst def_assm_ts nondef_assm_ts orig_t =
let
val print_nt = if is_mode_nt mode then Output.urgent_message else K ()
val print_t = if mode = TPTP then Output.urgent_message else K ()
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 17 18:18:27 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 17 22:54:38 2014 +0100
@@ -791,8 +791,7 @@
val ctrs2 =
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt co_s of
SOME (fp_sugar as {fp = BNF_FP_Util.Greatest_FP, ...}) =>
- map dest_Const
- (#ctrs (BNF_FP_Def_Sugar.of_fp_sugar #ctr_sugars fp_sugar))
+ map dest_Const (#ctrs (#ctr_sugar fp_sugar))
| _ => [])
in
exists (fn (s', T') => s = s' andalso repair_constr_type coT T' = T)
@@ -937,7 +936,7 @@
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt s of
SOME (fp_sugar as {fp = BNF_FP_Util.Greatest_FP, ...}) =>
map (apsnd (repair_constr_type T) o dest_Const)
- (#ctrs (BNF_FP_Def_Sugar.of_fp_sugar #ctr_sugars fp_sugar))
+ (#ctrs (#ctr_sugar fp_sugar))
| _ =>
if is_frac_type ctxt T then
case typedef_info ctxt s of
@@ -1465,12 +1464,12 @@
|> the |> #3 |> length))
(Datatype.get_all thy) [] @
map (apsnd length o snd) (#codatatypes (Data.get (Context.Proof ctxt))) @
- maps (fn {fp, ctr_sugars, ...} =>
- if fp = BNF_FP_Util.Greatest_FP then
- map (apsnd num_binder_types o dest_Const o #casex) ctr_sugars
- else
- [])
- (BNF_FP_Def_Sugar.fp_sugars_of ctxt)
+ map_filter (fn {fp, ctr_sugar = {casex, ...}, ...} =>
+ if fp = BNF_FP_Util.Greatest_FP then
+ SOME (apsnd num_binder_types (dest_Const casex))
+ else
+ NONE)
+ (BNF_FP_Def_Sugar.fp_sugars_of ctxt)
end
fun fixpoint_kind_of_const thy table x =
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Feb 17 18:18:27 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Feb 17 22:54:38 2014 +0100
@@ -31,7 +31,6 @@
val atom16_v1 = FreeName ("atom16_v1", dummy_T, Atom (16, 0))
val atom24_v1 = FreeName ("atom24_v1", dummy_T, Atom (24, 0))
val atom36_v1 = FreeName ("atom36_v1", dummy_T, Atom (36, 0))
-val atom81_v1 = FreeName ("atom81_v1", dummy_T, Atom (81, 0))
val struct_atom1_atom1_v1 =
FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Atom (1, 0), Atom (1, 0)])