tuned record field names to avoid confusion between low-level and high-level constants/theorems
authorblanchet
Thu Jun 06 11:33:41 2013 +0200 (2013-06-06)
changeset 52312f461dca57c66
parent 52311 e2f6ac15d79a
child 52313 62f794b9e9cc
tuned record field names to avoid confusion between low-level and high-level constants/theorems
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_fp_util.ML
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_lfp.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Jun 06 11:19:04 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Jun 06 11:33:41 2013 +0200
     1.3 @@ -1079,10 +1079,10 @@
     1.4        map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_sum_prod_Ts;
     1.5  
     1.6      val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0,
     1.7 -           un_folds = fp_folds0, co_recs = fp_recs0, co_induct = fp_induct,
     1.8 -           strong_co_induct = fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects,
     1.9 +           xtor_un_folds = fp_folds0, xtor_co_recs = fp_recs0, xtor_co_induct = fp_induct,
    1.10 +           xtor_strong_co_induct = fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects,
    1.11             map_thms = fp_map_thms, set_thmss = fp_set_thmss, rel_thms = fp_rel_thms,
    1.12 -           un_fold_thms = fp_fold_thms, co_rec_thms = fp_rec_thms, ...}, lthy)) =
    1.13 +           xtor_un_fold_thms = fp_fold_thms, xtor_co_rec_thms = fp_rec_thms, ...}, lthy)) =
    1.14        fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs
    1.15          no_defs_lthy0;
    1.16  
     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Jun 06 11:19:04 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Jun 06 11:33:41 2013 +0200
     2.3 @@ -15,18 +15,18 @@
     2.4       bnfs: BNF_Def.bnf list,
     2.5       ctors: term list,
     2.6       dtors: term list,
     2.7 -     un_folds: term list,
     2.8 -     co_recs: term list,
     2.9 -     co_induct: thm,
    2.10 -     strong_co_induct: thm,
    2.11 +     xtor_un_folds: term list,
    2.12 +     xtor_co_recs: term list,
    2.13 +     xtor_co_induct: thm,
    2.14 +     xtor_strong_co_induct: thm,
    2.15       dtor_ctors: thm list,
    2.16       ctor_dtors: thm list,
    2.17       ctor_injects: thm list,
    2.18       map_thms: thm list,
    2.19       set_thmss: thm list list,
    2.20       rel_thms: thm list,
    2.21 -     un_fold_thms: thm list,
    2.22 -     co_rec_thms: thm list}
    2.23 +     xtor_un_fold_thms: thm list,
    2.24 +     xtor_co_rec_thms: thm list}
    2.25  
    2.26    val morph_fp_result: morphism -> fp_result -> fp_result
    2.27    val eq_fp_result: fp_result * fp_result -> bool
    2.28 @@ -185,38 +185,38 @@
    2.29     bnfs: BNF_Def.bnf list,
    2.30     ctors: term list,
    2.31     dtors: term list,
    2.32 -   un_folds: term list,
    2.33 -   co_recs: term list,
    2.34 -   co_induct: thm,
    2.35 -   strong_co_induct: thm,
    2.36 +   xtor_un_folds: term list,
    2.37 +   xtor_co_recs: term list,
    2.38 +   xtor_co_induct: thm,
    2.39 +   xtor_strong_co_induct: thm,
    2.40     dtor_ctors: thm list,
    2.41     ctor_dtors: thm list,
    2.42     ctor_injects: thm list,
    2.43     map_thms: thm list,
    2.44     set_thmss: thm list list,
    2.45     rel_thms: thm list,
    2.46 -   un_fold_thms: thm list,
    2.47 -   co_rec_thms: thm list};
    2.48 +   xtor_un_fold_thms: thm list,
    2.49 +   xtor_co_rec_thms: thm list};
    2.50  
    2.51 -fun morph_fp_result phi {Ts, bnfs, ctors, dtors, un_folds, co_recs, co_induct, strong_co_induct,
    2.52 -    dtor_ctors, ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms, un_fold_thms,
    2.53 -    co_rec_thms} =
    2.54 +fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_un_folds, xtor_co_recs, xtor_co_induct,
    2.55 +    xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms,
    2.56 +    xtor_un_fold_thms, xtor_co_rec_thms} =
    2.57    {Ts = map (Morphism.typ phi) Ts,
    2.58     bnfs = map (morph_bnf phi) bnfs,
    2.59     ctors = map (Morphism.term phi) ctors,
    2.60     dtors = map (Morphism.term phi) dtors,
    2.61 -   un_folds = map (Morphism.term phi) un_folds,
    2.62 -   co_recs = map (Morphism.term phi) co_recs,
    2.63 -   co_induct = Morphism.thm phi co_induct,
    2.64 -   strong_co_induct = Morphism.thm phi strong_co_induct,
    2.65 +   xtor_un_folds = map (Morphism.term phi) xtor_un_folds,
    2.66 +   xtor_co_recs = map (Morphism.term phi) xtor_co_recs,
    2.67 +   xtor_co_induct = Morphism.thm phi xtor_co_induct,
    2.68 +   xtor_strong_co_induct = Morphism.thm phi xtor_strong_co_induct,
    2.69     dtor_ctors = map (Morphism.thm phi) dtor_ctors,
    2.70     ctor_dtors = map (Morphism.thm phi) ctor_dtors,
    2.71     ctor_injects = map (Morphism.thm phi) ctor_injects,
    2.72     map_thms = map (Morphism.thm phi) map_thms,
    2.73     set_thmss = map (map (Morphism.thm phi)) set_thmss,
    2.74     rel_thms = map (Morphism.thm phi) rel_thms,
    2.75 -   un_fold_thms = map (Morphism.thm phi) un_fold_thms,
    2.76 -   co_rec_thms = map (Morphism.thm phi) co_rec_thms};
    2.77 +   xtor_un_fold_thms = map (Morphism.thm phi) xtor_un_fold_thms,
    2.78 +   xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms};
    2.79  
    2.80  fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
    2.81    eq_list eq_bnf (bnfs1, bnfs2);
     3.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Jun 06 11:19:04 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Jun 06 11:33:41 2013 +0200
     3.3 @@ -3107,12 +3107,13 @@
     3.4            bs thmss)
     3.5    in
     3.6      timer;
     3.7 -    ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, un_folds = unfolds, co_recs = corecs,
     3.8 -      co_induct = dtor_coinduct_thm, strong_co_induct = dtor_strong_coinduct_thm,
     3.9 -      dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
    3.10 +    ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_un_folds = unfolds,
    3.11 +      xtor_co_recs = corecs, xtor_co_induct = dtor_coinduct_thm,
    3.12 +      xtor_strong_co_induct = dtor_strong_coinduct_thm, dtor_ctors = dtor_ctor_thms,
    3.13 +      ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
    3.14        map_thms = folded_dtor_map_thms, set_thmss = folded_dtor_set_thmss',
    3.15 -      rel_thms = dtor_Jrel_thms, un_fold_thms = ctor_dtor_unfold_thms,
    3.16 -      co_rec_thms = ctor_dtor_corec_thms},
    3.17 +      rel_thms = dtor_Jrel_thms, xtor_un_fold_thms = ctor_dtor_unfold_thms,
    3.18 +      xtor_co_rec_thms = ctor_dtor_corec_thms},
    3.19       lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    3.20    end;
    3.21  
     4.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Jun 06 11:19:04 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Jun 06 11:33:41 2013 +0200
     4.3 @@ -1856,11 +1856,12 @@
     4.4            bs thmss)
     4.5    in
     4.6      timer;
     4.7 -    ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, un_folds = folds, co_recs = recs,
     4.8 -      co_induct = ctor_induct_thm, strong_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
     4.9 +    ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_un_folds = folds,
    4.10 +      xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm,
    4.11 +      xtor_strong_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
    4.12        ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, map_thms = folded_ctor_map_thms,
    4.13 -      set_thmss = folded_ctor_set_thmss', rel_thms = ctor_Irel_thms, un_fold_thms = ctor_fold_thms,
    4.14 -      co_rec_thms = ctor_rec_thms},
    4.15 +      set_thmss = folded_ctor_set_thmss', rel_thms = ctor_Irel_thms,
    4.16 +      xtor_un_fold_thms = ctor_fold_thms, xtor_co_rec_thms = ctor_rec_thms},
    4.17       lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    4.18    end;
    4.19