--- a/src/HOL/ATP.thy Mon Sep 09 17:28:08 2013 +0200
+++ b/src/HOL/ATP.thy Mon Sep 09 20:24:15 2013 +0200
@@ -11,7 +11,6 @@
ML_file "Tools/lambda_lifting.ML"
ML_file "Tools/monomorph.ML"
-ML_file "Tools/legacy_monomorph.ML"
ML_file "Tools/ATP/atp_util.ML"
ML_file "Tools/ATP/atp_problem.ML"
ML_file "Tools/ATP/atp_proof.ML"
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Mon Sep 09 17:28:08 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Mon Sep 09 20:24:15 2013 +0200
@@ -23,7 +23,11 @@
split_asm: thm,
disc_thmss: thm list list,
discIs: thm list,
- sel_thmss: thm list list};
+ sel_thmss: thm list list,
+ disc_exhausts: thm list,
+ collapses: thm list,
+ expands: thm list,
+ case_convs: thm list};
val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
@@ -68,10 +72,15 @@
split_asm: thm,
disc_thmss: thm list list,
discIs: thm list,
- sel_thmss: thm list list};
+ sel_thmss: thm list list,
+ disc_exhausts: thm list,
+ collapses: thm list,
+ expands: thm list,
+ case_convs: thm list};
fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
- case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss} =
+ case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
+ disc_exhausts, collapses, expands, case_convs} =
{ctrs = map (Morphism.term phi) ctrs,
casex = Morphism.term phi casex,
discs = map (Morphism.term phi) discs,
@@ -87,7 +96,11 @@
split_asm = Morphism.thm phi split_asm,
disc_thmss = map (map (Morphism.thm phi)) disc_thmss,
discIs = map (Morphism.thm phi) discIs,
- sel_thmss = map (map (Morphism.thm phi)) sel_thmss};
+ sel_thmss = map (map (Morphism.thm phi)) sel_thmss,
+ disc_exhausts = map (Morphism.thm phi) disc_exhausts,
+ collapses = map (Morphism.thm phi) collapses,
+ expands = map (Morphism.thm phi) expands,
+ case_convs = map (Morphism.thm phi) case_convs};
val rep_compat_prefix = "new";
@@ -762,7 +775,8 @@
nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
- discIs = discI_thms, sel_thmss = sel_thmss},
+ discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
+ collapses = collapse_thms, expands = expand_thms, case_convs = case_conv_thms},
lthy
|> not rep_compat ?
(Local_Theory.declaration {syntax = false, pervasive = true}
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Sep 09 17:28:08 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Sep 09 20:24:15 2013 +0200
@@ -18,8 +18,11 @@
ctr_defss: thm list list,
ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list,
co_iterss: term list list,
+ mapss: thm list list,
co_inducts: thm list,
- co_iter_thmsss: thm list list list};
+ co_iter_thmsss: thm list list list,
+ disc_co_itersss: thm list list list,
+ sel_co_iterssss: thm list list list list};
val of_fp_sugar: (fp_sugar -> 'a list) -> fp_sugar -> 'a
val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
@@ -80,7 +83,7 @@
* (thm list list * thm list list * Args.src list)
* (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
* (thm list list * thm list list * Args.src list)
- * (thm list list * thm list list * Args.src list)
+ * (thm list list list * thm list list list * Args.src list)
val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
@@ -118,8 +121,11 @@
ctr_defss: thm list list,
ctr_sugars: ctr_sugar list,
co_iterss: term list list,
+ mapss: thm list list,
co_inducts: thm list,
- co_iter_thmsss: thm list 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, ...}) = nth (f fp_sugar) index;
@@ -128,15 +134,18 @@
T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
fun morph_fp_sugar phi {T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
- ctr_sugars, co_iterss, co_inducts, co_iter_thmsss} =
+ ctr_sugars, co_iterss, mapss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss} =
{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,
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,
co_inducts = map (Morphism.thm phi) co_inducts,
- co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss};
+ 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};
structure Data = Generic_Data
(
@@ -161,13 +170,14 @@
(fn phi => Data.map (Symtab.default (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 co_inducts co_iter_thmsss lthy =
+ ctr_sugars co_iterss mapss co_inducts 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,
- co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss}
+ ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss,
+ co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss, disc_co_itersss = disc_co_itersss,
+ sel_co_iterssss = sel_co_iterssss}
lthy)) Ts
|> snd;
@@ -999,10 +1009,10 @@
end;
fun mk_sel_coiter_thms coiter_thmss =
- map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss |> map flat;
+ map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss;
- val sel_unfold_thmss = mk_sel_coiter_thms unfold_thmss;
- val sel_corec_thmss = mk_sel_coiter_thms corec_thmss;
+ val sel_unfold_thmsss = mk_sel_coiter_thms unfold_thmss;
+ val sel_corec_thmsss = mk_sel_coiter_thms corec_thmss;
val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
@@ -1018,7 +1028,7 @@
(safe_unfold_thmss, safe_corec_thmss),
(disc_unfold_thmss, disc_corec_thmss, simp_attrs),
(disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs),
- (sel_unfold_thmss, sel_corec_thmss, simp_attrs))
+ (sel_unfold_thmsss, sel_corec_thmsss, simp_attrs))
end;
fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
@@ -1407,7 +1417,7 @@
@ rel_distincts @ flat setss);
fun derive_and_note_induct_iters_thms_for_types
- ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)),
+ ((((mapss, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)),
(iterss, iter_defss)), lthy) =
let
val ((induct_thms, induct_thm, induct_attrs), (fold_thmss, fold_attrs),
@@ -1419,7 +1429,7 @@
val induct_type_attr = Attrib.internal o K o Induct.induct_type;
val simp_thmss =
- mk_simp_thmss ctr_sugars fold_thmss rec_thmss mapsx rel_injects rel_distincts setss;
+ mk_simp_thmss ctr_sugars fold_thmss rec_thmss mapss rel_injects rel_distincts setss;
val common_notes =
(if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
@@ -1435,11 +1445,11 @@
lthy
|> 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 [induct_thm] (transpose [fold_thmss, rec_thmss])
+ iterss mapss [induct_thm] (transpose [fold_thmss, rec_thmss]) [] []
end;
fun derive_and_note_coinduct_coiters_thms_for_types
- ((((mapsx, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)),
+ ((((mapss, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)),
(coiterss, coiter_defss)), lthy) =
let
val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
@@ -1448,11 +1458,14 @@
(safe_unfold_thmss, safe_corec_thmss),
(disc_unfold_thmss, disc_corec_thmss, disc_coiter_attrs),
(disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs),
- (sel_unfold_thmss, sel_corec_thmss, sel_coiter_attrs)) =
+ (sel_unfold_thmsss, sel_corec_thmsss, sel_coiter_attrs)) =
derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
ctr_sugars coiterss coiter_defss (Proof_Context.export lthy' no_defs_lthy) lthy;
+ val sel_unfold_thmss = map flat sel_unfold_thmsss;
+ val sel_corec_thmss = map flat sel_corec_thmsss;
+
val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
fun flat_coiter_thms coiters disc_coiters sel_coiters =
@@ -1462,7 +1475,7 @@
mk_simp_thmss ctr_sugars
(map3 flat_coiter_thms safe_unfold_thmss disc_unfold_thmss sel_unfold_thmss)
(map3 flat_coiter_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss)
- mapsx rel_injects rel_distincts setss;
+ mapss rel_injects rel_distincts setss;
val anonymous_notes =
[(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)]
@@ -1494,8 +1507,9 @@
lthy
|> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
|> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss
- ctr_sugars coiterss [coinduct_thm, strong_coinduct_thm]
- (transpose [unfold_thmss, corec_thmss])
+ ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm]
+ (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss])
+ (transpose [sel_unfold_thmsss, sel_corec_thmsss])
end;
val lthy'' = lthy'
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Mon Sep 09 17:28:08 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Mon Sep 09 20:24:15 2013 +0200
@@ -59,6 +59,7 @@
end;
val ctr_defss = map (of_fp_sugar #ctr_defss) fp_sugars0;
+ val mapss = map (of_fp_sugar #mapss) fp_sugars0;
val ctr_sugars0 = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
val ctrss = map #ctrs ctr_sugars0;
@@ -145,27 +146,33 @@
val ctr_sugars = map inst_ctr_sugar ctr_sugars0;
- val (co_inducts, un_fold_thmss, co_rec_thmss) =
+ val (co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
+ sel_unfold_thmsss, sel_corec_thmsss) =
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 ((_, induct, _), (fold_thmss, _), (rec_thmss, _)) =>
- ([induct], fold_thmss, rec_thmss))
+ ([induct], fold_thmss, rec_thmss, [], [], [], []))
else
derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
- |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _, _, _, _) =>
- (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss));
+ |> (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, unfold_thmss, corec_thmss, disc_unfold_thmss,
+ disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss));
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_inducts = co_inducts, co_iterss = co_iterss,
- co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss]}
+ ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
+ 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]}
|> morph_fp_sugar phi;
in
((true, map_index mk_target_fp_sugar fpTs), lthy)
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Mon Sep 09 17:28:08 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Mon Sep 09 20:24:15 2013 +0200
@@ -54,8 +54,8 @@
fun mk_primcorec_disc_tac ctxt defs disc k m exclsss =
mk_primcorec_prelude ctxt defs disc THEN mk_primcorec_cases_tac ctxt k m exclsss;
-fun mk_primcorec_eq_tac ctxt defs sel k m exclsss maps map_idents map_comps =
- mk_primcorec_prelude ctxt defs (sel RS trans) THEN mk_primcorec_cases_tac ctxt k m exclsss THEN
+fun mk_primcorec_eq_tac ctxt defs eq_thm k m exclsss maps map_idents map_comps =
+ mk_primcorec_prelude ctxt defs (eq_thm RS trans) THEN mk_primcorec_cases_tac ctxt k m exclsss THEN
unfold_thms_tac ctxt (@{thms if_if_True if_if_False if_True if_False o_def split_def sum.cases} @
maps @ map_comps @ map_idents) THEN HEADGOAL (rtac refl);
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Mon Sep 09 17:28:08 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Mon Sep 09 20:24:15 2013 +0200
@@ -31,7 +31,10 @@
sels: term list,
pred: int option,
calls: corec_call list,
- corec_thm: thm}
+ collapse: thm,
+ corec_thm: thm,
+ disc_corec: thm,
+ sel_corecs: thm list}
type rec_spec =
{recx: term,
@@ -41,6 +44,9 @@
type corec_spec =
{corec: term,
+ nested_maps: thm list,
+ nested_map_idents: thm list,
+ nested_map_comps: thm list,
ctr_specs: corec_ctr_spec list}
val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
@@ -90,7 +96,10 @@
sels: term list,
pred: int option,
calls: corec_call list,
- corec_thm: thm};
+ collapse: thm,
+ corec_thm: thm,
+ disc_corec: thm,
+ sel_corecs: thm list};
type rec_spec =
{recx: term,
@@ -100,6 +109,9 @@
type corec_spec =
{corec: term,
+ nested_maps: thm list,
+ nested_map_idents: thm list,
+ nested_map_comps: thm list,
ctr_specs: corec_ctr_spec list};
val id_def = @{thm id_def};
@@ -260,6 +272,18 @@
fun find_index_eq hs h = find_index (curry (op =) h) hs;
+(*FIXME: remove special cases for products and sum once they are registered as datatypes*)
+fun map_thms_of_typ ctxt (Type (s, _)) =
+ if s = @{type_name prod} then
+ @{thms map_pair_simp}
+ else if s = @{type_name sum} then
+ @{thms sum_map.simps}
+ else
+ (case fp_sugar_of ctxt s of
+ SOME {index, mapss, ...} => nth mapss index
+ | NONE => [])
+ | map_thms_of_typ _ _ = [];
+
val lose_co_rec = false (*FIXME: try true?*);
fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
@@ -348,8 +372,8 @@
val thy = Proof_Context.theory_of lthy;
val ((nontriv, missing_res_Ts, perm0_kks,
- fp_sugars as {fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
- co_inducts = coinduct_thms, ...} :: _), lthy') =
+ fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
+ co_inducts = coinduct_thms, ...} :: _), lthy') =
nested_to_mutual_fps lose_co_rec Greatest_FP bs res_Ts get_indices callssss0 lthy;
val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
@@ -407,27 +431,38 @@
else No_Corec) g_i
| call_of _ [q_i] [g_i, g_i'] _ = Direct_Corec (q_i, g_i, g_i');
- fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss corec_thm =
+ fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss collapse corec_thm disc_corec sel_corecs =
let val nullary = not (can dest_funT (fastype_of ctr)) in
{ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_ho,
- calls = map3 (call_of nullary) q_iss f_iss f_Tss, corec_thm = corec_thm}
+ calls = map3 (call_of nullary) q_iss f_iss f_Tss, collapse = collapse,
+ corec_thm = corec_thm, 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 =
+ fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss
+ sel_coiterssss =
let
val ctrs = #ctrs (nth ctr_sugars index);
val discs = #discs (nth ctr_sugars index);
val selss = #selss (nth ctr_sugars index);
val p_ios = map SOME p_is @ [NONE];
- val corec_thmss = co_rec_of (nth coiter_thmsss index);
+ val collapses = #collapses (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);
in
- map8 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss corec_thmss
+ map11 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss collapses corec_thms
+ disc_corecs sel_corecss
end;
- fun mk_spec {T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss, ...}
+ 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, ...}
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)),
- ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss};
+ nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
+ nested_map_idents = map (unfold_thms lthy [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};
in
((nontriv, 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,
--- a/src/HOL/Tools/Metis/metis_generate.ML Mon Sep 09 17:28:08 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML Mon Sep 09 20:24:15 2013 +0200
@@ -215,9 +215,8 @@
else
conj_clauses @ fact_clauses
|> map (pair 0)
- |> rpair (ctxt |> Config.put Legacy_Monomorph.keep_partial_instances false)
- |-> Legacy_Monomorph.monomorph atp_schematic_consts_of
- |> fst |> chop (length conj_clauses)
+ |> Monomorph.monomorph atp_schematic_consts_of ctxt
+ |> chop (length conj_clauses)
|> pairself (maps (map (zero_var_indexes o snd)))
val num_conjs = length conj_clauses
(* Pretend every clause is a "simp" rule, to guide the term ordering. *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Sep 09 17:28:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Sep 09 20:24:15 2013 +0200
@@ -650,19 +650,14 @@
| _ => (maybe_isar_name, [])
in minimize_command override_params min_name end
-fun repair_legacy_monomorph_context max_iters best_max_iters max_new_instances
- best_max_new_instances =
- Config.put Legacy_Monomorph.max_rounds
- (max_iters |> the_default best_max_iters)
- #> Config.put Legacy_Monomorph.max_new_instances
- (max_new_instances |> the_default best_max_new_instances)
- #> Config.put Legacy_Monomorph.keep_partial_instances false
+val max_fact_instances = 10 (* FUDGE *)
fun repair_monomorph_context max_iters best_max_iters max_new_instances
best_max_new_instances =
Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
#> Config.put Monomorph.max_new_instances
(max_new_instances |> the_default best_max_new_instances)
+ #> Config.put Monomorph.max_thm_instances max_fact_instances
fun suffix_of_mode Auto_Try = "_try"
| suffix_of_mode Try = "_try"
@@ -757,7 +752,7 @@
let
val ctxt =
ctxt
- |> repair_legacy_monomorph_context max_mono_iters
+ |> repair_monomorph_context max_mono_iters
best_max_mono_iters max_new_mono_instances
best_max_new_mono_instances
(* pseudo-theorem involving the same constants as the subgoal *)
@@ -770,9 +765,8 @@
|> op @
|> cons (0, subgoal_th)
in
- Legacy_Monomorph.monomorph atp_schematic_consts_of rths ctxt
- |> fst |> tl
- |> curry ListPair.zip (map fst facts)
+ Monomorph.monomorph atp_schematic_consts_of ctxt rths
+ |> tl |> curry ListPair.zip (map fst facts)
|> maps (fn (name, rths) =>
map (pair name o zero_var_indexes o snd) rths)
end
--- a/src/HOL/Tools/legacy_monomorph.ML Mon Sep 09 17:28:08 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,331 +0,0 @@
-(* Title: HOL/Tools/legacy_monomorph.ML
- Author: Sascha Boehme, TU Muenchen
-
-Monomorphization of theorems, i.e., computation of all (necessary)
-instances. This procedure is incomplete in general, but works well for
-most practical problems.
-
-For a list of universally closed theorems (without schematic term
-variables), monomorphization computes a list of theorems with schematic
-term variables: all polymorphic constants (i.e., constants occurring both
-with ground types and schematic type variables) are instantiated with all
-(necessary) ground types; thereby theorems containing these constants are
-copied. To prevent nontermination, there is an upper limit for the number
-of iterations involved in the fixpoint construction.
-
-The search for instances is performed on the constants with schematic
-types, which are extracted from the initial set of theorems. The search
-constructs, for each theorem with those constants, a set of substitutions,
-which, in the end, is applied to all corresponding theorems. Remaining
-schematic type variables are substituted with fresh types.
-
-Searching for necessary substitutions is an iterative fixpoint
-construction: each iteration computes all required instances required by
-the ground instances computed in the previous step and which haven't been
-found before. Computed substitutions are always nontrivial: schematic type
-variables are never mapped to schematic type variables.
-*)
-
-signature LEGACY_MONOMORPH =
-sig
- (* utility function *)
- val typ_has_tvars: typ -> bool
- val all_schematic_consts_of: term -> typ list Symtab.table
- val add_schematic_consts_of: term -> typ list Symtab.table ->
- typ list Symtab.table
-
- (* configuration options *)
- val max_rounds: int Config.T
- val max_new_instances: int Config.T
- val keep_partial_instances: bool Config.T
-
- (* monomorphization *)
- val monomorph: (term -> typ list Symtab.table) -> (int * thm) list ->
- Proof.context -> (int * thm) list list * Proof.context
-end
-
-structure Legacy_Monomorph: LEGACY_MONOMORPH =
-struct
-
-(* utility functions *)
-
-val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false)
-
-fun add_schematic_const (c as (_, T)) =
- if typ_has_tvars T then Symtab.insert_list (op =) c else I
-
-fun add_schematic_consts_of t =
- Term.fold_aterms (fn Const c => add_schematic_const c | _ => I) t
-
-fun all_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
-
-
-
-(* configuration options *)
-
-val max_rounds = Attrib.setup_config_int @{binding legacy_monomorph_max_rounds} (K 5)
-val max_new_instances =
- Attrib.setup_config_int @{binding legacy_monomorph_max_new_instances} (K 300)
-val keep_partial_instances =
- Attrib.setup_config_bool @{binding legacy_monomorph_keep_partial_instances} (K true)
-
-
-
-(* monomorphization *)
-
-(** preparing the problem **)
-
-datatype thm_info =
- Ground of thm |
- Schematic of {
- index: int,
- theorem: thm,
- tvars: (indexname * sort) list,
- schematics: typ list Symtab.table,
- initial_round: int }
-
-fun prepare schematic_consts_of rthms =
- let
- val empty_sub = ((0, false, false), Vartab.empty)
-
- fun prep (r, thm) ((i, idx), (consts, subs)) =
- if not (Term.exists_type typ_has_tvars (Thm.prop_of thm)) then
- (Ground thm, ((i+1, idx + Thm.maxidx_of thm + 1), (consts, subs)))
- else
- let
- (* increase indices to avoid clashes of type variables *)
- val thm' = Thm.incr_indexes idx thm
- val idx' = Thm.maxidx_of thm' + 1
- val schematics = schematic_consts_of (Thm.prop_of thm')
- val consts' =
- Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics consts
- val subs' = Inttab.update (i, [empty_sub]) subs
- val thm_info = Schematic {
- index = i,
- theorem = thm',
- tvars = Term.add_tvars (Thm.prop_of thm') [],
- schematics = schematics,
- initial_round = r }
- in (thm_info, ((i+1, idx'), (consts', subs'))) end
- in fold_map prep rthms ((0, 0), (Symtab.empty, Inttab.empty)) ||> snd end
-
-
-
-(** collecting substitutions **)
-
-fun exceeded limit = (limit <= 0)
-fun exceeded_limit (limit, _, _) = exceeded limit
-
-
-fun derived_subst subst' subst = subst' |> Vartab.forall (fn (n, (_, T)) =>
- Vartab.lookup subst n |> Option.map (equal T o snd) |> the_default false)
-
-fun eq_subst (subst1, subst2) =
- derived_subst subst1 subst2 andalso derived_subst subst2 subst1
-
-
-fun with_all_grounds cx grounds f =
- if exceeded_limit cx then I else Symtab.fold f grounds
-
-fun with_all_type_combinations cx schematics f (n, Ts) =
- if exceeded_limit cx then I
- else fold_product f (Symtab.lookup_list schematics n) Ts
-
-fun derive_new_substs thy cx new_grounds schematics subst =
- with_all_grounds cx new_grounds
- (with_all_type_combinations cx schematics (fn T => fn U =>
- (case try (Sign.typ_match thy (T, U)) subst of
- NONE => I
- | SOME subst' => insert eq_subst subst'))) []
-
-
-fun known_subst sub subs1 subs2 subst' =
- let fun derived (_, subst) = derived_subst subst' subst
- in derived sub orelse exists derived subs1 orelse exists derived subs2 end
-
-fun within_limit f cx = if exceeded_limit cx then cx else f cx
-
-fun fold_partial_substs derive add = within_limit (
- let
- fun fold_partial [] cx = cx
- | fold_partial (sub :: subs) (limit, subs', next) =
- if exceeded limit then (limit, sub :: subs @ subs', next)
- else sub |> (fn ((generation, full, _), subst) =>
- if full then fold_partial subs (limit, sub :: subs', next)
- else
- (case filter_out (known_subst sub subs subs') (derive subst) of
- [] => fold_partial subs (limit, sub :: subs', next)
- | substs =>
- (limit, ((generation, full, true), subst) :: subs', next)
- |> fold (within_limit o add) substs
- |> fold_partial subs))
- in (fn (limit, subs, next) => fold_partial subs (limit, [], next)) end)
-
-
-fun refine ctxt round known_grounds new_grounds (tvars, schematics) cx =
- let
- val thy = Proof_Context.theory_of ctxt
- val count_partial = Config.get ctxt keep_partial_instances
-
- fun add_new_ground subst n T =
- let val T' = Envir.subst_type subst T
- in
- (* FIXME: maybe keep types in a table or net for known_grounds,
- that might improve efficiency here
- *)
- if typ_has_tvars T' then I
- else if member (op =) (Symtab.lookup_list known_grounds n) T' then I
- else Symtab.cons_list (n, T')
- end
-
- fun add_new_subst subst (limit, subs, next_grounds) =
- let
- val full = forall (Vartab.defined subst o fst) tvars
- val limit' =
- if full orelse count_partial then limit - 1 else limit
- val sub = ((round, full, false), subst)
- val next_grounds' =
- (schematics, next_grounds)
- |-> Symtab.fold (uncurry (fold o add_new_ground subst))
- in (limit', sub :: subs, next_grounds') end
- in
- fold_partial_substs (derive_new_substs thy cx new_grounds schematics)
- add_new_subst cx
- end
-
-
-(*
- 'known_grounds' are all constant names known to occur schematically
- associated with all ground instances considered so far
-*)
-fun add_relevant_instances known_grounds (Const (c as (n, T))) =
- if typ_has_tvars T orelse not (Symtab.defined known_grounds n) then I
- else if member (op =) (Symtab.lookup_list known_grounds n) T then I
- else Symtab.insert_list (op =) c
- | add_relevant_instances _ _ = I
-
-fun collect_instances known_grounds thm =
- Term.fold_aterms (add_relevant_instances known_grounds) (Thm.prop_of thm)
-
-
-fun make_subst_ctxt ctxt thm_infos known_grounds substitutions =
- let
- (* The total limit of returned (ground) facts is the number of facts
- given to the monomorphizer increased by max_new_instances. Since
- initially ground facts are returned anyway, the limit here is not
- counting them. *)
- val limit = Config.get ctxt max_new_instances +
- fold (fn Schematic _ => Integer.add 1 | _ => I) thm_infos 0
-
- fun add_ground_consts (Ground thm) = collect_instances known_grounds thm
- | add_ground_consts (Schematic _) = I
- val initial_grounds = fold add_ground_consts thm_infos Symtab.empty
- in (known_grounds, (limit, substitutions, initial_grounds)) end
-
-fun is_new round initial_round = (round = initial_round)
-fun is_active round initial_round = (round > initial_round)
-
-fun fold_schematic pred f = fold (fn
- Schematic {index, theorem, tvars, schematics, initial_round} =>
- if pred initial_round then f theorem (index, tvars, schematics) else I
- | Ground _ => I)
-
-fun focus f _ (index, tvars, schematics) (limit, subs, next_grounds) =
- let
- val (limit', isubs', next_grounds') =
- (limit, Inttab.lookup_list subs index, next_grounds)
- |> f (tvars, schematics)
- in (limit', Inttab.update (index, isubs') subs, next_grounds') end
-
-fun collect_substitutions thm_infos ctxt round subst_ctxt =
- let val (known_grounds, (limit, subs, next_grounds)) = subst_ctxt
- in
- if exceeded limit then subst_ctxt
- else
- let
- fun collect thm _ = collect_instances known_grounds thm
- val new = fold_schematic (is_new round) collect thm_infos next_grounds
-
- val known' = Symtab.merge_list (op =) (known_grounds, new)
- val step = focus o refine ctxt round known'
- in
- (limit, subs, Symtab.empty)
- |> not (Symtab.is_empty new) ?
- fold_schematic (is_active round) (step new) thm_infos
- |> fold_schematic (is_new round) (step known') thm_infos
- |> pair known'
- end
- end
-
-
-
-(** instantiating schematic theorems **)
-
-fun super_sort (Ground _) S = S
- | super_sort (Schematic {tvars, ...}) S = merge (op =) (S, maps snd tvars)
-
-fun new_super_type ctxt thm_infos =
- let val S = fold super_sort thm_infos @{sort type}
- in yield_singleton Variable.invent_types S ctxt |>> SOME o TFree end
-
-fun add_missing_tvar T (ix, S) subst =
- if Vartab.defined subst ix then subst
- else Vartab.update (ix, (S, T)) subst
-
-fun complete tvars subst T =
- subst
- |> Vartab.map (K (apsnd (Term.map_atyps (fn TVar _ => T | U => U))))
- |> fold (add_missing_tvar T) tvars
-
-fun instantiate_all' (mT, ctxt) subs thm_infos =
- let
- val thy = Proof_Context.theory_of ctxt
-
- fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
- fun cert' subst = Vartab.fold (cons o cert) subst []
- fun instantiate thm subst = Thm.instantiate (cert' subst, []) thm
-
- fun with_subst tvars f ((generation, full, _), subst) =
- if full then SOME (generation, f subst)
- else Option.map (pair generation o f o complete tvars subst) mT
-
- fun inst (Ground thm) = [(0, thm)]
- | inst (Schematic {theorem, tvars, index, ...}) =
- Inttab.lookup_list subs index
- |> map_filter (with_subst tvars (instantiate theorem))
- in (map inst thm_infos, ctxt) end
-
-fun instantiate_all ctxt thm_infos (_, (_, subs, _)) =
- if Config.get ctxt keep_partial_instances then
- let fun is_refined ((_, _, refined), _) = refined
- in
- (Inttab.map (K (filter_out is_refined)) subs, thm_infos)
- |-> instantiate_all' (new_super_type ctxt thm_infos)
- end
- else instantiate_all' (NONE, ctxt) subs thm_infos
-
-
-
-(** overall procedure **)
-
-fun limit_rounds ctxt f =
- let
- val max = Config.get ctxt max_rounds
- fun round i x = if i > max then x else round (i + 1) (f ctxt i x)
- in round 1 end
-
-fun monomorph schematic_consts_of rthms ctxt =
- let
- val (thm_infos, (known_grounds, subs)) = prepare schematic_consts_of rthms
- in
- if Symtab.is_empty known_grounds then
- (map (fn Ground thm => [(0, thm)] | _ => []) thm_infos, ctxt)
- else
- make_subst_ctxt ctxt thm_infos known_grounds subs
- |> limit_rounds ctxt (collect_substitutions thm_infos)
- |> instantiate_all ctxt thm_infos
- end
-
-
-end
-
--- a/src/HOL/Tools/monomorph.ML Mon Sep 09 17:28:08 2013 +0200
+++ b/src/HOL/Tools/monomorph.ML Mon Sep 09 20:24:15 2013 +0200
@@ -35,6 +35,7 @@
(* configuration options *)
val max_rounds: int Config.T
val max_new_instances: int Config.T
+ val max_thm_instances: int Config.T
(* monomorphization *)
val monomorph: (term -> typ list Symtab.table) -> Proof.context ->
@@ -67,14 +68,15 @@
val max_new_instances =
Attrib.setup_config_int @{binding monomorph_max_new_instances} (K 300)
+val max_thm_instances =
+ Attrib.setup_config_int @{binding max_thm_instances} (K 20)
+
fun limit_rounds ctxt f =
let
val max = Config.get ctxt max_rounds
fun round i x = if i > max then x else round (i + 1) (f ctxt i x)
in round 1 end
-fun reached_limit ctxt n = (n >= Config.get ctxt max_new_instances)
-
(* theorem information and related functions *)
@@ -175,25 +177,31 @@
in Term.fold_aterms add (Thm.prop_of thm) end
-fun add_insts ctxt round used_grounds new_grounds id thm tvars schematics cx =
+fun add_insts max_instances max_thm_instances ctxt round used_grounds
+ new_grounds id thm tvars schematics cx =
let
exception ENOUGH of
typ list Symtab.table * (int * (int * thm) list Inttab.table)
val thy = Proof_Context.theory_of ctxt
- fun add subst (next_grounds, (n, insts)) =
- let
- val thm' = instantiate thy subst thm
- val rthm = (round, thm')
- val n_insts' =
- if member (eq_snd Thm.eq_thm) (Inttab.lookup_list insts id) rthm then
- (n, insts)
- else (n + 1, Inttab.cons_list (id, rthm) insts)
- val next_grounds' =
- add_new_grounds used_grounds new_grounds thm' next_grounds
- val cx' = (next_grounds', n_insts')
- in if reached_limit ctxt n then raise ENOUGH cx' else cx' end
+ fun add subst (cx as (next_grounds, (n, insts))) =
+ if n >= max_instances then
+ raise ENOUGH cx
+ else
+ let
+ val thm' = instantiate thy subst thm
+ val rthm = (round, thm')
+ val rthms = Inttab.lookup_list insts id;
+ val n_insts' =
+ if member (eq_snd Thm.eq_thm) rthms rthm orelse
+ length rthms >= max_thm_instances then
+ (n, insts)
+ else
+ (n + 1, Inttab.cons_list (id, rthm) insts)
+ val next_grounds' =
+ add_new_grounds used_grounds new_grounds thm' next_grounds
+ in (next_grounds', n_insts') end
fun with_grounds (n, T) f subst (n', Us) =
let
@@ -239,12 +247,12 @@
fun is_active round initial_round = (round > initial_round)
-fun find_instances thm_infos ctxt round (known_grounds, new_grounds, insts) =
+fun find_instances max_instances max_thm_instances thm_infos ctxt round
+ (known_grounds, new_grounds, insts) =
let
- val add_new = add_insts ctxt round
+ val add_new = add_insts max_instances max_thm_instances ctxt round
fun consider_all pred f (cx as (_, (n, _))) =
- if reached_limit ctxt n then cx
- else fold_schematics pred f thm_infos cx
+ if n >= max_instances then cx else fold_schematics pred f thm_infos cx
val known_grounds' = Symtab.merge_list (op =) (known_grounds, new_grounds)
val empty_grounds = clear_grounds known_grounds'
@@ -266,9 +274,13 @@
let
val known_grounds = fold_grounds add_ground_types thm_infos consts
val empty_grounds = clear_grounds known_grounds
+ val max_instances = Config.get ctxt max_new_instances
+ |> fold (fn Schematic _ => Integer.add 1 | _ => I) thm_infos
+ val max_thm_instances = Config.get ctxt max_thm_instances
in
(empty_grounds, known_grounds, (0, Inttab.empty))
- |> limit_rounds ctxt (find_instances thm_infos)
+ |> limit_rounds ctxt
+ (find_instances max_instances max_thm_instances thm_infos)
|> (fn (_, _, (_, insts)) => insts)
end