src/HOL/BNF/Tools/bnf_fp_util.ML
changeset 52328 2f286a2b7f98
parent 52314 9606cf677021
child 52330 8ce7fba90bb3
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Jun 06 22:01:42 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Fri Jun 07 08:48:59 2013 +0200
     1.3 @@ -15,8 +15,7 @@
     1.4       bnfs: BNF_Def.bnf list,
     1.5       ctors: term list,
     1.6       dtors: term list,
     1.7 -     xtor_un_folds: term list,
     1.8 -     xtor_co_recs: term list,
     1.9 +     xtor_co_iterss: term list list,
    1.10       xtor_co_induct: thm,
    1.11       xtor_strong_co_induct: thm,
    1.12       dtor_ctors: thm list,
    1.13 @@ -25,8 +24,7 @@
    1.14       xtor_map_thms: thm list,
    1.15       xtor_set_thmss: thm list list,
    1.16       xtor_rel_thms: thm list,
    1.17 -     xtor_un_fold_thms: thm list,
    1.18 -     xtor_co_rec_thms: thm list}
    1.19 +     xtor_co_iter_thmss: thm list list}
    1.20  
    1.21    val morph_fp_result: morphism -> fp_result -> fp_result
    1.22    val eq_fp_result: fp_result * fp_result -> bool
    1.23 @@ -185,8 +183,7 @@
    1.24     bnfs: BNF_Def.bnf list,
    1.25     ctors: term list,
    1.26     dtors: term list,
    1.27 -   xtor_un_folds: term list,
    1.28 -   xtor_co_recs: term list,
    1.29 +   xtor_co_iterss: term list list,
    1.30     xtor_co_induct: thm,
    1.31     xtor_strong_co_induct: thm,
    1.32     dtor_ctors: thm list,
    1.33 @@ -195,18 +192,16 @@
    1.34     xtor_map_thms: thm list,
    1.35     xtor_set_thmss: thm list list,
    1.36     xtor_rel_thms: thm list,
    1.37 -   xtor_un_fold_thms: thm list,
    1.38 -   xtor_co_rec_thms: thm list};
    1.39 +   xtor_co_iter_thmss: thm list list};
    1.40  
    1.41 -fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_un_folds, xtor_co_recs, xtor_co_induct,
    1.42 +fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_iterss, xtor_co_induct,
    1.43      xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, xtor_map_thms, xtor_set_thmss,
    1.44 -    xtor_rel_thms, xtor_un_fold_thms, xtor_co_rec_thms} =
    1.45 +    xtor_rel_thms, xtor_co_iter_thmss} =
    1.46    {Ts = map (Morphism.typ phi) Ts,
    1.47     bnfs = map (morph_bnf phi) bnfs,
    1.48     ctors = map (Morphism.term phi) ctors,
    1.49     dtors = map (Morphism.term phi) dtors,
    1.50 -   xtor_un_folds = map (Morphism.term phi) xtor_un_folds,
    1.51 -   xtor_co_recs = map (Morphism.term phi) xtor_co_recs,
    1.52 +   xtor_co_iterss = map (map (Morphism.term phi)) xtor_co_iterss,
    1.53     xtor_co_induct = Morphism.thm phi xtor_co_induct,
    1.54     xtor_strong_co_induct = Morphism.thm phi xtor_strong_co_induct,
    1.55     dtor_ctors = map (Morphism.thm phi) dtor_ctors,
    1.56 @@ -215,8 +210,7 @@
    1.57     xtor_map_thms = map (Morphism.thm phi) xtor_map_thms,
    1.58     xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss,
    1.59     xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms,
    1.60 -   xtor_un_fold_thms = map (Morphism.thm phi) xtor_un_fold_thms,
    1.61 -   xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms};
    1.62 +   xtor_co_iter_thmss = map (map (Morphism.thm phi)) xtor_co_iter_thmss};
    1.63  
    1.64  fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
    1.65    eq_list eq_bnf (bnfs1, bnfs2);