# HG changeset patch # User blanchet # Date 1403856704 -7200 # Node ID 5004aca2082165b054c47902033ffa7dfdb73ba0 # Parent 42eede5610a91f5b6373a76299063042baec14f6 tuned variable names diff -r 42eede5610a9 -r 5004aca20821 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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; diff -r 42eede5610a9 -r 5004aca20821 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- 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 diff -r 42eede5610a9 -r 5004aca20821 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- 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; diff -r 42eede5610a9 -r 5004aca20821 src/HOL/Tools/BNF/bnf_fp_util.ML --- 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, diff -r 42eede5610a9 -r 5004aca20821 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- 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*) diff -r 42eede5610a9 -r 5004aca20821 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- 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) diff -r 42eede5610a9 -r 5004aca20821 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- 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; diff -r 42eede5610a9 -r 5004aca20821 src/HOL/Tools/BNF/bnf_lfp_size.ML --- 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;