src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 55868 37b99986d435
parent 55854 ee270328a781
child 55894 8f3fe443948a
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Mar 03 12:48:20 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Mar 03 12:48:20 2014 +0100
     1.3 @@ -236,7 +236,8 @@
     1.4        |> mk_Frees' "s" fold_strTs
     1.5        ||>> mk_Frees' "s" rec_strTs;
     1.6  
     1.7 -    val co_iters = of_fp_res #xtor_co_iterss;
     1.8 +    val co_folds = of_fp_res #xtor_co_folds;
     1.9 +    val co_recs = of_fp_res #xtor_co_recs;
    1.10      val ns = map (length o #Ts o #fp_res) fp_sugars;
    1.11  
    1.12      fun substT rho (Type (@{type_name "fun"}, [T, U])) = substT rho T --> substT rho U
    1.13 @@ -245,11 +246,11 @@
    1.14  
    1.15      val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single);
    1.16  
    1.17 -    fun force_iter is_rec i TU TU_rec raw_iters =
    1.18 +    fun force_iter is_rec i TU TU_rec raw_fold raw_rec =
    1.19        let
    1.20          val thy = Proof_Context.theory_of lthy;
    1.21  
    1.22 -        val approx_fold = un_fold_of raw_iters
    1.23 +        val approx_fold = raw_fold
    1.24            |> force_typ names_lthy
    1.25              (replicate (nth ns i) dummyT ---> (if is_rec then TU_rec else TU));
    1.26          val subst = Term.typ_subst_atomic fold_thetaAs;
    1.27 @@ -269,9 +270,8 @@
    1.28  
    1.29          val js = find_indices Type.could_unify TUs cands;
    1.30          val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
    1.31 -        val iter = raw_iters |> (if is_rec then co_rec_of else un_fold_of);
    1.32        in
    1.33 -        force_typ names_lthy (Tpats ---> TU) iter
    1.34 +        force_typ names_lthy (Tpats ---> TU) (if is_rec then raw_rec else raw_fold)
    1.35        end;
    1.36  
    1.37      fun mk_co_comp_abs_rep fp_absT absT fp_abs fp_rep abs rep t =
    1.38 @@ -286,10 +286,11 @@
    1.39          val i = find_index (fn T => x = T) Xs;
    1.40          val TUiter =
    1.41            (case find_first (fn f => body_fun_type (fastype_of f) = TU) iters of
    1.42 -            NONE => nth co_iters i
    1.43 -              |> force_iter is_rec i
    1.44 +            NONE => 
    1.45 +              force_iter is_rec i
    1.46                  (TU |> (is_none b_opt andalso not is_rec) ? substT (fpTs ~~ Xs))
    1.47 -                (TU |> (is_none b_opt) ? substT (map2 mk_co_productT fpTs Xs ~~ Xs))
    1.48 +                (TU |> is_none b_opt ? substT (map2 mk_co_productT fpTs Xs ~~ Xs))
    1.49 +                (nth co_folds i) (nth co_recs i)
    1.50            | SOME f => f);
    1.51  
    1.52          val TUs = binder_fun_types (fastype_of TUiter);
    1.53 @@ -373,6 +374,9 @@
    1.54      val un_folds = map (Morphism.term phi) raw_un_folds;
    1.55      val co_recs = map (Morphism.term phi) raw_co_recs;
    1.56  
    1.57 +    val fp_fold_o_maps = of_fp_res #xtor_co_fold_o_map_thms;
    1.58 +    val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_map_thms;
    1.59 +
    1.60      val (xtor_un_fold_thms, xtor_co_rec_thms) =
    1.61        let
    1.62          val folds = map (fn f => Term.list_comb (f, fold_strs)) raw_un_folds;
    1.63 @@ -419,13 +423,9 @@
    1.64  
    1.65          val unfold_map = map (unfold_thms lthy (id_apply :: pre_map_defs));
    1.66  
    1.67 -        val fp_xtor_co_iterss = of_fp_res #xtor_co_iter_thmss;
    1.68 -        val fp_xtor_un_folds = map (mk_pointfree lthy o un_fold_of) fp_xtor_co_iterss;
    1.69 -        val fp_xtor_co_recs = map (mk_pointfree lthy o co_rec_of) fp_xtor_co_iterss;
    1.70 +        val fp_xtor_un_folds = map (mk_pointfree lthy) (of_fp_res #xtor_co_fold_thms);
    1.71 +        val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms);
    1.72  
    1.73 -        val fp_co_iter_o_mapss = of_fp_res #xtor_co_iter_o_map_thmss;
    1.74 -        val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss;
    1.75 -        val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss;
    1.76          val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
    1.77            map (fn thm => thm RS rewrite_comp_comp) @{thms map_pair.comp sum_map.comp} @
    1.78            @{thms id_apply comp_id id_comp map_pair.comp map_pair.id sum_map.comp sum_map.id};
    1.79 @@ -464,12 +464,8 @@
    1.80      (* These results are half broken. This is deliberate. We care only about those fields that are
    1.81         used by "primrec", "primcorecursive", and "datatype_compat". *)
    1.82      val fp_res =
    1.83 -      ({Ts = fpTs,
    1.84 -        bnfs = of_fp_res #bnfs,
    1.85 -        dtors = dtors,
    1.86 -        ctors = ctors,
    1.87 -        xtor_co_iterss = transpose [un_folds, co_recs],
    1.88 -        xtor_co_induct = xtor_co_induct_thm,
    1.89 +      ({Ts = fpTs, bnfs = of_fp_res #bnfs, dtors = dtors, ctors = ctors, xtor_co_folds = un_folds,
    1.90 +        xtor_co_recs = co_recs, xtor_co_induct = xtor_co_induct_thm,
    1.91          dtor_ctors = of_fp_res #dtor_ctors (*too general types*),
    1.92          ctor_dtors = of_fp_res #ctor_dtors (*too general types*),
    1.93          ctor_injects = of_fp_res #ctor_injects (*too general types*),
    1.94 @@ -477,9 +473,10 @@
    1.95          xtor_map_thms = of_fp_res #xtor_map_thms (*too general types and terms*),
    1.96          xtor_set_thmss = of_fp_res #xtor_set_thmss (*too general types and terms*),
    1.97          xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
    1.98 -        xtor_co_iter_thmss = transpose [xtor_un_fold_thms, xtor_co_rec_thms],
    1.99 -        xtor_co_iter_o_map_thmss = of_fp_res #xtor_co_iter_o_map_thmss
   1.100 -          (*theorem about old constant*),
   1.101 +        xtor_co_fold_thms = xtor_un_fold_thms,
   1.102 +        xtor_co_rec_thms = xtor_co_rec_thms,
   1.103 +        xtor_co_fold_o_map_thms = fp_fold_o_maps (*theorems about old constants*),
   1.104 +        xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
   1.105          rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
   1.106         |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
   1.107    in