src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
changeset 53746 bd038e48526d
parent 53678 e55bb583342e
child 53808 b3e2022530e3
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Fri Sep 20 10:09:16 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Fri Sep 20 11:44:30 2013 +0200
     1.3 @@ -9,12 +9,17 @@
     1.4  sig
     1.5    val mutualize_fp_sugars: bool -> bool -> BNF_FP_Util.fp_kind -> binding list -> typ list ->
     1.6      (term -> int list) -> term list list list list -> BNF_FP_Def_Sugar.fp_sugar list ->
     1.7 -    local_theory -> (bool * BNF_FP_Def_Sugar.fp_sugar list) * local_theory
     1.8 +    local_theory ->
     1.9 +    (BNF_FP_Def_Sugar.fp_sugar list
    1.10 +     * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
    1.11 +    * local_theory
    1.12    val pad_and_indexify_calls: BNF_FP_Def_Sugar.fp_sugar list -> int ->
    1.13      (term * term list list) list list -> term list list list list
    1.14    val nested_to_mutual_fps: bool -> BNF_FP_Util.fp_kind -> binding list -> typ list ->
    1.15      (term -> int list) -> ((term * term list list) list) list -> local_theory ->
    1.16 -    (bool * typ list * int list * BNF_FP_Def_Sugar.fp_sugar list) * local_theory
    1.17 +    (typ list * int list * BNF_FP_Def_Sugar.fp_sugar list
    1.18 +     * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
    1.19 +    * local_theory
    1.20  end;
    1.21  
    1.22  structure BNF_FP_N2M_Sugar : BNF_FP_N2M_SUGAR =
    1.23 @@ -146,23 +151,25 @@
    1.24  
    1.25        val ctr_sugars = map inst_ctr_sugar ctr_sugars0;
    1.26  
    1.27 -      val (co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
    1.28 -           sel_unfold_thmsss, sel_corec_thmsss) =
    1.29 +      val ((co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
    1.30 +            sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
    1.31          if fp = Least_FP then
    1.32            derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
    1.33              xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
    1.34              co_iterss co_iter_defss lthy
    1.35 -          |> (fn ((_, induct, _), (fold_thmss, _), (rec_thmss, _)) =>
    1.36 +          |> `(fn ((_, induct, _), (fold_thmss, _), (rec_thmss, _)) =>
    1.37              ([induct], fold_thmss, rec_thmss, [], [], [], []))
    1.38 +          ||> (fn info => (SOME info, NONE))
    1.39          else
    1.40            derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
    1.41              dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
    1.42              ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
    1.43 -          |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _,
    1.44 +          |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _,
    1.45                    (disc_unfold_thmss, disc_corec_thmss, _), _,
    1.46                    (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
    1.47              (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
    1.48 -             disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss));
    1.49 +             disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss))
    1.50 +          ||> (fn info => (NONE, SOME info));
    1.51  
    1.52        val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
    1.53  
    1.54 @@ -175,11 +182,11 @@
    1.55           sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}
    1.56          |> morph_fp_sugar phi;
    1.57      in
    1.58 -      ((true, map_index mk_target_fp_sugar fpTs), lthy)
    1.59 +      ((map_index mk_target_fp_sugar fpTs, fp_sugar_thms), lthy)
    1.60      end
    1.61    else
    1.62      (* TODO: reorder hypotheses and predicates in (co)induction rules? *)
    1.63 -    ((false, fp_sugars0), no_defs_lthy0);
    1.64 +    ((fp_sugars0, (NONE, NONE)), no_defs_lthy0);
    1.65  
    1.66  fun indexify_callsss fp_sugar callsss =
    1.67    let
    1.68 @@ -256,13 +263,13 @@
    1.69  
    1.70      val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;
    1.71  
    1.72 -    val ((nontriv, perm_fp_sugars), lthy) =
    1.73 +    val ((perm_fp_sugars, fp_sugar_thms), lthy) =
    1.74        mutualize_fp_sugars lose_co_rec mutualize fp perm_bs perm_Ts get_perm_indices perm_callssss
    1.75          perm_fp_sugars0 lthy;
    1.76  
    1.77      val fp_sugars = unpermute perm_fp_sugars;
    1.78    in
    1.79 -    ((nontriv, missing_Ts, perm_kks, fp_sugars), lthy)
    1.80 +    ((missing_Ts, perm_kks, fp_sugars, fp_sugar_thms), lthy)
    1.81    end;
    1.82  
    1.83  end;