--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Jun 27 10:11:44 2014 +0200
@@ -17,7 +17,7 @@
val flat_corec_preds_predsss_gettersss: 'a list -> 'a list list list -> 'a list list list ->
'a list
- val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
+ val nesting_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
type lfp_sugar_thms =
(thm list * thm * Args.src list) * (thm list list * Args.src list)
@@ -142,20 +142,21 @@
#> fp = Least_FP ? generate_lfp_size fp_sugars
#> Local_Theory.background_theory (FP_Sugar_Interpretation.data fp_sugars);
-fun register_as_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
+fun register_as_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs live_nesting_bnfs fp_res
ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss common_co_inducts co_inductss
co_rec_thmss disc_co_recss sel_co_recsss rel_injectss rel_distinctss =
let
val fp_sugars =
map_index (fn (kk, T) =>
{T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk,
- pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk, nested_bnfs = nested_bnfs,
- nesting_bnfs = nesting_bnfs, ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk,
- ctr_sugar = nth ctr_sugars kk, co_rec = nth co_recs kk, co_rec_def = nth co_rec_defs kk,
- maps = nth mapss kk, common_co_inducts = common_co_inducts,
- co_inducts = nth co_inductss kk, co_rec_thms = nth co_rec_thmss kk,
- disc_co_recs = nth disc_co_recss kk, sel_co_recss = nth sel_co_recsss kk,
- rel_injects = nth rel_injectss kk, rel_distincts = nth rel_distinctss kk}) Ts
+ pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk,
+ fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
+ ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk,
+ co_rec = nth co_recs kk, co_rec_def = nth co_rec_defs kk, maps = nth mapss kk,
+ common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk,
+ co_rec_thms = nth co_rec_thmss kk, disc_co_recs = nth disc_co_recss kk,
+ sel_co_recss = nth sel_co_recsss kk, rel_injects = nth rel_injectss kk,
+ rel_distincts = nth rel_distinctss kk}) Ts
in
register_fp_sugars fp_sugars
end;
@@ -254,7 +255,7 @@
fun rel_binding_of_spec ((_, (_, b)), _) = b;
fun sel_default_eqs_of_spec (_, ts) = ts;
-fun add_nesty_bnf_names Us =
+fun add_nesting_bnf_names Us =
let
fun add (Type (s, Ts)) ss =
let val (needs, ss') = fold_map add Ts ss in
@@ -263,8 +264,8 @@
| add T ss = (member (op =) Us T, ss);
in snd oo add end;
-fun nesty_bnfs ctxt ctr_Tsss Us =
- map_filter (bnf_of ctxt) (fold (fold (fold (add_nesty_bnf_names Us))) ctr_Tsss []);
+fun nesting_bnfs ctxt ctr_Tsss Us =
+ map_filter (bnf_of ctxt) (fold (fold (fold (add_nesting_bnf_names Us))) ctr_Tsss []);
fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p;
@@ -444,8 +445,8 @@
end;
fun derive_induct_recs_thms_for_types pre_bnfs rec_args_typess ctor_induct ctor_rec_thms
- nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions abs_inverses
- ctrss ctr_defss recs rec_defs lthy =
+ live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions
+ abs_inverses ctrss ctr_defss recs rec_defs lthy =
let
val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss;
@@ -455,9 +456,10 @@
val pre_map_defs = map map_def_of_bnf pre_bnfs;
val pre_set_defss = map set_defs_of_bnf pre_bnfs;
- val nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
- val nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs;
- val nested_set_maps = maps set_map_of_bnf nested_bnfs;
+ val live_nesting_map_idents =
+ map (unfold_thms lthy [id_def] o map_id0_of_bnf) live_nesting_bnfs;
+ val fp_nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) fp_nesting_bnfs;
+ val fp_nesting_set_maps = maps set_map_of_bnf fp_nesting_bnfs;
val fp_b_names = map base_name_of_typ fpTs;
@@ -482,7 +484,7 @@
(T_name, map mk_set Us)
end;
- val setss_nested = map mk_sets_nested nested_bnfs;
+ val setss_nested = map mk_sets_nested fp_nesting_bnfs;
val (induct_thms, induct_thm) =
let
@@ -541,7 +543,7 @@
val thm =
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' fp_abs_inverses
- abs_inverses nested_set_maps pre_set_defss)
+ abs_inverses fp_nesting_set_maps pre_set_defss)
|> singleton (Proof_Context.export names_lthy lthy)
(* for "datatype_realizer.ML": *)
|> Thm.name_derivation (fst (dest_Type (hd fpTs)) ^ Long_Name.separator ^
@@ -580,8 +582,8 @@
val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss;
val goalss = map5 (map4 o mk_goal) frecs xctrss fss xsss fxsss;
- val tacss =
- map4 (map ooo mk_rec_tac pre_map_defs (nested_map_idents @ nesting_map_idents) rec_defs)
+ val tacss = map4 (map ooo
+ mk_rec_tac pre_map_defs (fp_nesting_map_idents @ live_nesting_map_idents) rec_defs)
ctor_rec_thms fp_abs_inverses abs_inverses ctr_defss;
fun prove goal tac =
@@ -721,8 +723,8 @@
end;
fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
- dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
- mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
+ dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
+ kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
corecs corec_defs export_args lthy =
let
fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec =
@@ -734,8 +736,9 @@
val pre_map_defs = map map_def_of_bnf pre_bnfs;
val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
- val nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
- val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
+ val live_nesting_map_idents =
+ map (unfold_thms lthy [id_def] o map_id0_of_bnf) live_nesting_bnfs;
+ val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs;
val fp_b_names = map base_name_of_typ fpTs;
@@ -806,8 +809,8 @@
fun prove dtor_coinduct' goal =
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_coinduct_tac ctxt nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs fp_abs_inverses
- abs_inverses dtor_ctors exhausts ctr_defss disc_thmsss sel_thmsss)
+ mk_coinduct_tac ctxt live_nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs
+ fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss disc_thmsss sel_thmsss)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;
@@ -852,7 +855,7 @@
val goalss = map8 (map4 oooo mk_goal) cs cpss gcorecs ns kss ctrss mss cqgsss';
val tacss =
- map4 (map ooo mk_corec_tac corec_defs nesting_map_idents)
+ map4 (map ooo mk_corec_tac corec_defs live_nesting_map_idents)
ctor_dtor_corec_thms pre_map_defs abs_inverses ctr_defss;
fun prove goal tac =
@@ -1073,14 +1076,14 @@
val time = time lthy;
val timer = time (Timer.startRealTimer ());
- val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
- val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
+ val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs;
+ val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As;
val pre_map_defs = map map_def_of_bnf pre_bnfs;
val pre_set_defss = map set_defs_of_bnf pre_bnfs;
val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
- val nesting_set_maps = maps set_map_of_bnf nesting_bnfs;
- val nested_set_maps = maps set_map_of_bnf nested_bnfs;
+ val fp_nesting_set_maps = maps set_map_of_bnf fp_nesting_bnfs;
+ val live_nesting_set_maps = maps set_map_of_bnf live_nesting_bnfs;
val live = live_of_bnf any_fp_bnf;
val _ =
@@ -1245,7 +1248,7 @@
fun mk_set_thm fp_set_thm ctr_def' cxIn =
fold_thms lthy [ctr_def']
- (unfold_thms lthy (pre_set_defs @ nested_set_maps @ nesting_set_maps @
+ (unfold_thms lthy (pre_set_defs @ fp_nesting_set_maps @ live_nesting_set_maps @
(if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_set @
abs_inverses)
(cterm_instantiate_pos [SOME cxIn] fp_set_thm))
@@ -1357,8 +1360,7 @@
let
val X = HOLogic.dest_setT (range_type (fastype_of set));
val (x, ctxt') = yield_singleton (mk_Frees "x") X ctxt;
- val assm = HOLogic.mk_Trueprop
- (HOLogic.mk_mem (x, set $ a));
+ val assm = HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ a));
in
travese_nested_types x ctxt'
|>> map (Logic.mk_implies o pair assm)
@@ -1527,7 +1529,7 @@
let
val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) =
derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct xtor_co_rec_thms
- nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses type_definitions
+ live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses type_definitions
abs_inverses ctrss ctr_defss recs rec_defs lthy;
val induct_type_attr = Attrib.internal o K o Induct.induct_type;
@@ -1548,8 +1550,8 @@
lthy
|> Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss)
|> Local_Theory.notes (common_notes @ notes) |> snd
- |> register_as_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs
- fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs mapss [induct_thm]
+ |> register_as_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos fp_nesting_bnfs
+ live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs mapss [induct_thm]
(map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) rel_injectss
rel_distinctss
end;
@@ -1563,8 +1565,8 @@
(corec_thmss, corec_attrs), (disc_corec_thmss, disc_corec_attrs),
(disc_corec_iff_thmss, disc_corec_iff_attrs), (sel_corec_thmsss, sel_corec_attrs)) =
derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
- dtor_injects dtor_ctors xtor_co_rec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
- abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
+ dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss
+ ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
(Proof_Context.export lthy' no_defs_lthy) lthy;
val ((rel_coinduct_thms, rel_coinduct_thm),
@@ -1611,8 +1613,8 @@
|> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs)
[flat sel_corec_thmss, flat corec_thmss]
|> Local_Theory.notes (common_notes @ notes) |> snd
- |> register_as_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos nested_bnfs
- nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs mapss
+ |> register_as_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos fp_nesting_bnfs
+ live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs mapss
[coinduct_thm, strong_coinduct_thm] (transpose [coinduct_thms, strong_coinduct_thms])
corec_thmss disc_corec_thmss sel_corec_thmsss rel_injectss rel_distinctss
end;
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Fri Jun 27 10:11:44 2014 +0200
@@ -71,9 +71,10 @@
val fp_absT_infos = map #absT_info fp_sugars;
val fp_bnfs = of_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);
+ val nesting_bnfss =
+ map (fn sugar => #fp_nesting_bnfs sugar @ #live_nesting_bnfs sugar) fp_sugars;
+ val fp_or_nesting_bnfss = fp_bnfs :: nesting_bnfss;
+ val fp_or_nesting_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_or_nesting_bnfss);
val fp_absTs = map #absT fp_absT_infos;
val fp_repTs = map #repT fp_absT_infos;
@@ -137,7 +138,7 @@
val rels =
let
- fun find_rel T As Bs = fp_nesty_bnfss
+ fun find_rel T As Bs = fp_or_nesting_bnfss
|> map (filter_out (curry (op = o pairself name_of_bnf) BNF_Comp.DEADID_bnf))
|> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)))
|> Option.map (fn bnf =>
@@ -186,7 +187,7 @@
xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs rel_monos)
lthy;
- val rel_eqs = no_refl (map rel_eq_of_bnf fp_nesty_bnfs);
+ val rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs);
val map_id0s = no_refl (map map_id0_of_bnf bnfs);
val xtor_co_induct_thm =
@@ -419,7 +420,8 @@
val map_thms = no_refl (maps (fn bnf =>
let val map_comp0 = map_comp0_of_bnf bnf RS sym
- in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end) fp_nesty_bnfs) @
+ in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end)
+ fp_or_nesting_bnfs) @
remove eq_thm_prop_untyped (case_fp fp @{thm comp_assoc[symmetric]} @{thm comp_assoc})
(map2 (fn thm => fn bnf =>
@{thm type_copy_map_comp0_undo} OF
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Jun 27 10:11:44 2014 +0200
@@ -237,8 +237,8 @@
val repTs = map #repT absT_infos;
val abs_inverses = map #abs_inverse absT_infos;
- val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
- val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
+ val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs;
+ val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As;
val ((xtor_co_recs, recs_args_types, corecs_args_types), _) =
mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
@@ -256,15 +256,16 @@
fp_sugar_thms) =
if fp = Least_FP then
derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct
- xtor_co_rec_thms nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses
- fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs lthy
+ xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
+ fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs
+ lthy
|> `(fn ((inducts, induct, _), (rec_thmss, _)) =>
([induct], [inducts], rec_thmss, replicate nn [], replicate nn []))
||> (fn info => (SOME info, NONE))
else
derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
- dtor_injects dtor_ctors xtor_co_rec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
- fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss
+ dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
+ mss ns fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss
ctr_sugars co_recs co_rec_defs (Proof_Context.export lthy no_defs_lthy) lthy
|> `(fn ((coinduct_thms_pairs, _), (corec_thmss, _), (disc_corec_thmss, _), _,
(sel_corec_thmsss, _)) =>
@@ -278,11 +279,11 @@
co_rec_def maps co_inducts co_rec_thms disc_corec_thms sel_corec_thmss
({rel_injects, rel_distincts, ...} : fp_sugar) =
{T = T, BT = Term.dummyT (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res,
- fp_res_index = kk, pre_bnf = pre_bnf, absT_info = absT_info, nested_bnfs = nested_bnfs,
- nesting_bnfs = nesting_bnfs, ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs,
- ctr_sugar = ctr_sugar, co_rec = co_rec, co_rec_def = co_rec_def, maps = maps,
- common_co_inducts = common_co_inducts, co_inducts = co_inducts,
- co_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms,
+ fp_res_index = kk, pre_bnf = pre_bnf, absT_info = absT_info,
+ fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
+ ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_rec = co_rec,
+ co_rec_def = co_rec_def, maps = maps, common_co_inducts = common_co_inducts,
+ co_inducts = co_inducts, co_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms,
sel_co_recss = sel_corec_thmss, rel_injects = rel_injects, rel_distincts = rel_distincts}
|> morph_fp_sugar phi;
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Jun 27 10:11:44 2014 +0200
@@ -37,8 +37,8 @@
fp_res: fp_result,
pre_bnf: BNF_Def.bnf,
absT_info: BNF_Comp.absT_info,
- nested_bnfs: BNF_Def.bnf list,
- nesting_bnfs: BNF_Def.bnf list,
+ fp_nesting_bnfs: BNF_Def.bnf list,
+ live_nesting_bnfs: BNF_Def.bnf list,
ctrXs_Tss: typ list list,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
@@ -264,8 +264,8 @@
fp_res: fp_result,
pre_bnf: bnf,
absT_info: absT_info,
- nested_bnfs: bnf list,
- nesting_bnfs: bnf list,
+ fp_nesting_bnfs: bnf list,
+ live_nesting_bnfs: bnf list,
ctrXs_Tss: typ list list,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
@@ -280,8 +280,8 @@
rel_injects: thm list,
rel_distincts: thm list};
-fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, nested_bnfs,
- nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
+fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs,
+ live_nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
co_inducts, co_rec_thms, disc_co_recs, sel_co_recss, rel_injects, rel_distincts} : fp_sugar) =
{T = Morphism.typ phi T,
BT = Morphism.typ phi BT,
@@ -291,8 +291,8 @@
fp_res_index = fp_res_index,
pre_bnf = morph_bnf phi pre_bnf,
absT_info = morph_absT_info phi absT_info,
- nested_bnfs = map (morph_bnf phi) nested_bnfs,
- nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
+ fp_nesting_bnfs = map (morph_bnf phi) fp_nesting_bnfs,
+ live_nesting_bnfs = map (morph_bnf phi) live_nesting_bnfs,
ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
ctr_defs = map (Morphism.thm phi) ctr_defs,
ctr_sugar = morph_ctr_sugar phi ctr_sugar,
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Jun 27 10:11:44 2014 +0200
@@ -79,9 +79,9 @@
{corec: term,
disc_exhausts: thm list,
sel_defs: thm list,
- nested_maps: thm list,
- nested_map_idents: thm list,
- nested_map_comps: thm list,
+ fp_nesting_maps: thm list,
+ fp_nesting_map_idents: thm list,
+ fp_nesting_map_comps: thm list,
ctr_specs: corec_ctr_spec list};
exception NOT_A_MAP of term;
@@ -375,7 +375,7 @@
let
val thy = Proof_Context.theory_of lthy0;
- val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs,
+ val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs,
common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0;
@@ -464,9 +464,11 @@
co_rec_thms = corec_thms, disc_co_recs = disc_corecs,
sel_co_recss = sel_corecss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
{corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec, disc_exhausts = disc_exhausts,
- sel_defs = sel_defs, 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,
+ sel_defs = sel_defs,
+ fp_nesting_maps = maps (map_thms_of_typ lthy o T_of_bnf) fp_nesting_bnfs,
+ fp_nesting_map_idents =
+ map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) fp_nesting_bnfs,
+ fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs,
ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms disc_corecs
sel_corecss};
in
@@ -1173,8 +1175,8 @@
|> single
end;
- fun prove_sel ({sel_defs, nested_maps, nested_map_idents, nested_map_comps, ctr_specs, ...}
- : corec_spec) (disc_eqns : coeqn_data_disc list) excludesss
+ fun prove_sel ({sel_defs, fp_nesting_maps, fp_nesting_map_idents, fp_nesting_map_comps,
+ ctr_specs, ...} : corec_spec) (disc_eqns : coeqn_data_disc list) excludesss
({fun_name, fun_T, fun_args, ctr, sel, rhs_term, code_rhs_opt, eqn_pos, ...}
: coeqn_data_sel) =
let
@@ -1195,8 +1197,8 @@
|> curry Logic.list_all (map dest_Free fun_args);
val (distincts, _, _, sel_splits, sel_split_asms) = case_thms_of_term lthy rhs_term;
in
- mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_maps
- nested_map_idents nested_map_comps sel_corec k m excludesss
+ mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms fp_nesting_maps
+ fp_nesting_map_idents fp_nesting_map_comps sel_corec k m excludesss
|> K |> Goal.prove_sorry lthy [] [] goal
|> Thm.close_derivation
|> `(is_some code_rhs_opt ? fold_thms lthy sel_defs) (*mildly too aggressive*)
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Jun 27 10:11:44 2014 +0200
@@ -79,8 +79,8 @@
type rec_spec =
{recx: term,
- nested_map_idents: thm list,
- nested_map_comps: thm list,
+ fp_nesting_map_idents: thm list,
+ fp_nesting_map_comps: thm list,
ctr_specs: rec_ctr_spec list};
type basic_lfp_sugar =
@@ -135,7 +135,7 @@
let
val thy = Proof_Context.theory_of lthy0;
- val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, nested_map_idents, nested_map_comps,
+ val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, fp_nesting_map_idents, fp_nesting_map_comps,
common_induct, n2m, lthy) =
get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0;
@@ -195,7 +195,7 @@
fun mk_spec ctr_offset
({T, fp_res_index, ctr_sugar = {ctrs, ...}, recx, rec_thms, ...} : basic_lfp_sugar) =
{recx = mk_co_rec thy Least_FP (substAT T) perm_Cs' recx,
- nested_map_idents = nested_map_idents, nested_map_comps = nested_map_comps,
+ fp_nesting_map_idents = fp_nesting_map_idents, fp_nesting_map_comps = fp_nesting_map_comps,
ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs rec_thms};
in
((n2m, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, common_induct, inducts), lthy)
@@ -464,8 +464,8 @@
val defs = build_defs lthy nonexhaustive bs mxs funs_data rec_specs has_call;
- fun prove lthy' def_thms' ({ctr_specs, nested_map_idents, nested_map_comps, ...} : rec_spec)
- (fun_data : eqn_data list) =
+ fun prove lthy' def_thms' ({ctr_specs, fp_nesting_map_idents, fp_nesting_map_comps, ...}
+ : rec_spec) (fun_data : eqn_data list) =
let
val js =
find_indices (op = o pairself (fn {fun_name, ctr, ...} => (fun_name, ctr)))
@@ -477,8 +477,8 @@
|> map_filter (try (fn (x, [y]) =>
(#fun_name x, #user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
|> map2 (fn j => fn (fun_name, user_eqn, num_extra_args, rec_thm) =>
- mk_primrec_tac lthy' num_extra_args nested_map_idents nested_map_comps def_thms
- rec_thm
+ mk_primrec_tac lthy' num_extra_args fp_nesting_map_idents fp_nesting_map_comps
+ def_thms rec_thm
|> K |> Goal.prove_sorry lthy' [] [] user_eqn
(* for code extraction from proof terms: *)
|> singleton (Proof_Context.export lthy' lthy)
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Jun 27 10:11:44 2014 +0200
@@ -29,7 +29,7 @@
fun get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0 =
let
val ((missing_arg_Ts, perm0_kks,
- fp_sugars as {nested_bnfs, common_co_inducts = [common_induct], ...} :: _,
+ fp_sugars as {fp_nesting_bnfs, common_co_inducts = [common_induct], ...} :: _,
(lfp_sugar_thms, _)), lthy) =
nested_to_mutual_fps Least_FP bs arg_Ts callers callssss0 lthy0;
@@ -47,11 +47,12 @@
val ctrXs_Tsss = map #ctrXs_Tss fp_sugars;
val fun_arg_Tssss = map (map (map zip_recT)) ctrXs_Tsss;
- val nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs;
- val nested_map_comps = map map_comp_of_bnf nested_bnfs;
+ val fp_nesting_map_idents =
+ map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) fp_nesting_bnfs;
+ val fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs;
in
(missing_arg_Ts, perm0_kks, map3 basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars,
- nested_map_idents, nested_map_comps, common_induct, is_some lfp_sugar_thms, lthy)
+ fp_nesting_map_idents, fp_nesting_map_comps, common_induct, is_some lfp_sugar_thms, lthy)
end;
exception NOT_A_MAP of term;
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Jun 27 10:11:44 2014 +0200
@@ -66,12 +66,12 @@
val rec_o_map_simp_thms =
@{thms o_def id_def case_prod_app case_sum_map_sum case_prod_map_prod BNF_Comp.id_bnf_comp_def};
-fun mk_rec_o_map_tac ctxt rec_def pre_map_defs nesting_map_idents abs_inverses ctor_rec_o_map =
+fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_idents abs_inverses ctor_rec_o_map =
unfold_thms_tac ctxt [rec_def] THEN
HEADGOAL (rtac (ctor_rec_o_map RS trans)) THEN
PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion) THEN
HEADGOAL (asm_simp_tac (ss_only (pre_map_defs @
- distinct Thm.eq_thm_prop (nesting_map_idents @ abs_inverses) @ rec_o_map_simp_thms) ctxt));
+ distinct Thm.eq_thm_prop (live_nesting_map_idents @ abs_inverses) @ rec_o_map_simp_thms) ctxt));
val size_o_map_simp_thms = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
@@ -82,8 +82,8 @@
IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl));
fun generate_lfp_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs),
- fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_map_thms = ctor_rec_o_maps, ...}, nested_bnfs,
- nesting_bnfs, ...} : fp_sugar) :: _) lthy0 =
+ fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_map_thms = ctor_rec_o_maps, ...}, fp_nesting_bnfs,
+ live_nesting_bnfs, ...} : fp_sugar) :: _) lthy0 =
let
val data = Data.get (Context.Proof lthy0);
@@ -221,7 +221,7 @@
|> map_filter (try (fn (Spec_Rules.Equational, (_, [thm])) => thm)));
val nested_size_maps = map (pointfill lthy2) nested_size_o_maps @ nested_size_o_maps;
- val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ nested_bnfs @ nesting_bnfs)
+ val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ fp_nesting_bnfs @ live_nesting_bnfs)
|> distinct Thm.eq_thm_prop;
fun derive_size_simp size_def' simp0 =
@@ -258,7 +258,7 @@
let
val pre_bnfs = map #pre_bnf fp_sugars;
val pre_map_defs = map map_def_of_bnf pre_bnfs;
- val nesting_map_idents = map map_ident_of_bnf nesting_bnfs;
+ val live_nesting_map_idents = map map_ident_of_bnf live_nesting_bnfs;
val abs_inverses = map (#abs_inverse o #absT_info) fp_sugars;
val rec_defs = map #co_rec_def fp_sugars;
@@ -303,7 +303,7 @@
val rec_o_map_thms =
map3 (fn goal => fn rec_def => fn ctor_rec_o_map =>
Goal.prove lthy2 [] [] goal (fn {context = ctxt, ...} =>
- mk_rec_o_map_tac ctxt rec_def pre_map_defs nesting_map_idents abs_inverses
+ mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_idents abs_inverses
ctor_rec_o_map)
|> Thm.close_derivation)
rec_o_map_goals rec_defs ctor_rec_o_maps;