1(* Title: HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML 2 Author: Jasmin Blanchette, Inria, LORIA, MPII 3 Copyright 2016 4 5Tactics for generalized corecursor sugar. 6*) 7 8signature BNF_GFP_GREC_SUGAR_TACTICS = 9sig 10 val rho_transfer_simps: thm list 11 12 val mk_case_dtor_tac: Proof.context -> term -> thm -> thm -> thm list -> thm -> thm list -> tactic 13 val mk_cong_intro_ctr_or_friend_tac: Proof.context -> thm -> thm list -> thm -> tactic 14 val mk_code_tac: Proof.context -> int -> term list -> term -> term -> thm -> thm -> thm list -> 15 thm list -> thm list -> thm list -> thm -> thm -> thm list -> thm list -> thm -> thm list -> 16 thm list -> thm list -> thm list -> thm list -> thm list -> thm -> tactic 17 val mk_eq_algrho_tac: Proof.context -> term list -> term -> term -> term -> term -> term -> thm -> 18 thm -> thm list -> thm list -> thm list -> thm list -> thm -> thm -> thm -> thm list -> 19 thm list -> thm list -> thm -> thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> 20 thm list -> thm list -> thm list -> thm list -> thm list -> tactic 21 val mk_eq_corecUU_tac: Proof.context -> int -> term list -> term -> term -> thm -> thm -> 22 thm list -> thm list -> thm list -> thm list -> thm -> thm -> thm list -> thm list -> 23 thm list -> thm list -> thm list -> thm list -> thm list -> thm -> thm -> tactic 24 val mk_last_disc_tac: Proof.context -> term -> thm -> thm list -> tactic 25 val mk_rho_transfer_tac: Proof.context -> bool -> thm -> thm list -> tactic 26 val mk_unique_tac: Proof.context -> int -> term list -> term -> term -> thm -> thm -> thm list -> 27 thm list -> thm list -> thm list -> thm -> thm -> thm list -> thm list -> thm list -> 28 thm list -> thm list -> thm list -> thm list -> thm -> thm -> tactic 29end; 30 31structure BNF_GFP_Grec_Sugar_Tactics : BNF_GFP_GREC_SUGAR_TACTICS = 32struct 33 34open Ctr_Sugar 35open BNF_Util 36open BNF_Tactics 37open BNF_FP_Def_Sugar_Tactics 38open BNF_GFP_Grec_Tactics 39open BNF_GFP_Grec_Sugar_Util 40 41fun apply_func f = 42 let 43 val arg_Ts = binder_fun_types (fastype_of f); 44 val args = map_index (fn (j, T) => Var (("a" ^ string_of_int j, 0), T)) arg_Ts; 45 in 46 list_comb (f, args) 47 end; 48 49fun instantiate_distrib thm ctxt t = 50 infer_instantiate' ctxt [SOME (Thm.incr_indexes_cterm 1 (Thm.cterm_of ctxt t))] thm; 51 52val mk_if_distrib_of = instantiate_distrib @{thm if_distrib}; 53val mk_case_sum_distrib_of = instantiate_distrib @{thm sum.case_distrib}; 54 55fun mk_case_dtor_tac ctxt u abs_inverse dtor_ctor ctr_defs exhaust cases = 56 let val exhaust' = infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt u)] exhaust in 57 HEADGOAL (rtac ctxt exhaust') THEN 58 REPEAT_DETERM (HEADGOAL (etac ctxt ssubst THEN' 59 SELECT_GOAL (unfold_thms_tac ctxt cases THEN 60 unfold_thms_tac ctxt (abs_inverse :: dtor_ctor :: ctr_defs @ 61 @{thms prod.case sum.case})) THEN' 62 rtac ctxt refl)) 63 end; 64 65fun mk_cong_intro_ctr_or_friend_tac ctxt ctr_or_friend_def extra_simps cong_alg_intro = 66 HEADGOAL (REPEAT_DETERM_N 2 o subst_tac ctxt NONE [ctr_or_friend_def] THEN' 67 rtac ctxt cong_alg_intro) THEN 68 unfold_thms_tac ctxt (extra_simps @ sumprod_thms_rel @ 69 @{thms vimage2p_def prod.rel_eq sum.rel_eq}) THEN 70 REPEAT_DETERM (HEADGOAL (rtac ctxt conjI ORELSE' assume_tac ctxt ORELSE' rtac ctxt refl ORELSE' 71 etac ctxt subst)); 72 73val shared_simps = 74 @{thms map_prod_simp map_sum.simps sum.case prod.case_eq_if split_beta' prod.sel 75 sum.disc(1)[THEN eq_True[THEN iffD2]] sum.disc(2)[THEN eq_False[THEN iffD2]] sum.sel 76 isl_map_sum map_sum_sel if_True if_False if_True_False Let_def[abs_def] o_def[abs_def] id_def 77 BNF_Composition.id_bnf_def}; 78 79fun mk_code_tac ctxt num_args fpsig_nesting_maps ssig_map eval pre_map_def abs_inverse 80 fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms 81 live_nesting_map_ident0s fp_map_ident case_trivial ctr_defs case_eq_ifs corecUU all_sig_maps 82 ssig_map_thms all_algLam_alg_pointfuls all_algrho_eqs eval_simps inner_fp_simps fun_def = 83 let 84 val fun_def' = 85 if null inner_fp_simps andalso num_args > 0 then 86 HOLogic.mk_obj_eq fun_def RS (mk_curry_uncurryN_balanced ctxt num_args RS iffD2) RS sym 87 else 88 fun_def; 89 val case_trivial' = unfold_thms ctxt (case_eq_ifs @ ctr_defs @ shared_simps) case_trivial; 90 val case_eq_ifs' = map (Drule.abs_def o (fn thm => thm RS eq_reflection)) case_eq_ifs; 91 val if_distribs = @{thm if_distrib_fun} :: map (mk_if_distrib_of ctxt) 92 (eval :: map apply_func (ssig_map :: fpsig_nesting_maps)); 93 94 val unfold_tac = unfold_thms_tac ctxt (case_trivial' :: pre_map_def :: abs_inverse :: 95 fp_map_ident :: (if null inner_fp_simps then [] else [corecUU]) @ fpsig_nesting_map_ident0s @ 96 fpsig_nesting_map_comps @ fpsig_nesting_map_thms @ live_nesting_map_ident0s @ ctr_defs @ 97 case_eq_ifs' @ all_sig_maps @ ssig_map_thms @ all_algLam_alg_pointfuls @ all_algrho_eqs @ 98 eval_simps @ if_distribs @ shared_simps); 99 in 100 HEADGOAL (subst_tac ctxt NONE [fun_def] THEN' subst_tac ctxt NONE [corecUU] THEN' 101 (if null inner_fp_simps then K all_tac else subst_tac ctxt NONE inner_fp_simps)) THEN 102 unfold_thms_tac ctxt [fun_def'] THEN 103 unfold_tac THEN HEADGOAL (CONVERSION Thm.eta_long_conversion) THEN unfold_tac THEN 104 HEADGOAL (rtac ctxt refl) 105 end; 106 107fun mk_eq_algrho_tac ctxt fpsig_nesting_maps abs rep ctor ssig_map eval pre_map_def abs_inverse 108 fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms 109 live_nesting_map_ident0s fp_map_ident dtor_ctor ctor_iff_dtor ctr_defs nullary_disc_defs 110 disc_sel_eq_cases case_dtor case_eq_ifs const_pointful_naturals fp_nesting_k_map_disc_sels' 111 rho_def dtor_algrho corecUU_unique eq_corecUU all_sig_maps ssig_map_thms 112 all_algLam_alg_pointfuls all_algrho_eqs eval_simps = 113 let 114 val nullary_disc_defs' = nullary_disc_defs 115 |> map (fn thm => thm RS sym) 116 |> maps (fn thm => [thm, thm RS @{thm subst[OF eq_commute, of "%e. e = z" for z]}]); 117 118 val case_dtor' = unfold_thms ctxt shared_simps case_dtor; 119 val disc_sel_eq_cases' = map (mk_abs_def 120 o unfold_thms ctxt (case_dtor' :: ctr_defs @ shared_simps)) disc_sel_eq_cases; 121 val extra_naturals = Facts.retrieve (Context.Proof ctxt) (Proof_Context.facts_of ctxt) 122 ("friend_of_corec_simps", Position.none) |> #thms; 123 val const_pointful_naturals' = map (unfold_thms ctxt shared_simps) 124 (extra_naturals @ const_pointful_naturals); 125 val const_pointful_naturals_sym' = map (fn thm => thm RS sym) const_pointful_naturals'; 126 val case_eq_ifs' = map mk_abs_def (@{thm sum.case_eq_if} :: case_eq_ifs); 127 128 val distrib_consts = 129 abs :: rep :: ctor :: eval :: map apply_func (ssig_map :: fpsig_nesting_maps); 130 val if_distribs = @{thm if_distrib_fun} :: map (mk_if_distrib_of ctxt) distrib_consts; 131 val case_sum_distribs = map (mk_case_sum_distrib_of ctxt) distrib_consts; 132 133 val simp_ctxt = (ctxt 134 |> Context_Position.set_visible false 135 |> put_simpset (simpset_of (Proof_Context.init_global \<^theory>\<open>Main\<close>)) 136 |> Raw_Simplifier.add_cong @{thm if_cong}) 137 addsimps pre_map_def :: abs_inverse :: fp_map_ident :: dtor_ctor :: rho_def :: 138 @{thm convol_def} :: fpsig_nesting_map_ident0s @ fpsig_nesting_map_comps @ 139 fpsig_nesting_map_thms @ live_nesting_map_ident0s @ ctr_defs @ disc_sel_eq_cases' @ 140 fp_nesting_k_map_disc_sels' @ case_eq_ifs' @ all_sig_maps @ ssig_map_thms @ 141 all_algLam_alg_pointfuls @ all_algrho_eqs @ eval_simps @ if_distribs @ case_sum_distribs @ 142 shared_simps; 143 144 fun mk_main_simp const_pointful_naturals_maybe_sym' = 145 simp_tac (simp_ctxt addsimps const_pointful_naturals_maybe_sym'); 146 in 147 unfold_thms_tac ctxt [eq_corecUU] THEN 148 HEADGOAL (REPEAT_DETERM o rtac ctxt ext THEN' 149 rtac ctxt (corecUU_unique RS sym RS fun_cong) THEN' 150 subst_tac ctxt NONE [dtor_algrho RS (ctor_iff_dtor RS iffD2)] THEN' rtac ctxt ext) THEN 151 unfold_thms_tac ctxt (nullary_disc_defs' @ shared_simps) THEN 152 HEADGOAL (rtac ctxt meta_eq_to_obj_eq) THEN 153 REPEAT_DETERM_N (length const_pointful_naturals' + 1) 154 (ALLGOALS (mk_main_simp const_pointful_naturals_sym') THEN 155 ALLGOALS (mk_main_simp const_pointful_naturals')) 156 end; 157 158fun mk_eq_corecUU_tac ctxt num_args fpsig_nesting_maps ssig_map eval pre_map_def abs_inverse 159 fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms 160 live_nesting_map_ident0s fp_map_ident case_trivial ctr_defs case_eq_ifs all_sig_maps 161 ssig_map_thms all_algLam_alg_pointfuls all_algrho_eqs eval_simps corecUU_unique fun_code = 162 let 163 val case_trivial' = unfold_thms ctxt (case_eq_ifs @ ctr_defs @ shared_simps) case_trivial; 164 val case_eq_ifs' = map (Drule.abs_def o (fn thm => thm RS eq_reflection)) case_eq_ifs; 165 val if_distribs = @{thm if_distrib_fun} :: map (mk_if_distrib_of ctxt) 166 (eval :: map apply_func (ssig_map :: fpsig_nesting_maps)); 167 168 val unfold_tac = unfold_thms_tac ctxt (case_trivial' :: pre_map_def :: abs_inverse :: 169 fp_map_ident :: fpsig_nesting_map_ident0s @ fpsig_nesting_map_comps @ fpsig_nesting_map_thms @ 170 live_nesting_map_ident0s @ ctr_defs @ case_eq_ifs' @ all_sig_maps @ ssig_map_thms @ 171 all_algLam_alg_pointfuls @ all_algrho_eqs @ eval_simps @ if_distribs @ shared_simps); 172 in 173 HEADGOAL (rtac ctxt (mk_curry_uncurryN_balanced ctxt num_args RS iffD1) THEN' 174 rtac ctxt corecUU_unique THEN' rtac ctxt ext) THEN 175 unfold_thms_tac ctxt @{thms prod.case_eq_if} THEN 176 HEADGOAL (rtac ctxt (fun_code RS trans)) THEN 177 unfold_tac THEN HEADGOAL (CONVERSION Thm.eta_long_conversion) THEN unfold_tac THEN 178 HEADGOAL (rtac ctxt refl) 179 end; 180 181fun mk_last_disc_tac ctxt u exhaust discs' = 182 let val exhaust' = infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt u)] exhaust in 183 HEADGOAL (rtac ctxt exhaust') THEN 184 REPEAT_DETERM (HEADGOAL (etac ctxt ssubst THEN' 185 simp_tac (ss_only (distinct Thm.eq_thm discs' @ @{thms simp_thms}) ctxt))) 186 end; 187 188val rho_transfer_simps = @{thms BNF_Def.vimage2p_def[abs_def] BNF_Composition.id_bnf_def}; 189 190fun mk_rho_transfer_tac ctxt unfold rel_def const_transfers = 191 (if unfold then unfold_thms_tac ctxt (rel_def :: rho_transfer_simps) else all_tac) THEN 192 HEADGOAL (transfer_prover_add_tac ctxt [] const_transfers); 193 194fun mk_unique_tac ctxt num_args fpsig_nesting_maps ssig_map eval pre_map_def abs_inverse 195 fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms 196 live_nesting_map_ident0s fp_map_ident case_trivial ctr_defs case_eq_ifs all_sig_maps 197 ssig_map_thms all_algLam_alg_pointfuls all_algrho_eqs eval_simps corecUU_unique eq_corecUU = 198 let 199 val case_trivial' = unfold_thms ctxt (case_eq_ifs @ ctr_defs @ shared_simps) case_trivial; 200 val case_eq_ifs' = map (Drule.abs_def o (fn thm => thm RS eq_reflection)) case_eq_ifs; 201 val if_distribs = @{thm if_distrib_fun} :: map (mk_if_distrib_of ctxt) 202 (eval :: map apply_func (ssig_map :: fpsig_nesting_maps)); 203 204 val unfold_tac = unfold_thms_tac ctxt (case_trivial' :: pre_map_def :: abs_inverse :: 205 fp_map_ident :: fpsig_nesting_map_ident0s @ fpsig_nesting_map_comps @ fpsig_nesting_map_thms @ 206 live_nesting_map_ident0s @ ctr_defs @ case_eq_ifs' @ all_sig_maps @ ssig_map_thms @ 207 all_algLam_alg_pointfuls @ all_algrho_eqs @ eval_simps @ if_distribs @ shared_simps); 208 in 209 HEADGOAL (subst_tac ctxt NONE [eq_corecUU] THEN' 210 rtac ctxt (mk_curry_uncurryN_balanced ctxt num_args RS iffD1) THEN' 211 rtac ctxt corecUU_unique THEN' rtac ctxt ext THEN' 212 etac ctxt @{thm ssubst[of _ _ "\<lambda>x. f x = u" for f u]}) THEN 213 unfold_tac THEN HEADGOAL (CONVERSION Thm.eta_long_conversion) THEN unfold_tac THEN 214 HEADGOAL (rtac ctxt refl) 215 end; 216 217end; 218