# HG changeset patch # User blanchet # Date 1393847300 -3600 # Node ID bddaada24074c3c731e23c5403cb9f0455d77559 # Parent 98ad5680173a3a7d5ca3aa0979a66e6ed34b3c1b got rid of automatically generated fold constant and theorems (to reduce overhead) diff -r 98ad5680173a -r bddaada24074 src/HOL/BNF_LFP.thy --- a/src/HOL/BNF_LFP.thy Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/BNF_LFP.thy Mon Mar 03 12:48:20 2014 +0100 @@ -264,4 +264,6 @@ hide_fact (open) id_transfer +datatype_new 'a F = F 'a + end diff -r 98ad5680173a -r bddaada24074 src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Mon Mar 03 12:48:20 2014 +0100 @@ -21,7 +21,7 @@ exception BAD_DEAD of typ * typ - val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) -> + val bnf_of_typ: BNF_Def.inline_policy -> (binding -> binding) -> ((string * sort) list list -> (string * sort) list) -> (string * sort) list -> (string * sort) list -> typ -> (comp_cache * unfold_set) * Proof.context -> (BNF_Def.bnf * (typ list * typ list)) * ((comp_cache * unfold_set) * Proof.context) diff -r 98ad5680173a -r bddaada24074 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Mar 03 12:48:20 2014 +0100 @@ -41,17 +41,17 @@ val nesty_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 * thm list list * Args.src list) + (thm list * thm * Args.src list) * (thm list list * Args.src list) val morph_lfp_sugar_thms: morphism -> lfp_sugar_thms -> lfp_sugar_thms val transfer_lfp_sugar_thms: Proof.context -> lfp_sugar_thms -> lfp_sugar_thms type gfp_sugar_thms = ((thm list * thm) 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 * thm list list * Args.src list) - * (thm list list list * thm list list list * Args.src list) + * (thm list list * Args.src list) + * (thm list list * Args.src list) + * (thm list list * Args.src list) + * (thm list list list * Args.src list) val morph_gfp_sugar_thms: morphism -> gfp_sugar_thms -> gfp_sugar_thms val transfer_gfp_sugar_thms: Proof.context -> gfp_sugar_thms -> gfp_sugar_thms @@ -320,11 +320,11 @@ fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p; type lfp_sugar_thms = - (thm list * thm * Args.src list) * (thm list list * thm list list * Args.src list) + (thm list * thm * Args.src list) * (thm list list * Args.src list); -fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (foldss, recss, iter_attrs)) = +fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (recss, iter_attrs)) = ((map (Morphism.thm phi) inducts, Morphism.thm phi induct, induct_attrs), - (map (map (Morphism.thm phi)) foldss, map (map (Morphism.thm phi)) recss, iter_attrs)) + (map (map (Morphism.thm phi)) recss, iter_attrs)) : lfp_sugar_thms; val transfer_lfp_sugar_thms = @@ -332,24 +332,20 @@ type gfp_sugar_thms = ((thm list * thm) 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 * thm list list * Args.src list) - * (thm list list list * thm list list list * Args.src list); + * (thm list list * Args.src list) + * (thm list list * Args.src list) + * (thm list list * Args.src list) + * (thm list list list * Args.src list); fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs), - (unfoldss, corecss, coiter_attrs), (disc_unfoldss, disc_corecss, disc_iter_attrs), - (disc_unfold_iffss, disc_corec_iffss, disc_iter_iff_attrs), - (sel_unfoldsss, sel_corecsss, sel_iter_attrs)) = + (corecss, coiter_attrs), (disc_corecss, disc_iter_attrs), + (disc_corec_iffss, disc_iter_iff_attrs), (sel_corecsss, sel_iter_attrs)) = ((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs, coinduct_attrs), - (map (map (Morphism.thm phi)) unfoldss, map (map (Morphism.thm phi)) corecss, coiter_attrs), - (map (map (Morphism.thm phi)) disc_unfoldss, map (map (Morphism.thm phi)) disc_corecss, - disc_iter_attrs), - (map (map (Morphism.thm phi)) disc_unfold_iffss, map (map (Morphism.thm phi)) disc_corec_iffss, - disc_iter_iff_attrs), - (map (map (map (Morphism.thm phi))) sel_unfoldsss, - map (map (map (Morphism.thm phi))) sel_corecsss, sel_iter_attrs)) : gfp_sugar_thms; + (map (map (Morphism.thm phi)) corecss, coiter_attrs), + (map (map (Morphism.thm phi)) disc_corecss, disc_iter_attrs), + (map (map (Morphism.thm phi)) disc_corec_iffss, disc_iter_iff_attrs), + (map (map (map (Morphism.thm phi))) sel_corecsss, sel_iter_attrs)) : gfp_sugar_thms; val transfer_gfp_sugar_thms = morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of; @@ -386,7 +382,7 @@ |> mk_Freessss "y" (map (map (map tl)) z_Tssss); val zssss = map2 (map2 (map2 cons)) zssss_hd zssss_tl; in - ([(g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)], lthy) + ([(h_Tss, z_Tssss, hss, zssss)], lthy) end; (*avoid "'a itself" arguments in coiterators*) @@ -425,23 +421,17 @@ (q_Tssss, f_Tsss, f_Tssss, f_repTs) end; - val (r_Tssss, g_Tsss, g_Tssss, unfold_types) = mk_types un_fold_of; val (s_Tssss, h_Tsss, h_Tssss, corec_types) = mk_types co_rec_of; - val ((((Free (z, _), cs), pss), gssss), lthy) = + val ((((((Free (z, _), cs), pss), sssss), hssss_hd), hssss_tl), lthy) = lthy |> yield_singleton (mk_Frees "z") dummyT ||>> mk_Frees "a" Cs ||>> mk_Freess "p" p_Tss - ||>> mk_Freessss "g" g_Tssss; - val rssss = map (map (map (fn [] => []))) r_Tssss; - - val hssss_hd = map2 (map2 (map2 (fn T :: _ => fn [g] => retype_free T g))) h_Tssss gssss; - val ((sssss, hssss_tl), lthy) = - lthy - |> mk_Freessss "q" s_Tssss + ||>> mk_Freessss "q" s_Tssss + ||>> mk_Freessss "g" h_Tssss ||>> mk_Freessss "h" (map (map (map tl)) h_Tssss); - val hssss = map2 (map2 (map2 cons)) hssss_hd hssss_tl; + val hssss = map2 (map2 (map2 append)) hssss_hd hssss_tl; val cpss = map2 (map o rapp) cs pss; @@ -460,10 +450,9 @@ val cqfsss = map3 (map3 (map3 build_dtor_coiter_arg)) f_Tsss cqssss cfssss; in (pfss, cqfsss) end; - val unfold_args = mk_args rssss gssss g_Tsss; val corec_args = mk_args sssss hssss h_Tsss; in - ((z, cs, cpss, [(unfold_args, unfold_types), (corec_args, corec_types)]), lthy) + ((z, cs, cpss, [(corec_args, corec_types)]), lthy) end; fun mk_co_iters_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_iterss0 lthy = @@ -518,7 +507,7 @@ fun define_iters iterNs iter_args_typess' mk_binding fpTs Cs reps ctor_iters lthy = let val nn = length fpTs; - val fpT = domain_type (snd (strip_typeN nn (fastype_of (un_fold_of ctor_iters)))); + val fpT = domain_type (snd (strip_typeN nn (fastype_of (co_rec_of ctor_iters)))); fun generate_iter pre (_, _, fss, xssss) ctor_iter = let val ctor_iter_absTs = map domain_type (fst (strip_typeN nn (fastype_of ctor_iter))) in @@ -549,15 +538,15 @@ (map3 generate_coiter coiterNs coiter_args_typess' dtor_coiters) lthy end; -fun derive_induct_iters_thms_for_types pre_bnfs [fold_args_types, rec_args_types] ctor_induct - ctor_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses - fp_type_definitions abs_inverses ctrss ctr_defss iterss iter_defss lthy = +fun derive_induct_iters_thms_for_types pre_bnfs [rec_args_types] ctor_induct ctor_iter_thmss + nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions abs_inverses + ctrss ctr_defss iterss iter_defss lthy = let val iterss' = transpose iterss; val iter_defss' = transpose iter_defss; - val [folds, recs] = iterss'; - val [fold_defs, rec_defs] = iter_defss'; + val [recs] = iterss'; + val [rec_defs] = iter_defss'; val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss; @@ -704,15 +693,14 @@ map2 (map2 prove) goalss tacss end; - val fold_thmss = mk_iter_thmss fold_args_types folds fold_defs (map un_fold_of ctor_iter_thmss); val rec_thmss = mk_iter_thmss rec_args_types recs rec_defs (map co_rec_of ctor_iter_thmss); in ((induct_thms, induct_thm, [induct_case_names_attr]), - (fold_thmss, rec_thmss, code_nitpicksimp_attrs @ simp_attrs)) + (rec_thmss, code_nitpicksimp_attrs @ simp_attrs)) end; fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss, - coiters_args_types as [((pgss, crgsss), _), ((phss, cshsss), _)]) + coiters_args_types as [((phss, cshsss), _)]) dtor_coinduct dtor_injects dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list) coiterss coiter_defss export_args lthy = @@ -726,7 +714,7 @@ val coiterss' = transpose coiterss; val coiter_defss' = transpose coiter_defss; - val [unfold_defs, corec_defs] = coiter_defss'; + val [corec_defs] = coiter_defss'; val nn = length pre_bnfs; @@ -840,10 +828,10 @@ fun mk_maybe_not pos = not pos ? HOLogic.mk_not; - val fcoiterss' as [gunfolds, hcorecs] = + val fcoiterss' as [hcorecs] = map2 (fn (pfss, _) => map (lists_bmoc pfss)) (map fst coiters_args_types) coiterss'; - val (unfold_thmss, corec_thmss) = + val corec_thmss = let fun mk_goal pfss c cps fcoiter n k ctr m cfs' = fold_rev (fold_rev Logic.all) ([c] :: pfss) @@ -869,50 +857,37 @@ cqf end; - val crgsss' = map (map (map (build_coiter (un_fold_of fcoiterss') (K I) (K I)))) crgsss; val cshsss' = map (map (map (build_coiter (co_rec_of fcoiterss') (curry mk_sumT) (tack z)))) cshsss; - val unfold_goalss = map8 (map4 oooo mk_goal pgss) cs cpss gunfolds ns kss ctrss mss crgsss'; - val corec_goalss = map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss'; + val goalss = map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss'; - val unfold_tacss = - map4 (map ooo mk_coiter_tac unfold_defs nesting_map_idents) - (map un_fold_of ctor_dtor_coiter_thmss) pre_map_defs abs_inverses ctr_defss; - val corec_tacss = + val tacss = map4 (map ooo mk_coiter_tac corec_defs nesting_map_idents) (map co_rec_of ctor_dtor_coiter_thmss) pre_map_defs abs_inverses ctr_defss; fun prove goal tac = Goal.prove_sorry lthy [] [] goal (tac o #context) |> Thm.close_derivation; - - val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss; - val corec_thmss = - map2 (map2 prove) corec_goalss corec_tacss - |> map (map (unfold_thms lthy @{thms case_sum_if})); in - (unfold_thmss, corec_thmss) + map2 (map2 prove) goalss tacss + |> map (map (unfold_thms lthy @{thms case_sum_if})) end; - val (disc_unfold_iff_thmss, disc_corec_iff_thmss) = + val disc_corec_iff_thmss = let fun mk_goal c cps fcoiter n k disc = mk_Trueprop_eq (disc $ (fcoiter $ c), if n = 1 then @{const True} else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps)); - val unfold_goalss = map6 (map2 oooo mk_goal) cs cpss gunfolds ns kss discss; - val corec_goalss = map6 (map2 oooo mk_goal) cs cpss hcorecs ns kss discss; + val goalss = map6 (map2 oooo mk_goal) cs cpss hcorecs ns kss discss; fun mk_case_split' cp = Drule.instantiate' [] [SOME (certify lthy cp)] @{thm case_split}; val case_splitss' = map (map mk_case_split') cpss; - val unfold_tacss = - map3 (map oo mk_disc_coiter_iff_tac) case_splitss' unfold_thmss disc_thmsss; - val corec_tacss = - map3 (map oo mk_disc_coiter_iff_tac) case_splitss' corec_thmss disc_thmsss; + val tacss = map3 (map oo mk_disc_coiter_iff_tac) case_splitss' corec_thmss disc_thmsss; fun prove goal tac = Goal.prove_sorry lthy [] [] goal (tac o #context) @@ -923,12 +898,11 @@ fun proves [_] [_] = [] | proves goals tacs = map2 prove goals tacs; in - (map2 proves unfold_goalss unfold_tacss, map2 proves corec_goalss corec_tacss) + map2 proves goalss tacss end; fun mk_disc_coiter_thms coiters discIs = map (op RS) (coiters ~~ discIs); - val disc_unfold_thmss = map2 mk_disc_coiter_thms unfold_thmss discIss; val disc_corec_thmss = map2 mk_disc_coiter_thms corec_thmss discIss; fun mk_sel_coiter_thm coiter_thm sel sel_thm = @@ -946,7 +920,6 @@ fun mk_sel_coiter_thms coiter_thmss = map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss; - 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)); @@ -959,10 +932,10 @@ coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs; in ((coinduct_thms_pairs, coinduct_case_attrs), - (unfold_thmss, corec_thmss, code_nitpicksimp_attrs), - (disc_unfold_thmss, disc_corec_thmss, []), - (disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs), - (sel_unfold_thmsss, sel_corec_thmsss, simp_attrs)) + (corec_thmss, code_nitpicksimp_attrs), + (disc_corec_thmss, []), + (disc_corec_iff_thmss, simp_attrs), + (sel_corec_thmsss, simp_attrs)) end; fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp @@ -1368,11 +1341,9 @@ (wrap_ctrs #> derive_maps_sets_rels ##>> - (if fp = Least_FP then - define_iters [foldN, recN] (the iters_args_types) mk_binding fpTs Cs reps xtor_co_iters - else - define_coiters [unfoldN, corecN] (the coiters_args_types) mk_binding fpTs Cs abss - xtor_co_iters) + (if fp = Least_FP then define_iters [recN] (the iters_args_types) mk_binding fpTs Cs reps + else define_coiters [corecN] (the coiters_args_types) mk_binding fpTs Cs abss) + [co_rec_of xtor_co_iters] #> massage_res, lthy') end; @@ -1381,16 +1352,15 @@ |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list4 o split_list) o split_list; - fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) un_folds co_recs - mapsx rel_injects rel_distincts setss = - injects @ distincts @ case_thms @ co_recs @ un_folds @ mapsx @ rel_injects @ rel_distincts - @ flat setss; + fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs mapsx rel_injects + rel_distincts setss = + injects @ distincts @ case_thms @ co_recs @ mapsx @ rel_injects @ rel_distincts @ flat setss; fun derive_note_induct_iters_thms_for_types ((((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, rec_thmss, iter_attrs)) = + val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, iter_attrs)) = 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 abs_inverses type_definitions abs_inverses ctrss ctr_defss iterss iter_defss lthy; @@ -1398,26 +1368,24 @@ val induct_type_attr = Attrib.internal o K o Induct.induct_type; val simp_thmss = - map7 mk_simp_thms ctr_sugars fold_thmss rec_thmss mapss rel_injects rel_distincts setss; + map6 mk_simp_thms ctr_sugars rec_thmss mapss rel_injects rel_distincts setss; val common_notes = (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else []) |> massage_simple_notes fp_common_name; val notes = - [(foldN, fold_thmss, K iter_attrs), - (inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]), + [(inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]), (recN, rec_thmss, K iter_attrs), (simpsN, simp_thmss, K [])] |> massage_multi_notes; in lthy - |> Spec_Rules.add Spec_Rules.Equational (map un_fold_of iterss, flat fold_thmss) |> Spec_Rules.add Spec_Rules.Equational (map co_rec_of iterss, flat rec_thmss) |> Local_Theory.notes (common_notes @ notes) |> snd |> register_fp_sugars Xs Least_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars iterss mapss [induct_thm] (map single induct_thms) - (transpose [fold_thmss, rec_thmss]) (replicate nn []) (replicate nn []) + (map single rec_thmss) (replicate nn []) (replicate nn []) end; fun derive_note_coinduct_coiters_thms_for_types @@ -1426,16 +1394,15 @@ let val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)], coinduct_attrs), - (unfold_thmss, corec_thmss, coiter_attrs), - (disc_unfold_thmss, disc_corec_thmss, disc_coiter_attrs), - (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs), - (sel_unfold_thmsss, sel_corec_thmsss, sel_coiter_attrs)) = + (corec_thmss, coiter_attrs), + (disc_corec_thmss, disc_coiter_attrs), + (disc_corec_iff_thmss, disc_coiter_iff_attrs), + (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 Xs ctrXs_Tsss kss mss ns abs_inverses abs_inverses I 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; @@ -1443,8 +1410,7 @@ val flat_coiter_thms = append oo append; val simp_thmss = - map7 mk_simp_thms ctr_sugars - (map3 flat_coiter_thms disc_unfold_thmss disc_unfold_iff_thmss sel_unfold_thmss) + map6 mk_simp_thms ctr_sugars (map3 flat_coiter_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss) mapss rel_injects rel_distincts setss; @@ -1462,13 +1428,9 @@ (corecN, corec_thmss, K coiter_attrs), (disc_corecN, disc_corec_thmss, K disc_coiter_attrs), (disc_corec_iffN, disc_corec_iff_thmss, K disc_coiter_iff_attrs), - (disc_unfoldN, disc_unfold_thmss, K disc_coiter_attrs), - (disc_unfold_iffN, disc_unfold_iff_thmss, K disc_coiter_iff_attrs), (sel_corecN, sel_corec_thmss, K sel_coiter_attrs), - (sel_unfoldN, sel_unfold_thmss, K sel_coiter_attrs), (simpsN, simp_thmss, K []), - (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs), - (unfoldN, unfold_thmss, K coiter_attrs)] + (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs)] |> massage_multi_notes; (* TODO: code theorems *) @@ -1477,14 +1439,12 @@ [flat sel_thmss, flat ctr_thmss] in lthy - |> add_spec_rules un_fold_of sel_unfold_thmss unfold_thmss |> add_spec_rules co_rec_of sel_corec_thmss corec_thmss |> Local_Theory.notes (common_notes @ notes) |> snd |> register_fp_sugars Xs Greatest_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm] - (transpose [coinduct_thms, strong_coinduct_thms]) - (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss]) - (transpose [sel_unfold_thmsss, sel_corec_thmsss]) + (transpose [coinduct_thms, strong_coinduct_thms]) (map single corec_thmss) + (map single disc_corec_thmss) (map single sel_corec_thmsss) end; val lthy'' = lthy' diff -r 98ad5680173a -r bddaada24074 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Mar 03 12:48:20 2014 +0100 @@ -248,53 +248,47 @@ val ((co_iterss, co_iter_defss), lthy) = fold_map2 (fn b => if fp = Least_FP then - define_iters [foldN, recN] (the iters_args_types) (mk_binding b) fpTs Cs reps + define_iters [recN] (the iters_args_types) (mk_binding b) fpTs Cs reps else - define_coiters [unfoldN, corecN] (the coiters_args_types) (mk_binding b) fpTs Cs abss) - fp_bs xtor_co_iterss lthy + define_coiters [corecN] (the coiters_args_types) (mk_binding b) fpTs Cs abss) + fp_bs (map (single o co_rec_of) xtor_co_iterss) lthy |>> split_list; - 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) = + val ((common_co_inducts, co_inductss, co_rec_thmss, disc_corec_thmss, 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 fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss co_iterss co_iter_defss lthy - |> `(fn ((inducts, induct, _), (fold_thmss, rec_thmss, _)) => - ([induct], [inducts], fold_thmss, rec_thmss, replicate nn [], - replicate nn [], replicate nn [], replicate nn [])) + |> `(fn ((inducts, induct, _), (rec_thmss, _)) => + ([induct], [inducts], rec_thmss, 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 dtor_injects dtor_ctors xtor_co_iter_thmss 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_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy - |> `(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)) + |> `(fn ((coinduct_thms_pairs, _), (corec_thmss, _), (disc_corec_thmss, _), _, + (sel_corec_thmsss, _)) => + (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss, + disc_corec_thmss, 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 T X kk pre_bnf absT_info ctrXs_Tss 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 = + co_inducts co_rec_thms disc_corec_thms sel_corec_thmss = {T = T, 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_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]} + co_iter_thmss = [co_rec_thms], disc_co_iterss = [disc_corec_thms], + sel_co_itersss = [sel_corec_thmss]} |> morph_fp_sugar phi; val target_fp_sugars = - map17 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss 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; + map14 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars + co_iterss mapss (transpose co_inductss) co_rec_thmss disc_corec_thmss sel_corec_thmsss; val n2m_sugar = (target_fp_sugars, fp_sugar_thms); in diff -r 98ad5680173a -r bddaada24074 src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Mon Mar 03 12:48:20 2014 +0100 @@ -34,7 +34,6 @@ val permute_args: int -> term -> term val mk_partial_compN: int -> typ -> term -> term - val mk_partial_comp: typ -> typ -> term -> term val mk_compN: int -> typ list -> term * term -> term val mk_comp: typ list -> term * term -> term @@ -93,13 +92,10 @@ fun permute_args n t = list_comb (t, map Bound (0 :: (n downto 1))) |> fold (K (Term.abs (Name.uu, dummyT))) (0 upto n); -fun mk_partial_comp gT fT g = fst (Term.dest_comb (HOLogic.mk_comp (g, Free (Name.uu, fT)))); +fun mk_partial_comp fT g = fst (Term.dest_comb (HOLogic.mk_comp (g, Free (Name.uu, fT)))); fun mk_partial_compN 0 _ g = g - | mk_partial_compN n fT g = - let val g' = mk_partial_compN (n - 1) (range_type fT) g in - mk_partial_comp (fastype_of g') fT g' - end; + | mk_partial_compN n fT g = mk_partial_comp fT (mk_partial_compN (n - 1) (range_type fT) g); fun mk_compN n bound_Ts (g, f) = let val typof = curry fastype_of1 bound_Ts in diff -r 98ad5680173a -r bddaada24074 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 03 12:48:20 2014 +0100 @@ -62,8 +62,6 @@ val ctor_relN: string val ctor_set_inclN: string val ctor_set_set_inclN: string - val disc_unfoldN: string - val disc_unfold_iffN: string val disc_corecN: string val disc_corec_iffN: string val dtorN: string @@ -87,7 +85,6 @@ val dtor_unfold_transferN: string val dtor_unfold_uniqueN: string val exhaustN: string - val foldN: string val hsetN: string val hset_recN: string val inductN: string @@ -108,7 +105,6 @@ val sel_corecN: string val set_inclN: string val set_set_inclN: string - val sel_unfoldN: string val setN: string val simpsN: string val strTN: string @@ -116,7 +112,6 @@ val strong_coinductN: string val sum_bdN: string val sum_bdTN: string - val unfoldN: string val uniqueN: string (* TODO: Don't index set facts. Isabelle packages traditionally generate uniform names. *) @@ -232,7 +227,9 @@ rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm}; fun un_fold_of [f, _] = f; -fun co_rec_of [_, r] = r; + +fun co_rec_of [r] = r + | co_rec_of [_, r] = r; fun time ctxt timer msg = (if Config.get ctxt bnf_timing then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^ @@ -325,10 +322,8 @@ val caseN = "case" val discN = "disc" -val disc_unfoldN = discN ^ "_" ^ unfoldN val disc_corecN = discN ^ "_" ^ corecN val iffN = "_iff" -val disc_unfold_iffN = discN ^ "_" ^ unfoldN ^ iffN val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN val distinctN = "distinct" val rel_distinctN = relN ^ "_" ^ distinctN @@ -337,7 +332,6 @@ val rel_coinductN = relN ^ "_" ^ coinductN val rel_inductN = relN ^ "_" ^ inductN val selN = "sel" -val sel_unfoldN = selN ^ "_" ^ unfoldN val sel_corecN = selN ^ "_" ^ corecN fun co_prefix fp = (if fp = Greatest_FP then "co" else ""); diff -r 98ad5680173a -r bddaada24074 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Mar 03 12:48:20 2014 +0100 @@ -163,7 +163,7 @@ val all_notes = (case lfp_sugar_thms of NONE => [] - | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, rec_thmss, _)) => + | SOME ((induct_thms, induct_thm, induct_attrs), (rec_thmss, _)) => let val common_notes = (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else []) @@ -172,8 +172,7 @@ ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])])); val notes = - [(foldN, fold_thmss, []), - (inductN, map single induct_thms, induct_attrs), + [(inductN, map single induct_thms, induct_attrs), (recN, rec_thmss, code_nitpicksimp_simp_attrs)] |> filter_out (null o #2) |> maps (fn (thmN, thmss, attrs) => diff -r 98ad5680173a -r bddaada24074 src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_util.ML Mon Mar 03 12:48:20 2014 +0100 @@ -35,19 +35,6 @@ 'o) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list - val map15: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n -> - 'o -> 'p) -> - 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> - 'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list - val map16: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n -> - 'o -> 'p -> 'q) -> - 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> - 'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list -> 'q list - val map17: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n -> - 'o -> 'p -> 'q -> 'r) -> - 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> - 'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list -> - 'q list -> 'r list val fold_map4: ('a -> 'b -> 'c -> 'd -> 'e -> 'f * 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e -> 'f list * 'e val fold_map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g * 'f) -> @@ -216,29 +203,6 @@ map14 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s | map14 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; -fun map15 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = [] - | map15 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) - (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s) = - f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 :: - map15 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s - | map15 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun map16 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = [] - | map16 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) - (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s) - (x16::x16s) = - f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 :: - map16 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s x16s - | map16 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun map17 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = [] - | map17 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) - (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s) - (x16::x16s) (x17::x17s) = - f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 :: - map17 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s x16s x17s - | map17 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - fun fold_map4 _ [] [] [] [] acc = ([], acc) | fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc = let