N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
authortraytel
Tue Mar 04 12:32:33 2014 +0100 (2014-03-04)
changeset 558998c0a13e84963
parent 55898 307115c3b969
child 55900 21aa30ea6806
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_lfp.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Mar 04 10:35:37 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Mar 04 12:32:33 2014 +0100
     1.3 @@ -55,6 +55,7 @@
     1.4      fun mk_co_algT T U = fp_case fp (T --> U) (U --> T);
     1.5      fun co_swap pair = fp_case fp I swap pair;
     1.6      val mk_co_comp = HOLogic.mk_comp o co_swap;
     1.7 +    val co_productC = BNF_FP_Rec_Sugar_Util.fp_case fp @{type_name prod} @{type_name sum};
     1.8  
     1.9      val dest_co_algT = co_swap o dest_funT;
    1.10      val co_alg_argT = fp_case fp range_type domain_type;
    1.11 @@ -234,7 +235,6 @@
    1.12      val ((rec_strs, rec_strs'), names_lthy) = names_lthy
    1.13        |> mk_Frees' "s" rec_strTs;
    1.14  
    1.15 -    val co_folds = of_fp_res #xtor_co_folds;
    1.16      val co_recs = of_fp_res #xtor_co_recs;
    1.17      val ns = map (length o #Ts o #fp_res) fp_sugars;
    1.18  
    1.19 @@ -244,11 +244,22 @@
    1.20  
    1.21      val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single);
    1.22  
    1.23 -    fun force_rec i TU TU_rec raw_fold raw_rec =
    1.24 +    fun foldT_of_recT recT =
    1.25 +      let
    1.26 +        val ((FTXs, Xs), TX) = strip_fun_type recT |>> map_split dest_co_algT;
    1.27 +        fun subst (Type (C, Ts as [_, X])) =
    1.28 +            if C = co_productC andalso member op = Xs X then X else Type (C, map subst Ts)
    1.29 +          | subst (Type (C, Ts)) = Type (C, map subst Ts)
    1.30 +          | subst T = T;
    1.31 +      in
    1.32 +        map2 (mk_co_algT o subst) FTXs Xs ---> TX
    1.33 +      end;
    1.34 +
    1.35 +    fun force_rec i TU TU_rec raw_rec =
    1.36        let
    1.37          val thy = Proof_Context.theory_of lthy;
    1.38  
    1.39 -        val approx_fold = raw_fold
    1.40 +        val approx_rec = raw_rec
    1.41            |> force_typ names_lthy (replicate (nth ns i) dummyT ---> TU_rec);
    1.42          val subst = Term.typ_subst_atomic fold_thetaAs;
    1.43  
    1.44 @@ -260,7 +271,7 @@
    1.45          val fold_pre_deads_only_Ts =
    1.46            map (typ_subst_nonatomic_sorted (map (rpair dummyT) (As @ fpTs))) fold_preTs';
    1.47  
    1.48 -        val TUs = map_split dest_co_algT (binder_fun_types (fastype_of approx_fold))
    1.49 +        val TUs = map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec)))
    1.50            |>> map subst
    1.51            |> uncurry (map2 mk_co_algT);
    1.52          val cands = map2 mk_co_algT fold_preTs' Xs;
    1.53 @@ -285,8 +296,7 @@
    1.54            (case find_first (fn f => body_fun_type (fastype_of f) = TU) recs of
    1.55              NONE => 
    1.56                force_rec i TU
    1.57 -                (TU |> is_none b_opt ? substT (map2 mk_co_productT fpTs Xs ~~ Xs))
    1.58 -                (nth co_folds i) (nth co_recs i)
    1.59 +                (TU |> is_none b_opt ? substT (map2 mk_co_productT fpTs Xs ~~ Xs)) (nth co_recs i)
    1.60            | SOME f => f);
    1.61  
    1.62          val TUs = binder_fun_types (fastype_of TUrec);
    1.63 @@ -436,7 +446,6 @@
    1.64         used by "primrec", "primcorecursive", and "datatype_compat". *)
    1.65      val fp_res =
    1.66        ({Ts = fpTs, bnfs = of_fp_res #bnfs, dtors = dtors, ctors = ctors,
    1.67 -        xtor_co_folds = co_recs (*theorems about wrong constants*),
    1.68          xtor_co_recs = co_recs, xtor_co_induct = xtor_co_induct_thm,
    1.69          dtor_ctors = of_fp_res #dtor_ctors (*too general types*),
    1.70          ctor_dtors = of_fp_res #ctor_dtors (*too general types*),
    1.71 @@ -445,9 +454,7 @@
    1.72          xtor_map_thms = of_fp_res #xtor_map_thms (*too general types and terms*),
    1.73          xtor_set_thmss = of_fp_res #xtor_set_thmss (*too general types and terms*),
    1.74          xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
    1.75 -        xtor_co_fold_thms = xtor_co_rec_thms (*theorems about wrong constants*),
    1.76          xtor_co_rec_thms = xtor_co_rec_thms,
    1.77 -        xtor_co_fold_o_map_thms = fp_rec_o_maps (*theorems about wrong, old constants*),
    1.78          xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
    1.79          rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
    1.80         |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Mar 04 10:35:37 2014 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Mar 04 12:32:33 2014 +0100
     2.3 @@ -13,7 +13,6 @@
     2.4       bnfs: BNF_Def.bnf list,
     2.5       ctors: term list,
     2.6       dtors: term list,
     2.7 -     xtor_co_folds: term list,
     2.8       xtor_co_recs: term list,
     2.9       xtor_co_induct: thm,
    2.10       dtor_ctors: thm list,
    2.11 @@ -23,9 +22,7 @@
    2.12       xtor_map_thms: thm list,
    2.13       xtor_set_thmss: thm list list,
    2.14       xtor_rel_thms: thm list,
    2.15 -     xtor_co_fold_thms: thm list,
    2.16       xtor_co_rec_thms: thm list,
    2.17 -     xtor_co_fold_o_map_thms: thm list,
    2.18       xtor_co_rec_o_map_thms: thm list,
    2.19       rel_xtor_co_induct_thm: thm}
    2.20  
    2.21 @@ -194,7 +191,6 @@
    2.22     bnfs: BNF_Def.bnf list,
    2.23     ctors: term list,
    2.24     dtors: term list,
    2.25 -   xtor_co_folds: term list,
    2.26     xtor_co_recs: term list,
    2.27     xtor_co_induct: thm,
    2.28     dtor_ctors: thm list,
    2.29 @@ -204,21 +200,17 @@
    2.30     xtor_map_thms: thm list,
    2.31     xtor_set_thmss: thm list list,
    2.32     xtor_rel_thms: thm list,
    2.33 -   xtor_co_fold_thms: thm list,
    2.34     xtor_co_rec_thms: thm list,
    2.35 -   xtor_co_fold_o_map_thms: thm list,
    2.36     xtor_co_rec_o_map_thms: thm list,
    2.37     rel_xtor_co_induct_thm: thm};
    2.38  
    2.39 -fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_folds, xtor_co_recs, xtor_co_induct,
    2.40 +fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct,
    2.41      dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss,
    2.42 -    xtor_rel_thms, xtor_co_fold_thms, xtor_co_rec_thms, xtor_co_fold_o_map_thms,
    2.43 -    xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm} =
    2.44 +    xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm} =
    2.45    {Ts = map (Morphism.typ phi) Ts,
    2.46     bnfs = map (morph_bnf phi) bnfs,
    2.47     ctors = map (Morphism.term phi) ctors,
    2.48     dtors = map (Morphism.term phi) dtors,
    2.49 -   xtor_co_folds = map (Morphism.term phi) xtor_co_folds,
    2.50     xtor_co_recs = map (Morphism.term phi) xtor_co_recs,
    2.51     xtor_co_induct = Morphism.thm phi xtor_co_induct,
    2.52     dtor_ctors = map (Morphism.thm phi) dtor_ctors,
    2.53 @@ -228,9 +220,7 @@
    2.54     xtor_map_thms = map (Morphism.thm phi) xtor_map_thms,
    2.55     xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss,
    2.56     xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms,
    2.57 -   xtor_co_fold_thms = map (Morphism.thm phi) xtor_co_fold_thms,
    2.58     xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
    2.59 -   xtor_co_fold_o_map_thms = map (Morphism.thm phi) xtor_co_fold_o_map_thms,
    2.60     xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms,
    2.61     rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm};
    2.62  
     3.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Mar 04 10:35:37 2014 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Mar 04 12:32:33 2014 +0100
     3.3 @@ -2599,12 +2599,11 @@
     3.4      val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal));
     3.5    in
     3.6      timer;
     3.7 -    ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_co_folds = unfolds,
     3.8 -      xtor_co_recs = corecs, xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms,
     3.9 +    ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_co_recs = corecs,
    3.10 +      xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms,
    3.11        ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
    3.12        xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
    3.13 -      xtor_rel_thms = dtor_Jrel_thms, xtor_co_fold_thms = dtor_unfold_thms,
    3.14 -      xtor_co_rec_thms = dtor_corec_thms, xtor_co_fold_o_map_thms = dtor_unfold_o_Jmap_thms,
    3.15 +      xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
    3.16        xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm},
    3.17       lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Jbnf_notes)) |> snd)
    3.18    end;
     4.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Mar 04 10:35:37 2014 +0100
     4.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Mar 04 12:32:33 2014 +0100
     4.3 @@ -1854,12 +1854,11 @@
     4.4      val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal));
     4.5    in
     4.6      timer;
     4.7 -    ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_folds = folds,
     4.8 -      xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
     4.9 +    ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_recs = recs,
    4.10 +      xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
    4.11        ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
    4.12        xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
    4.13 -      xtor_rel_thms = ctor_Irel_thms, xtor_co_fold_thms = ctor_fold_thms,
    4.14 -      xtor_co_rec_thms = ctor_rec_thms, xtor_co_fold_o_map_thms = ctor_fold_o_Imap_thms,
    4.15 +      xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
    4.16        xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm},
    4.17       lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Ibnf_notes)) |> snd)
    4.18    end;