src/HOL/Tools/BNF/bnf_fp_util.ML
changeset 62905 52c5a25e0c96
parent 62863 e0b894bba6ff
child 62907 9ad0bac25a84
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Apr 07 17:26:22 2016 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Apr 07 17:56:22 2016 +0200
     1.3 @@ -188,6 +188,8 @@
     1.4    val mk_sum_Cinfinite: thm list -> thm
     1.5    val mk_sum_card_order: thm list -> thm
     1.6  
     1.7 +  val force_typ: Proof.context -> typ -> term -> term
     1.8 +
     1.9    val mk_xtor_rel_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list ->
    1.10      term list -> term list -> term list -> term list -> term list ->
    1.11      ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm
    1.12 @@ -196,6 +198,10 @@
    1.13      ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm list
    1.14    val mk_xtor_co_iter_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list ->
    1.15      thm list -> thm list -> thm list
    1.16 +  val derive_xtor_co_recs: BNF_Util.fp_kind -> binding list -> (typ list -> typ list) ->
    1.17 +    (typ list list * typ list) -> BNF_Def.bnf list -> term list -> term list ->
    1.18 +    thm -> thm list -> thm list -> thm list -> thm list -> local_theory ->
    1.19 +    (term list * (thm list * thm * thm list * thm list)) * local_theory
    1.20  
    1.21    val fixpoint_bnf: (binding -> binding) ->
    1.22        (binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
    1.23 @@ -213,6 +219,7 @@
    1.24  open BNF_Comp
    1.25  open BNF_Def
    1.26  open BNF_Util
    1.27 +open BNF_FP_Util_Tactics
    1.28  
    1.29  type fp_result =
    1.30    {Ts: typ list,
    1.31 @@ -611,6 +618,232 @@
    1.32      split_conj_thm (un_fold_unique OF map (case_fp fp I mk_sym) unique_prems)
    1.33    end;
    1.34  
    1.35 +fun force_typ ctxt T =
    1.36 +  Term.map_types Type_Infer.paramify_vars
    1.37 +  #> Type.constraint T
    1.38 +  #> Syntax.check_term ctxt
    1.39 +  #> singleton (Variable.polymorphic ctxt);
    1.40 +
    1.41 +fun mk_xtor_un_fold_xtor_thms fp xtor_un_fold_unique_thm map_id0s =
    1.42 +  (xtor_un_fold_unique_thm OF
    1.43 +    map (fn thm => case_fp fp
    1.44 +      (mk_trans @{thm id_o}
    1.45 +        (mk_sym (thm RS @{thm trans[OF arg_cong2[of _ _ _ _ "op o", OF refl] o_id]})))
    1.46 +      (mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]})
    1.47 +        @{thm trans[OF id_o o_id[symmetric]]}))
    1.48 +    map_id0s)
    1.49 +  |> split_conj_thm |> map mk_sym;
    1.50 +
    1.51 +fun derive_xtor_co_recs fp bs mk_Ts (Dss, resDs) pre_bnfs xtors0 un_folds0
    1.52 +    xtor_un_fold_unique xtor_un_folds xtor_un_fold_transfers xtor_maps xtor_rels lthy =
    1.53 +  let
    1.54 +    fun co_swap pair = case_fp fp I swap pair;
    1.55 +    val mk_co_comp = curry (HOLogic.mk_comp o co_swap);
    1.56 +    fun mk_co_algT T U = case_fp fp (T --> U) (U --> T);
    1.57 +    val co_alg_funT = case_fp fp domain_type range_type;
    1.58 +    val mk_co_product = curry (case_fp fp mk_convol mk_case_sum);
    1.59 +    val co_proj1_const = case_fp fp fst_const (uncurry Inl_const o dest_sumT) o co_alg_funT;
    1.60 +    val co_proj2_const = case_fp fp snd_const (uncurry Inr_const o dest_sumT) o co_alg_funT;
    1.61 +    val mk_co_productT = curry (case_fp fp HOLogic.mk_prodT mk_sumT);
    1.62 +
    1.63 +    val n = length pre_bnfs;
    1.64 +    val live = live_of_bnf (hd pre_bnfs);
    1.65 +    val m = live - n;
    1.66 +    val ks = 1 upto n;
    1.67 +
    1.68 +    val map_id0s = map map_id0_of_bnf pre_bnfs;
    1.69 +    val map_comps = map map_comp_of_bnf pre_bnfs;
    1.70 +    val map_cong0s = map map_cong0_of_bnf pre_bnfs;
    1.71 +    val map_transfers = map map_transfer_of_bnf pre_bnfs;
    1.72 +    val sym_map_comp0s = map (mk_sym o map_comp0_of_bnf) pre_bnfs;
    1.73 +
    1.74 +    val deads = fold (union (op =)) Dss resDs;
    1.75 +    val ((((As, Bs), Xs), Ys), names_lthy) = lthy
    1.76 +      |> fold Variable.declare_typ deads
    1.77 +      |> mk_TFrees m
    1.78 +      ||>> mk_TFrees m
    1.79 +      ||>> mk_TFrees n
    1.80 +      ||>> mk_TFrees n;
    1.81 +
    1.82 +    val XFTs = @{map 2} (fn Ds => mk_T_of_bnf Ds (As @ Xs)) Dss pre_bnfs;
    1.83 +    val co_algXFTs = @{map 2} mk_co_algT XFTs Xs;
    1.84 +    val Ts = mk_Ts As;
    1.85 +    val un_foldTs = @{map 2} (fn T => fn X => co_algXFTs ---> mk_co_algT T X) Ts Xs;
    1.86 +    val un_folds = @{map 2} (force_typ names_lthy) un_foldTs un_folds0;
    1.87 +    val ABs = As ~~ Bs;
    1.88 +    val XYs = Xs ~~ Ys;
    1.89 +
    1.90 +    val Us = map (typ_subst_atomic ABs) Ts;
    1.91 +
    1.92 +    val TFTs = @{map 2} (fn Ds => mk_T_of_bnf Ds (As @ Ts)) Dss pre_bnfs;
    1.93 +
    1.94 +    val xtors = @{map 3} (force_typ names_lthy oo mk_co_algT) TFTs Ts xtors0;
    1.95 +
    1.96 +    val ids = map HOLogic.id_const As;
    1.97 +    val co_rec_Xs = @{map 2} mk_co_productT Ts Xs;
    1.98 +    val co_rec_Ys = @{map 2} mk_co_productT Us Ys;
    1.99 +    val co_rec_algXs = @{map 2} mk_co_algT co_rec_Xs Xs;
   1.100 +    val co_proj1s = map co_proj1_const co_rec_algXs;
   1.101 +    val co_rec_maps = @{map 2} (fn Ds =>
   1.102 +      mk_map_of_bnf Ds (As @ case_fp fp co_rec_Xs Ts) (As @ case_fp fp Ts co_rec_Xs)) Dss pre_bnfs;
   1.103 +    val co_rec_Ts = @{map 2} (fn Ds => mk_T_of_bnf Ds (As @ co_rec_Xs)) Dss pre_bnfs
   1.104 +    val co_rec_argTs = @{map 2} mk_co_algT co_rec_Ts Xs;
   1.105 +    val co_rec_resTs = @{map 2} mk_co_algT Ts Xs;
   1.106 +
   1.107 +    val (((co_rec_ss, fs), xs), names_lthy) = names_lthy
   1.108 +      |> mk_Frees "s" co_rec_argTs
   1.109 +      ||>> mk_Frees "f" co_rec_resTs
   1.110 +      ||>> mk_Frees "x" (case_fp fp TFTs Xs);
   1.111 +
   1.112 +    val co_rec_strs =
   1.113 +      @{map 3} (fn xtor => fn s => fn mapx =>
   1.114 +        mk_co_product (mk_co_comp xtor (list_comb (mapx, ids @ co_proj1s))) s)
   1.115 +      xtors co_rec_ss co_rec_maps;
   1.116 +
   1.117 +    val theta = Xs ~~ co_rec_Xs;
   1.118 +    val co_rec_un_folds = map (subst_atomic_types theta) un_folds;
   1.119 +
   1.120 +    val co_rec_spec0s = map (fn un_fold => list_comb (un_fold, co_rec_strs)) co_rec_un_folds;
   1.121 +
   1.122 +    val co_rec_ids = @{map 2} (mk_co_comp o co_proj1_const) co_rec_algXs co_rec_spec0s;
   1.123 +    val co_rec_specs = @{map 2} (mk_co_comp o co_proj2_const) co_rec_algXs co_rec_spec0s;
   1.124 +
   1.125 +    val co_recN = case_fp fp ctor_recN dtor_corecN;
   1.126 +    fun co_rec_bind i = nth bs (i - 1) |> Binding.prefix_name (co_recN ^ "_");
   1.127 +    val co_rec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o co_rec_bind;
   1.128 +
   1.129 +    fun co_rec_spec i =
   1.130 +      fold_rev (Term.absfree o Term.dest_Free) co_rec_ss (nth co_rec_specs (i - 1));
   1.131 +
   1.132 +    val ((co_rec_frees, (_, co_rec_def_frees)), (lthy, lthy_old)) =
   1.133 +      lthy
   1.134 +      |> Local_Theory.open_target |> snd
   1.135 +      |> fold_map (fn i =>
   1.136 +        Local_Theory.define ((co_rec_bind i, NoSyn), (co_rec_def_bind i, co_rec_spec i))) ks
   1.137 +      |>> apsnd split_list o split_list
   1.138 +      ||> `Local_Theory.close_target;
   1.139 +
   1.140 +    val phi = Proof_Context.export_morphism lthy_old lthy;
   1.141 +    val co_rec_names = map (fst o dest_Const o Morphism.term phi) co_rec_frees;
   1.142 +    val co_recs = @{map 2} (fn name => fn resT =>
   1.143 +      Const (name, co_rec_argTs ---> resT)) co_rec_names co_rec_resTs;
   1.144 +    val co_rec_defs = map (fn def =>
   1.145 +      mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) co_rec_def_frees;
   1.146 +
   1.147 +    val xtor_un_fold_xtor_thms = mk_xtor_un_fold_xtor_thms fp xtor_un_fold_unique map_id0s;
   1.148 +
   1.149 +    val co_rec_id_thms =
   1.150 +      let
   1.151 +        val goal = @{map 2} (fn T => fn t => HOLogic.mk_eq (t, HOLogic.id_const T)) Ts co_rec_ids
   1.152 +          |> Library.foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop;
   1.153 +        val vars = Variable.add_free_names lthy goal [];
   1.154 +      in
   1.155 +        Goal.prove_sorry lthy vars [] goal
   1.156 +          (fn {context = ctxt, prems = _} => mk_xtor_co_rec_id_tac ctxt xtor_un_fold_xtor_thms
   1.157 +            xtor_un_fold_unique xtor_un_folds map_comps)
   1.158 +          |> Thm.close_derivation
   1.159 +          |> split_conj_thm
   1.160 +      end;
   1.161 +
   1.162 +    val co_rec_app_ss = map (fn co_rec => list_comb (co_rec, co_rec_ss)) co_recs;
   1.163 +    val co_products = @{map 2} (fn T => mk_co_product (HOLogic.id_const T)) Ts co_rec_app_ss;
   1.164 +    val co_rec_maps_rev = @{map 2} (fn Ds =>
   1.165 +      mk_map_of_bnf Ds (As @ case_fp fp Ts co_rec_Xs) (As @ case_fp fp co_rec_Xs Ts)) Dss pre_bnfs;
   1.166 +    fun mk_co_app f g x = case_fp fp (f $ (g $ x)) (g $ (f $ x));
   1.167 +    val co_rec_expand_thms = map (fn thm => thm RS
   1.168 +      case_fp fp @{thm convol_expand_snd} @{thm case_sum_expand_Inr_pointfree}) co_rec_id_thms;
   1.169 +    val xtor_co_rec_thms =
   1.170 +      let
   1.171 +        fun mk_goal co_rec s mapx xtor x =
   1.172 +          let
   1.173 +            val lhs = mk_co_app co_rec xtor x;
   1.174 +            val rhs = mk_co_app s (list_comb (mapx, ids @ co_products)) x;
   1.175 +          in
   1.176 +            mk_Trueprop_eq (lhs, rhs)
   1.177 +          end;
   1.178 +        val goals = @{map 5} mk_goal co_rec_app_ss co_rec_ss co_rec_maps_rev xtors xs;
   1.179 +      in
   1.180 +        map2 (fn goal => fn un_fold =>
   1.181 +          Variable.add_free_names lthy goal []
   1.182 +          |> (fn vars => Goal.prove_sorry lthy vars [] goal
   1.183 +            (fn {context = ctxt, prems = _} =>
   1.184 +              mk_xtor_co_rec_tac ctxt un_fold co_rec_defs co_rec_expand_thms))
   1.185 +          |> Thm.close_derivation)
   1.186 +        goals xtor_un_folds
   1.187 +      end;
   1.188 +
   1.189 +    val co_product_fs = @{map 2} (fn T => mk_co_product (HOLogic.id_const T)) Ts fs;
   1.190 +    val co_rec_expand'_thms = map (fn thm =>
   1.191 +      thm RS case_fp fp @{thm convol_expand_snd'} @{thm case_sum_expand_Inr'}) co_rec_id_thms;
   1.192 +    val xtor_co_rec_unique_thm =
   1.193 +      let
   1.194 +        fun mk_prem f s mapx xtor =
   1.195 +          let
   1.196 +            val lhs = mk_co_comp f xtor;
   1.197 +            val rhs = mk_co_comp s (list_comb (mapx, ids @ co_product_fs));
   1.198 +          in
   1.199 +            mk_Trueprop_eq (co_swap (lhs, rhs))
   1.200 +          end;
   1.201 +        val prems = @{map 4} mk_prem fs co_rec_ss co_rec_maps_rev xtors;
   1.202 +        val concl = @{map 2} (curry HOLogic.mk_eq) fs co_rec_app_ss
   1.203 +          |> Library.foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop;
   1.204 +        val goal = Logic.list_implies (prems, concl);
   1.205 +        val vars = Variable.add_free_names lthy goal [];
   1.206 +      in
   1.207 +        Goal.prove_sorry lthy vars [] goal
   1.208 +          (fn {context = ctxt, prems = _} => mk_xtor_co_rec_unique_tac ctxt fp co_rec_defs
   1.209 +            co_rec_expand'_thms xtor_un_fold_unique map_id0s sym_map_comp0s)
   1.210 +        |> Thm.close_derivation
   1.211 +      end;
   1.212 +
   1.213 +    val xtor_co_rec_o_map_thms = mk_xtor_co_iter_o_map_thms fp true m xtor_co_rec_unique_thm
   1.214 +      (map (mk_pointfree lthy) xtor_maps) (map (mk_pointfree lthy) xtor_co_rec_thms)
   1.215 +      sym_map_comp0s map_cong0s;
   1.216 +
   1.217 +    val ABphiTs = @{map 2} mk_pred2T As Bs;
   1.218 +    val XYphiTs = @{map 2} mk_pred2T Xs Ys;
   1.219 +
   1.220 +    val ((ABphis, XYphis), names_lthy) = names_lthy
   1.221 +      |> mk_Frees "R" ABphiTs
   1.222 +      ||>> mk_Frees "S" XYphiTs;
   1.223 +
   1.224 +    val pre_rels =
   1.225 +      @{map 2} (fn Ds => mk_rel_of_bnf Ds (As @ co_rec_Xs) (Bs @ co_rec_Ys)) Dss pre_bnfs;
   1.226 +    val rels = @{map 3} (fn T => fn T' => Thm.prop_of #> HOLogic.dest_Trueprop
   1.227 +        #> fst o dest_comb #> fst o dest_comb #> funpow n (snd o dest_comb)
   1.228 +        #> case_fp fp (fst o dest_comb #> snd o dest_comb) (snd o dest_comb) #> head_of
   1.229 +        #> force_typ names_lthy (ABphiTs ---> mk_pred2T T T'))
   1.230 +      Ts Us xtor_un_fold_transfers;
   1.231 +
   1.232 +    fun tac {context = ctxt, prems = _} = mk_xtor_co_rec_transfer_tac ctxt fp n m co_rec_defs
   1.233 +      xtor_un_fold_transfers map_transfers xtor_rels;
   1.234 +
   1.235 +    val mk_rel_co_product = case_fp fp mk_rel_prod mk_rel_sum;
   1.236 +    val rec_phis =
   1.237 +      map2 (fn rel => mk_rel_co_product (Term.list_comb (rel, ABphis))) rels XYphis;
   1.238 +
   1.239 +    val xtor_co_rec_transfer_thms =
   1.240 +      mk_xtor_co_iter_transfer_thms fp pre_rels rec_phis XYphis rels ABphis
   1.241 +        co_recs (map (subst_atomic_types (ABs @ XYs)) co_recs) tac lthy;
   1.242 +
   1.243 +    val notes =
   1.244 +      [(case_fp fp ctor_recN dtor_corecN, xtor_co_rec_thms),
   1.245 +       (case_fp fp ctor_rec_uniqueN dtor_corec_uniqueN, split_conj_thm xtor_co_rec_unique_thm),
   1.246 +       (case_fp fp ctor_rec_o_mapN dtor_corec_o_mapN, xtor_co_rec_o_map_thms),
   1.247 +       (case_fp fp ctor_rec_transferN dtor_corec_transferN, xtor_co_rec_transfer_thms)]
   1.248 +      |> map (apsnd (map single))
   1.249 +      |> maps (fn (thmN, thmss) =>
   1.250 +        map2 (fn b => fn thms =>
   1.251 +          ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
   1.252 +        bs thmss);
   1.253 +
   1.254 +     val lthy = lthy |> Config.get lthy bnf_internals ? snd o Local_Theory.notes notes;
   1.255 +  in
   1.256 +    ((co_recs,
   1.257 +     (xtor_co_rec_thms, xtor_co_rec_unique_thm, xtor_co_rec_o_map_thms, xtor_co_rec_transfer_thms)),
   1.258 +      lthy)
   1.259 +  end;
   1.260 +
   1.261  fun fixpoint_bnf extra_qualify construct_fp bs resBs Ds0 fp_eqs comp_cache0 lthy =
   1.262    let
   1.263      val time = time lthy;