src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML
changeset 62692 0701f25fac39
child 62723 3d7fe7ec7981
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML	Tue Mar 22 12:39:37 2016 +0100
     1.3 @@ -0,0 +1,217 @@
     1.4 +(*  Title:      HOL/Tools/BNF/bnf_gfp_grec_tactics.ML
     1.5 +    Author:     Jasmin Blanchette, Inria, LORIA, MPII
     1.6 +    Copyright   2016
     1.7 +
     1.8 +Tactics for generalized corecursor sugar.
     1.9 +*)
    1.10 +
    1.11 +signature BNF_GFP_GREC_SUGAR_TACTICS =
    1.12 +sig
    1.13 +  val rho_transfer_simps: thm list
    1.14 +
    1.15 +  val mk_case_dtor_tac: Proof.context -> term -> thm -> thm -> thm list -> thm -> thm list -> tactic
    1.16 +  val mk_cong_intro_ctr_or_friend_tac: Proof.context -> thm -> thm list -> thm -> tactic
    1.17 +  val mk_code_tac: Proof.context -> int -> term list -> term -> term -> thm -> thm -> thm list ->
    1.18 +    thm list -> thm list -> thm list -> thm -> thm -> thm list -> thm list -> thm -> thm list ->
    1.19 +    thm list -> thm list -> thm list -> thm list -> thm list -> thm -> tactic
    1.20 +  val mk_eq_algrho_tac: Proof.context -> term list -> term -> term -> term -> term -> term -> thm ->
    1.21 +    thm -> thm list -> thm list -> thm list -> thm list -> thm -> thm -> thm -> thm list ->
    1.22 +    thm list -> thm list -> thm -> thm list -> thm list -> thm list -> thm -> thm -> thm -> thm ->
    1.23 +    thm list -> thm list -> thm list -> thm list -> thm list -> tactic
    1.24 +  val mk_eq_corecUU_tac: Proof.context -> int -> term list -> term -> term -> thm -> thm ->
    1.25 +    thm list -> thm list -> thm list -> thm list -> thm -> thm -> thm list -> thm list ->
    1.26 +    thm list -> thm list -> thm list -> thm list -> thm list -> thm -> thm -> tactic
    1.27 +  val mk_last_disc_tac: Proof.context -> term -> thm -> thm list -> tactic
    1.28 +  val mk_rho_transfer_tac: Proof.context -> bool -> thm -> thm list -> tactic
    1.29 +  val mk_unique_tac: Proof.context -> int -> term list -> term -> term -> thm -> thm -> thm list ->
    1.30 +    thm list -> thm list -> thm list -> thm -> thm -> thm list -> thm list -> thm list ->
    1.31 +    thm list -> thm list -> thm list -> thm list -> thm -> thm -> tactic
    1.32 +end;
    1.33 +
    1.34 +structure BNF_GFP_Grec_Sugar_Tactics : BNF_GFP_GREC_SUGAR_TACTICS =
    1.35 +struct
    1.36 +
    1.37 +open Ctr_Sugar
    1.38 +open BNF_Util
    1.39 +open BNF_Tactics
    1.40 +open BNF_FP_Def_Sugar_Tactics
    1.41 +open BNF_GFP_Grec_Tactics
    1.42 +open BNF_GFP_Grec_Sugar_Util
    1.43 +
    1.44 +fun apply_func f =
    1.45 +  let
    1.46 +    val arg_Ts = binder_fun_types (fastype_of f);
    1.47 +    val args = map_index (fn (j, T) => Var (("a" ^ string_of_int j, 0), T)) arg_Ts;
    1.48 +  in
    1.49 +    list_comb (f, args)
    1.50 +  end;
    1.51 +
    1.52 +fun instantiate_distrib thm ctxt t =
    1.53 +  Drule.infer_instantiate' ctxt [SOME (Thm.incr_indexes_cterm 1 (Thm.cterm_of ctxt t))] thm;
    1.54 +
    1.55 +(* TODO (here and elsewhere): Use metaequality in goal instead and keep uninstianted version of
    1.56 +   theorem? *)
    1.57 +val mk_if_distrib_of = instantiate_distrib @{thm if_distrib};
    1.58 +val mk_case_sum_distrib_of = instantiate_distrib @{thm sum.case_distrib};
    1.59 +
    1.60 +fun mk_case_dtor_tac ctxt u abs_inverse dtor_ctor ctr_defs exhaust cases =
    1.61 +  let val exhaust' = Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt u)] exhaust in
    1.62 +    HEADGOAL (rtac ctxt exhaust') THEN
    1.63 +    REPEAT_DETERM (HEADGOAL (etac ctxt ssubst THEN'
    1.64 +      SELECT_GOAL (unfold_thms_tac ctxt cases THEN
    1.65 +        unfold_thms_tac ctxt (abs_inverse :: dtor_ctor :: ctr_defs @
    1.66 +        @{thms prod.case sum.case})) THEN'
    1.67 +      rtac ctxt refl))
    1.68 +  end;
    1.69 +
    1.70 +fun mk_cong_intro_ctr_or_friend_tac ctxt ctr_or_friend_def extra_simps cong_alg_intro =
    1.71 +  HEADGOAL (REPEAT_DETERM_N 2 o subst_tac ctxt NONE [ctr_or_friend_def] THEN'
    1.72 +    rtac ctxt cong_alg_intro) THEN
    1.73 +  unfold_thms_tac ctxt (extra_simps @ sumprod_thms_rel @
    1.74 +    @{thms vimage2p_def prod.rel_eq sum.rel_eq}) THEN
    1.75 +  REPEAT_DETERM (HEADGOAL (rtac ctxt conjI ORELSE' assume_tac ctxt ORELSE' rtac ctxt refl));
    1.76 +
    1.77 +val shared_simps =
    1.78 +  @{thms map_prod_simp map_sum.simps sum.case prod.case_eq_if split_beta' prod.sel
    1.79 +      sum.disc(1)[THEN eq_True[THEN iffD2]] sum.disc(2)[THEN eq_False[THEN iffD2]] sum.sel
    1.80 +      isl_map_sum map_sum_sel if_True if_False if_True_False Let_def[abs_def] o_def[abs_def] id_def
    1.81 +      BNF_Composition.id_bnf_def};
    1.82 +
    1.83 +fun mk_code_tac ctxt num_args fpsig_nesting_maps ssig_map eval pre_map_def abs_inverse
    1.84 +    fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms
    1.85 +    live_nesting_map_ident0s fp_map_ident case_trivial ctr_defs case_eq_ifs corecUU all_sig_maps
    1.86 +    ssig_map_thms all_algLam_alg_pointfuls all_algrho_eqs eval_simps inner_fp_simps fun_def =
    1.87 +  let
    1.88 +    val fun_def' =
    1.89 +      if null inner_fp_simps andalso num_args > 0 then
    1.90 +        fun_def RS meta_eq_to_obj_eq RS (mk_curry_uncurryN_balanced ctxt num_args RS iffD2) RS sym
    1.91 +      else
    1.92 +        fun_def;
    1.93 +    val case_trivial' = unfold_thms ctxt (case_eq_ifs @ ctr_defs @ shared_simps) case_trivial;
    1.94 +    val case_eq_ifs' = map (Drule.abs_def o (fn thm => thm RS eq_reflection)) case_eq_ifs;
    1.95 +    val if_distribs = @{thm if_distrib_fun} :: map (mk_if_distrib_of ctxt)
    1.96 +      (eval :: map apply_func (ssig_map :: fpsig_nesting_maps));
    1.97 +
    1.98 +    val unfold_tac = unfold_thms_tac ctxt (case_trivial' :: pre_map_def :: abs_inverse ::
    1.99 +      fp_map_ident :: (if null inner_fp_simps then [] else [corecUU]) @ fpsig_nesting_map_ident0s @
   1.100 +      fpsig_nesting_map_comps @ fpsig_nesting_map_thms @ live_nesting_map_ident0s @ ctr_defs @
   1.101 +      case_eq_ifs' @ all_sig_maps @ ssig_map_thms @ all_algLam_alg_pointfuls @ all_algrho_eqs @
   1.102 +      eval_simps @ if_distribs @ shared_simps);
   1.103 +  in
   1.104 +    HEADGOAL (subst_tac ctxt NONE [fun_def] THEN' subst_tac ctxt NONE [corecUU] THEN'
   1.105 +      (if null inner_fp_simps then K all_tac else subst_tac ctxt NONE inner_fp_simps)) THEN
   1.106 +    unfold_thms_tac ctxt [fun_def'] THEN
   1.107 +    unfold_tac THEN HEADGOAL (CONVERSION Thm.eta_long_conversion) THEN unfold_tac THEN
   1.108 +    HEADGOAL (rtac ctxt refl)
   1.109 +  end;
   1.110 +
   1.111 +fun mk_eq_algrho_tac ctxt fpsig_nesting_maps abs rep ctor ssig_map eval pre_map_def abs_inverse
   1.112 +    fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms
   1.113 +    live_nesting_map_ident0s fp_map_ident dtor_ctor ctor_iff_dtor ctr_defs nullary_disc_defs
   1.114 +    disc_sel_eq_cases case_dtor case_eq_ifs const_pointful_naturals fp_nesting_k_map_disc_sels'
   1.115 +    rho_def dtor_algrho corecUU_unique eq_corecUU all_sig_maps ssig_map_thms
   1.116 +    all_algLam_alg_pointfuls all_algrho_eqs eval_simps =
   1.117 +  let
   1.118 +    fun mk_abs_def thm = Drule.abs_def (thm RS eq_reflection);
   1.119 +
   1.120 +    val nullary_disc_defs' = nullary_disc_defs
   1.121 +      |> map (fn thm => thm RS sym)
   1.122 +      |> maps (fn thm => [thm, thm RS @{thm subst[OF eq_commute, of "%e. e = z" for z]}]);
   1.123 +
   1.124 +    val case_dtor' = unfold_thms ctxt shared_simps case_dtor;
   1.125 +    val disc_sel_eq_cases' = map (mk_abs_def
   1.126 +      o unfold_thms ctxt (case_dtor' :: ctr_defs @ shared_simps)) disc_sel_eq_cases;
   1.127 +    val const_pointful_naturals' = map (unfold_thms ctxt shared_simps) const_pointful_naturals;
   1.128 +    val const_pointful_naturals_sym' = map (fn thm => thm RS sym) const_pointful_naturals';
   1.129 +    val case_eq_ifs' = map mk_abs_def (@{thm sum.case_eq_if} :: case_eq_ifs);
   1.130 +
   1.131 +    val distrib_consts =
   1.132 +      abs :: rep :: ctor :: eval :: map apply_func (ssig_map :: fpsig_nesting_maps);
   1.133 +    val if_distribs = @{thm if_distrib_fun} :: map (mk_if_distrib_of ctxt) distrib_consts;
   1.134 +    val case_sum_distribs = map (mk_case_sum_distrib_of ctxt) distrib_consts;
   1.135 +
   1.136 +    val simp_ctxt = (ctxt
   1.137 +        |> Context_Position.set_visible false
   1.138 +        |> put_simpset (simpset_of (Proof_Context.init_global @{theory Main}))
   1.139 +        |> Raw_Simplifier.add_cong @{thm if_cong})
   1.140 +      addsimps pre_map_def :: abs_inverse :: fp_map_ident :: dtor_ctor :: rho_def ::
   1.141 +        @{thm convol_def} :: fpsig_nesting_map_ident0s @ fpsig_nesting_map_comps @
   1.142 +        fpsig_nesting_map_thms @ live_nesting_map_ident0s @ ctr_defs @ disc_sel_eq_cases' @
   1.143 +        fp_nesting_k_map_disc_sels' @ case_eq_ifs' @ all_sig_maps @ ssig_map_thms @
   1.144 +        all_algLam_alg_pointfuls @ all_algrho_eqs @ eval_simps @ if_distribs @ case_sum_distribs @
   1.145 +        shared_simps;
   1.146 +
   1.147 +    fun mk_main_simp const_pointful_naturals_maybe_sym' =
   1.148 +      simp_tac (simp_ctxt addsimps const_pointful_naturals_maybe_sym');
   1.149 +  in
   1.150 +    unfold_thms_tac ctxt [eq_corecUU] THEN
   1.151 +    HEADGOAL (REPEAT_DETERM o rtac ctxt ext THEN'
   1.152 +      rtac ctxt (corecUU_unique RS sym RS fun_cong) THEN'
   1.153 +      subst_tac ctxt NONE [dtor_algrho RS (ctor_iff_dtor RS iffD2)] THEN' rtac ctxt ext) THEN
   1.154 +    unfold_thms_tac ctxt (nullary_disc_defs' @ shared_simps) THEN
   1.155 +    HEADGOAL (rtac ctxt meta_eq_to_obj_eq) THEN
   1.156 +    REPEAT_DETERM_N (length const_pointful_naturals' + 1)
   1.157 +      (ALLGOALS (mk_main_simp const_pointful_naturals_sym') THEN
   1.158 +       ALLGOALS (mk_main_simp const_pointful_naturals'))
   1.159 +  end;
   1.160 +
   1.161 +fun mk_eq_corecUU_tac ctxt num_args fpsig_nesting_maps ssig_map eval pre_map_def abs_inverse
   1.162 +    fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms
   1.163 +    live_nesting_map_ident0s fp_map_ident case_trivial ctr_defs case_eq_ifs all_sig_maps
   1.164 +    ssig_map_thms all_algLam_alg_pointfuls all_algrho_eqs eval_simps corecUU_unique fun_code =
   1.165 +  let
   1.166 +    val case_trivial' = unfold_thms ctxt (case_eq_ifs @ ctr_defs @ shared_simps) case_trivial;
   1.167 +    val case_eq_ifs' = map (Drule.abs_def o (fn thm => thm RS eq_reflection)) case_eq_ifs;
   1.168 +    val if_distribs = @{thm if_distrib_fun} :: map (mk_if_distrib_of ctxt)
   1.169 +      (eval :: map apply_func (ssig_map :: fpsig_nesting_maps));
   1.170 +
   1.171 +    val unfold_tac = unfold_thms_tac ctxt (case_trivial' :: pre_map_def :: abs_inverse ::
   1.172 +      fp_map_ident :: fpsig_nesting_map_ident0s @ fpsig_nesting_map_comps @ fpsig_nesting_map_thms @
   1.173 +      live_nesting_map_ident0s @ ctr_defs @ case_eq_ifs' @ all_sig_maps @ ssig_map_thms @
   1.174 +      all_algLam_alg_pointfuls @ all_algrho_eqs @ eval_simps @ if_distribs @ shared_simps);
   1.175 +  in
   1.176 +    HEADGOAL (rtac ctxt (mk_curry_uncurryN_balanced ctxt num_args RS iffD1) THEN'
   1.177 +      rtac ctxt corecUU_unique THEN' rtac ctxt ext) THEN
   1.178 +    unfold_thms_tac ctxt @{thms prod.case_eq_if} THEN
   1.179 +    HEADGOAL (rtac ctxt (fun_code RS trans)) THEN
   1.180 +    unfold_tac THEN HEADGOAL (CONVERSION Thm.eta_long_conversion) THEN unfold_tac THEN
   1.181 +    HEADGOAL (rtac ctxt refl)
   1.182 +  end;
   1.183 +
   1.184 +fun mk_last_disc_tac ctxt u exhaust discs' =
   1.185 +  let val exhaust' = Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt u)] exhaust in
   1.186 +    HEADGOAL (rtac ctxt exhaust') THEN
   1.187 +    REPEAT_DETERM (HEADGOAL (etac ctxt ssubst THEN'
   1.188 +      simp_tac (ss_only (distinct Thm.eq_thm discs' @ @{thms simp_thms}) ctxt)))
   1.189 +  end;
   1.190 +
   1.191 +val rho_transfer_simps = @{thms BNF_Def.vimage2p_def[abs_def] BNF_Composition.id_bnf_def};
   1.192 +
   1.193 +fun mk_rho_transfer_tac ctxt unfold rel_def const_transfers =
   1.194 +  (if unfold then unfold_thms_tac ctxt (rel_def :: rho_transfer_simps) else all_tac) THEN
   1.195 +  HEADGOAL (transfer_prover_add_tac ctxt [] const_transfers);
   1.196 +
   1.197 +fun mk_unique_tac ctxt num_args fpsig_nesting_maps ssig_map eval pre_map_def abs_inverse
   1.198 +    fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms
   1.199 +    live_nesting_map_ident0s fp_map_ident case_trivial ctr_defs case_eq_ifs all_sig_maps
   1.200 +    ssig_map_thms all_algLam_alg_pointfuls all_algrho_eqs eval_simps corecUU_unique eq_corecUU =
   1.201 +  let
   1.202 +    val case_trivial' = unfold_thms ctxt (case_eq_ifs @ ctr_defs @ shared_simps) case_trivial;
   1.203 +    val case_eq_ifs' = map (Drule.abs_def o (fn thm => thm RS eq_reflection)) case_eq_ifs;
   1.204 +    val if_distribs = @{thm if_distrib_fun} :: map (mk_if_distrib_of ctxt)
   1.205 +      (eval :: map apply_func (ssig_map :: fpsig_nesting_maps));
   1.206 +
   1.207 +    val unfold_tac = unfold_thms_tac ctxt (case_trivial' :: pre_map_def :: abs_inverse ::
   1.208 +      fp_map_ident :: fpsig_nesting_map_ident0s @ fpsig_nesting_map_comps @ fpsig_nesting_map_thms @
   1.209 +      live_nesting_map_ident0s @ ctr_defs @ case_eq_ifs' @ all_sig_maps @ ssig_map_thms @
   1.210 +      all_algLam_alg_pointfuls @ all_algrho_eqs @ eval_simps @ if_distribs @ shared_simps);
   1.211 +  in
   1.212 +    HEADGOAL (subst_tac ctxt NONE [eq_corecUU] THEN'
   1.213 +      rtac ctxt (mk_curry_uncurryN_balanced ctxt num_args RS iffD1) THEN'
   1.214 +      rtac ctxt corecUU_unique THEN' rtac ctxt ext THEN'
   1.215 +      etac ctxt @{thm ssubst[of _ _ "\<lambda>x. f x = u" for f u]}) THEN
   1.216 +    unfold_tac THEN HEADGOAL (CONVERSION Thm.eta_long_conversion) THEN unfold_tac THEN
   1.217 +    HEADGOAL (rtac ctxt refl)
   1.218 +  end;
   1.219 +
   1.220 +end;