more debugging
authorblanchet
Tue Mar 22 08:00:15 2016 +0100 (2016-03-22)
changeset 626899b8b3db6ac03
parent 62688 a3cccaef566a
child 62690 c4fad0569a24
more debugging
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_lfp.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Mar 22 07:57:02 2016 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Mar 22 08:00:15 2016 +0100
     1.3 @@ -50,11 +50,18 @@
     1.4  fun construct_mutualized_fp fp mutual_cliques fpTs (fp_results : (int * fp_result) list) bs resBs
     1.5      (resDs, Dss) bnfs (absT_infos : absT_info list) lthy =
     1.6    let
     1.7 +    val time = time lthy;
     1.8 +    val timer = time (Timer.startRealTimer ());
     1.9 +
    1.10 +    val b_names = map Binding.name_of bs;
    1.11 +    val b_name = mk_common_name b_names;
    1.12 +    val b = Binding.name b_name;
    1.13 +
    1.14      fun of_fp_res get = map (uncurry nth o swap o apsnd get) fp_results;
    1.15      fun mk_co_algT T U = case_fp fp (T --> U) (U --> T);
    1.16      fun co_swap pair = case_fp fp I swap pair;
    1.17      val mk_co_comp = HOLogic.mk_comp o co_swap;
    1.18 -    val co_productC = BNF_FP_Rec_Sugar_Util.case_fp fp @{type_name prod} @{type_name sum};
    1.19 +    val co_productC = case_fp fp @{type_name prod} @{type_name sum};
    1.20  
    1.21      val dest_co_algT = co_swap o dest_funT;
    1.22      val co_alg_argT = case_fp fp range_type domain_type;
    1.23 @@ -251,6 +258,8 @@
    1.24              |> funpow n (fn thm => thm RS mp)
    1.25            end);
    1.26  
    1.27 +    val timer = time (timer "Nested-to-mutual (co)induction");
    1.28 +
    1.29      val fold_preTs = map2 (fn Ds => mk_T_of_bnf Ds allAs) Dss bnfs;
    1.30      val rec_preTs = map (Term.typ_subst_atomic rec_theta) fold_preTs;
    1.31  
    1.32 @@ -260,7 +269,7 @@
    1.33      val ((rec_strs, rec_strs'), names_lthy) = names_lthy
    1.34        |> mk_Frees' "s" rec_strTs;
    1.35  
    1.36 -    val co_recs = of_fp_res #xtor_co_recs;
    1.37 +    val xtor_co_recs = of_fp_res #xtor_co_recs;
    1.38      val ns = map (length o #Ts o snd) fp_results;
    1.39  
    1.40      fun foldT_of_recT recT =
    1.41 @@ -317,7 +326,7 @@
    1.42          val i = find_index (fn T => x = T) Xs;
    1.43          val TUrec =
    1.44            (case find_first (fn f => body_fun_type (fastype_of f) = TU) recs of
    1.45 -            NONE => force_rec i TU (nth co_recs i)
    1.46 +            NONE => force_rec i TU (nth xtor_co_recs i)
    1.47            | SOME f => f);
    1.48  
    1.49          val TUs = binder_fun_types (fastype_of TUrec);
    1.50 @@ -395,21 +404,21 @@
    1.51          mk_rec (SOME b) recs lthy TU |>> (fn (f, d) => (f :: recs, d :: defs)))
    1.52        resTs (map (Binding.suffix_name ("_" ^ recN)) bs) (([], []), lthy)
    1.53        |>> map_prod rev rev;
    1.54 -    val ((raw_co_recs, raw_co_rec_defs), (lthy, raw_lthy)) = lthy
    1.55 +    val ((raw_xtor_co_recs, raw_xtor_co_rec_defs), (lthy, raw_lthy)) = lthy
    1.56        |> Local_Theory.open_target |> snd
    1.57        |> mk_recs
    1.58        ||> `Local_Theory.close_target;
    1.59  
    1.60      val phi = Proof_Context.export_morphism raw_lthy lthy;
    1.61  
    1.62 -    val co_recs = map (Morphism.term phi) raw_co_recs;
    1.63 +    val xtor_co_recs = map (Morphism.term phi) raw_xtor_co_recs;
    1.64  
    1.65      val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_maps
    1.66        |> maps (fn thm => [thm, thm RS rewrite_comp_comp]);
    1.67  
    1.68      val xtor_co_rec_thms =
    1.69        let
    1.70 -        val recs = map (fn r => Term.list_comb (r, rec_strs)) raw_co_recs;
    1.71 +        val recs = map (fn r => Term.list_comb (r, rec_strs)) raw_xtor_co_recs;
    1.72          val rec_mapTs = co_swap (As @ fpTs, As @ map2 mk_co_productT fpTs Xs);
    1.73          val pre_rec_maps =
    1.74            map2 (fn Ds => fn bnf =>
    1.75 @@ -463,7 +472,7 @@
    1.76          val Rep_o_Abss = maps mk_Rep_o_Abs type_definitions;
    1.77  
    1.78          fun tac {context = ctxt, prems = _} =
    1.79 -          unfold_thms_tac ctxt (flat [rec_thms, raw_co_rec_defs, pre_map_defs,
    1.80 +          unfold_thms_tac ctxt (flat [rec_thms, raw_xtor_co_rec_defs, pre_map_defs,
    1.81              fp_pre_map_defs, fp_xtor_co_recs, fp_rec_o_maps, map_thms, fp_Rep_o_Abss,
    1.82              Rep_o_Abss]) THEN
    1.83            CONJ_WRAP (K (HEADGOAL (rtac ctxt refl))) bnfs;
    1.84 @@ -478,12 +487,38 @@
    1.85          |> map (fn thm => thm RS @{thm comp_eq_dest})
    1.86        end;
    1.87  
    1.88 +    val timer = time (timer "Nested-to-mutual (co)recursion");
    1.89 +
    1.90 +    val common_notes =
    1.91 +      (case fp of
    1.92 +        Least_FP =>
    1.93 +        [(ctor_inductN, [xtor_co_induct_thm]),
    1.94 +         (ctor_rel_inductN, [xtor_rel_co_induct])]
    1.95 +      | Greatest_FP =>
    1.96 +        [(dtor_coinductN, [xtor_co_induct_thm]),
    1.97 +         (dtor_rel_coinductN, [xtor_rel_co_induct])])
    1.98 +      |> map (fn (thmN, thms) =>
    1.99 +        ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
   1.100 +
   1.101 +    val notes =
   1.102 +      (case fp of
   1.103 +        Least_FP => [(ctor_recN, xtor_co_rec_thms)]
   1.104 +      | Greatest_FP => [(dtor_corecN, xtor_co_rec_thms)])
   1.105 +      |> map (apsnd (map single))
   1.106 +      |> maps (fn (thmN, thmss) =>
   1.107 +        map2 (fn b => fn thms =>
   1.108 +          ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
   1.109 +        bs thmss);
   1.110 +
   1.111 +    val lthy = lthy |> Config.get lthy bnf_internals
   1.112 +      ? snd o Local_Theory.notes (common_notes @ notes);
   1.113 +
   1.114      (* These results are half broken. This is deliberate. We care only about those fields that are
   1.115         used by "primrec", "primcorecursive", and "datatype_compat". *)
   1.116      val fp_res =
   1.117        ({Ts = fpTs, bnfs = of_fp_res #bnfs, pre_bnfs = bnfs, absT_infos = absT_infos,
   1.118          dtors = dtors, ctors = ctors,
   1.119 -        xtor_un_folds = co_recs (*wrong*), xtor_co_recs = co_recs,
   1.120 +        xtor_un_folds = xtor_co_recs (*wrong*), xtor_co_recs = xtor_co_recs,
   1.121          xtor_co_induct = xtor_co_induct_thm,
   1.122          dtor_ctors = of_fp_res #dtor_ctors (*too general types*),
   1.123          ctor_dtors = of_fp_res #ctor_dtors (*too general types*),
   1.124 @@ -501,7 +536,7 @@
   1.125          xtor_rel_co_induct = xtor_rel_co_induct, dtor_set_inducts = []}
   1.126         |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
   1.127    in
   1.128 -    (fp_res, lthy)
   1.129 +    timer; (fp_res, lthy)
   1.130    end;
   1.131  
   1.132  end;
     2.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Mar 22 07:57:02 2016 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Mar 22 08:00:15 2016 +0100
     2.3 @@ -580,7 +580,6 @@
     2.4  
     2.5      val timer = time (timer "Bounds");
     2.6  
     2.7 -
     2.8      (* minimal algebra *)
     2.9  
    2.10      fun mk_minG Asi i k = mk_UNION (mk_underS suc_bd $ i)