src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
changeset 53475 185ad6cf6576
parent 53303 ae49b835ca01
child 53476 eb3865c3ee58
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Sun Sep 08 19:25:06 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Sep 09 13:47:58 2013 +0200
     1.3 @@ -145,19 +145,23 @@
     1.4  
     1.5        val ctr_sugars = map inst_ctr_sugar ctr_sugars0;
     1.6  
     1.7 -      val (co_inducts, un_fold_thmss, co_rec_thmss) =
     1.8 +      val (co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
     1.9 +           sel_unfold_thmsss, sel_corec_thmsss) =
    1.10          if fp = Least_FP then
    1.11            derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
    1.12              xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
    1.13              co_iterss co_iter_defss lthy
    1.14            |> (fn ((_, induct, _), (fold_thmss, _), (rec_thmss, _)) =>
    1.15 -            ([induct], fold_thmss, rec_thmss))
    1.16 +            ([induct], fold_thmss, rec_thmss, [], [], [], []))
    1.17          else
    1.18            derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
    1.19              dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
    1.20              ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
    1.21 -          |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _, _, _, _) =>
    1.22 -            (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss));
    1.23 +          |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _, _,
    1.24 +                  (disc_unfold_thmss, disc_corec_thmss, _),
    1.25 +                  (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
    1.26 +            (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
    1.27 +             disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss));
    1.28  
    1.29        val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
    1.30  
    1.31 @@ -165,7 +169,9 @@
    1.32          {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
    1.33           nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
    1.34           ctr_sugars = ctr_sugars, co_inducts = co_inducts, co_iterss = co_iterss,
    1.35 -         co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss]}
    1.36 +         co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss],
    1.37 +         disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss],
    1.38 +         sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}
    1.39          |> morph_fp_sugar phi;
    1.40      in
    1.41        ((true, map_index mk_target_fp_sugar fpTs), lthy)