generate proper attributes for coinduction rules

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Apr 25 13:22:45 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Apr 25 17:13:24 2013 +0200
@@ -31,7 +31,9 @@
 open BNF_FP
 open BNF_FP_Def_Sugar_Tactics
 
-(* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A") *)
+val EqN = "Eq";
+
+(* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *)
 fun quasi_unambiguous_case_names names =
   let
     val ps = map (`Long_Name.base_name) names;
@@ -987,6 +989,21 @@
             (postproc nn (prove fp_induct goal), postproc nn (prove fp_strong_induct strong_goal))
           end;
 
+        fun mk_coinduct_concls ms discs ctrs =
+          let
+            fun mk_disc_concl disc = [name_of_disc disc];
+            fun mk_ctr_concl 0 _ = []
+              | mk_ctr_concl _ ctor = [name_of_ctr ctor];
+            val disc_concls = map mk_disc_concl (fst (split_last discs)) @ [[]];
+            val ctr_concls = map2 mk_ctr_concl ms ctrs;
+          in
+            flat (map2 append disc_concls ctr_concls)
+          end;
+
+        val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names);
+        val coinduct_conclss =
+          map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
+
         fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
 
         val gunfolds = map (lists_bmoc pgss) unfolds;
@@ -1133,18 +1150,26 @@
           [(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)]
           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
 
+        val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
+        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 =
+          coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
+
         val common_notes =
           (if nn > 1 then
-             (* FIXME: attribs *)
-             [(coinductN, [coinduct_thm], []),
-              (strong_coinductN, [strong_coinduct_thm], [])]
+             [(coinductN, [coinduct_thm], coinduct_case_attrs),
+              (strong_coinductN, [strong_coinduct_thm], coinduct_case_attrs)]
            else
              [])
           |> map (fn (thmN, thms, attrs) =>
             ((qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
 
         val notes =
-          [(coinductN, map single coinduct_thms, []), (* FIXME: attribs *)
+          [(coinductN, map single coinduct_thms, coinduct_case_attrs),
            (corecN, corec_thmss, []),
            (disc_corecN, disc_corec_thmss, simp_attrs),
            (disc_corec_iffN, disc_corec_iff_thmss, simp_attrs),
@@ -1153,7 +1178,7 @@
            (sel_corecN, sel_corec_thmss, simp_attrs),
            (sel_unfoldN, sel_unfold_thmss, simp_attrs),
            (simpsN, simp_thmss, []),
-           (strong_coinductN, map single strong_coinduct_thms, []), (* FIXME: attribs *)
+           (strong_coinductN, map single strong_coinduct_thms, coinduct_case_attrs),
            (unfoldN, unfold_thmss, [])]
           |> maps (fn (thmN, thmss, attrs) =>
             map_filter (fn (_, []) => NONE | (fp_b_name, thms) =>

--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Apr 25 13:22:45 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Apr 25 17:13:24 2013 +0200
@@ -16,6 +16,7 @@
   val mk_disc_or_sel: typ list -> term -> term
 
   val name_of_ctr: term -> string
+  val name_of_disc: term -> string
 
   val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     (((bool * bool) * term list) * term) *
@@ -96,11 +97,27 @@
     Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) t
   end;
 
-fun name_of_ctr c =
-  (case head_of c of
+fun name_of_const what t =
+  (case head_of t of
     Const (s, _) => s
   | Free (s, _) => s
-  | _ => error "Cannot extract name of constructor");
+  | _ => error ("Cannot extract name of " ^ what));
+
+val name_of_ctr = name_of_const "constructor";
+
+val notN = "not_";
+val eqN = "eq_";
+val neqN = "neq_";
+
+fun name_of_disc t =
+  (case head_of t of
+    Abs (_, _, @{const Not} $ (t' $ Bound 0)) =>
+    Long_Name.map_base_name (prefix notN) (name_of_disc t')
+  | Abs (_, _, Const (@{const_name HOL.eq}, _) $ Bound 0 $ t') =>
+    Long_Name.map_base_name (prefix eqN) (name_of_disc t')
+  | Abs (_, _, @{const Not} $ (Const (@{const_name HOL.eq}, _) $ Bound 0 $ t')) =>
+    Long_Name.map_base_name (prefix neqN) (name_of_disc t')
+  | t' => name_of_const "destructor" t');
 
 val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
 
@@ -200,7 +217,6 @@
     val xgs = map2 (curry Term.list_comb) gs xss;
 
     val fcase = Term.list_comb (casex, fs);
-    val gcase = Term.list_comb (casex, gs);
 
     val ufcase = fcase $ u;
     val vfcase = fcase $ v;