src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 55894 8f3fe443948a
parent 55868 37b99986d435
child 55899 8c0a13e84963
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Mar 03 23:05:30 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Mar 03 23:05:49 2014 +0100
     1.3 @@ -228,13 +228,11 @@
     1.4      val fold_preTs = map2 (fn Ds => mk_T_of_bnf Ds allAs) Dss bnfs;
     1.5      val rec_preTs = map (Term.typ_subst_atomic rec_theta) fold_preTs;
     1.6  
     1.7 -    val fold_strTs = map2 mk_co_algT fold_preTs Xs;
     1.8      val rec_strTs = map2 mk_co_algT rec_preTs Xs;
     1.9      val resTs = map2 mk_co_algT fpTs Xs;
    1.10  
    1.11 -    val (((fold_strs, fold_strs'), (rec_strs, rec_strs')), names_lthy) = names_lthy
    1.12 -      |> mk_Frees' "s" fold_strTs
    1.13 -      ||>> mk_Frees' "s" rec_strTs;
    1.14 +    val ((rec_strs, rec_strs'), names_lthy) = names_lthy
    1.15 +      |> mk_Frees' "s" rec_strTs;
    1.16  
    1.17      val co_folds = of_fp_res #xtor_co_folds;
    1.18      val co_recs = of_fp_res #xtor_co_recs;
    1.19 @@ -246,13 +244,12 @@
    1.20  
    1.21      val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single);
    1.22  
    1.23 -    fun force_iter is_rec i TU TU_rec raw_fold raw_rec =
    1.24 +    fun force_rec i TU TU_rec raw_fold raw_rec =
    1.25        let
    1.26          val thy = Proof_Context.theory_of lthy;
    1.27  
    1.28          val approx_fold = raw_fold
    1.29 -          |> force_typ names_lthy
    1.30 -            (replicate (nth ns i) dummyT ---> (if is_rec then TU_rec else TU));
    1.31 +          |> force_typ names_lthy (replicate (nth ns i) dummyT ---> TU_rec);
    1.32          val subst = Term.typ_subst_atomic fold_thetaAs;
    1.33  
    1.34          fun mk_fp_absT_repT fp_repT fp_absT = mk_absT thy fp_repT fp_absT ooo mk_repT;
    1.35 @@ -271,31 +268,28 @@
    1.36          val js = find_indices Type.could_unify TUs cands;
    1.37          val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
    1.38        in
    1.39 -        force_typ names_lthy (Tpats ---> TU) (if is_rec then raw_rec else raw_fold)
    1.40 +        force_typ names_lthy (Tpats ---> TU) raw_rec
    1.41        end;
    1.42  
    1.43      fun mk_co_comp_abs_rep fp_absT absT fp_abs fp_rep abs rep t =
    1.44        fp_case fp (HOLogic.mk_comp (HOLogic.mk_comp (t, mk_abs absT abs), mk_rep fp_absT fp_rep))
    1.45          (HOLogic.mk_comp (mk_abs fp_absT fp_abs, HOLogic.mk_comp (mk_rep absT rep, t)));
    1.46  
    1.47 -    fun mk_iter b_opt is_rec iters lthy TU =
    1.48 +    fun mk_rec b_opt recs lthy TU =
    1.49        let
    1.50          val thy = Proof_Context.theory_of lthy;
    1.51  
    1.52          val x = co_alg_argT TU;
    1.53          val i = find_index (fn T => x = T) Xs;
    1.54 -        val TUiter =
    1.55 -          (case find_first (fn f => body_fun_type (fastype_of f) = TU) iters of
    1.56 +        val TUrec =
    1.57 +          (case find_first (fn f => body_fun_type (fastype_of f) = TU) recs of
    1.58              NONE => 
    1.59 -              force_iter is_rec i
    1.60 -                (TU |> (is_none b_opt andalso not is_rec) ? substT (fpTs ~~ Xs))
    1.61 +              force_rec i TU
    1.62                  (TU |> is_none b_opt ? substT (map2 mk_co_productT fpTs Xs ~~ Xs))
    1.63                  (nth co_folds i) (nth co_recs i)
    1.64            | SOME f => f);
    1.65  
    1.66 -        val TUs = binder_fun_types (fastype_of TUiter);
    1.67 -        val iter_preTs = if is_rec then rec_preTs else fold_preTs;
    1.68 -        val iter_strs = if is_rec then rec_strs else fold_strs;
    1.69 +        val TUs = binder_fun_types (fastype_of TUrec);
    1.70  
    1.71          fun mk_s TU' =
    1.72            let
    1.73 @@ -310,8 +304,8 @@
    1.74              val sF' =
    1.75                mk_absT_fp_repT (nth repTs' i) (nth absTs' i) (nth fp_absTs i) (nth fp_repTs i) sF
    1.76                  handle Term.TYPE _ => sF;
    1.77 -            val F = nth iter_preTs i;
    1.78 -            val s = nth iter_strs i;
    1.79 +            val F = nth rec_preTs i;
    1.80 +            val s = nth rec_strs i;
    1.81            in
    1.82              if sF = F then s
    1.83              else if sF' = F then mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep s
    1.84 @@ -327,67 +321,53 @@
    1.85                  fun mk_smap_arg TU =
    1.86                    (if domain_type TU = range_type TU then
    1.87                      HOLogic.id_const (domain_type TU)
    1.88 -                  else if is_rec then
    1.89 +                  else
    1.90                      let
    1.91                        val (TY, (U, X)) = TU |> dest_co_algT ||> dest_co_productT;
    1.92                        val T = mk_co_algT TY U;
    1.93                      in
    1.94 -                      (case try (force_typ lthy T o build_map lthy co_proj1_const o dest_funT) T of
    1.95 +                      (case try (force_typ names_lthy T o build_map lthy co_proj1_const o dest_funT) T of
    1.96                          SOME f => mk_co_product f
    1.97 -                          (fst (fst (mk_iter NONE is_rec iters lthy (mk_co_algT TY X))))
    1.98 +                          (fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X))))
    1.99                        | NONE => mk_map_co_product
   1.100                            (build_map lthy co_proj1_const
   1.101                              (dest_funT (mk_co_algT (dest_co_productT TY |> fst) U)))
   1.102                            (HOLogic.id_const X))
   1.103 -                    end
   1.104 -                  else
   1.105 -                    fst (fst (mk_iter NONE is_rec iters lthy TU)))
   1.106 +                    end)
   1.107                  val smap_args = map mk_smap_arg smap_argTs;
   1.108                in
   1.109                  mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep
   1.110                    (mk_co_comp (s, Term.list_comb (smap, smap_args)))
   1.111                end
   1.112            end;
   1.113 -        val t = Term.list_comb (TUiter, map mk_s TUs);
   1.114 +        val t = Term.list_comb (TUrec, map mk_s TUs);
   1.115        in
   1.116          (case b_opt of
   1.117            NONE => ((t, Drule.dummy_thm), lthy)
   1.118          | SOME b => Local_Theory.define ((b, NoSyn), ((Binding.conceal (Thm.def_binding b), []),
   1.119 -            fold_rev Term.absfree (if is_rec then rec_strs' else fold_strs') t)) lthy |>> apsnd snd)
   1.120 +            fold_rev Term.absfree rec_strs' t)) lthy |>> apsnd snd)
   1.121        end;
   1.122  
   1.123 -    fun mk_iters is_rec name lthy =
   1.124 -      fold2 (fn TU => fn b => fn ((iters, defs), lthy) =>
   1.125 -        mk_iter (SOME b) is_rec iters lthy TU |>> (fn (f, d) => (f :: iters, d :: defs)))
   1.126 -      resTs (map (Binding.suffix_name ("_" ^ name)) bs) (([], []), lthy)
   1.127 +    val recN = fp_case fp ctor_recN dtor_corecN;
   1.128 +    fun mk_recs lthy =
   1.129 +      fold2 (fn TU => fn b => fn ((recs, defs), lthy) =>
   1.130 +        mk_rec (SOME b) recs lthy TU |>> (fn (f, d) => (f :: recs, d :: defs)))
   1.131 +      resTs (map (Binding.suffix_name ("_" ^ recN)) bs) (([], []), lthy)
   1.132        |>> apfst rev o apsnd rev;
   1.133 -    val foldN = fp_case fp ctor_foldN dtor_unfoldN;
   1.134 -    val recN = fp_case fp ctor_recN dtor_corecN;
   1.135 -    val (((raw_un_folds, raw_un_fold_defs), (raw_co_recs, raw_co_rec_defs)), (lthy, raw_lthy)) =
   1.136 -      lthy
   1.137 -      |> mk_iters false foldN
   1.138 -      ||>> mk_iters true recN
   1.139 +    val ((raw_co_recs, raw_co_rec_defs), (lthy, raw_lthy)) = lthy
   1.140 +      |> mk_recs
   1.141        ||> `Local_Theory.restore;
   1.142  
   1.143      val phi = Proof_Context.export_morphism raw_lthy lthy;
   1.144  
   1.145 -    val un_folds = map (Morphism.term phi) raw_un_folds;
   1.146      val co_recs = map (Morphism.term phi) raw_co_recs;
   1.147  
   1.148 -    val fp_fold_o_maps = of_fp_res #xtor_co_fold_o_map_thms;
   1.149      val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_map_thms;
   1.150  
   1.151 -    val (xtor_un_fold_thms, xtor_co_rec_thms) =
   1.152 +    val xtor_co_rec_thms =
   1.153        let
   1.154 -        val folds = map (fn f => Term.list_comb (f, fold_strs)) raw_un_folds;
   1.155          val recs = map (fn r => Term.list_comb (r, rec_strs)) raw_co_recs;
   1.156 -        val fold_mapTs = co_swap (As @ fpTs, As @ Xs);
   1.157          val rec_mapTs = co_swap (As @ fpTs, As @ map2 mk_co_productT fpTs Xs);
   1.158 -        val pre_fold_maps =
   1.159 -          map2 (fn Ds => fn bnf =>
   1.160 -            Term.list_comb (uncurry (mk_map_of_bnf Ds) fold_mapTs bnf,
   1.161 -              map HOLogic.id_const As @ folds))
   1.162 -          Dss bnfs;
   1.163          val pre_rec_maps =
   1.164            map2 (fn Ds => fn bnf =>
   1.165              Term.list_comb (uncurry (mk_map_of_bnf Ds) rec_mapTs bnf,
   1.166 @@ -404,26 +384,13 @@
   1.167                  fp_abs fp_rep abs rep rhs)
   1.168            end;
   1.169  
   1.170 -        val fold_goals =
   1.171 -          map8 mk_goals folds xtors fold_strs pre_fold_maps fp_abss fp_reps abss reps;
   1.172 -        val rec_goals = map8 mk_goals recs xtors rec_strs pre_rec_maps fp_abss fp_reps abss reps;
   1.173 -
   1.174 -        fun mk_thms ss goals tac =
   1.175 -          Library.foldr1 HOLogic.mk_conj goals
   1.176 -          |> HOLogic.mk_Trueprop
   1.177 -          |> fold_rev Logic.all ss
   1.178 -          |> (fn goal => Goal.prove_sorry raw_lthy [] [] goal tac)
   1.179 -          |> Thm.close_derivation
   1.180 -          |> Morphism.thm phi
   1.181 -          |> split_conj_thm
   1.182 -          |> map (fn thm => thm RS @{thm comp_eq_dest});
   1.183 +        val goals = map8 mk_goals recs xtors rec_strs pre_rec_maps fp_abss fp_reps abss reps;
   1.184  
   1.185          val pre_map_defs = no_refl (map map_def_of_bnf bnfs);
   1.186          val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs);
   1.187  
   1.188          val unfold_map = map (unfold_thms lthy (id_apply :: pre_map_defs));
   1.189  
   1.190 -        val fp_xtor_un_folds = map (mk_pointfree lthy) (of_fp_res #xtor_co_fold_thms);
   1.191          val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms);
   1.192  
   1.193          val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
   1.194 @@ -450,21 +417,26 @@
   1.195          val fp_Rep_o_Abss = map mk_Rep_o_Abs fp_type_definitions;
   1.196          val Rep_o_Abss = map mk_Rep_o_Abs type_definitions;
   1.197  
   1.198 -        fun mk_tac defs o_map_thms xtor_thms thms {context = ctxt, prems = _} =
   1.199 -          unfold_thms_tac ctxt (flat [thms, defs, pre_map_defs, fp_pre_map_defs,
   1.200 -            xtor_thms, o_map_thms, map_thms, fp_Rep_o_Abss, Rep_o_Abss]) THEN
   1.201 +        fun tac {context = ctxt, prems = _} =
   1.202 +          unfold_thms_tac ctxt (flat [rec_thms, raw_co_rec_defs, pre_map_defs, fp_pre_map_defs,
   1.203 +            fp_xtor_co_recs, fp_rec_o_maps, map_thms, fp_Rep_o_Abss, Rep_o_Abss]) THEN
   1.204            CONJ_WRAP (K (HEADGOAL (rtac refl))) bnfs;
   1.205 -
   1.206 -        val fold_tac = mk_tac raw_un_fold_defs fp_fold_o_maps fp_xtor_un_folds fold_thms;
   1.207 -        val rec_tac = mk_tac raw_co_rec_defs fp_rec_o_maps fp_xtor_co_recs rec_thms;
   1.208        in
   1.209 -        (mk_thms fold_strs fold_goals fold_tac, mk_thms rec_strs rec_goals rec_tac)
   1.210 +        Library.foldr1 HOLogic.mk_conj goals
   1.211 +        |> HOLogic.mk_Trueprop
   1.212 +        |> fold_rev Logic.all rec_strs
   1.213 +        |> (fn goal => Goal.prove_sorry raw_lthy [] [] goal tac)
   1.214 +        |> Thm.close_derivation
   1.215 +        |> Morphism.thm phi
   1.216 +        |> split_conj_thm
   1.217 +        |> map (fn thm => thm RS @{thm comp_eq_dest})
   1.218        end;
   1.219  
   1.220      (* These results are half broken. This is deliberate. We care only about those fields that are
   1.221         used by "primrec", "primcorecursive", and "datatype_compat". *)
   1.222      val fp_res =
   1.223 -      ({Ts = fpTs, bnfs = of_fp_res #bnfs, dtors = dtors, ctors = ctors, xtor_co_folds = un_folds,
   1.224 +      ({Ts = fpTs, bnfs = of_fp_res #bnfs, dtors = dtors, ctors = ctors,
   1.225 +        xtor_co_folds = co_recs (*theorems about wrong constants*),
   1.226          xtor_co_recs = co_recs, xtor_co_induct = xtor_co_induct_thm,
   1.227          dtor_ctors = of_fp_res #dtor_ctors (*too general types*),
   1.228          ctor_dtors = of_fp_res #ctor_dtors (*too general types*),
   1.229 @@ -473,9 +445,9 @@
   1.230          xtor_map_thms = of_fp_res #xtor_map_thms (*too general types and terms*),
   1.231          xtor_set_thmss = of_fp_res #xtor_set_thmss (*too general types and terms*),
   1.232          xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
   1.233 -        xtor_co_fold_thms = xtor_un_fold_thms,
   1.234 +        xtor_co_fold_thms = xtor_co_rec_thms (*theorems about wrong constants*),
   1.235          xtor_co_rec_thms = xtor_co_rec_thms,
   1.236 -        xtor_co_fold_o_map_thms = fp_fold_o_maps (*theorems about old constants*),
   1.237 +        xtor_co_fold_o_map_thms = fp_rec_o_maps (*theorems about wrong, old constants*),
   1.238          xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
   1.239          rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
   1.240         |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));