src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

 
   val morph_lfp_sugar_thms: morphism -> lfp_sugar_thms -> lfp_sugar_thms
   val transfer_lfp_sugar_thms: Proof.context -> lfp_sugar_thms -> lfp_sugar_thms
 
   type gfp_sugar_thms =
-    ((thm list * thm) list * Args.src list)
+    ((thm list * thm) list * (Args.src list * Args.src list))
     * (thm list list * Args.src list)
     * (thm list list * Args.src list)
     * (thm list list * Args.src list)
     * (thm list list list * Args.src list)
 

 
 val transfer_lfp_sugar_thms =
   morph_lfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
 
 type gfp_sugar_thms =
-  ((thm list * thm) list * Args.src list)
+  ((thm list * thm) list * (Args.src list * Args.src list))
   * (thm list list * Args.src list)
   * (thm list list * Args.src list)
   * (thm list list * Args.src list)
   * (thm list list list * Args.src list);
 
-fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs),
+fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs_pair),
     (corecss, corec_attrs), (disc_corecss, disc_corec_attrs),
     (disc_corec_iffss, disc_corec_iff_attrs), (sel_corecsss, sel_corec_attrs)) =
   ((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs,
-    coinduct_attrs),
+    coinduct_attrs_pair),
    (map (map (Morphism.thm phi)) corecss, corec_attrs),
    (map (map (Morphism.thm phi)) disc_corecss, disc_corec_attrs),
    (map (map (Morphism.thm phi)) disc_corec_iffss, disc_corec_iff_attrs),
    (map (map (map (Morphism.thm phi))) sel_corecsss, sel_corec_attrs)) : gfp_sugar_thms;
 

             mk_coinduct_tac ctxt nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs fp_abs_inverses
               abs_inverses dtor_ctors exhausts ctr_defss disc_thmsss sel_thmsss)
           |> singleton (Proof_Context.export names_lthy lthy)
           |> Thm.close_derivation;
 
-        fun postproc nn thm =
-          Thm.permute_prems 0 nn
-            (if nn = 1 then thm RS mp else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm)
-          |> Drule.zero_var_indexes
-          |> `(conj_dests nn);
+        val postproc =
+          Drule.zero_var_indexes
+          #> `(conj_dests nn)
+          #>> map (fn thm => Thm.permute_prems 0 nn (thm RS mp))
+          ##> (fn thm => Thm.permute_prems 0 nn
+            (if nn = 1 then thm RS mp
+             else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm));
 
         val rel_eqs = map rel_eq_of_bnf pre_bnfs;
         val rel_monos = map rel_mono_of_bnf pre_bnfs;
         val dtor_coinducts =
           [dtor_coinduct, mk_strong_coinduct_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy]
       in
-        map2 (postproc nn oo prove) dtor_coinducts goals
+        map2 (postproc oo prove) dtor_coinducts goals
       end;
 
     fun mk_coinduct_concls ms discs ctrs =
       let
         fun mk_disc_concl disc = [name_of_disc disc];

     fun mk_sel_corec_thms corec_thmss =
       map3 (map3 (map2 o mk_sel_corec_thm)) corec_thmss selsss sel_thmsss;
 
     val sel_corec_thmsss = mk_sel_corec_thms corec_thmss;
 
-    val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
+    val common_coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
+    val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
+
     val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
     val coinduct_case_concl_attrs =
       map2 (fn casex => fn concls =>
           Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls))))
         coinduct_cases coinduct_conclss;
-    val coinduct_case_attrs =
+
+    val common_coinduct_attrs =
+      common_coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
+    val coinduct_attrs =
       coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
   in
-    ((coinduct_thms_pairs, coinduct_case_attrs),
+    ((coinduct_thms_pairs, (coinduct_attrs, common_coinduct_attrs)),
      (corec_thmss, code_nitpicksimp_attrs),
      (disc_corec_thmss, []),
      (disc_corec_iff_thmss, simp_attrs),
      (sel_corec_thmsss, simp_attrs))
   end;

                   val (((Ds, As), Bs), names_lthy) = lthy
                     |> mk_TFrees (dead_of_bnf fp_bnf)
                     ||>> mk_TFrees (live_of_bnf fp_bnf)
                     ||>> mk_TFrees (live_of_bnf fp_bnf);
                   val TA as Type (_, ADs) = mk_T_of_bnf Ds As fp_bnf;
-                  val TB as Type (_, BDs) = mk_T_of_bnf Ds Bs fp_bnf;
+                  val Type (_, BDs) = mk_T_of_bnf Ds Bs fp_bnf;
                   val fTs = map2 (curry op -->) As Bs;
                   val ((fs, ta), names_lthy) = names_lthy
                     |> mk_Frees "f" fTs
                     ||>> yield_singleton (mk_Frees "a") TA;
                   val map_term = mk_map_of_bnf Ds As Bs fp_bnf;

     fun derive_note_coinduct_corecs_thms_for_types
         ((((mapss, rel_injectss, rel_distinctss, setss), (_, _, ctr_defss, ctr_sugars)),
           (corecs, corec_defs)), lthy) =
       let
         val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
-              coinduct_attrs),
+              (coinduct_attrs, common_coinduct_attrs)),
              (corec_thmss, corec_attrs), (disc_corec_thmss, disc_corec_attrs),
              (disc_corec_iff_thmss, disc_corec_iff_attrs), (sel_corec_thmsss, sel_corec_attrs)) =
           derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
             dtor_injects dtor_ctors xtor_co_rec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
             abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs

             (map3 flat_corec_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss)
             mapss rel_injectss rel_distinctss setss;
 
         val common_notes =
           (if nn > 1 then
-             [(coinductN, [coinduct_thm], coinduct_attrs),
-              (strong_coinductN, [strong_coinduct_thm], coinduct_attrs)]
+             [(coinductN, [coinduct_thm], common_coinduct_attrs),
+              (strong_coinductN, [strong_coinduct_thm], common_coinduct_attrs)]
            else
              [])
           |> massage_simple_notes fp_common_name;
 
         val notes =