src/HOL/Tools/BNF/bnf_gfp.ML
changeset 62905 52c5a25e0c96
parent 62863 e0b894bba6ff
child 62907 9ad0bac25a84
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Apr 07 17:26:22 2016 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Apr 07 17:56:22 2016 +0200
     1.3 @@ -1602,52 +1602,6 @@
     1.4  
     1.5      val timer = time (timer "ctor definitions & thms");
     1.6  
     1.7 -    val corec_Inl_sum_thms =
     1.8 -      let
     1.9 -        val mor = mor_comp_thm OF [mor_case_sum_thm, mor_unfold_thm];
    1.10 -      in
    1.11 -        map2 (fn unique => fn unfold_dtor =>
    1.12 -          trans OF [mor RS unique, unfold_dtor]) unfold_unique_mor_thms unfold_dtor_thms
    1.13 -      end;
    1.14 -
    1.15 -    fun corec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_corecN ^ "_");
    1.16 -    val corec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o corec_bind;
    1.17 -
    1.18 -    fun mk_corec_strs corec_ss =
    1.19 -      @{map 3} (fn dtor => fn sum_s => fn mapx =>
    1.20 -        mk_case_sum
    1.21 -          (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), dtor), sum_s))
    1.22 -      dtors corec_ss corec_maps;
    1.23 -
    1.24 -    fun corec_spec i T AT =
    1.25 -      fold_rev (Term.absfree o Term.dest_Free) corec_ss
    1.26 -        (HOLogic.mk_comp (mk_unfold Ts (mk_corec_strs corec_ss) i, Inr_const T AT));
    1.27 -
    1.28 -    val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) =
    1.29 -      lthy
    1.30 -      |> Local_Theory.open_target |> snd
    1.31 -      |> @{fold_map 3} (fn i => fn T => fn AT =>
    1.32 -        Local_Theory.define ((corec_bind i, NoSyn), (corec_def_bind i, corec_spec i T AT)))
    1.33 -          ks Ts activeAs
    1.34 -      |>> apsnd split_list o split_list
    1.35 -      ||> `Local_Theory.close_target;
    1.36 -
    1.37 -    val phi = Proof_Context.export_morphism lthy_old lthy;
    1.38 -    val corecs = map (Morphism.term phi) corec_frees;
    1.39 -    val corec_names = map (fst o dest_Const) corecs;
    1.40 -    fun mk_corecs Ts passives actives =
    1.41 -      let val Tactives = map2 (curry mk_sumT) Ts actives;
    1.42 -      in
    1.43 -        @{map 3} (fn name => fn T => fn active =>
    1.44 -          Const (name, Library.foldr (op -->)
    1.45 -            (map2 (curry op -->) actives (mk_FTs (passives @ Tactives)), active --> T)))
    1.46 -        corec_names Ts actives
    1.47 -      end;
    1.48 -    fun mk_corec ss i = Term.list_comb (Const (nth corec_names (i - 1), Library.foldr (op -->)
    1.49 -      (map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
    1.50 -    val corec_defs = map (fn def =>
    1.51 -      mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) corec_def_frees;
    1.52 -
    1.53      val ((((((((zs, Jzs), Jzs_copy), Jzs1), Jzs2), unfold_fs), corec_ss), phis), _) =
    1.54        lthy
    1.55        |> mk_Frees "b" activeAs
    1.56 @@ -1659,57 +1613,6 @@
    1.57        ||>> mk_Frees "s" corec_sTs
    1.58        ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts);
    1.59  
    1.60 -    val case_sums =
    1.61 -      map2 (fn T => fn i => mk_case_sum (HOLogic.id_const T, mk_corec corec_ss i)) Ts ks;
    1.62 -    val dtor_corec_thms =
    1.63 -      let
    1.64 -        fun mk_goal i corec_s corec_map dtor z =
    1.65 -          let
    1.66 -            val lhs = dtor $ (mk_corec corec_ss i $ z);
    1.67 -            val rhs = Term.list_comb (corec_map, passive_ids @ case_sums) $ (corec_s $ z);
    1.68 -          in
    1.69 -            mk_Trueprop_eq (lhs, rhs)
    1.70 -          end;
    1.71 -        val goals = @{map 5} mk_goal ks corec_ss corec_maps_rev dtors zs;
    1.72 -      in
    1.73 -        @{map 3} (fn goal => fn unfold => fn map_cong0 =>
    1.74 -          Variable.add_free_names lthy goal []
    1.75 -          |> (fn vars => Goal.prove_sorry lthy vars [] goal
    1.76 -            (fn {context = ctxt, prems = _} => mk_corec_tac ctxt m corec_defs unfold map_cong0
    1.77 -              corec_Inl_sum_thms))
    1.78 -          |> Thm.close_derivation)
    1.79 -        goals dtor_unfold_thms map_cong0s
    1.80 -      end;
    1.81 -
    1.82 -    val corec_unique_mor_thm =
    1.83 -      let
    1.84 -        val id_fs = map2 (fn T => fn f => mk_case_sum (HOLogic.id_const T, f)) Ts unfold_fs;
    1.85 -        val prem = HOLogic.mk_Trueprop (mk_mor corec_UNIVs (mk_corec_strs corec_ss) UNIVs dtors id_fs);
    1.86 -        fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_corec corec_ss i);
    1.87 -        val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
    1.88 -          (map2 mk_fun_eq unfold_fs ks));
    1.89 -        val vars = fold (Variable.add_free_names lthy) [prem, unique] [];
    1.90 -      in
    1.91 -        Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique))
    1.92 -          (fn {context = ctxt, prems = _} => mk_corec_unique_mor_tac ctxt corec_defs
    1.93 -            corec_Inl_sum_thms unfold_unique_mor_thm)
    1.94 -          |> Thm.close_derivation
    1.95 -      end;
    1.96 -
    1.97 -    val map_id0s_o_id =
    1.98 -      map (fn thm =>
    1.99 -        mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}) @{thm id_comp})
   1.100 -      map_id0s;
   1.101 -
   1.102 -    val (dtor_corec_unique_thms, dtor_corec_unique_thm) =
   1.103 -      `split_conj_thm (split_conj_prems n
   1.104 -        (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm)
   1.105 -        |> unfold_thms lthy (@{thms o_case_sum comp_id id_comp comp_assoc[symmetric]
   1.106 -           case_sum_o_inj(1)} @ map_id0s_o_id @ sym_map_comps)
   1.107 -        OF replicate n @{thm arg_cong2[of _ _ _ _ case_sum, OF refl]});
   1.108 -
   1.109 -    val timer = time (timer "corec definitions & thms");
   1.110 -
   1.111      val (coinduct_params, dtor_coinduct_thm) =
   1.112        let
   1.113          val rels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs;
   1.114 @@ -2661,9 +2564,6 @@
   1.115      val dtor_unfold_o_Jmap_thms = mk_xtor_co_iter_o_map_thms Greatest_FP false m
   1.116        dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_unfold_thms)
   1.117        sym_map_comps map_cong0s;
   1.118 -    val dtor_corec_o_Jmap_thms = mk_xtor_co_iter_o_map_thms Greatest_FP true m
   1.119 -      dtor_corec_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_corec_thms)
   1.120 -      sym_map_comps map_cong0s;
   1.121  
   1.122      val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
   1.123      val Jrels = if m = 0 then map HOLogic.eq_const Ts
   1.124 @@ -2676,20 +2576,19 @@
   1.125            (map map_transfer_of_bnf bnfs) dtor_unfold_thms)
   1.126          lthy;
   1.127  
   1.128 -    val corec_allAs = passiveAs @ map2 (curry mk_sumT) Ts activeAs;
   1.129 -    val corec_allBs = passiveBs @ map2 (curry mk_sumT) Ts' activeBs;
   1.130 -    val corec_rels = map2 (fn Ds => mk_rel_of_bnf Ds corec_allAs corec_allBs) Dss bnfs;
   1.131 -    val corec_activephis =
   1.132 -      map2 (fn Jrel => mk_rel_sum (Term.list_comb (Jrel, Jphis))) Jrels activephis;
   1.133 -    val dtor_corec_transfer_thms =
   1.134 -      mk_xtor_co_iter_transfer_thms Greatest_FP corec_rels corec_activephis activephis Jrels Jphis
   1.135 -        (mk_corecs Ts passiveAs activeAs) (mk_corecs Ts' passiveBs activeBs)
   1.136 -        (fn {context = ctxt, prems = _} => mk_dtor_corec_transfer_tac ctxt n m corec_defs
   1.137 -           dtor_unfold_transfer_thms (map map_transfer_of_bnf bnfs) dtor_Jrel_thms)
   1.138 -        lthy;
   1.139 -
   1.140      val timer = time (timer "relator coinduction");
   1.141  
   1.142 +    fun mk_Ts As = map (typ_subst_atomic (passiveAs ~~ As)) Ts;
   1.143 +    val export = map (Morphism.term (Local_Theory.target_morphism lthy))
   1.144 +    val ((corecs, (dtor_corec_thms, dtor_corec_unique_thm, dtor_corec_o_Jmap_thms,
   1.145 +        dtor_corec_transfer_thms)), lthy) = lthy
   1.146 +      |> derive_xtor_co_recs Greatest_FP external_bs mk_Ts (Dss, resDs) bnfs
   1.147 +        (export dtors) (export unfolds)
   1.148 +        dtor_unfold_unique_thm dtor_unfold_thms dtor_unfold_transfer_thms
   1.149 +        dtor_Jmap_thms dtor_Jrel_thms;
   1.150 +
   1.151 +    val timer = time (timer "recursor");
   1.152 +
   1.153      val common_notes =
   1.154        [(dtor_coinductN, [dtor_coinduct_thm]),
   1.155        (dtor_rel_coinductN, [Jrel_coinduct_thm])]
   1.156 @@ -2700,10 +2599,6 @@
   1.157        [(ctor_dtorN, ctor_dtor_thms),
   1.158        (ctor_exhaustN, ctor_exhaust_thms),
   1.159        (ctor_injectN, ctor_inject_thms),
   1.160 -      (dtor_corecN, dtor_corec_thms),
   1.161 -      (dtor_corec_o_mapN, dtor_corec_o_Jmap_thms),
   1.162 -      (dtor_corec_transferN, dtor_corec_transfer_thms),
   1.163 -      (dtor_corec_uniqueN, dtor_corec_unique_thms),
   1.164        (dtor_ctorN, dtor_ctor_thms),
   1.165        (dtor_exhaustN, dtor_exhaust_thms),
   1.166        (dtor_injectN, dtor_inject_thms),
   1.167 @@ -2721,7 +2616,7 @@
   1.168  
   1.169      val fp_res =
   1.170        {Ts = Ts, bnfs = Jbnfs, pre_bnfs = bnfs, absT_infos = absT_infos,
   1.171 -       ctors = ctors, dtors = dtors, xtor_un_folds_legacy = unfolds, xtor_co_recs = corecs,
   1.172 +       ctors = ctors, dtors = dtors, xtor_un_folds_legacy = unfolds, xtor_co_recs = export corecs,
   1.173         xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms,
   1.174         ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_maps = dtor_Jmap_thms,
   1.175         xtor_map_unique = dtor_Jmap_unique_thm, xtor_setss = dtor_Jset_thmss',