src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 53203 222ea6acbdd6
parent 53143 ba80154a1118
child 53210 7219c61796c0
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Aug 26 12:14:41 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Aug 26 13:44:46 2013 +0200
     1.3 @@ -70,9 +70,10 @@
     1.4    val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list ->
     1.5      string * term list * term list list * ((term list list * term list list list)
     1.6        * (typ list * typ list list)) list ->
     1.7 -    thm -> thm list -> thm list list -> BNF_Def.bnf list -> typ list -> typ list -> typ list ->
     1.8 -    int list list -> int list list -> int list -> thm list list -> BNF_Ctr_Sugar.ctr_sugar list ->
     1.9 -    term list list -> thm list list -> (thm list -> thm list) -> local_theory ->
    1.10 +    thm -> thm list -> thm list -> thm list list -> BNF_Def.bnf list -> typ list -> typ list ->
    1.11 +    typ list -> int list list -> int list list -> int list -> thm list list ->
    1.12 +    BNF_Ctr_Sugar.ctr_sugar list -> term list list -> thm list list -> (thm list -> thm list) ->
    1.13 +    local_theory ->
    1.14      ((thm list * thm) list * Args.src list)
    1.15      * (thm list list * thm list list * Args.src list)
    1.16      * (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
    1.17 @@ -727,9 +728,15 @@
    1.18  
    1.19  fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss,
    1.20        coiters_args_types as [((pgss, crgsss), _), ((phss, cshsss), _)])
    1.21 -    dtor_coinduct dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs As kss mss ns ctr_defss
    1.22 -    ctr_sugars coiterss coiter_defss export_args lthy =
    1.23 +    dtor_coinduct dtor_injects dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs As kss mss ns
    1.24 +    ctr_defss ctr_sugars coiterss coiter_defss export_args lthy =
    1.25    let
    1.26 +    fun mk_ctor_dtor_coiter_thm dtor_inject dtor_ctor coiter =
    1.27 +      iffD1 OF [dtor_inject, trans OF [coiter, dtor_ctor RS sym]];
    1.28 +
    1.29 +    val ctor_dtor_coiter_thmss =
    1.30 +      map3 (map oo mk_ctor_dtor_coiter_thm) dtor_injects dtor_ctors dtor_coiter_thmss;
    1.31 +
    1.32      val coiterss' = transpose coiterss;
    1.33      val coiter_defss' = transpose coiter_defss;
    1.34  
    1.35 @@ -896,10 +903,10 @@
    1.36  
    1.37          val unfold_tacss =
    1.38            map3 (map oo mk_coiter_tac unfold_defs nesting_map_ids'')
    1.39 -            (map un_fold_of dtor_coiter_thmss) pre_map_defs ctr_defss;
    1.40 +            (map un_fold_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss;
    1.41          val corec_tacss =
    1.42            map3 (map oo mk_coiter_tac corec_defs nesting_map_ids'')
    1.43 -            (map co_rec_of dtor_coiter_thmss) pre_map_defs ctr_defss;
    1.44 +            (map co_rec_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss;
    1.45  
    1.46          fun prove goal tac =
    1.47            Goal.prove_sorry lthy [] [] goal (tac o #context)
    1.48 @@ -1111,7 +1118,8 @@
    1.49  
    1.50      val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0,
    1.51             xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects,
    1.52 -           xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, ...}, lthy)) =
    1.53 +           dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, ...},
    1.54 +           lthy)) =
    1.55        fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs
    1.56          no_defs_lthy0;
    1.57  
    1.58 @@ -1404,8 +1412,8 @@
    1.59               (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs),
    1.60               (sel_unfold_thmss, sel_corec_thmss, sel_coiter_attrs)) =
    1.61            derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
    1.62 -            dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs As kss mss ns ctr_defss ctr_sugars
    1.63 -            coiterss coiter_defss (Proof_Context.export lthy' no_defs_lthy) lthy;
    1.64 +            dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs As kss mss ns ctr_defss
    1.65 +            ctr_sugars coiterss coiter_defss (Proof_Context.export lthy' no_defs_lthy) lthy;
    1.66  
    1.67          val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
    1.68