src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 58579 b7bc5ba2f3fb
parent 58578 9ff8ca957c02
child 58580 8ee2d984caa8
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 13:37:38 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 13:38:13 2014 +0200
     1.3 @@ -164,7 +164,7 @@
     1.4      val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;
     1.5  
     1.6      val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) pre_bnfs;
     1.7 -    val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #rel_xtor_co_induct_thm)
     1.8 +    val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #xtor_rel_co_induct)
     1.9        |> map (unfold_thms lthy (id_apply :: rel_unfolds));
    1.10  
    1.11      val rel_defs = map rel_def_of_bnf bnfs;
    1.12 @@ -185,8 +185,8 @@
    1.13      val fp_or_nesting_rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs);
    1.14      val fp_or_nesting_rel_monos = map rel_mono_of_bnf fp_or_nesting_bnfs;
    1.15  
    1.16 -    val rel_xtor_co_induct_thm =
    1.17 -      mk_rel_xtor_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys
    1.18 +    val xtor_rel_co_induct =
    1.19 +      mk_xtor_rel_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys
    1.20          xtors xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs
    1.21            rel_monos fp_or_nesting_rel_eqs fp_or_nesting_rel_monos)
    1.22          lthy;
    1.23 @@ -208,7 +208,7 @@
    1.24              fun mk_type_copy_thms thm = map (curry op RS thm)
    1.25                @{thms type_copy_Rep_o_Abs type_copy_vimage2p_Grp_Abs};
    1.26            in
    1.27 -            cterm_instantiate_pos cts rel_xtor_co_induct_thm
    1.28 +            cterm_instantiate_pos cts xtor_rel_co_induct
    1.29              |> singleton (Proof_Context.export names_lthy lthy)
    1.30              |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @
    1.31                  fp_or_nesting_rel_eqs)
    1.32 @@ -225,7 +225,7 @@
    1.33            let
    1.34              val cts = NONE :: map (SOME o certify lthy) (map HOLogic.eq_const As);
    1.35            in
    1.36 -            cterm_instantiate_pos cts rel_xtor_co_induct_thm
    1.37 +            cterm_instantiate_pos cts xtor_rel_co_induct
    1.38              |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @
    1.39                  fp_or_nesting_rel_eqs)
    1.40              |> funpow (2 * n) (fn thm => thm RS spec)
    1.41 @@ -476,7 +476,7 @@
    1.42          xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
    1.43          xtor_co_rec_thms = xtor_co_rec_thms,
    1.44          xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*),
    1.45 -        rel_xtor_co_induct_thm = rel_xtor_co_induct_thm,
    1.46 +        xtor_rel_co_induct = xtor_rel_co_induct,
    1.47          dtor_set_induct_thms = [],
    1.48          xtor_co_rec_transfer_thms = []}
    1.49         |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));