1(* Title: HOL/Tools/BNF/bnf_gfp_grec_tactics.ML 2 Author: Jasmin Blanchette, Inria, LORIA, MPII 3 Author: Dmitriy Traytel, ETH Zurich 4 Copyright 2015, 2016 5 6Tactics for generalized corecursor construction. 7*) 8 9signature BNF_GFP_GREC_TACTICS = 10sig 11 val transfer_prover_eq_tac: Proof.context -> int -> tactic 12 val transfer_prover_add_tac: Proof.context -> thm list -> thm list -> int -> tactic 13 14 val mk_algLam_algLam_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> 15 tactic 16 val mk_algLam_algrho_tac: Proof.context -> thm -> thm -> tactic 17 val mk_algLam_base_tac: Proof.context -> term -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> 18 thm list -> thm -> thm list -> thm list -> thm -> thm -> tactic 19 val mk_algLam_step_tac: Proof.context -> thm -> thm -> thm -> tactic 20 val mk_cong_locale_tac: Proof.context -> thm -> thm list -> thm -> thm -> thm list -> thm -> 21 thm -> tactic 22 val mk_corecU_pointfree_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm list -> thm -> 23 thm list -> thm -> thm -> thm -> tactic 24 val mk_corecUU_pointfree_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> 25 thm -> thm -> thm -> thm -> thm -> thm -> tactic 26 val mk_corecUU_unique_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> 27 thm -> thm -> thm -> thm -> thm -> thm -> tactic 28 val mk_corecUU_Inl_tac: Proof.context -> term -> thm -> thm -> thm -> thm -> thm list -> thm -> 29 thm list -> thm -> thm -> thm -> thm -> tactic 30 val mk_dtor_algLam_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm list -> 31 thm -> thm -> thm list -> thm -> thm -> thm -> thm -> tactic 32 val mk_dtor_algrho_tac: Proof.context -> thm -> thm -> thm -> thm -> tactic 33 val mk_dtor_transfer_tac: Proof.context -> thm -> tactic 34 val mk_equivp_Retr_tac: Proof.context -> thm -> thm -> thm -> thm -> tactic 35 val mk_eval_core_embL_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> 36 thm -> thm -> thm -> thm list -> thm list -> thm list -> thm -> tactic 37 val mk_eval_core_flat_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> 38 thm list -> thm -> thm list -> thm -> thm -> thm -> thm list -> tactic 39 val mk_eval_core_k_as_ssig_tac: Proof.context -> thm -> thm -> thm -> thm list -> thm -> thm -> 40 thm -> thm list -> tactic 41 val mk_eval_embL_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> tactic 42 val mk_eval_flat_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> 43 tactic 44 val mk_eval_sctr_tac: Proof.context -> thm -> thm -> thm -> thm -> tactic 45 val mk_eval_Oper_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> thm -> thm list -> 46 thm -> thm -> tactic 47 val mk_eval_V_or_CLeaf_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm list -> thm -> 48 tactic 49 val mk_extdd_mor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> 50 thm -> thm -> thm -> tactic 51 val mk_extdd_o_VLeaf_tac: Proof.context -> thm -> thm -> thm -> thm list -> thm list -> thm -> 52 thm -> thm -> tactic 53 val mk_flat_embL_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list -> 54 thm list -> thm list -> tactic 55 val mk_flat_VLeaf_or_flat_tac: Proof.context -> thm -> thm -> thm list -> tactic 56 val mk_Lam_Inl_Inr_tac: Proof.context -> thm -> thm -> tactic 57 val mk_mor_cutSsig_flat_tac: Proof.context -> term -> thm -> thm -> thm -> thm -> thm -> thm -> 58 thm list -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> tactic 59 val mk_natural_from_transfer_tac: Proof.context -> int -> bool list -> thm -> thm list -> 60 thm list -> thm list -> tactic 61 val mk_natural_by_unfolding_tac: Proof.context -> thm list -> tactic 62 val mk_Retr_coinduct_tac: Proof.context -> thm -> thm -> tactic 63 val mk_sig_transfer_tac: Proof.context -> thm -> thm list -> thm -> tactic 64 val mk_transfer_by_transfer_prover_tac: Proof.context -> thm list -> thm list -> thm list -> 65 tactic 66end; 67 68structure BNF_GFP_Grec_Tactics : BNF_GFP_GREC_TACTICS = 69struct 70 71open BNF_Util 72open BNF_Tactics 73open BNF_FP_Util 74 75val o_assoc = @{thm o_assoc}; 76val o_def = @{thm o_def}; 77 78fun ss_only_silent thms ctxt = 79 ss_only thms (ctxt |> Context_Position.set_visible false); 80 81fun context_relator_eq_add rel_eqs ctxt = 82 fold (snd oo Thm.proof_attributes (map (Attrib.attribute ctxt) @{attributes [relator_eq]})) 83 rel_eqs ctxt; 84val context_transfer_rule_add = fold (snd oo Thm.proof_attributes [Transfer.transfer_add]); 85 86fun transfer_prover_eq_tac ctxt = 87 SELECT_GOAL (Local_Defs.fold_tac ctxt (Transfer.get_relator_eq ctxt)) THEN' 88 Transfer.transfer_prover_tac ctxt; 89 90fun transfer_prover_add_tac ctxt rel_eqs transfers = 91 transfer_prover_eq_tac (ctxt 92 |> context_relator_eq_add rel_eqs 93 |> context_transfer_rule_add transfers); 94 95fun instantiate_natural_rule_with_id ctxt live = 96 Rule_Insts.of_rule ctxt ([], NONE :: replicate live (SOME \<^const_name>\<open>id\<close>)) []; 97 98fun instantiate_transfer_rule_with_Grp_UNIV ctxt alives thm = 99 let 100 val n = length alives; 101 val fs = map (prefix "f" o string_of_int) (1 upto n); 102 val ss = map2 (fn live => fn f => SOME (\<^const_name>\<open>BNF_Def.Grp\<close> ^ " " ^ \<^const_name>\<open>top\<close> ^ 103 " " ^ (if live then f else \<^const_name>\<open>id\<close>))) alives fs; 104 val bs = map_filter (fn (live, f) => if live then SOME (Binding.name f, NONE, NoSyn) else NONE) 105 (alives ~~ fs); 106 in 107 Rule_Insts.of_rule ctxt ([], ss) bs thm 108 end; 109 110fun mk_algLam_algLam_tac ctxt dead_pre_map_comp dtor_inject unsig sig_map Lam_def eval_embL 111 old_dtor_algLam dtor_algLam = 112 HEADGOAL (rtac ctxt ext THEN' rtac ctxt (dtor_inject RS iffD1)) THEN 113 unfold_thms_tac ctxt (dead_pre_map_comp :: unsig :: sig_map :: Lam_def :: eval_embL :: 114 old_dtor_algLam :: dtor_algLam :: @{thms o_apply id_o map_sum.simps sum.case}) THEN 115 HEADGOAL (rtac ctxt refl); 116 117fun mk_algLam_algrho_tac ctxt algLam_def algrho_def = 118 HEADGOAL (rtac ctxt ext) THEN unfold_thms_tac ctxt [algLam_def, algrho_def, o_apply] THEN 119 HEADGOAL (rtac ctxt refl); 120 121fun mk_algLam_base_tac ctxt dead_pre_map_dtor dead_pre_map_id dead_pre_map_comp ctor_dtor dtor_ctor 122 dtor_unfold_unique unsig Sig_pointful_natural ssig_maps Lam_def flat_simps eval_core_simps eval 123 algLam_def = 124 HEADGOAL (rtac ctxt (infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt dead_pre_map_dtor)] 125 (trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym]) OF [ext, ext])) THEN 126 ALLGOALS (asm_simp_tac (ss_only_silent (dead_pre_map_id :: ctor_dtor :: dtor_ctor :: unsig :: 127 Sig_pointful_natural :: Lam_def :: eval :: algLam_def :: 128 unfold_thms ctxt [o_def] dead_pre_map_comp :: ssig_maps @ flat_simps @ eval_core_simps @ 129 @{thms o_apply id_apply id_def[symmetric] snd_conv convol_apply}) ctxt)); 130 131fun mk_algLam_step_tac ctxt proto_sctr_def old_algLam_pointful algLam_algLam_pointful = 132 HEADGOAL (rtac ctxt ext) THEN 133 unfold_thms_tac ctxt [proto_sctr_def, old_algLam_pointful, algLam_algLam_pointful, o_apply] THEN 134 HEADGOAL (rtac ctxt refl); 135 136fun mk_cong_locale_tac ctxt dead_pre_rel_mono dead_pre_rel_maps equivp_Retr 137 ssig_rel_mono ssig_rel_maps eval eval_core_transfer = 138 HEADGOAL (resolve_tac ctxt (Locale.get_unfolds \<^context>) THEN' 139 etac ctxt ssig_rel_mono THEN' etac ctxt equivp_Retr) THEN 140 unfold_thms_tac ctxt (eval :: dead_pre_rel_maps @ @{thms id_apply}) THEN 141 HEADGOAL (rtac ctxt (@{thm predicate2I} RS (dead_pre_rel_mono RS @{thm predicate2D})) THEN' 142 etac ctxt @{thm rel_funD} THEN' assume_tac ctxt THEN' 143 rtac ctxt (eval_core_transfer RS @{thm rel_funD})) THEN 144 unfold_thms_tac ctxt (ssig_rel_maps @ @{thms vimage2p_rel_prod vimage2p_id}) THEN 145 unfold_thms_tac ctxt @{thms vimage2p_def} THEN HEADGOAL (assume_tac ctxt); 146 147fun mk_corecU_pointfree_tac ctxt dead_pre_map_comp dtor_unfold ssig_maps dead_ssig_map_comp0 148 flat_simps flat_VLeaf eval_core_simps cutSsig_def mor_cutSsig_flat corecU_def = 149 unfold_thms_tac ctxt [corecU_def, dead_ssig_map_comp0, o_assoc] THEN 150 HEADGOAL (subst_tac ctxt NONE [ext RS mor_cutSsig_flat] THEN' 151 asm_simp_tac (ss_only_silent [dtor_unfold, o_apply] ctxt) THEN' 152 asm_simp_tac (ss_only_silent (dtor_unfold :: flat_VLeaf :: cutSsig_def :: ssig_maps @ 153 flat_simps @ eval_core_simps @ unfold_thms ctxt [o_def] dead_pre_map_comp :: 154 @{thms o_def id_apply id_def[symmetric] snd_conv convol_apply}) ctxt)); 155 156fun mk_corecUU_tail_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor ssig_map_comp 157 flat_pointful_natural eval_core_pointful_natural eval eval_flat sctr_pointful_natural 158 eval_sctr_pointful = 159 asm_simp_tac (ss_only_silent (dtor_ctor :: flat_pointful_natural :: eval :: eval_flat :: 160 map (unfold_thms ctxt [o_def]) [dead_pre_map_comp, ssig_map_comp] @ 161 @{thms o_apply id_apply id_def[symmetric] convol_apply}) ctxt) THEN' 162 asm_simp_tac (ss_only_silent (eval_core_pointful_natural :: sctr_pointful_natural :: 163 eval_sctr_pointful :: map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, ssig_map_comp] @ 164 @{thms id_apply id_def[symmetric] convol_apply map_prod_simp}) ctxt); 165 166fun mk_corecUU_pointfree_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor dtor_inject 167 ssig_map_comp flat_pointful_natural eval_core_pointful_natural eval eval_flat corecU_ctor 168 sctr_pointful_natural eval_sctr_pointful corecUU_def = 169 unfold_thms_tac ctxt [corecUU_def] THEN 170 HEADGOAL (rtac ctxt ext THEN' subst_tac ctxt NONE [corecU_ctor RS sym]) THEN 171 unfold_thms_tac ctxt [corecUU_def RS symmetric_thm] THEN 172 HEADGOAL (rtac ctxt (dtor_inject RS iffD1) THEN' 173 mk_corecUU_tail_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor ssig_map_comp 174 flat_pointful_natural eval_core_pointful_natural eval eval_flat sctr_pointful_natural 175 eval_sctr_pointful); 176 177fun mk_corecUU_unique_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor ssig_map_comp 178 flat_pointful_natural eval_core_pointful_natural eval eval_flat corecU_unique 179 sctr_pointful_natural eval_sctr_pointful corecUU_def prem = 180 unfold_thms_tac ctxt [corecUU_def] THEN 181 HEADGOAL (rtac ctxt corecU_unique THEN' rtac ctxt sym THEN' subst_tac ctxt NONE [prem] THEN' 182 rtac ctxt ext THEN' 183 mk_corecUU_tail_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor ssig_map_comp 184 flat_pointful_natural eval_core_pointful_natural eval eval_flat sctr_pointful_natural 185 eval_sctr_pointful); 186 187fun mk_corecUU_Inl_tac ctxt inl_case' pre_map_comp dead_pre_map_ident dead_pre_map_comp0 ctor_dtor 188 ssig_maps ssig_map_id0 eval_core_simps eval_core_pointful_natural eval_VLeaf corecUU_pointfree 189 corecUU_unique = 190 HEADGOAL (rtac ctxt (infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt inl_case')] 191 (trans OF [corecUU_unique, corecUU_unique RS sym]) OF [ext, ext]) THEN' 192 subst_tac ctxt NONE [corecUU_pointfree] THEN' 193 asm_simp_tac (ss_only_silent (dead_pre_map_comp0 :: eval_core_pointful_natural :: ssig_maps @ 194 @{thms o_apply sum.case convol_apply id_apply map_prod_simp}) ctxt) THEN' 195 asm_simp_tac (ss_only_silent (dead_pre_map_ident :: ctor_dtor :: ssig_map_id0 :: 196 eval_core_pointful_natural :: eval_VLeaf :: unfold_thms ctxt [o_def] pre_map_comp :: 197 ssig_maps @ eval_core_simps @ @{thms o_apply prod.map_id convol_apply snd_conv id_apply}) 198 ctxt)); 199 200fun mk_dtor_algLam_tac ctxt pre_map_comp dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp 201 sig_map_comp Oper_pointful_natural ssig_maps dead_ssig_map_comp0 Lam_pointful_natural 202 eval_core_simps eval eval_flat eval_VLeaf algLam_def = 203 unfold_thms_tac ctxt [dead_ssig_map_comp0, o_assoc] THEN 204 HEADGOAL (asm_simp_tac (ss_only_silent (sig_map_comp :: Oper_pointful_natural :: eval :: 205 eval_flat :: algLam_def :: unfold_thms ctxt [o_def] dead_pre_map_comp :: eval_core_simps @ 206 @{thms o_apply id_apply id_def[symmetric]}) ctxt) THEN' 207 asm_simp_tac (ss_only_silent (Lam_pointful_natural :: eval_VLeaf :: 208 map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, sig_map_comp] @ ssig_maps @ 209 eval_core_simps @ 210 @{thms o_apply convol_apply snd_conv fst_conv id_apply map_prod_simp}) ctxt) THEN' 211 asm_simp_tac (ss_only_silent (dead_pre_map_id :: eval_VLeaf :: 212 unfold_thms ctxt [o_def] pre_map_comp :: 213 @{thms id_apply id_def[symmetric] convol_def}) ctxt)); 214 215fun mk_dtor_algrho_tac ctxt eval k_as_ssig_natural_pointful eval_core_k_as_ssig algrho_def = 216 HEADGOAL (asm_simp_tac (ss_only_silent [eval, k_as_ssig_natural_pointful, algrho_def, 217 eval_core_k_as_ssig RS sym, o_apply] ctxt)); 218 219fun mk_dtor_transfer_tac ctxt dtor_rel = 220 HEADGOAL (rtac ctxt refl ORELSE' 221 rtac ctxt @{thm rel_funI} THEN' rtac ctxt (dtor_rel RS iffD1) THEN' assume_tac ctxt); 222 223fun mk_equivp_Retr_tac ctxt dead_pre_rel_refl dead_pre_rel_flip dead_pre_rel_mono 224 dead_pre_rel_compp = 225 HEADGOAL (EVERY' [etac ctxt @{thm equivpE}, rtac ctxt @{thm equivpI}, 226 rtac ctxt @{thm reflpI}, rtac ctxt dead_pre_rel_refl, etac ctxt @{thm reflpD}, 227 SELECT_GOAL (unfold_thms_tac ctxt @{thms symp_iff}), 228 REPEAT_DETERM o rtac ctxt ext, rtac ctxt (dead_pre_rel_flip RS sym RS trans), 229 rtac ctxt ((@{thm conversep_iff} RS sym) RSN (2, trans)), 230 asm_simp_tac (ss_only_silent @{thms conversep_eq} ctxt), 231 SELECT_GOAL (unfold_thms_tac ctxt @{thms transp_relcompp}), 232 rtac ctxt @{thm predicate2I}, etac ctxt @{thm relcomppE}, 233 etac ctxt (dead_pre_rel_mono RS @{thm rev_predicate2D[rotated -1]}), 234 SELECT_GOAL (unfold_thms_tac ctxt 235 (unfold_thms ctxt [@{thm eq_OO}] dead_pre_rel_compp :: @{thms relcompp_apply})), 236 REPEAT_DETERM o resolve_tac ctxt [exI, conjI], assume_tac ctxt, assume_tac ctxt]); 237 238fun mk_eval_core_k_as_ssig_tac ctxt pre_map_comp dead_pre_map_id sig_map_comp ssig_maps 239 Lam_natural_pointful Lam_Inr flat_VLeaf eval_core_simps = 240 HEADGOAL (asm_simp_tac (ss_only_silent (dead_pre_map_id :: flat_VLeaf :: (Lam_Inr RS sym) :: 241 o_apply :: id_apply :: @{thm id_def[symmetric]} :: 242 unfold_thms ctxt @{thms map_prod_def split_def} Lam_natural_pointful :: ssig_maps @ 243 eval_core_simps @ map (unfold_thms ctxt [o_def]) [pre_map_comp, sig_map_comp]) ctxt)); 244 245fun mk_eval_embL_tac ctxt dead_pre_map_comp0 dtor_unfold_unique embL_pointful_natural eval_core_embL 246 old_eval eval = 247 HEADGOAL (rtac ctxt (unfold_thms ctxt [o_apply] 248 (trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym] OF [ext, ext]) 249 OF [asm_rl, old_eval RS sym])) THEN 250 unfold_thms_tac ctxt [dead_pre_map_comp0, embL_pointful_natural, eval_core_embL, eval, 251 o_apply] THEN 252 HEADGOAL (rtac ctxt refl); 253 254fun mk_eval_flat_tac ctxt dead_pre_map_comp0 ssig_map_id ssig_map_comp flat_pointful_natural 255 eval_core_pointful_natural eval_core_flat eval cond_eval_o_flat = 256 HEADGOAL (rtac ctxt (unfold_thms ctxt [o_apply] cond_eval_o_flat)) THEN 257 unfold_thms_tac ctxt [dead_pre_map_comp0, flat_pointful_natural, eval_core_flat, eval, 258 o_apply] THEN 259 HEADGOAL (rtac ctxt refl THEN' 260 asm_simp_tac (ss_only_silent (ssig_map_id :: eval_core_pointful_natural :: eval :: 261 map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, ssig_map_comp] @ 262 @{thms id_apply id_def[symmetric] fst_conv map_prod_simp convol_apply}) 263 ctxt)); 264 265fun instantiate_map_comp_with_f_g ctxt = 266 Rule_Insts.of_rule ctxt ([], [NONE, SOME ("%x. f (g x)")]) 267 [(Binding.name "f", NONE, NoSyn), (Binding.name "g", NONE, NoSyn)]; 268 269fun mk_eval_core_embL_tac ctxt old_ssig_induct dead_pre_map_comp0 dead_pre_map_comp 270 Sig_pointful_natural unsig_thm old_sig_map_comp old_sig_map_cong old_Lam_pointful_natural 271 Lam_def flat_embL old_eval_core_simps eval_core_simps embL_simps embL_pointful_natural = 272 HEADGOAL (rtac ctxt old_ssig_induct) THEN 273 ALLGOALS (asm_simp_tac (ss_only_silent (Sig_pointful_natural :: unsig_thm :: Lam_def :: 274 (flat_embL RS sym) :: unfold_thms ctxt [o_def] dead_pre_map_comp :: embL_simps @ 275 old_eval_core_simps @ eval_core_simps @ 276 @{thms id_apply id_def[symmetric] o_apply map_sum.simps sum.case}) ctxt)) THEN 277 HEADGOAL (asm_simp_tac (Simplifier.add_cong old_sig_map_cong (ss_only_silent 278 (old_Lam_pointful_natural :: embL_pointful_natural :: 279 map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, instantiate_map_comp_with_f_g ctxt 280 dead_pre_map_comp0, old_sig_map_comp] @ @{thms map_prod_simp}) ctxt))); 281 282fun mk_eval_core_flat_tac ctxt ssig_induct dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp 283 fp_map_id sig_map_comp sig_map_cong ssig_maps ssig_map_comp flat_simps flat_natural flat_flat 284 Lam_natural_sym eval_core_simps = 285 HEADGOAL (rtac ctxt ssig_induct) THEN 286 ALLGOALS (full_simp_tac (ss_only_silent ((flat_flat RS sym) :: dead_pre_map_id :: 287 dead_pre_map_comp :: fp_map_id :: sig_map_comp :: ssig_map_comp :: ssig_maps @ flat_simps @ 288 eval_core_simps @ @{thms o_def id_def[symmetric] convol_apply id_apply snd_conv}) ctxt)) THEN 289 HEADGOAL (asm_simp_tac (Simplifier.add_cong sig_map_cong (ss_only_silent 290 (map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, sig_map_comp] @ 291 flat_natural :: Lam_natural_sym :: @{thms id_apply fst_conv map_prod_simp}) 292 ctxt))); 293 294fun mk_eval_sctr_tac ctxt proto_sctr_pointful_natural eval_Oper algLam sctr_def = 295 HEADGOAL (rtac ctxt ext) THEN 296 unfold_thms_tac ctxt [proto_sctr_pointful_natural, eval_Oper, algLam RS sym, sctr_def, 297 o_apply] THEN 298 HEADGOAL (rtac ctxt refl); 299 300fun mk_eval_V_or_CLeaf_tac ctxt dead_pre_map_id dead_pre_map_comp fp_map_id dtor_unfold_unique 301 V_or_CLeaf_map eval_core_simps eval = 302 HEADGOAL (rtac ctxt (trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym] RS fun_cong 303 OF [ext, ext])) THEN 304 ALLGOALS (asm_simp_tac (ss_only_silent (dead_pre_map_id :: fp_map_id :: 305 unfold_thms ctxt @{thms o_def} dead_pre_map_comp :: V_or_CLeaf_map :: eval :: eval_core_simps @ 306 @{thms o_apply id_def[symmetric] id_apply snd_conv convol_apply}) ctxt)); 307 308fun mk_eval_Oper_tac ctxt live sig_map_ident sig_map_comp0 sig_map_comp Oper_natural_pointful 309 VLeaf_natural flat_simps eval_flat algLam_def = 310 let val VLeaf_natural' = instantiate_natural_rule_with_id ctxt live VLeaf_natural in 311 unfold_thms_tac ctxt [sig_map_comp, VLeaf_natural', algLam_def, o_apply] THEN 312 unfold_thms_tac ctxt (sig_map_comp0 :: Oper_natural_pointful :: (eval_flat RS sym) :: o_apply :: 313 flat_simps) THEN 314 unfold_thms_tac ctxt (@{thm id_apply} :: sig_map_ident :: unfold_thms ctxt [o_def] sig_map_comp :: 315 flat_simps) THEN 316 HEADGOAL (rtac ctxt refl) 317 end; 318 319fun mk_extdd_mor_tac ctxt dead_pre_map_comp0 dead_pre_map_comp VLeaf_map ssig_map_comp 320 flat_pointful_natural eval_core_pointful_natural eval eval_flat eval_VLeaf cutSsig_def prem = 321 HEADGOAL (rtac ctxt ext) THEN 322 unfold_thms_tac ctxt (ssig_map_comp :: unfold_thms ctxt [o_def] dead_pre_map_comp :: 323 flat_pointful_natural :: eval :: eval_flat :: cutSsig_def :: 324 @{thms o_apply convol_o id_o id_apply id_def[symmetric]}) THEN 325 unfold_thms_tac ctxt (unfold_thms ctxt [dead_pre_map_comp0] prem :: dead_pre_map_comp0 :: 326 ssig_map_comp :: eval_core_pointful_natural :: 327 @{thms o_def[symmetric] o_apply map_prod_o_convol}) THEN 328 unfold_thms_tac ctxt (VLeaf_map :: eval_VLeaf :: @{thms o_def id_apply id_def[symmetric]}) THEN 329 HEADGOAL (rtac ctxt refl); 330 331fun mk_extdd_o_VLeaf_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_inject ssig_maps 332 eval_core_simps eval eval_VLeaf prem = 333 HEADGOAL (rtac ctxt ext THEN' rtac ctxt (dtor_inject RS iffD1) THEN' 334 asm_simp_tac (ss_only_silent (dead_pre_map_comp0 :: ssig_maps @ eval_core_simps @ eval :: 335 eval_VLeaf :: (mk_pointful ctxt prem RS sym) :: unfold_thms ctxt [o_def] dead_pre_map_comp :: 336 @{thms o_apply convol_apply snd_conv id_apply}) ctxt)); 337 338fun mk_flat_embL_tac ctxt old_ssig_induct fp_map_id Sig_pointful_natural old_sig_map_comp 339 old_sig_map_cong old_ssig_maps old_flat_simps flat_simps embL_simps = 340 HEADGOAL (rtac ctxt old_ssig_induct) THEN 341 ALLGOALS (asm_simp_tac (Simplifier.add_cong old_sig_map_cong (ss_only_silent 342 (fp_map_id :: Sig_pointful_natural :: unfold_thms ctxt [o_def] old_sig_map_comp :: 343 old_ssig_maps @ old_flat_simps @ flat_simps @ embL_simps @ 344 @{thms id_apply id_def[symmetric] map_sum.simps}) ctxt))); 345 346fun mk_flat_VLeaf_or_flat_tac ctxt ssig_induct cong simps = 347 HEADGOAL (rtac ctxt ssig_induct) THEN 348 ALLGOALS (asm_simp_tac (Simplifier.add_cong cong (ss_only_silent simps ctxt))); 349 350fun mk_Lam_Inl_Inr_tac ctxt unsig Lam_def = 351 TRYALL Goal.conjunction_tac THEN ALLGOALS (rtac ctxt ext) THEN 352 unfold_thms_tac ctxt (o_apply :: Lam_def :: unsig :: @{thms sum.case}) THEN 353 ALLGOALS (rtac ctxt refl); 354 355fun mk_mor_cutSsig_flat_tac ctxt eval_core_o_map dead_pre_map_comp0 dead_pre_map_comp 356 dead_pre_map_cong dtor_unfold_unique dead_ssig_map_comp0 ssig_map_comp flat_simps 357 flat_pointful_natural eval_core_pointful_natural flat_flat flat_VLeaf eval_core_flat cutSsig_def 358 cutSsig_def_pointful_natural eval_thm prem = 359 HEADGOAL (rtac ctxt (infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt eval_core_o_map)] 360 (trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym]) OF [ext, ext]) THEN' 361 asm_simp_tac (ss_only_silent ((prem RS sym) :: dead_pre_map_comp0 :: ssig_map_comp :: 362 eval_core_pointful_natural :: eval_thm :: 363 @{thms o_apply map_prod_o_convol o_id convol_o id_o}) ctxt) THEN' 364 asm_simp_tac (ss_only_silent ((mk_pointful ctxt prem RS sym) :: dead_pre_map_comp0 :: 365 cutSsig_def_pointful_natural :: flat_simps @ 366 @{thms o_apply convol_apply map_prod_simp id_apply}) ctxt) THEN' 367 rtac ctxt (dead_pre_map_cong OF [asm_rl, refl]) THEN' 368 asm_simp_tac (ss_only_silent (ssig_map_comp :: cutSsig_def :: flat_pointful_natural :: 369 eval_core_flat :: unfold_thms ctxt [o_def] dead_pre_map_comp :: (dead_ssig_map_comp0 RS sym) :: 370 (flat_flat RS sym) :: 371 @{thms o_apply convol_o fst_convol id_apply id_def[symmetric]}) ctxt) THEN' 372 asm_simp_tac (ss_only_silent (eval_core_pointful_natural :: flat_VLeaf :: 373 map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, ssig_map_comp] @ 374 @{thms o_apply id_apply id_def[symmetric] map_prod_simp convol_def}) ctxt)); 375 376fun mk_natural_from_transfer_tac ctxt m alives transfer map_ids rel_Grps subst_rel_Grps = 377 let 378 val unfold_eq = unfold_thms ctxt @{thms Grp_UNIV_id[symmetric]}; 379 val (rel_Grps', subst_rel_Grps') = 380 apply2 (map (fn thm => unfold_eq (thm RS eq_reflection))) (rel_Grps, subst_rel_Grps); 381 val transfer' = instantiate_transfer_rule_with_Grp_UNIV ctxt alives (unfold_eq transfer) 382 |> unfold_thms ctxt rel_Grps'; 383 in 384 HEADGOAL (Method.insert_tac ctxt [transfer'] THEN' 385 EVERY' (map (subst_asm_tac ctxt NONE o single) subst_rel_Grps')) THEN 386 unfold_thms_tac ctxt (map_ids @ @{thms Grp_def rel_fun_def}) THEN 387 HEADGOAL (REPEAT_DETERM_N m o rtac ctxt ext THEN' 388 asm_full_simp_tac (ss_only_silent @{thms simp_thms id_apply o_apply mem_Collect_eq 389 top_greatest UNIV_I subset_UNIV[simplified UNIV_def]} ctxt)) THEN 390 ALLGOALS (REPEAT_DETERM o etac ctxt @{thm meta_allE} THEN' REPEAT_DETERM o etac ctxt allE THEN' 391 forward_tac ctxt [sym] THEN' assume_tac ctxt) 392 end; 393 394fun mk_natural_by_unfolding_tac ctxt maps = 395 HEADGOAL (rtac ctxt ext) THEN 396 unfold_thms_tac ctxt (@{thms o_def[abs_def] id_apply id_def[symmetric]} @ maps) THEN 397 HEADGOAL (rtac ctxt refl); 398 399fun mk_Retr_coinduct_tac ctxt dtor_rel_coinduct rel_eq = 400 HEADGOAL (EVERY' [rtac ctxt allI, rtac ctxt impI, 401 rtac ctxt (@{thm ord_le_eq_trans} OF [dtor_rel_coinduct, rel_eq]), 402 etac ctxt @{thm predicate2D}, assume_tac ctxt]); 403 404fun mk_sig_transfer_tac ctxt pre_rel_def rel_eqs0 transfer = 405 let 406 val rel_eqs = no_refl rel_eqs0; 407 val rel_eq_syms = map (fn thm => thm RS sym) rel_eqs; 408 val transfer' = unfold_thms ctxt rel_eq_syms transfer 409 in 410 HEADGOAL (rtac ctxt transfer') ORELSE 411 unfold_thms_tac ctxt (pre_rel_def :: rel_eq_syms @ 412 @{thms BNF_Def.vimage2p_def BNF_Composition.id_bnf_def}) THEN 413 HEADGOAL (rtac ctxt transfer') 414 end; 415 416fun mk_transfer_by_transfer_prover_tac ctxt defs rel_eqs0 transfers = 417 let 418 val rel_eqs = no_refl rel_eqs0; 419 val rel_eq_syms = map (fn thm => thm RS sym) rel_eqs; 420 in 421 unfold_thms_tac ctxt (defs @ rel_eq_syms) THEN 422 HEADGOAL (transfer_prover_add_tac ctxt rel_eqs transfers) 423 end; 424 425end; 426