src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 51777 48a0ae342ea0
parent 51769 5c657ca97d99
child 51780 67e4ed510dfb
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Apr 25 13:22:45 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Apr 25 17:13:24 2013 +0200
     1.3 @@ -31,7 +31,9 @@
     1.4  open BNF_FP
     1.5  open BNF_FP_Def_Sugar_Tactics
     1.6  
     1.7 -(* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A") *)
     1.8 +val EqN = "Eq";
     1.9 +
    1.10 +(* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *)
    1.11  fun quasi_unambiguous_case_names names =
    1.12    let
    1.13      val ps = map (`Long_Name.base_name) names;
    1.14 @@ -987,6 +989,21 @@
    1.15              (postproc nn (prove fp_induct goal), postproc nn (prove fp_strong_induct strong_goal))
    1.16            end;
    1.17  
    1.18 +        fun mk_coinduct_concls ms discs ctrs =
    1.19 +          let
    1.20 +            fun mk_disc_concl disc = [name_of_disc disc];
    1.21 +            fun mk_ctr_concl 0 _ = []
    1.22 +              | mk_ctr_concl _ ctor = [name_of_ctr ctor];
    1.23 +            val disc_concls = map mk_disc_concl (fst (split_last discs)) @ [[]];
    1.24 +            val ctr_concls = map2 mk_ctr_concl ms ctrs;
    1.25 +          in
    1.26 +            flat (map2 append disc_concls ctr_concls)
    1.27 +          end;
    1.28 +
    1.29 +        val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names);
    1.30 +        val coinduct_conclss =
    1.31 +          map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
    1.32 +
    1.33          fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
    1.34  
    1.35          val gunfolds = map (lists_bmoc pgss) unfolds;
    1.36 @@ -1133,18 +1150,26 @@
    1.37            [(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)]
    1.38            |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
    1.39  
    1.40 +        val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
    1.41 +        val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
    1.42 +        val coinduct_case_concl_attrs =
    1.43 +          map2 (fn casex => fn concls =>
    1.44 +              Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls))))
    1.45 +            coinduct_cases coinduct_conclss;
    1.46 +        val coinduct_case_attrs =
    1.47 +          coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
    1.48 +
    1.49          val common_notes =
    1.50            (if nn > 1 then
    1.51 -             (* FIXME: attribs *)
    1.52 -             [(coinductN, [coinduct_thm], []),
    1.53 -              (strong_coinductN, [strong_coinduct_thm], [])]
    1.54 +             [(coinductN, [coinduct_thm], coinduct_case_attrs),
    1.55 +              (strong_coinductN, [strong_coinduct_thm], coinduct_case_attrs)]
    1.56             else
    1.57               [])
    1.58            |> map (fn (thmN, thms, attrs) =>
    1.59              ((qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
    1.60  
    1.61          val notes =
    1.62 -          [(coinductN, map single coinduct_thms, []), (* FIXME: attribs *)
    1.63 +          [(coinductN, map single coinduct_thms, coinduct_case_attrs),
    1.64             (corecN, corec_thmss, []),
    1.65             (disc_corecN, disc_corec_thmss, simp_attrs),
    1.66             (disc_corec_iffN, disc_corec_iff_thmss, simp_attrs),
    1.67 @@ -1153,7 +1178,7 @@
    1.68             (sel_corecN, sel_corec_thmss, simp_attrs),
    1.69             (sel_unfoldN, sel_unfold_thmss, simp_attrs),
    1.70             (simpsN, simp_thmss, []),
    1.71 -           (strong_coinductN, map single strong_coinduct_thms, []), (* FIXME: attribs *)
    1.72 +           (strong_coinductN, map single strong_coinduct_thms, coinduct_case_attrs),
    1.73             (unfoldN, unfold_thmss, [])]
    1.74            |> maps (fn (thmN, thmss, attrs) =>
    1.75              map_filter (fn (_, []) => NONE | (fp_b_name, thms) =>