# HG changeset patch # User blanchet # Date 1410177782 -7200 # Node ID d81d39278d483f1315fda5a4c6036b9afe84a669 # Parent e02d867dfbc6655288c866b52282615fc8609f7d tuning diff -r e02d867dfbc6 -r d81d39278d48 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 08 14:03:02 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 08 14:03:02 2014 +0200 @@ -119,7 +119,7 @@ fold_map3 (define_co_rec_as Least_FP Cs) fpTs bs rhss lthy end; -fun mk_split_rec_thmss ctxt fpTs ctrss rec0_thmss (recs as rec1 :: _) rec_defs = +fun mk_split_rec_thmss ctxt Xs fpTs ctr_Tsss ctrss rec0_thmss (recs as rec1 :: _) rec_defs = let val f_Ts = binder_fun_types (fastype_of rec1); val (fs, _) = mk_Frees "f" f_Ts ctxt; @@ -136,23 +136,20 @@ val xg = Term.list_comb (g, map Bound (n - 1 downto 0)); in frec $ xg end; - fun mk_rec_arg_arg g_T g = - g :: (if exists_subtype_in fpTs g_T then [mk_rec_call g 0 g_T] else []); + fun mk_rec_arg_arg ctr_T g = + g :: (if exists_subtype_in fpTs ctr_T then [mk_rec_call g 0 ctr_T] else []); - fun mk_goal frec ctr f = + fun mk_goal frec ctr_Ts ctr f = let - val g_Ts = binder_types (fastype_of ctr); - val (gs, _) = mk_Frees "g" g_Ts ctxt; + val (gs, _) = mk_Frees "g" ctr_Ts ctxt; val gctr = Term.list_comb (ctr, gs); - val fgs = flat_rec_arg_args (map2 mk_rec_arg_arg g_Ts gs); + val fgs = flat_rec_arg_args (map2 mk_rec_arg_arg ctr_Ts gs); in fold_rev (fold_rev Logic.all) [fs, gs] (mk_Trueprop_eq (frec $ gctr, Term.list_comb (f, fgs))) end; - fun mk_goals ctrs fs frec = map2 (mk_goal frec) ctrs fs; - - val goalss = map3 mk_goals ctrss fss frecs; + val goalss = map4 (map3 o mk_goal) frecs ctr_Tsss ctrss fss; fun tac ctxt = unfold_thms_tac ctxt (@{thms o_apply fst_conv snd_conv} @ rec_defs @ flat rec0_thmss) THEN @@ -165,7 +162,8 @@ map (map prove) goalss end; -fun define_split_rec_derive_induct_rec_thms fpTs ctrss inducts induct recs0 rec_thmss lthy = +fun define_split_rec_derive_induct_rec_thms Xs fpTs ctr_Tsss ctrss inducts induct recs0 rec_thmss + lthy = let val thy = Proof_Context.theory_of lthy; @@ -179,7 +177,7 @@ val Cs = map ((fn TVar ((s, _), S) => TFree (s, S)) o body_type o fastype_of) recs0; val recs = map2 (mk_co_rec thy Least_FP Cs) fpTs recs0; val ((recs', rec'_defs), lthy') = define_split_recs fpTs Cs recs lthy |>> split_list; - val rec'_thmss = mk_split_rec_thmss lthy' fpTs ctrss rec_thmss recs' rec'_defs; + val rec'_thmss = mk_split_rec_thmss lthy' Xs fpTs ctr_Tsss ctrss rec_thmss recs' rec'_defs; in ((inducts', induct', recs', rec'_thmss), lthy') end; @@ -265,7 +263,7 @@ val fpTs' = Old_Datatype_Aux.get_rec_types descr; val nn = length fpTs'; - val fp_sugars0 = map (lfp_sugar_of o fst o dest_Type) fpTs'; + val fp_sugars = map (lfp_sugar_of o fst o dest_Type) fpTs'; val ctr_Tsss = map (map (map dest_dtyp o snd) o #3 o snd) descr; val kkssss = map (map (map (fn Old_Datatype_Aux.DtRec kk => [kk] | _ => []) o snd) o #3 o snd) descr; @@ -282,32 +280,34 @@ val compat_b_names = map (prefix compat_N) b_names; val compat_bs = map Binding.name compat_b_names; - val ((fp_sugars, (lfp_sugar_thms, _)), lthy') = + val ((fp_sugars', (lfp_sugar_thms', _)), lthy') = if nn > nn_fp then - mutualize_fp_sugars Least_FP cliques compat_bs fpTs' callers callssss fp_sugars0 lthy + mutualize_fp_sugars Least_FP cliques compat_bs fpTs' callers callssss fp_sugars lthy else - ((fp_sugars0, (NONE, NONE)), lthy); + ((fp_sugars, (NONE, NONE)), lthy); + + fun mk_ctr_of {ctr_sugar = {ctrs, ...}, ...} (Type (_, Ts)) = map (mk_ctr Ts) ctrs; - fun mk_ctrs_of (Type (T_name, As)) = - map (mk_ctr As) (#ctrs (the (ctr_sugar_of lthy' T_name))); - - val ctrss' = map mk_ctrs_of fpTs'; - val {common_co_inducts = [induct], ...} :: _ = fp_sugars; - val inducts = map (the_single o #co_inducts) fp_sugars; - val recs = map #co_rec fp_sugars; - val rec_thmss = map #co_rec_thms fp_sugars; + val Xs' = map #X fp_sugars'; + val ctr_Tsss' = map (map (binder_types o fastype_of) o #ctrs o #ctr_sugar) fp_sugars'; (*###*) + val ctrss' = map2 mk_ctr_of fp_sugars' fpTs'; + val {common_co_inducts = [induct], ...} :: _ = fp_sugars'; + val inducts = map (the_single o #co_inducts) fp_sugars'; + val recs = map #co_rec fp_sugars'; + val rec_thmss = map #co_rec_thms fp_sugars'; fun is_nested_rec_type (Type (@{type_name fun}, [_, T])) = member (op =) fpTs' (body_type T) | is_nested_rec_type _ = false; - val ((lfp_sugar_thms', (inducts', induct', recs', rec'_thmss)), lthy'') = + val ((lfp_sugar_thms'', (inducts', induct', recs', rec'_thmss)), lthy'') = if nesting_pref = Unfold_Nesting andalso - exists (exists (exists is_nested_rec_type)) ctr_Tsss then - define_split_rec_derive_induct_rec_thms fpTs' ctrss' inducts induct recs rec_thmss lthy' + exists (exists (exists is_nested_rec_type)) ctr_Tsss' then + define_split_rec_derive_induct_rec_thms Xs' fpTs' ctr_Tsss' ctrss' inducts induct recs + rec_thmss lthy' |>> `(fn (inducts', induct', _, rec'_thmss) => SOME ((inducts', induct', mk_induct_attrs ctrss'), (rec'_thmss, []))) else - ((lfp_sugar_thms, (inducts, induct, recs, rec_thmss)), lthy'); + ((lfp_sugar_thms', (inducts, induct, recs, rec_thmss)), lthy'); val rec'_names = map (fst o dest_Const) recs'; val rec'_thms = flat rec'_thmss; @@ -321,9 +321,9 @@ case_cong = case_cong, case_cong_weak = case_cong_weak, split = split, split_asm = split_asm}); - val infos = map_index mk_info (take nn_fp fp_sugars); + val infos = map_index mk_info (take nn_fp fp_sugars'); in - (nn, b_names, compat_b_names, lfp_sugar_thms', infos, lthy'') + (nn, b_names, compat_b_names, lfp_sugar_thms'', infos, lthy'') end; fun infos_of_new_datatype_mutual_cluster lthy fpT_name =