src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 55539 0819931d652d
parent 55531 601ca8efa000
child 55566 ab0a547b5aee
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Feb 17 18:18:27 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Feb 17 22:54:38 2014 +0100
     1.3 @@ -47,7 +47,8 @@
     1.4  
     1.5  fun construct_mutualized_fp fp fpTs fp_sugars bs resBs (resDs, Dss) bnfs lthy =
     1.6    let
     1.7 -    fun steal get = map (of_fp_sugar (get o #fp_res)) fp_sugars;
     1.8 +    fun steal_fp_res get =
     1.9 +      map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars;
    1.10  
    1.11      val n = length bnfs;
    1.12      val deads = fold (union (op =)) Dss resDs;
    1.13 @@ -77,8 +78,8 @@
    1.14  
    1.15      val ((ctors, dtors), (xtor's, xtors)) =
    1.16        let
    1.17 -        val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (steal #ctors);
    1.18 -        val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (steal #dtors);
    1.19 +        val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (steal_fp_res #ctors);
    1.20 +        val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (steal_fp_res #dtors);
    1.21        in
    1.22          ((ctors, dtors), `(map (Term.subst_atomic_types theta)) (fp_case fp ctors dtors))
    1.23        end;
    1.24 @@ -92,9 +93,8 @@
    1.25        ||>> mk_Frees "x" xTs
    1.26        ||>> mk_Frees "y" yTs;
    1.27  
    1.28 -    val fp_bnfs = steal #bnfs;
    1.29 -    val pre_bnfs = map (of_fp_sugar #pre_bnfs) fp_sugars;
    1.30 -    val pre_bnfss = map #pre_bnfs fp_sugars;
    1.31 +    val fp_bnfs = steal_fp_res #bnfs;
    1.32 +    val pre_bnfs = map #pre_bnf fp_sugars;
    1.33      val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
    1.34      val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
    1.35      val fp_nesty_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_nesty_bnfss);
    1.36 @@ -126,9 +126,9 @@
    1.37  
    1.38      val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;
    1.39  
    1.40 -    val rel_unfoldss = map (maps (fn bnf => no_refl [rel_def_of_bnf bnf])) pre_bnfss;
    1.41 -    val rel_xtor_co_inducts = steal (split_conj_thm o #rel_xtor_co_induct_thm)
    1.42 -      |> map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) rel_unfoldss;
    1.43 +    val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) pre_bnfs;
    1.44 +    val rel_xtor_co_inducts = steal_fp_res (split_conj_thm o #rel_xtor_co_induct_thm)
    1.45 +      |> map (unfold_thms lthy (id_apply :: rel_unfolds));
    1.46  
    1.47      val rel_defs = map rel_def_of_bnf bnfs;
    1.48      val rel_monos = map rel_mono_of_bnf bnfs;
    1.49 @@ -185,11 +185,13 @@
    1.50        |> mk_Frees' "s" fold_strTs
    1.51        ||>> mk_Frees' "s" rec_strTs;
    1.52  
    1.53 -    val co_iters = steal #xtor_co_iterss;
    1.54 -    val ns = map (length o #pre_bnfs) fp_sugars;
    1.55 +    val co_iters = steal_fp_res #xtor_co_iterss;
    1.56 +    val ns = map (length o #Ts o #fp_res) fp_sugars;
    1.57 +
    1.58      fun substT rho (Type (@{type_name "fun"}, [T, U])) = substT rho T --> substT rho U
    1.59        | substT rho (Type (s, Ts)) = Type (s, map (typ_subst_nonatomic rho) Ts)
    1.60        | substT _ T = T;
    1.61 +
    1.62      fun force_iter is_rec i TU TU_rec raw_iters =
    1.63        let
    1.64          val approx_fold = un_fold_of raw_iters
    1.65 @@ -325,14 +327,14 @@
    1.66          val pre_map_defs = no_refl (map map_def_of_bnf bnfs);
    1.67          val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs);
    1.68  
    1.69 -        val map_unfoldss = map (maps (fn bnf => no_refl [map_def_of_bnf bnf])) pre_bnfss;
    1.70 -        val unfold_map = map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) map_unfoldss;
    1.71 +        val map_unfolds = maps (fn bnf => no_refl [map_def_of_bnf bnf]) pre_bnfs;
    1.72 +        val unfold_map = map (unfold_thms lthy (id_apply :: map_unfolds));
    1.73  
    1.74 -        val fp_xtor_co_iterss = steal #xtor_co_iter_thmss;
    1.75 +        val fp_xtor_co_iterss = steal_fp_res #xtor_co_iter_thmss;
    1.76          val fp_xtor_un_folds = map (mk_pointfree lthy o un_fold_of) fp_xtor_co_iterss |> unfold_map;
    1.77          val fp_xtor_co_recs = map (mk_pointfree lthy o co_rec_of) fp_xtor_co_iterss |> unfold_map;
    1.78  
    1.79 -        val fp_co_iter_o_mapss = steal #xtor_co_iter_o_map_thmss;
    1.80 +        val fp_co_iter_o_mapss = steal_fp_res #xtor_co_iter_o_map_thmss;
    1.81          val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss |> unfold_map;
    1.82          val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss |> unfold_map;
    1.83          val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} :: @{thms id_apply
    1.84 @@ -358,20 +360,21 @@
    1.85         used by "primrec", "primcorecursive", and "datatype_compat". *)
    1.86      val fp_res =
    1.87        ({Ts = fpTs,
    1.88 -        bnfs = steal #bnfs,
    1.89 +        bnfs = steal_fp_res #bnfs,
    1.90          dtors = dtors,
    1.91          ctors = ctors,
    1.92          xtor_co_iterss = transpose [un_folds, co_recs],
    1.93          xtor_co_induct = xtor_co_induct_thm,
    1.94 -        dtor_ctors = steal #dtor_ctors (*too general types*),
    1.95 -        ctor_dtors = steal #ctor_dtors (*too general types*),
    1.96 -        ctor_injects = steal #ctor_injects (*too general types*),
    1.97 -        dtor_injects = steal #dtor_injects (*too general types*),
    1.98 -        xtor_map_thms = steal #xtor_map_thms (*too general types and terms*),
    1.99 -        xtor_set_thmss = steal #xtor_set_thmss (*too general types and terms*),
   1.100 -        xtor_rel_thms = steal #xtor_rel_thms (*too general types and terms*),
   1.101 +        dtor_ctors = steal_fp_res #dtor_ctors (*too general types*),
   1.102 +        ctor_dtors = steal_fp_res #ctor_dtors (*too general types*),
   1.103 +        ctor_injects = steal_fp_res #ctor_injects (*too general types*),
   1.104 +        dtor_injects = steal_fp_res #dtor_injects (*too general types*),
   1.105 +        xtor_map_thms = steal_fp_res #xtor_map_thms (*too general types and terms*),
   1.106 +        xtor_set_thmss = steal_fp_res #xtor_set_thmss (*too general types and terms*),
   1.107 +        xtor_rel_thms = steal_fp_res #xtor_rel_thms (*too general types and terms*),
   1.108          xtor_co_iter_thmss = transpose [xtor_un_fold_thms, xtor_co_rec_thms],
   1.109 -        xtor_co_iter_o_map_thmss = steal #xtor_co_iter_o_map_thmss (*theorem about old constant*),
   1.110 +        xtor_co_iter_o_map_thmss = steal_fp_res #xtor_co_iter_o_map_thmss
   1.111 +          (*theorem about old constant*),
   1.112          rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
   1.113         |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
   1.114    in