File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML›
signature BNF_GFP_GREC_TACTICS =
sig
val transfer_prover_eq_tac: Proof.context -> int -> tactic
val transfer_prover_add_tac: Proof.context -> thm list -> thm list -> int -> tactic
val mk_algLam_algLam_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
tactic
val mk_algLam_algrho_tac: Proof.context -> thm -> thm -> tactic
val mk_algLam_base_tac: Proof.context -> term -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
thm list -> thm -> thm list -> thm list -> thm -> thm -> tactic
val mk_algLam_step_tac: Proof.context -> thm -> thm -> thm -> tactic
val mk_cong_locale_tac: Proof.context -> thm -> thm list -> thm -> thm -> thm list -> thm ->
thm -> tactic
val mk_corecU_pointfree_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm list -> thm ->
thm list -> thm -> thm -> thm -> tactic
val mk_corecUU_pointfree_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
thm -> thm -> thm -> thm -> thm -> thm -> tactic
val mk_corecUU_unique_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
thm -> thm -> thm -> thm -> thm -> thm -> tactic
val mk_corecUU_Inl_tac: Proof.context -> term -> thm -> thm -> thm -> thm -> thm list -> thm ->
thm list -> thm -> thm -> thm -> thm -> tactic
val mk_dtor_algLam_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
thm -> thm -> thm list -> thm -> thm -> thm -> thm -> tactic
val mk_dtor_algrho_tac: Proof.context -> thm -> thm -> thm -> thm -> tactic
val mk_dtor_transfer_tac: Proof.context -> thm -> tactic
val mk_equivp_Retr_tac: Proof.context -> thm -> thm -> thm -> thm -> tactic
val mk_eval_core_embL_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
thm -> thm -> thm -> thm list -> thm list -> thm list -> thm -> tactic
val mk_eval_core_flat_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
thm list -> thm -> thm list -> thm -> thm -> thm -> thm list -> tactic
val mk_eval_core_k_as_ssig_tac: Proof.context -> thm -> thm -> thm -> thm list -> thm -> thm ->
thm -> thm list -> tactic
val mk_eval_embL_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> tactic
val mk_eval_flat_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
tactic
val mk_eval_sctr_tac: Proof.context -> thm -> thm -> thm -> thm -> tactic
val mk_eval_Oper_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> thm -> thm list ->
thm -> thm -> tactic
val mk_eval_V_or_CLeaf_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm list -> thm ->
tactic
val mk_extdd_mor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
thm -> thm -> thm -> tactic
val mk_extdd_o_VLeaf_tac: Proof.context -> thm -> thm -> thm -> thm list -> thm list -> thm ->
thm -> thm -> tactic
val mk_flat_embL_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list ->
thm list -> thm list -> tactic
val mk_flat_VLeaf_or_flat_tac: Proof.context -> thm -> thm -> thm list -> tactic
val mk_Lam_Inl_Inr_tac: Proof.context -> thm -> thm -> tactic
val mk_mor_cutSsig_flat_tac: Proof.context -> term -> thm -> thm -> thm -> thm -> thm -> thm ->
thm list -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> tactic
val mk_natural_from_transfer_tac: Proof.context -> int -> bool list -> thm -> thm list ->
thm list -> thm list -> tactic
val mk_natural_by_unfolding_tac: Proof.context -> thm list -> tactic
val mk_Retr_coinduct_tac: Proof.context -> thm -> thm -> tactic
val mk_sig_transfer_tac: Proof.context -> thm -> thm list -> thm -> tactic
val mk_transfer_by_transfer_prover_tac: Proof.context -> thm list -> thm list -> thm list ->
tactic
end;
structure BNF_GFP_Grec_Tactics : BNF_GFP_GREC_TACTICS =
struct
open BNF_Util
open BNF_Tactics
open BNF_FP_Util
val o_assoc = @{thm o_assoc};
val o_def = @{thm o_def};
fun ss_only_silent thms ctxt =
ss_only thms (ctxt |> Context_Position.set_visible false);
fun context_relator_eq_add rel_eqs ctxt =
fold (snd oo Thm.proof_attributes (map (Attrib.attribute ctxt) @{attributes [relator_eq]}))
rel_eqs ctxt;
val context_transfer_rule_add = fold (snd oo Thm.proof_attributes [Transfer.transfer_add]);
fun transfer_prover_eq_tac ctxt =
SELECT_GOAL (Local_Defs.fold_tac ctxt (Transfer.get_relator_eq ctxt)) THEN'
Transfer.transfer_prover_tac ctxt;
fun transfer_prover_add_tac ctxt rel_eqs transfers =
transfer_prover_eq_tac (ctxt
|> context_relator_eq_add rel_eqs
|> context_transfer_rule_add transfers);
fun instantiate_natural_rule_with_id ctxt live =
Rule_Insts.of_rule ctxt ([], NONE :: replicate live (SOME \<^const_name>‹id›)) [];
fun instantiate_transfer_rule_with_Grp_UNIV ctxt alives thm =
let
val n = length alives;
val fs = map (prefix "f" o string_of_int) (1 upto n);
val ss = map2 (fn live => fn f => SOME (\<^const_name>‹BNF_Def.Grp› ^ " " ^ \<^const_name>‹top› ^
" " ^ (if live then f else \<^const_name>‹id›))) alives fs;
val bs = map_filter (fn (live, f) => if live then SOME (Binding.name f, NONE, NoSyn) else NONE)
(alives ~~ fs);
in
Rule_Insts.of_rule ctxt ([], ss) bs thm
end;
fun mk_algLam_algLam_tac ctxt dead_pre_map_comp dtor_inject unsig sig_map Lam_def eval_embL
old_dtor_algLam dtor_algLam =
HEADGOAL (rtac ctxt ext THEN' rtac ctxt (dtor_inject RS iffD1)) THEN
unfold_thms_tac ctxt (dead_pre_map_comp :: unsig :: sig_map :: Lam_def :: eval_embL ::
old_dtor_algLam :: dtor_algLam :: @{thms o_apply id_o map_sum.simps sum.case}) THEN
HEADGOAL (rtac ctxt refl);
fun mk_algLam_algrho_tac ctxt algLam_def algrho_def =
HEADGOAL (rtac ctxt ext) THEN unfold_thms_tac ctxt [algLam_def, algrho_def, o_apply] THEN
HEADGOAL (rtac ctxt refl);
fun mk_algLam_base_tac ctxt dead_pre_map_dtor dead_pre_map_id dead_pre_map_comp ctor_dtor dtor_ctor
dtor_unfold_unique unsig Sig_pointful_natural ssig_maps Lam_def flat_simps eval_core_simps eval
algLam_def =
HEADGOAL (rtac ctxt (infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt dead_pre_map_dtor)]
(trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym]) OF [ext, ext])) THEN
ALLGOALS (asm_simp_tac (ss_only_silent (dead_pre_map_id :: ctor_dtor :: dtor_ctor :: unsig ::
Sig_pointful_natural :: Lam_def :: eval :: algLam_def ::
unfold_thms ctxt [o_def] dead_pre_map_comp :: ssig_maps @ flat_simps @ eval_core_simps @
@{thms o_apply id_apply id_def[symmetric] snd_conv convol_apply}) ctxt));
fun mk_algLam_step_tac ctxt proto_sctr_def old_algLam_pointful algLam_algLam_pointful =
HEADGOAL (rtac ctxt ext) THEN
unfold_thms_tac ctxt [proto_sctr_def, old_algLam_pointful, algLam_algLam_pointful, o_apply] THEN
HEADGOAL (rtac ctxt refl);
fun mk_cong_locale_tac ctxt dead_pre_rel_mono dead_pre_rel_maps equivp_Retr
ssig_rel_mono ssig_rel_maps eval eval_core_transfer =
HEADGOAL (resolve_tac ctxt (Locale.get_unfolds \<^context>) THEN'
etac ctxt ssig_rel_mono THEN' etac ctxt equivp_Retr) THEN
unfold_thms_tac ctxt (eval :: dead_pre_rel_maps @ @{thms id_apply}) THEN
HEADGOAL (rtac ctxt (@{thm predicate2I} RS (dead_pre_rel_mono RS @{thm predicate2D})) THEN'
etac ctxt @{thm rel_funD} THEN' assume_tac ctxt THEN'
rtac ctxt (eval_core_transfer RS @{thm rel_funD})) THEN
unfold_thms_tac ctxt (ssig_rel_maps @ @{thms vimage2p_rel_prod vimage2p_id}) THEN
unfold_thms_tac ctxt @{thms vimage2p_def} THEN HEADGOAL (assume_tac ctxt);
fun mk_corecU_pointfree_tac ctxt dead_pre_map_comp dtor_unfold ssig_maps dead_ssig_map_comp0
flat_simps flat_VLeaf eval_core_simps cutSsig_def mor_cutSsig_flat corecU_def =
unfold_thms_tac ctxt [corecU_def, dead_ssig_map_comp0, o_assoc] THEN
HEADGOAL (subst_tac ctxt NONE [ext RS mor_cutSsig_flat] THEN'
asm_simp_tac (ss_only_silent [dtor_unfold, o_apply] ctxt) THEN'
asm_simp_tac (ss_only_silent (dtor_unfold :: flat_VLeaf :: cutSsig_def :: ssig_maps @
flat_simps @ eval_core_simps @ unfold_thms ctxt [o_def] dead_pre_map_comp ::
@{thms o_def id_apply id_def[symmetric] snd_conv convol_apply}) ctxt));
fun mk_corecUU_tail_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor ssig_map_comp
flat_pointful_natural eval_core_pointful_natural eval eval_flat sctr_pointful_natural
eval_sctr_pointful =
asm_simp_tac (ss_only_silent (dtor_ctor :: flat_pointful_natural :: eval :: eval_flat ::
map (unfold_thms ctxt [o_def]) [dead_pre_map_comp, ssig_map_comp] @
@{thms o_apply id_apply id_def[symmetric] convol_apply}) ctxt) THEN'
asm_simp_tac (ss_only_silent (eval_core_pointful_natural :: sctr_pointful_natural ::
eval_sctr_pointful :: map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, ssig_map_comp] @
@{thms id_apply id_def[symmetric] convol_apply map_prod_simp}) ctxt);
fun mk_corecUU_pointfree_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor dtor_inject
ssig_map_comp flat_pointful_natural eval_core_pointful_natural eval eval_flat corecU_ctor
sctr_pointful_natural eval_sctr_pointful corecUU_def =
unfold_thms_tac ctxt [corecUU_def] THEN
HEADGOAL (rtac ctxt ext THEN' subst_tac ctxt NONE [corecU_ctor RS sym]) THEN
unfold_thms_tac ctxt [corecUU_def RS symmetric_thm] THEN
HEADGOAL (rtac ctxt (dtor_inject RS iffD1) THEN'
mk_corecUU_tail_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor ssig_map_comp
flat_pointful_natural eval_core_pointful_natural eval eval_flat sctr_pointful_natural
eval_sctr_pointful);
fun mk_corecUU_unique_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor ssig_map_comp
flat_pointful_natural eval_core_pointful_natural eval eval_flat corecU_unique
sctr_pointful_natural eval_sctr_pointful corecUU_def prem =
unfold_thms_tac ctxt [corecUU_def] THEN
HEADGOAL (rtac ctxt corecU_unique THEN' rtac ctxt sym THEN' subst_tac ctxt NONE [prem] THEN'
rtac ctxt ext THEN'
mk_corecUU_tail_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor ssig_map_comp
flat_pointful_natural eval_core_pointful_natural eval eval_flat sctr_pointful_natural
eval_sctr_pointful);
fun mk_corecUU_Inl_tac ctxt inl_case' pre_map_comp dead_pre_map_ident dead_pre_map_comp0 ctor_dtor
ssig_maps ssig_map_id0 eval_core_simps eval_core_pointful_natural eval_VLeaf corecUU_pointfree
corecUU_unique =
HEADGOAL (rtac ctxt (infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt inl_case')]
(trans OF [corecUU_unique, corecUU_unique RS sym]) OF [ext, ext]) THEN'
subst_tac ctxt NONE [corecUU_pointfree] THEN'
asm_simp_tac (ss_only_silent (dead_pre_map_comp0 :: eval_core_pointful_natural :: ssig_maps @
@{thms o_apply sum.case convol_apply id_apply map_prod_simp}) ctxt) THEN'
asm_simp_tac (ss_only_silent (dead_pre_map_ident :: ctor_dtor :: ssig_map_id0 ::
eval_core_pointful_natural :: eval_VLeaf :: unfold_thms ctxt [o_def] pre_map_comp ::
ssig_maps @ eval_core_simps @ @{thms o_apply prod.map_id convol_apply snd_conv id_apply})
ctxt));
fun mk_dtor_algLam_tac ctxt pre_map_comp dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp
sig_map_comp Oper_pointful_natural ssig_maps dead_ssig_map_comp0 Lam_pointful_natural
eval_core_simps eval eval_flat eval_VLeaf algLam_def =
unfold_thms_tac ctxt [dead_ssig_map_comp0, o_assoc] THEN
HEADGOAL (asm_simp_tac (ss_only_silent (sig_map_comp :: Oper_pointful_natural :: eval ::
eval_flat :: algLam_def :: unfold_thms ctxt [o_def] dead_pre_map_comp :: eval_core_simps @
@{thms o_apply id_apply id_def[symmetric]}) ctxt) THEN'
asm_simp_tac (ss_only_silent (Lam_pointful_natural :: eval_VLeaf ::
map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, sig_map_comp] @ ssig_maps @
eval_core_simps @
@{thms o_apply convol_apply snd_conv fst_conv id_apply map_prod_simp}) ctxt) THEN'
asm_simp_tac (ss_only_silent (dead_pre_map_id :: eval_VLeaf ::
unfold_thms ctxt [o_def] pre_map_comp ::
@{thms id_apply id_def[symmetric] convol_def}) ctxt));
fun mk_dtor_algrho_tac ctxt eval k_as_ssig_natural_pointful eval_core_k_as_ssig algrho_def =
HEADGOAL (asm_simp_tac (ss_only_silent [eval, k_as_ssig_natural_pointful, algrho_def,
eval_core_k_as_ssig RS sym, o_apply] ctxt));
fun mk_dtor_transfer_tac ctxt dtor_rel =
HEADGOAL (rtac ctxt refl ORELSE'
rtac ctxt @{thm rel_funI} THEN' rtac ctxt (dtor_rel RS iffD1) THEN' assume_tac ctxt);
fun mk_equivp_Retr_tac ctxt dead_pre_rel_refl dead_pre_rel_flip dead_pre_rel_mono
dead_pre_rel_compp =
HEADGOAL (EVERY' [etac ctxt @{thm equivpE}, rtac ctxt @{thm equivpI},
rtac ctxt @{thm reflpI}, rtac ctxt dead_pre_rel_refl, etac ctxt @{thm reflpD},
SELECT_GOAL (unfold_thms_tac ctxt @{thms symp_iff}),
REPEAT_DETERM o rtac ctxt ext, rtac ctxt (dead_pre_rel_flip RS sym RS trans),
rtac ctxt ((@{thm conversep_iff} RS sym) RSN (2, trans)),
asm_simp_tac (ss_only_silent @{thms conversep_eq} ctxt),
SELECT_GOAL (unfold_thms_tac ctxt @{thms transp_relcompp}),
rtac ctxt @{thm predicate2I}, etac ctxt @{thm relcomppE},
etac ctxt (dead_pre_rel_mono RS @{thm rev_predicate2D[rotated -1]}),
SELECT_GOAL (unfold_thms_tac ctxt
(unfold_thms ctxt [@{thm eq_OO}] dead_pre_rel_compp :: @{thms relcompp_apply})),
REPEAT_DETERM o resolve_tac ctxt [exI, conjI], assume_tac ctxt, assume_tac ctxt]);
fun mk_eval_core_k_as_ssig_tac ctxt pre_map_comp dead_pre_map_id sig_map_comp ssig_maps
Lam_natural_pointful Lam_Inr flat_VLeaf eval_core_simps =
HEADGOAL (asm_simp_tac (ss_only_silent (dead_pre_map_id :: flat_VLeaf :: (Lam_Inr RS sym) ::
o_apply :: id_apply :: @{thm id_def[symmetric]} ::
unfold_thms ctxt @{thms map_prod_def split_def} Lam_natural_pointful :: ssig_maps @
eval_core_simps @ map (unfold_thms ctxt [o_def]) [pre_map_comp, sig_map_comp]) ctxt));
fun mk_eval_embL_tac ctxt dead_pre_map_comp0 dtor_unfold_unique embL_pointful_natural eval_core_embL
old_eval eval =
HEADGOAL (rtac ctxt (unfold_thms ctxt [o_apply]
(trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym] OF [ext, ext])
OF [asm_rl, old_eval RS sym])) THEN
unfold_thms_tac ctxt [dead_pre_map_comp0, embL_pointful_natural, eval_core_embL, eval,
o_apply] THEN
HEADGOAL (rtac ctxt refl);
fun mk_eval_flat_tac ctxt dead_pre_map_comp0 ssig_map_id ssig_map_comp flat_pointful_natural
eval_core_pointful_natural eval_core_flat eval cond_eval_o_flat =
HEADGOAL (rtac ctxt (unfold_thms ctxt [o_apply] cond_eval_o_flat)) THEN
unfold_thms_tac ctxt [dead_pre_map_comp0, flat_pointful_natural, eval_core_flat, eval,
o_apply] THEN
HEADGOAL (rtac ctxt refl THEN'
asm_simp_tac (ss_only_silent (ssig_map_id :: eval_core_pointful_natural :: eval ::
map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, ssig_map_comp] @
@{thms id_apply id_def[symmetric] fst_conv map_prod_simp convol_apply})
ctxt));
fun instantiate_map_comp_with_f_g ctxt =
Rule_Insts.of_rule ctxt ([], [NONE, SOME ("%x. f (g x)")])
[(Binding.name "f", NONE, NoSyn), (Binding.name "g", NONE, NoSyn)];
fun mk_eval_core_embL_tac ctxt old_ssig_induct dead_pre_map_comp0 dead_pre_map_comp
Sig_pointful_natural unsig_thm old_sig_map_comp old_sig_map_cong old_Lam_pointful_natural
Lam_def flat_embL old_eval_core_simps eval_core_simps embL_simps embL_pointful_natural =
HEADGOAL (rtac ctxt old_ssig_induct) THEN
ALLGOALS (asm_simp_tac (ss_only_silent (Sig_pointful_natural :: unsig_thm :: Lam_def ::
(flat_embL RS sym) :: unfold_thms ctxt [o_def] dead_pre_map_comp :: embL_simps @
old_eval_core_simps @ eval_core_simps @
@{thms id_apply id_def[symmetric] o_apply map_sum.simps sum.case}) ctxt)) THEN
HEADGOAL (asm_simp_tac (Simplifier.add_cong old_sig_map_cong (ss_only_silent
(old_Lam_pointful_natural :: embL_pointful_natural ::
map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, instantiate_map_comp_with_f_g ctxt
dead_pre_map_comp0, old_sig_map_comp] @ @{thms map_prod_simp}) ctxt)));
fun mk_eval_core_flat_tac ctxt ssig_induct dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp
fp_map_id sig_map_comp sig_map_cong ssig_maps ssig_map_comp flat_simps flat_natural flat_flat
Lam_natural_sym eval_core_simps =
HEADGOAL (rtac ctxt ssig_induct) THEN
ALLGOALS (full_simp_tac (ss_only_silent ((flat_flat RS sym) :: dead_pre_map_id ::
dead_pre_map_comp :: fp_map_id :: sig_map_comp :: ssig_map_comp :: ssig_maps @ flat_simps @
eval_core_simps @ @{thms o_def id_def[symmetric] convol_apply id_apply snd_conv}) ctxt)) THEN
HEADGOAL (asm_simp_tac (Simplifier.add_cong sig_map_cong (ss_only_silent
(map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, sig_map_comp] @
flat_natural :: Lam_natural_sym :: @{thms id_apply fst_conv map_prod_simp})
ctxt)));
fun mk_eval_sctr_tac ctxt proto_sctr_pointful_natural eval_Oper algLam sctr_def =
HEADGOAL (rtac ctxt ext) THEN
unfold_thms_tac ctxt [proto_sctr_pointful_natural, eval_Oper, algLam RS sym, sctr_def,
o_apply] THEN
HEADGOAL (rtac ctxt refl);
fun mk_eval_V_or_CLeaf_tac ctxt dead_pre_map_id dead_pre_map_comp fp_map_id dtor_unfold_unique
V_or_CLeaf_map eval_core_simps eval =
HEADGOAL (rtac ctxt (trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym] RS fun_cong
OF [ext, ext])) THEN
ALLGOALS (asm_simp_tac (ss_only_silent (dead_pre_map_id :: fp_map_id ::
unfold_thms ctxt @{thms o_def} dead_pre_map_comp :: V_or_CLeaf_map :: eval :: eval_core_simps @
@{thms o_apply id_def[symmetric] id_apply snd_conv convol_apply}) ctxt));
fun mk_eval_Oper_tac ctxt live sig_map_ident sig_map_comp0 sig_map_comp Oper_natural_pointful
VLeaf_natural flat_simps eval_flat algLam_def =
let val VLeaf_natural' = instantiate_natural_rule_with_id ctxt live VLeaf_natural in
unfold_thms_tac ctxt [sig_map_comp, VLeaf_natural', algLam_def, o_apply] THEN
unfold_thms_tac ctxt (sig_map_comp0 :: Oper_natural_pointful :: (eval_flat RS sym) :: o_apply ::
flat_simps) THEN
unfold_thms_tac ctxt (@{thm id_apply} :: sig_map_ident :: unfold_thms ctxt [o_def] sig_map_comp ::
flat_simps) THEN
HEADGOAL (rtac ctxt refl)
end;
fun mk_extdd_mor_tac ctxt dead_pre_map_comp0 dead_pre_map_comp VLeaf_map ssig_map_comp
flat_pointful_natural eval_core_pointful_natural eval eval_flat eval_VLeaf cutSsig_def prem =
HEADGOAL (rtac ctxt ext) THEN
unfold_thms_tac ctxt (ssig_map_comp :: unfold_thms ctxt [o_def] dead_pre_map_comp ::
flat_pointful_natural :: eval :: eval_flat :: cutSsig_def ::
@{thms o_apply convol_o id_o id_apply id_def[symmetric]}) THEN
unfold_thms_tac ctxt (unfold_thms ctxt [dead_pre_map_comp0] prem :: dead_pre_map_comp0 ::
ssig_map_comp :: eval_core_pointful_natural ::
@{thms o_def[symmetric] o_apply map_prod_o_convol}) THEN
unfold_thms_tac ctxt (VLeaf_map :: eval_VLeaf :: @{thms o_def id_apply id_def[symmetric]}) THEN
HEADGOAL (rtac ctxt refl);
fun mk_extdd_o_VLeaf_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_inject ssig_maps
eval_core_simps eval eval_VLeaf prem =
HEADGOAL (rtac ctxt ext THEN' rtac ctxt (dtor_inject RS iffD1) THEN'
asm_simp_tac (ss_only_silent (dead_pre_map_comp0 :: ssig_maps @ eval_core_simps @ eval ::
eval_VLeaf :: (mk_pointful ctxt prem RS sym) :: unfold_thms ctxt [o_def] dead_pre_map_comp ::
@{thms o_apply convol_apply snd_conv id_apply}) ctxt));
fun mk_flat_embL_tac ctxt old_ssig_induct fp_map_id Sig_pointful_natural old_sig_map_comp
old_sig_map_cong old_ssig_maps old_flat_simps flat_simps embL_simps =
HEADGOAL (rtac ctxt old_ssig_induct) THEN
ALLGOALS (asm_simp_tac (Simplifier.add_cong old_sig_map_cong (ss_only_silent
(fp_map_id :: Sig_pointful_natural :: unfold_thms ctxt [o_def] old_sig_map_comp ::
old_ssig_maps @ old_flat_simps @ flat_simps @ embL_simps @
@{thms id_apply id_def[symmetric] map_sum.simps}) ctxt)));
fun mk_flat_VLeaf_or_flat_tac ctxt ssig_induct cong simps =
HEADGOAL (rtac ctxt ssig_induct) THEN
ALLGOALS (asm_simp_tac (Simplifier.add_cong cong (ss_only_silent simps ctxt)));
fun mk_Lam_Inl_Inr_tac ctxt unsig Lam_def =
TRYALL Goal.conjunction_tac THEN ALLGOALS (rtac ctxt ext) THEN
unfold_thms_tac ctxt (o_apply :: Lam_def :: unsig :: @{thms sum.case}) THEN
ALLGOALS (rtac ctxt refl);
fun mk_mor_cutSsig_flat_tac ctxt eval_core_o_map dead_pre_map_comp0 dead_pre_map_comp
dead_pre_map_cong dtor_unfold_unique dead_ssig_map_comp0 ssig_map_comp flat_simps
flat_pointful_natural eval_core_pointful_natural flat_flat flat_VLeaf eval_core_flat cutSsig_def
cutSsig_def_pointful_natural eval_thm prem =
HEADGOAL (rtac ctxt (infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt eval_core_o_map)]
(trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym]) OF [ext, ext]) THEN'
asm_simp_tac (ss_only_silent ((prem RS sym) :: dead_pre_map_comp0 :: ssig_map_comp ::
eval_core_pointful_natural :: eval_thm ::
@{thms o_apply map_prod_o_convol o_id convol_o id_o}) ctxt) THEN'
asm_simp_tac (ss_only_silent ((mk_pointful ctxt prem RS sym) :: dead_pre_map_comp0 ::
cutSsig_def_pointful_natural :: flat_simps @
@{thms o_apply convol_apply map_prod_simp id_apply}) ctxt) THEN'
rtac ctxt (dead_pre_map_cong OF [asm_rl, refl]) THEN'
asm_simp_tac (ss_only_silent (ssig_map_comp :: cutSsig_def :: flat_pointful_natural ::
eval_core_flat :: unfold_thms ctxt [o_def] dead_pre_map_comp :: (dead_ssig_map_comp0 RS sym) ::
(flat_flat RS sym) ::
@{thms o_apply convol_o fst_convol id_apply id_def[symmetric]}) ctxt) THEN'
asm_simp_tac (ss_only_silent (eval_core_pointful_natural :: flat_VLeaf ::
map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, ssig_map_comp] @
@{thms o_apply id_apply id_def[symmetric] map_prod_simp convol_def}) ctxt));
fun mk_natural_from_transfer_tac ctxt m alives transfer map_ids rel_Grps subst_rel_Grps =
let
val unfold_eq = unfold_thms ctxt @{thms Grp_UNIV_id[symmetric]};
val (rel_Grps', subst_rel_Grps') =
apply2 (map (fn thm => unfold_eq (thm RS eq_reflection))) (rel_Grps, subst_rel_Grps);
val transfer' = instantiate_transfer_rule_with_Grp_UNIV ctxt alives (unfold_eq transfer)
|> unfold_thms ctxt rel_Grps';
in
HEADGOAL (Method.insert_tac ctxt [transfer'] THEN'
EVERY' (map (subst_asm_tac ctxt NONE o single) subst_rel_Grps')) THEN
unfold_thms_tac ctxt (map_ids @ @{thms Grp_def rel_fun_def}) THEN
HEADGOAL (REPEAT_DETERM_N m o rtac ctxt ext THEN'
asm_full_simp_tac (ss_only_silent @{thms simp_thms id_apply o_apply mem_Collect_eq
top_greatest UNIV_I subset_UNIV[simplified UNIV_def]} ctxt)) THEN
ALLGOALS (REPEAT_DETERM o etac ctxt @{thm meta_allE} THEN' REPEAT_DETERM o etac ctxt allE THEN'
forward_tac ctxt [sym] THEN' assume_tac ctxt)
end;
fun mk_natural_by_unfolding_tac ctxt maps =
HEADGOAL (rtac ctxt ext) THEN
unfold_thms_tac ctxt (@{thms o_def[abs_def] id_apply id_def[symmetric]} @ maps) THEN
HEADGOAL (rtac ctxt refl);
fun mk_Retr_coinduct_tac ctxt dtor_rel_coinduct rel_eq =
HEADGOAL (EVERY' [rtac ctxt allI, rtac ctxt impI,
rtac ctxt (@{thm ord_le_eq_trans} OF [dtor_rel_coinduct, rel_eq]),
etac ctxt @{thm predicate2D}, assume_tac ctxt]);
fun mk_sig_transfer_tac ctxt pre_rel_def rel_eqs0 transfer =
let
val rel_eqs = no_refl rel_eqs0;
val rel_eq_syms = map (fn thm => thm RS sym) rel_eqs;
val transfer' = unfold_thms ctxt rel_eq_syms transfer
in
HEADGOAL (rtac ctxt transfer') ORELSE
unfold_thms_tac ctxt (pre_rel_def :: rel_eq_syms @
@{thms BNF_Def.vimage2p_def BNF_Composition.id_bnf_def}) THEN
HEADGOAL (rtac ctxt transfer')
end;
fun mk_transfer_by_transfer_prover_tac ctxt defs rel_eqs0 transfers =
let
val rel_eqs = no_refl rel_eqs0;
val rel_eq_syms = map (fn thm => thm RS sym) rel_eqs;
in
unfold_thms_tac ctxt (defs @ rel_eq_syms) THEN
HEADGOAL (transfer_prover_add_tac ctxt rel_eqs transfers)
end;
end;