tuning
authorblanchet
Mon Nov 04 10:52:41 2013 +0100 (2013-11-04)
changeset 542353aed2ae6eb91
parent 54234 b5310a1b807c
child 54236 e00009523727
tuning
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Nov 04 10:52:41 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Nov 04 10:52:41 2013 +0100
     1.3 @@ -87,8 +87,9 @@
     1.4      string * term list * term list list * ((term list list * term list list list)
     1.5        * (typ list * typ list list)) list ->
     1.6      thm -> thm list -> thm list -> thm list list -> BNF_Def.bnf list -> typ list -> typ list ->
     1.7 -    int list list -> int list list -> int list -> thm list list -> Ctr_Sugar.ctr_sugar list ->
     1.8 -    term list list -> thm list list -> (thm list -> thm list) -> local_theory -> gfp_sugar_thms
     1.9 +    typ list -> typ list list list -> int list list -> int list list -> int list -> thm list list ->
    1.10 +    Ctr_Sugar.ctr_sugar list -> term list list -> thm list list -> (thm list -> thm list) ->
    1.11 +    local_theory -> gfp_sugar_thms
    1.12    val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
    1.13        binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
    1.14        BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
    1.15 @@ -299,8 +300,6 @@
    1.16      Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
    1.17    end;
    1.18  
    1.19 -local
    1.20 -
    1.21  fun build_map_or_rel mk const of_bnf dest lthy build_simple =
    1.22    let
    1.23      fun build (TU as (T, U)) =
    1.24 @@ -321,13 +320,9 @@
    1.25          | _ => build_simple TU);
    1.26    in build end;
    1.27  
    1.28 -in
    1.29 -
    1.30  val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT;
    1.31  val build_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T;
    1.32  
    1.33 -end;
    1.34 -
    1.35  val dummy_var_name = "?f"
    1.36  
    1.37  fun mk_map_pattern ctxt s =
    1.38 @@ -770,8 +765,8 @@
    1.39  
    1.40  fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss,
    1.41        coiters_args_types as [((pgss, crgsss), _), ((phss, cshsss), _)])
    1.42 -    dtor_coinduct dtor_injects dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs kss mss ns
    1.43 -    ctr_defss (ctr_sugars : ctr_sugar list) coiterss coiter_defss export_args lthy =
    1.44 +    dtor_coinduct dtor_injects dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
    1.45 +    mss ns ctr_defss (ctr_sugars : ctr_sugar list) coiterss coiter_defss export_args lthy =
    1.46    let
    1.47      fun mk_ctor_dtor_coiter_thm dtor_inject dtor_ctor coiter =
    1.48        iffD1 OF [dtor_inject, trans OF [coiter, dtor_ctor RS sym]];
    1.49 @@ -823,7 +818,6 @@
    1.50            map4 (fn u => fn v => fn uvr => fn uv_eq =>
    1.51              fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs;
    1.52  
    1.53 -        (* TODO: generalize (cf. "build_map") *)
    1.54          fun build_rel rs' T =
    1.55            (case find_index (curry op = T) fpTs of
    1.56              ~1 =>
    1.57 @@ -1466,8 +1460,9 @@
    1.58               (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs),
    1.59               (sel_unfold_thmsss, sel_corec_thmsss, sel_coiter_attrs)) =
    1.60            derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
    1.61 -            dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
    1.62 -            ctr_sugars coiterss coiter_defss (Proof_Context.export lthy' no_defs_lthy) lthy;
    1.63 +            dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
    1.64 +            ctr_defss ctr_sugars coiterss coiter_defss (Proof_Context.export lthy' no_defs_lthy)
    1.65 +            lthy;
    1.66  
    1.67          val sel_unfold_thmss = map flat sel_unfold_thmsss;
    1.68          val sel_corec_thmss = map flat sel_corec_thmsss;
     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 04 10:52:41 2013 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 04 10:52:41 2013 +0100
     2.3 @@ -159,8 +159,9 @@
     2.4            ||> (fn info => (SOME info, NONE))
     2.5          else
     2.6            derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
     2.7 -            dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
     2.8 -            ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
     2.9 +            dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
    2.10 +            ctr_defss ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy)
    2.11 +            lthy
    2.12            |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
    2.13                    (disc_unfold_thmss, disc_corec_thmss, _), _,
    2.14                    (sel_unfold_thmsss, sel_corec_thmsss, _)) =>