# HG changeset patch
# User blanchet
# Date 1379670270 -7200
# Node ID bd038e48526dfb3d0ab0f33f955a31bb993cd467
# Parent  788730ab7da495ebe1ba7b533308d21b22eb1f88
have "datatype_new_compat" register induction and recursion theorems in nested case

diff -r 788730ab7da4 -r bd038e48526d src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Sep 20 10:09:16 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Sep 20 11:44:30 2013 +0200
@@ -44,6 +44,19 @@
   val build_rel: local_theory -> (typ * typ -> term) -> typ * typ -> term
   val dest_map: Proof.context -> string -> term -> term * term list
   val dest_ctr: Proof.context -> string -> term -> term * term list
+
+  type lfp_sugar_thms =
+    (thm list * thm * Args.src list)
+    * (thm list list * Args.src list)
+    * (thm list list * Args.src list)
+
+  type gfp_sugar_thms =
+    ((thm list * thm) list * Args.src list)
+    * (thm list list * thm list list * Args.src list)
+    * (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
+    * (thm list list * thm list list * Args.src list)
+    * (thm list list list * thm list list list * Args.src list)
+
   val mk_co_iters_prelims: BNF_FP_Util.fp_kind -> typ list list list -> typ list -> typ list ->
     int list -> int list list -> term list list -> Proof.context ->
     (term list list
@@ -52,7 +65,6 @@
      * (string * term list * term list list
         * ((term list list * term list list list) * (typ list * typ list list)) list) option)
     * Proof.context
-
   val mk_iter_fun_arg_types: typ list list list -> int list -> int list list -> term ->
     typ list list list list
   val mk_coiter_fun_arg_types: typ list list list -> typ list -> int list -> term ->
@@ -70,21 +82,13 @@
     (typ list list * typ list list list list * term list list * term list list list list) list ->
     thm -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list ->
     typ list -> typ list list list -> term list list -> thm list list -> term list list ->
-    thm list list -> local_theory ->
-    (thm list * thm * Args.src list) * (thm list list * Args.src list)
-    * (thm list list * Args.src list)
+    thm list list -> local_theory -> lfp_sugar_thms
   val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list ->
     string * term list * term list list * ((term list list * term list list list)
       * (typ list * typ list list)) list ->
     thm -> thm list -> thm list -> thm list list -> BNF_Def.bnf list -> typ list -> typ list ->
     int list list -> int list list -> int list -> thm list list -> BNF_Ctr_Sugar.ctr_sugar list ->
-    term list list -> thm list list -> (thm list -> thm list) -> local_theory ->
-    ((thm list * thm) list * Args.src list)
-    * (thm list list * thm list list * Args.src list)
-    * (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
-    * (thm list list * thm list list * Args.src list)
-    * (thm list list list * thm list list list * Args.src list)
-
+    term list list -> thm list list -> (thm list -> thm list) -> local_theory -> gfp_sugar_thms
   val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
       binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
       BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
@@ -396,6 +400,18 @@
 
 fun indexify proj xs f p = f (find_index (curry op = (proj p)) xs) p;
 
+type lfp_sugar_thms =
+  (thm list * thm * Args.src list)
+  * (thm list list * Args.src list)
+  * (thm list list * Args.src list);
+
+type gfp_sugar_thms =
+  ((thm list * thm) list * Args.src list)
+  * (thm list list * thm list list * Args.src list)
+  * (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
+  * (thm list list * thm list list * Args.src list)
+  * (thm list list list * thm list list list * Args.src list);
+
 fun mk_iter_fun_arg_types0 n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
 
 fun mk_iter_fun_arg_types ctr_Tsss ns mss =
diff -r 788730ab7da4 -r bd038e48526d src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Fri Sep 20 10:09:16 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Fri Sep 20 11:44:30 2013 +0200
@@ -9,12 +9,17 @@
 sig
   val mutualize_fp_sugars: bool -> bool -> BNF_FP_Util.fp_kind -> binding list -> typ list ->
     (term -> int list) -> term list list list list -> BNF_FP_Def_Sugar.fp_sugar list ->
-    local_theory -> (bool * BNF_FP_Def_Sugar.fp_sugar list) * local_theory
+    local_theory ->
+    (BNF_FP_Def_Sugar.fp_sugar list
+     * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
+    * local_theory
   val pad_and_indexify_calls: BNF_FP_Def_Sugar.fp_sugar list -> int ->
     (term * term list list) list list -> term list list list list
   val nested_to_mutual_fps: bool -> BNF_FP_Util.fp_kind -> binding list -> typ list ->
     (term -> int list) -> ((term * term list list) list) list -> local_theory ->
-    (bool * typ list * int list * BNF_FP_Def_Sugar.fp_sugar list) * local_theory
+    (typ list * int list * BNF_FP_Def_Sugar.fp_sugar list
+     * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
+    * local_theory
 end;
 
 structure BNF_FP_N2M_Sugar : BNF_FP_N2M_SUGAR =
@@ -146,23 +151,25 @@
 
       val ctr_sugars = map inst_ctr_sugar ctr_sugars0;
 
-      val (co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
-           sel_unfold_thmsss, sel_corec_thmsss) =
+      val ((co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
+            sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
         if fp = Least_FP then
           derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
             xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
             co_iterss co_iter_defss lthy
-          |> (fn ((_, induct, _), (fold_thmss, _), (rec_thmss, _)) =>
+          |> `(fn ((_, induct, _), (fold_thmss, _), (rec_thmss, _)) =>
             ([induct], fold_thmss, rec_thmss, [], [], [], []))
+          ||> (fn info => (SOME info, NONE))
         else
           derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
             dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
             ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
-          |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _,
+          |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _,
                   (disc_unfold_thmss, disc_corec_thmss, _), _,
                   (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
             (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
-             disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss));
+             disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss))
+          ||> (fn info => (NONE, SOME info));
 
       val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
 
@@ -175,11 +182,11 @@
          sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}
         |> morph_fp_sugar phi;
     in
-      ((true, map_index mk_target_fp_sugar fpTs), lthy)
+      ((map_index mk_target_fp_sugar fpTs, fp_sugar_thms), lthy)
     end
   else
     (* TODO: reorder hypotheses and predicates in (co)induction rules? *)
-    ((false, fp_sugars0), no_defs_lthy0);
+    ((fp_sugars0, (NONE, NONE)), no_defs_lthy0);
 
 fun indexify_callsss fp_sugar callsss =
   let
@@ -256,13 +263,13 @@
 
     val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;
 
-    val ((nontriv, perm_fp_sugars), lthy) =
+    val ((perm_fp_sugars, fp_sugar_thms), lthy) =
       mutualize_fp_sugars lose_co_rec mutualize fp perm_bs perm_Ts get_perm_indices perm_callssss
         perm_fp_sugars0 lthy;
 
     val fp_sugars = unpermute perm_fp_sugars;
   in
-    ((nontriv, missing_Ts, perm_kks, fp_sugars), lthy)
+    ((missing_Ts, perm_kks, fp_sugars, fp_sugar_thms), lthy)
   end;
 
 end;
diff -r 788730ab7da4 -r bd038e48526d src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Fri Sep 20 10:09:16 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Fri Sep 20 11:44:30 2013 +0200
@@ -348,9 +348,9 @@
   let
     val thy = Proof_Context.theory_of lthy;
 
-    val ((nontriv, missing_arg_Ts, perm0_kks,
+    val ((missing_arg_Ts, perm0_kks,
           fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = ctor_iters1 :: _, ...},
-            co_inducts = [induct_thm], ...} :: _), lthy') =
+            co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)), lthy') =
       nested_to_mutual_fps lose_co_rec Least_FP bs arg_Ts get_indices callssss0 lthy;
 
     val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
@@ -423,16 +423,17 @@
        nested_map_comps = map map_comp_of_bnf nested_bnfs,
        ctr_specs = mk_ctr_specs index ctr_sugars iter_thmsss};
   in
-    ((nontriv, map mk_spec fp_sugars, missing_arg_Ts, induct_thm, induct_thms), lthy')
+    ((is_some lfp_sugar_thms, map mk_spec fp_sugars, missing_arg_Ts, induct_thm, induct_thms),
+     lthy')
   end;
 
 fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
   let
     val thy = Proof_Context.theory_of lthy;
 
-    val ((nontriv, missing_res_Ts, perm0_kks,
+    val ((missing_res_Ts, perm0_kks,
           fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
-            co_inducts = coinduct_thms, ...} :: _), lthy') =
+            co_inducts = coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy') =
       nested_to_mutual_fps lose_co_rec Greatest_FP bs res_Ts get_indices callssss0 lthy;
 
     val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
@@ -526,7 +527,7 @@
        ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss
          disc_coitersss sel_coiterssss};
   in
-    ((nontriv, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
+    ((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
       co_induct_of coinduct_thms, strong_co_induct_of coinduct_thms, co_induct_of coinduct_thmss,
       strong_co_induct_of coinduct_thmss), lthy')
   end;
diff -r 788730ab7da4 -r bd038e48526d src/HOL/BNF/Tools/bnf_lfp_compat.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Fri Sep 20 10:09:16 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Fri Sep 20 11:44:30 2013 +0200
@@ -82,17 +82,20 @@
             " not associated with new-style datatype (cf. \"datatype_new\")"));
 
     val Ts = add_nested_types_of fpT1 [];
-    val bs = map (Binding.name o prefix compatN o base_name_of_typ) Ts;
+    val b_names = map base_name_of_typ Ts;
+    val compat_b_names = map (prefix compatN) b_names;
+    val compat_bs = map Binding.name compat_b_names;
+    val common_name = compatN ^ mk_common_name b_names;
     val nn_fp = length fpTs;
     val nn = length Ts;
     val get_indices = K [];
-    val fp_sugars0 =
-      if nn = 1 then [fp_sugar0] else map (lfp_sugar_of o fst o dest_Type) Ts;
+    val fp_sugars0 = if nn = 1 then [fp_sugar0] else map (lfp_sugar_of o fst o dest_Type) Ts;
     val callssss = pad_and_indexify_calls fp_sugars0 nn [];
     val has_nested = nn > nn_fp;
 
-    val ((_, fp_sugars), lthy) =
-      mutualize_fp_sugars false has_nested Least_FP bs Ts get_indices callssss fp_sugars0 lthy;
+    val ((fp_sugars, (lfp_sugar_thms, _)), lthy) =
+      mutualize_fp_sugars false has_nested Least_FP compat_bs Ts get_indices callssss fp_sugars0
+        lthy;
 
     val {ctr_sugars, co_inducts = [induct], co_iterss, co_iter_thmsss = iter_thmsss, ...} :: _ =
       fp_sugars;
@@ -125,11 +128,41 @@
 
     val infos = map mk_info (take nn_fp fp_sugars);
 
-    val register_and_interpret =
+    val all_notes =
+      (case lfp_sugar_thms of
+        NONE => []
+      | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, fold_attrs),
+              (rec_thmss, rec_attrs)) =>
+        let
+          val common_notes =
+            (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
+            |> filter_out (null o #2)
+            |> map (fn (thmN, thms, attrs) =>
+              ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
+
+          val notes =
+            [(foldN, fold_thmss, fold_attrs),
+             (inductN, map single induct_thms, induct_attrs),
+             (recN, rec_thmss, rec_attrs)]
+            |> filter_out (null o #2)
+            |> maps (fn (thmN, thmss, attrs) =>
+              if forall null thmss then
+                []
+              else
+                map2 (fn b_name => fn thms =>
+                    ((Binding.qualify true b_name (Binding.name thmN), attrs), [(thms, [])]))
+                  compat_b_names thmss);
+        in
+          common_notes @ notes
+        end);
+
+    val register_interpret =
       Datatype_Data.register infos
       #> Datatype_Data.interpretation_data (Datatype_Aux.default_config, map fst infos)
   in
-    Local_Theory.raw_theory register_and_interpret lthy
+    lthy
+    |> Local_Theory.raw_theory register_interpret
+    |> Local_Theory.notes all_notes |> snd
   end;
 
 val _ =