src/HOL/Codatatype/Tools/bnf_gfp.ML
changeset 49231 43d2df313559
parent 49228 e43910ccee74
child 49255 2ecc533d6697
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sun Sep 09 12:51:17 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sun Sep 09 13:04:57 2012 +0200
     1.3 @@ -2121,9 +2121,10 @@
     1.4      val fld_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_fld_thms;
     1.5      val fld_exhaust_thms = map (fn thm => thm RS exE) fld_nchotomy_thms;
     1.6  
     1.7 -    val fld_coiter_thms = map3 (fn unf_inject => fn coiter => fn unf_fld =>
     1.8 -      iffD1 OF [unf_inject, trans OF [coiter, unf_fld RS sym]])
     1.9 -      unf_inject_thms coiter_thms unf_fld_thms;
    1.10 +    fun mk_fld_unf_coiter_like_thm unf_inject unf_fld coiter =
    1.11 +      iffD1 OF [unf_inject, trans OF [coiter, unf_fld RS sym]];
    1.12 +
    1.13 +    val fld_coiter_thms = map3 mk_fld_unf_coiter_like_thm unf_inject_thms unf_fld_thms coiter_thms;
    1.14  
    1.15      val timer = time (timer "fld definitions & thms");
    1.16  
    1.17 @@ -2189,6 +2190,8 @@
    1.18          goals coiter_thms map_congs
    1.19        end;
    1.20  
    1.21 +    val fld_corec_thms = map3 mk_fld_unf_coiter_like_thm unf_inject_thms unf_fld_thms corec_thms;
    1.22 +
    1.23      val timer = time (timer "corec definitions & thms");
    1.24  
    1.25      val (unf_coinduct_thm, coinduct_params, rel_coinduct_thm, pred_coinduct_thm,
    1.26 @@ -2989,7 +2992,8 @@
    1.27          (unf_exhaustN, unf_exhaust_thms),
    1.28          (fld_injectN, fld_inject_thms),
    1.29          (fld_exhaustN, fld_exhaust_thms),
    1.30 -        (fld_unf_coitersN, fld_coiter_thms)]
    1.31 +        (fld_unf_coitersN, fld_coiter_thms),
    1.32 +        (fld_unf_corecsN, fld_corec_thms)]
    1.33          |> map (apsnd (map single))
    1.34          |> maps (fn (thmN, thmss) =>
    1.35            map2 (fn b => fn thms =>
    1.36 @@ -2997,7 +3001,7 @@
    1.37            bs thmss)
    1.38    in
    1.39      ((unfs, flds, coiters, corecs, unf_fld_thms, fld_unf_thms, fld_inject_thms, fld_coiter_thms,
    1.40 -      corec_thms (* FIXME: should be "fld_corec_thms" *)),
    1.41 +      fld_corec_thms),
    1.42       lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    1.43    end;
    1.44