generate "fld_unf_corecs" as well
authorblanchet
Sun Sep 09 13:04:57 2012 +0200 (2012-09-09)
changeset 4923143d2df313559
parent 49230 0e551c2d5d8b
child 49232 9ea11f0c53e4
generate "fld_unf_corecs" as well
src/HOL/Codatatype/Tools/bnf_fp_util.ML
src/HOL/Codatatype/Tools/bnf_gfp.ML
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sun Sep 09 12:51:17 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sun Sep 09 13:04:57 2012 +0200
     1.3 @@ -22,7 +22,6 @@
     1.4    val corecN: string
     1.5    val exhaustN: string
     1.6    val fldN: string
     1.7 -  val fld_unf_coitersN: string
     1.8    val fld_exhaustN: string
     1.9    val fld_induct2N: string
    1.10    val fld_inductN: string
    1.11 @@ -32,6 +31,8 @@
    1.12    val fld_recN: string
    1.13    val fld_recsN: string
    1.14    val fld_unfN: string
    1.15 +  val fld_unf_coitersN: string
    1.16 +  val fld_unf_corecsN: string
    1.17    val hsetN: string
    1.18    val hset_recN: string
    1.19    val inductN: string
    1.20 @@ -166,6 +167,7 @@
    1.21  val fld_recsN = fld_recN ^ "s"
    1.22  val unf_corecN = unfN ^ "_" ^ corecN
    1.23  val unf_corecsN = unf_corecN ^ "s"
    1.24 +val fld_unf_corecsN = fldN ^ "_" ^ unf_corecN ^ "s"
    1.25  
    1.26  val fld_unfN = fldN ^ "_" ^ unfN
    1.27  val unf_fldN = unfN ^ "_" ^ fldN
     2.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sun Sep 09 12:51:17 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sun Sep 09 13:04:57 2012 +0200
     2.3 @@ -2121,9 +2121,10 @@
     2.4      val fld_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_fld_thms;
     2.5      val fld_exhaust_thms = map (fn thm => thm RS exE) fld_nchotomy_thms;
     2.6  
     2.7 -    val fld_coiter_thms = map3 (fn unf_inject => fn coiter => fn unf_fld =>
     2.8 -      iffD1 OF [unf_inject, trans OF [coiter, unf_fld RS sym]])
     2.9 -      unf_inject_thms coiter_thms unf_fld_thms;
    2.10 +    fun mk_fld_unf_coiter_like_thm unf_inject unf_fld coiter =
    2.11 +      iffD1 OF [unf_inject, trans OF [coiter, unf_fld RS sym]];
    2.12 +
    2.13 +    val fld_coiter_thms = map3 mk_fld_unf_coiter_like_thm unf_inject_thms unf_fld_thms coiter_thms;
    2.14  
    2.15      val timer = time (timer "fld definitions & thms");
    2.16  
    2.17 @@ -2189,6 +2190,8 @@
    2.18          goals coiter_thms map_congs
    2.19        end;
    2.20  
    2.21 +    val fld_corec_thms = map3 mk_fld_unf_coiter_like_thm unf_inject_thms unf_fld_thms corec_thms;
    2.22 +
    2.23      val timer = time (timer "corec definitions & thms");
    2.24  
    2.25      val (unf_coinduct_thm, coinduct_params, rel_coinduct_thm, pred_coinduct_thm,
    2.26 @@ -2989,7 +2992,8 @@
    2.27          (unf_exhaustN, unf_exhaust_thms),
    2.28          (fld_injectN, fld_inject_thms),
    2.29          (fld_exhaustN, fld_exhaust_thms),
    2.30 -        (fld_unf_coitersN, fld_coiter_thms)]
    2.31 +        (fld_unf_coitersN, fld_coiter_thms),
    2.32 +        (fld_unf_corecsN, fld_corec_thms)]
    2.33          |> map (apsnd (map single))
    2.34          |> maps (fn (thmN, thmss) =>
    2.35            map2 (fn b => fn thms =>
    2.36 @@ -2997,7 +3001,7 @@
    2.37            bs thmss)
    2.38    in
    2.39      ((unfs, flds, coiters, corecs, unf_fld_thms, fld_unf_thms, fld_inject_thms, fld_coiter_thms,
    2.40 -      corec_thms (* FIXME: should be "fld_corec_thms" *)),
    2.41 +      fld_corec_thms),
    2.42       lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    2.43    end;
    2.44