register coinductive type's coinduct rule
authorblanchet
Thu Apr 25 18:14:04 2013 +0200 (2013-04-25)
changeset 5178067e4ed510dfb
parent 51779 273e7a90b167
child 51781 0504e286d66d
register coinductive type's coinduct rule
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Apr 25 17:25:10 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Apr 25 18:14:04 2013 +0200
     1.3 @@ -309,6 +309,20 @@
     1.4  
     1.5      val fpTs = map (domain_type o fastype_of) dtors;
     1.6  
     1.7 +    fun massage_simple_notes base =
     1.8 +      filter_out (null o #2)
     1.9 +      #> map (fn (thmN, thms, attrs) =>
    1.10 +        ((qualify true base (Binding.name thmN), attrs), [(thms, [])]));
    1.11 +
    1.12 +    val massage_multi_notes =
    1.13 +      maps (fn (thmN, thmss, attrs) =>
    1.14 +        if forall null thmss then
    1.15 +          []
    1.16 +        else
    1.17 +          map3 (fn fp_b_name => fn Type (T_name, _) => fn thms =>
    1.18 +            ((qualify true fp_b_name (Binding.name thmN), attrs T_name),
    1.19 +             [(thms, [])])) fp_b_names fpTs thmss);
    1.20 +
    1.21      val exists_fp_subtype = exists_subtype (member (op =) fpTs);
    1.22      val exists_Cs_subtype = exists_subtype (member (op =) Cs);
    1.23  
    1.24 @@ -598,9 +612,7 @@
    1.25                 (rel_distinctN, rel_distinct_thms, code_simp_attrs),
    1.26                 (rel_injectN, rel_inject_thms, code_simp_attrs),
    1.27                 (setsN, flat set_thmss, code_simp_attrs)]
    1.28 -              |> filter_out (null o #2)
    1.29 -              |> map (fn (thmN, thms, attrs) =>
    1.30 -                ((qualify true fp_b_name (Binding.name thmN), attrs), [(thms, [])]));
    1.31 +              |> massage_simple_notes fp_b_name;
    1.32            in
    1.33              (wrap_res, lthy |> Local_Theory.notes notes |> snd)
    1.34            end;
    1.35 @@ -883,8 +895,7 @@
    1.36  
    1.37          val common_notes =
    1.38            (if nn > 1 then [(inductN, [induct_thm], [induct_case_names_attr])] else [])
    1.39 -          |> map (fn (thmN, thms, attrs) =>
    1.40 -            ((qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
    1.41 +          |> massage_simple_notes fp_common_name;
    1.42  
    1.43          val notes =
    1.44            [(foldN, fold_thmss, K code_simp_attrs),
    1.45 @@ -892,10 +903,7 @@
    1.46              fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
    1.47             (recN, rec_thmss, K code_simp_attrs),
    1.48             (simpsN, simp_thmss, K [])]
    1.49 -          |> maps (fn (thmN, thmss, attrs) =>
    1.50 -            map3 (fn fp_b_name => fn Type (T_name, _) => fn thms =>
    1.51 -              ((qualify true fp_b_name (Binding.name thmN), attrs T_name),
    1.52 -               [(thms, [])])) fp_b_names fpTs thmss);
    1.53 +          |> massage_multi_notes;
    1.54        in
    1.55          lthy |> Local_Theory.notes (common_notes @ notes) |> snd
    1.56        end;
    1.57 @@ -1158,6 +1166,7 @@
    1.58              coinduct_cases coinduct_conclss;
    1.59          val coinduct_case_attrs =
    1.60            coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
    1.61 +        fun coinduct_type_attr T_name = Attrib.internal (K (Induct.coinduct_type T_name));
    1.62  
    1.63          val common_notes =
    1.64            (if nn > 1 then
    1.65 @@ -1165,25 +1174,22 @@
    1.66                (strong_coinductN, [strong_coinduct_thm], coinduct_case_attrs)]
    1.67             else
    1.68               [])
    1.69 -          |> map (fn (thmN, thms, attrs) =>
    1.70 -            ((qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
    1.71 +          |> massage_simple_notes fp_common_name;
    1.72  
    1.73          val notes =
    1.74 -          [(coinductN, map single coinduct_thms, coinduct_case_attrs),
    1.75 -           (corecN, corec_thmss, []),
    1.76 -           (disc_corecN, disc_corec_thmss, simp_attrs),
    1.77 -           (disc_corec_iffN, disc_corec_iff_thmss, simp_attrs),
    1.78 -           (disc_unfoldN, disc_unfold_thmss, simp_attrs),
    1.79 -           (disc_unfold_iffN, disc_unfold_iff_thmss, simp_attrs),
    1.80 -           (sel_corecN, sel_corec_thmss, simp_attrs),
    1.81 -           (sel_unfoldN, sel_unfold_thmss, simp_attrs),
    1.82 -           (simpsN, simp_thmss, []),
    1.83 -           (strong_coinductN, map single strong_coinduct_thms, coinduct_case_attrs),
    1.84 -           (unfoldN, unfold_thmss, [])]
    1.85 -          |> maps (fn (thmN, thmss, attrs) =>
    1.86 -            map_filter (fn (_, []) => NONE | (fp_b_name, thms) =>
    1.87 -              SOME ((qualify true fp_b_name (Binding.name thmN), attrs),
    1.88 -                [(thms, [])])) (fp_b_names ~~ thmss));
    1.89 +          [(coinductN, map single coinduct_thms,
    1.90 +            fn T_name => coinduct_case_attrs @ [coinduct_type_attr T_name]),
    1.91 +           (corecN, corec_thmss, K []),
    1.92 +           (disc_corecN, disc_corec_thmss, K simp_attrs),
    1.93 +           (disc_corec_iffN, disc_corec_iff_thmss, K simp_attrs),
    1.94 +           (disc_unfoldN, disc_unfold_thmss, K simp_attrs),
    1.95 +           (disc_unfold_iffN, disc_unfold_iff_thmss, K simp_attrs),
    1.96 +           (sel_corecN, sel_corec_thmss, K simp_attrs),
    1.97 +           (sel_unfoldN, sel_unfold_thmss, K simp_attrs),
    1.98 +           (simpsN, simp_thmss, K []),
    1.99 +           (strong_coinductN, map single strong_coinduct_thms, K coinduct_case_attrs),
   1.100 +           (unfoldN, unfold_thmss, K [])]
   1.101 +          |> massage_multi_notes;
   1.102        in
   1.103          lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
   1.104        end;