1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     1.3 @@ -20,6 +20,7 @@
     1.4       co_iterss: term list list,
     1.5       mapss: thm list list,
     1.6       co_inducts: thm list,
     1.7 +     co_inductss: thm list list,
     1.8       co_iter_thmsss: thm list list list,
     1.9       disc_co_itersss: thm list list list,
    1.10       sel_co_iterssss: thm list list list list};
    1.11 @@ -129,6 +130,7 @@
    1.12     co_iterss: term list list,
    1.13     mapss: thm list list,
    1.14     co_inducts: thm list,
    1.15 +   co_inductss: thm list list,
    1.16     co_iter_thmsss: thm list list list,
    1.17     disc_co_itersss: thm list list list,
    1.18     sel_co_iterssss: thm list list list list};
    1.19 @@ -136,8 +138,8 @@
    1.20  fun of_fp_sugar f (fp_sugar as ({index, ...}: fp_sugar)) = nth (f fp_sugar) index;
    1.21  
    1.22  fun morph_fp_sugar phi ({T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
    1.23 -    ctr_sugars, co_iterss, mapss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss}
    1.24 -    : fp_sugar) =
    1.25 +    ctr_sugars, co_iterss, mapss, co_inducts, co_inductss, co_iter_thmsss, disc_co_itersss,
    1.26 +    sel_co_iterssss} : fp_sugar) =
    1.27    {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
    1.28      nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
    1.29     fp_res = morph_fp_result phi fp_res,
    1.30 @@ -146,6 +148,7 @@
    1.31     co_iterss = map (map (Morphism.term phi)) co_iterss,
    1.32     mapss = map (map (Morphism.thm phi)) mapss,
    1.33     co_inducts = map (Morphism.thm phi) co_inducts,
    1.34 +   co_inductss = map (map (Morphism.thm phi)) co_inductss,
    1.35     co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss,
    1.36     disc_co_itersss = map (map (map (Morphism.thm phi))) disc_co_itersss,
    1.37     sel_co_iterssss = map (map (map (map (Morphism.thm phi)))) sel_co_iterssss};
    1.38 @@ -178,14 +181,15 @@
    1.39      (fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar)));
    1.40  
    1.41  fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss
    1.42 -    ctr_sugars co_iterss mapss co_inducts co_iter_thmsss disc_co_itersss sel_co_iterssss lthy =
    1.43 +    ctr_sugars co_iterss mapss co_inducts co_inductss co_iter_thmsss disc_co_itersss
    1.44 +    sel_co_iterssss lthy =
    1.45    (0, lthy)
    1.46    |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
    1.47      register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
    1.48          nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
    1.49          ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
    1.50 -        co_iter_thmsss = co_iter_thmsss, disc_co_itersss = disc_co_itersss,
    1.51 -        sel_co_iterssss = sel_co_iterssss}
    1.52 +        co_inductss = co_inductss, co_iter_thmsss = co_iter_thmsss,
    1.53 +        disc_co_itersss = disc_co_itersss, sel_co_iterssss = sel_co_iterssss}
    1.54        lthy)) Ts
    1.55    |> snd;
    1.56  
    1.57 @@ -664,7 +668,10 @@
    1.58              mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' nested_set_maps
    1.59                pre_set_defss)
    1.60            |> singleton (Proof_Context.export names_lthy lthy)
    1.61 -          |> Thm.close_derivation;
    1.62 +          (* for "datatype_realizer.ML": *)
    1.63 +          |> Thm.name_derivation (fst (dest_Type (hd fpTs)) ^ Long_Name.separator ^
    1.64 +            (if nn > 1 then space_implode "_" (tl fp_b_names) ^ Long_Name.separator else "") ^
    1.65 +            inductN);
    1.66        in
    1.67          `(conj_dests nn) thm
    1.68        end;
    1.69 @@ -1218,8 +1225,8 @@
    1.70                      Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
    1.71                        mk_ctor_iff_dtor_tac ctxt (map (SOME o certifyT lthy) [dtorT, fpT])
    1.72                          (certify lthy ctor) (certify lthy dtor) ctor_dtor dtor_ctor)
    1.73 +                    |> Morphism.thm phi
    1.74                      |> Thm.close_derivation
    1.75 -                    |> Morphism.thm phi
    1.76                    end;
    1.77  
    1.78                  val sumEN_thm' =
    1.79 @@ -1391,7 +1398,8 @@
    1.80          lthy
    1.81          |> Local_Theory.notes (common_notes @ notes) |> snd
    1.82          |> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars
    1.83 -          iterss mapss [induct_thm] (transpose [fold_thmss, rec_thmss]) [] []
    1.84 +          iterss mapss [induct_thm] (transpose [induct_thms]) (transpose [fold_thmss, rec_thmss])
    1.85 +          [] []
    1.86        end;
    1.87  
    1.88      fun derive_note_coinduct_coiters_thms_for_types
    1.89 @@ -1449,6 +1457,7 @@
    1.90          |> Local_Theory.notes (common_notes @ notes) |> snd
    1.91          |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss
    1.92            ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm]
    1.93 +          (transpose [coinduct_thms, strong_coinduct_thms])
    1.94            (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss])
    1.95            (transpose [sel_unfold_thmsss, sel_corec_thmsss])
    1.96        end;

     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     2.3 @@ -212,14 +212,14 @@
     2.4                (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
     2.5            |>> split_list;
     2.6  
     2.7 -        val ((co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
     2.8 -              sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
     2.9 +        val ((co_inducts, co_inductss, un_fold_thmss, co_rec_thmss, disc_unfold_thmss,
    2.10 +              disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
    2.11            if fp = Least_FP then
    2.12              derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
    2.13                xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
    2.14                co_iterss co_iter_defss lthy
    2.15 -            |> `(fn ((_, induct, _), (fold_thmss, rec_thmss, _)) =>
    2.16 -              ([induct], fold_thmss, rec_thmss, [], [], [], []))
    2.17 +            |> `(fn ((inducts, induct, _), (fold_thmss, rec_thmss, _)) =>
    2.18 +              ([induct], [inducts], fold_thmss, rec_thmss, [], [], [], []))
    2.19              ||> (fn info => (SOME info, NONE))
    2.20            else
    2.21              derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
    2.22 @@ -229,8 +229,8 @@
    2.23              |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
    2.24                      (disc_unfold_thmss, disc_corec_thmss, _), _,
    2.25                      (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
    2.26 -              (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
    2.27 -               disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss))
    2.28 +              (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, unfold_thmss, corec_thmss,
    2.29 +               disc_unfold_thmss, disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss))
    2.30              ||> (fn info => (NONE, SOME info));
    2.31  
    2.32          val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
    2.33 @@ -239,6 +239,7 @@
    2.34            {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
    2.35             nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
    2.36             ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
    2.37 +           co_inductss = transpose co_inductss,
    2.38             co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss],
    2.39             disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss],
    2.40             sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}

     3.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Feb 12 08:35:56 2014 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Feb 12 08:35:56 2014 +0100
     3.3 @@ -99,9 +99,9 @@
     3.4        else
     3.5          ((fp_sugars0, (NONE, NONE)), lthy);
     3.6  
     3.7 -    val {ctr_sugars, co_inducts = [induct], co_iterss, co_iter_thmsss = iter_thmsss, ...} :: _ =
     3.8 -      fp_sugars;
     3.9 -    val inducts = conj_dests nn induct;
    3.10 +    val {ctr_sugars, co_inducts = [induct], co_inductss = inductss, co_iterss,
    3.11 +      co_iter_thmsss = iter_thmsss, ...} :: _ = fp_sugars;
    3.12 +    val inducts = map the_single inductss;
    3.13  
    3.14      val mk_dtyp = dtyp_of_typ Ts;
    3.15  

     4.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     4.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     4.3 @@ -359,8 +359,10 @@
     4.4  
     4.5      val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
     4.6  
     4.7 -    val ((((((((xss, xss'), yss), fs), gs), [u', v']), [w]), (p, p')), names_lthy) = no_defs_lthy |>
     4.8 -      mk_Freess' "x" ctr_Tss
     4.9 +    val (((((((([exh_y], (xss, xss')), yss), fs), gs), [u', v']), [w]), (p, p')), names_lthy) =
    4.10 +      no_defs_lthy
    4.11 +      |> mk_Frees "y" [fcT] (* for compatibility with "datatype_realizer.ML" *)
    4.12 +      ||>> mk_Freess' "x" ctr_Tss
    4.13        ||>> mk_Freess "y" ctr_Tss
    4.14        ||>> mk_Frees "f" case_Ts
    4.15        ||>> mk_Frees "g" case_Ts
    4.16 @@ -529,8 +531,8 @@
    4.17      fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
    4.18  
    4.19      val exhaust_goal =
    4.20 -      let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (u, xctr)]) in
    4.21 -        fold_rev Logic.all [p, u] (mk_imp_p (map2 mk_prem xctrs xss))
    4.22 +      let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (exh_y, xctr)]) in
    4.23 +        fold_rev Logic.all [p, exh_y] (mk_imp_p (map2 mk_prem xctrs xss))
    4.24        end;
    4.25  
    4.26      val inject_goalss =
    4.27 @@ -556,7 +558,10 @@
    4.28  
    4.29      fun after_qed thmss lthy =
    4.30        let
    4.31 -        val ([exhaust_thm], (inject_thmss, half_distinct_thmss)) = (hd thmss, chop n (tl thmss));
    4.32 +        val ([exhaust_thm0], (inject_thmss, half_distinct_thmss)) = (hd thmss, chop n (tl thmss));
    4.33 +        (* for "datatype_realizer.ML": *)
    4.34 +        val exhaust_thm =
    4.35 +          Thm.name_derivation (fcT_name ^ Long_Name.separator ^ exhaustN) exhaust_thm0;
    4.36  
    4.37          val inject_thms = flat inject_thmss;
    4.38  
    4.39 @@ -611,7 +616,8 @@
    4.40            in
    4.41              (Goal.prove_sorry lthy [] [] goal (fn _ => mk_case_cong_tac lthy uexhaust_thm case_thms),
    4.42               Goal.prove_sorry lthy [] [] weak_goal (K (etac arg_cong 1)))
    4.43 -            |> pairself (Thm.close_derivation #> singleton (Proof_Context.export names_lthy lthy))
    4.44 +            |> pairself (singleton (Proof_Context.export names_lthy lthy) #>
    4.45 +              Thm.close_derivation)
    4.46            end;
    4.47  
    4.48          val split_lhs = q $ ufcase;
    4.49 @@ -632,14 +638,14 @@
    4.50          fun prove_split selss goal =
    4.51            Goal.prove_sorry lthy [] [] goal (fn _ =>
    4.52              mk_split_tac lthy uexhaust_thm case_thms selss inject_thmss distinct_thmsss)
    4.53 -          |> Thm.close_derivation
    4.54 -          |> singleton (Proof_Context.export names_lthy lthy);
    4.55 +          |> singleton (Proof_Context.export names_lthy lthy)
    4.56 +          |> Thm.close_derivation;
    4.57  
    4.58          fun prove_split_asm asm_goal split_thm =
    4.59            Goal.prove_sorry lthy [] [] asm_goal (fn {context = ctxt, ...} =>
    4.60              mk_split_asm_tac ctxt split_thm)
    4.61 -          |> Thm.close_derivation
    4.62 -          |> singleton (Proof_Context.export names_lthy lthy);
    4.63 +          |> singleton (Proof_Context.export names_lthy lthy)
    4.64 +          |> Thm.close_derivation;
    4.65  
    4.66          val (split_thm, split_asm_thm) =
    4.67            let
    4.68 @@ -693,8 +699,8 @@
    4.69                    val goal = mk_Trueprop_eq (mk_uu_eq (), the_single exist_xs_u_eq_ctrs);
    4.70                  in
    4.71                    Goal.prove_sorry lthy [] [] goal (fn _ => mk_unique_disc_def_tac m uexhaust_thm)
    4.72 +                  |> singleton (Proof_Context.export names_lthy lthy)
    4.73                    |> Thm.close_derivation
    4.74 -                  |> singleton (Proof_Context.export names_lthy lthy)
    4.75                  end;
    4.76  
    4.77                fun mk_alternate_disc_def k =
    4.78 @@ -706,8 +712,8 @@
    4.79                    Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
    4.80                      mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k))
    4.81                        (nth distinct_thms (2 - k)) uexhaust_thm)
    4.82 +                  |> singleton (Proof_Context.export names_lthy lthy)
    4.83                    |> Thm.close_derivation
    4.84 -                  |> singleton (Proof_Context.export names_lthy lthy)
    4.85                  end;
    4.86  
    4.87                val has_alternate_disc_def =
    4.88 @@ -843,8 +849,8 @@
    4.89                      mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm)
    4.90                        (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
    4.91                        disc_exclude_thmsss')
    4.92 +                  |> singleton (Proof_Context.export names_lthy lthy)
    4.93                    |> Thm.close_derivation
    4.94 -                  |> singleton (Proof_Context.export names_lthy lthy)
    4.95                  end;
    4.96  
    4.97                val (sel_split_thm, sel_split_asm_thm) =
    4.98 @@ -865,8 +871,8 @@
    4.99                  in
   4.100                    Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   4.101                      mk_case_eq_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
   4.102 +                  |> singleton (Proof_Context.export names_lthy lthy)
   4.103                    |> Thm.close_derivation
   4.104 -                  |> singleton (Proof_Context.export names_lthy lthy)
   4.105                  end;
   4.106              in
   4.107                (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,