1(* Title: HOL/Tools/BNF/bnf_fp_n2m_tactics.ML 2 Author: Dmitriy Traytel, TU Muenchen 3 Copyright 2013 4 5Tactics for mutualization of nested (co)datatypes. 6*) 7 8signature BNF_FP_N2M_TACTICS = 9sig 10 val mk_rel_xtor_co_induct_tac: BNF_Util.fp_kind -> thm list -> thm list -> thm list -> 11 thm list -> thm list -> thm list -> {prems: thm list, context: Proof.context} -> tactic 12 val mk_xtor_un_fold_unique_tac: BNF_Util.fp_kind -> thm list -> thm list -> thm list -> 13 thm list -> thm list -> thm list -> thm list -> thm list -> thm list -> 14 {context: Proof.context, prems: thm list} -> tactic 15 val mk_xtor_un_fold_tac: Proof.context -> int -> thm list -> thm list -> tactic 16 val mk_xtor_un_fold_transfer_tac: Proof.context -> int -> thm list -> thm list -> thm list -> 17 thm list -> thm list -> thm list -> thm list -> tactic 18end; 19 20structure BNF_FP_N2M_Tactics : BNF_FP_N2M_TACTICS = 21struct 22 23open BNF_Util 24open BNF_Tactics 25open BNF_FP_Util 26 27val vimage2p_unfolds = o_apply :: @{thms vimage2p_def}; 28 29fun unfold_at_most_once_tac ctxt thms = 30 CONVERSION (Conv.top_sweep_conv (K (Conv.rewrs_conv thms)) ctxt); 31val unfold_once_tac = CHANGED ooo unfold_at_most_once_tac; 32 33fun mk_rel_xtor_co_induct_tac fp abs_inverses co_inducts0 rel_defs rel_monos nesting_rel_eqs0 34 nesting_rel_monos0 {context = ctxt, prems = raw_C_IHs} = 35 let 36 val nesting_rel_eqs = @{thms prod.rel_eq sum.rel_eq} @ nesting_rel_eqs0; 37 val nesting_rel_monos = map (fn thm => rotate_prems ~1 (thm RS @{thm predicate2D})) 38 (@{thms prod.rel_mono sum.rel_mono} @ nesting_rel_monos0); 39 val co_inducts = map (unfold_thms ctxt (vimage2p_unfolds @ nesting_rel_eqs)) co_inducts0; 40 val unfolds = map (fn def => 41 unfold_thms ctxt (id_apply :: vimage2p_unfolds @ abs_inverses @ no_reflexive [def])) rel_defs; 42 val folded_C_IHs = map (fn thm => thm RS @{thm spec2} RS mp) raw_C_IHs; 43 val C_IHs = map2 (curry op |>) folded_C_IHs unfolds; 44 val C_IH_monos = 45 @{map 3} (fn C_IH => fn mono => fn unfold => 46 (mono RSN (2, @{thm vimage2p_mono}), C_IH) 47 |> fp = Greatest_FP ? swap 48 |> op RS 49 |> unfold) 50 folded_C_IHs rel_monos unfolds; 51 52 val sym_nested_rel_eqs = map mk_sym nesting_rel_eqs; 53 in 54 unfold_thms_tac ctxt vimage2p_unfolds THEN 55 HEADGOAL (CONJ_WRAP_GEN' (rtac ctxt @{thm context_conjI}) 56 (fn thm => rtac ctxt thm THEN_ALL_NEW (rotate_tac ~1 THEN' 57 REPEAT_ALL_NEW (FIRST' [eresolve_tac ctxt C_IHs, eresolve_tac ctxt C_IH_monos, 58 SELECT_GOAL (unfold_thms_tac ctxt nesting_rel_eqs) THEN' rtac ctxt @{thm order_refl}, 59 assume_tac ctxt, resolve_tac ctxt co_inducts, 60 resolve_tac ctxt C_IH_monos THEN_ALL_NEW (TRY o FIRST' 61 [SELECT_GOAL (unfold_thms_tac ctxt sym_nested_rel_eqs) THEN' assume_tac ctxt, 62 rtac ctxt @{thm order_refl}, 63 REPEAT_ALL_NEW (eresolve_tac ctxt nesting_rel_monos)])]))) 64 co_inducts) 65 end; 66 67fun mk_xtor_un_fold_unique_tac fp xtor_un_fold_defs map_arg_congs xtor_un_fold_o_maps 68 Rep_o_Abss fp_un_fold_uniques simp_thms map_thms map_defs cache_defs {context = ctxt, prems} = 69 unfold_thms_tac ctxt xtor_un_fold_defs THEN 70 HEADGOAL (REPEAT_DETERM o FIRST' [hyp_subst_tac_thin true ctxt, rtac ctxt refl, 71 rtac ctxt conjI, 72 rtac ctxt @{thm arg_cong2[of _ _ _ _ "(\<circ>)", OF refl]}, 73 rtac ctxt @{thm arg_cong2[of _ _ _ _ "(\<circ>)", OF _ refl]}, 74 resolve_tac ctxt map_arg_congs, 75 resolve_tac ctxt fp_un_fold_uniques THEN_ALL_NEW case_fp fp (K all_tac) (rtac ctxt sym), 76 SELECT_GOAL (CHANGED (unfold_thms_tac ctxt (flat [simp_thms, map_thms, map_defs, 77 xtor_un_fold_defs, xtor_un_fold_o_maps, Rep_o_Abss, prems]))), 78 unfold_once_tac ctxt cache_defs]); 79 80fun mk_xtor_un_fold_tac ctxt n simps cache_defs = 81 REPEAT_DETERM (CHANGED (unfold_thms_tac ctxt simps) ORELSE 82 CHANGED (ALLGOALS (unfold_at_most_once_tac ctxt cache_defs))) THEN 83 CONJ_WRAP (K (HEADGOAL (rtac ctxt refl))) (1 upto n); 84 85fun mk_xtor_un_fold_transfer_tac ctxt n xtor_un_fold_defs rel_defs fp_un_fold_transfers 86 map_transfers Abs_transfers fp_or_nesting_rel_eqs cache_defs = 87 let 88 val unfold = SELECT_GOAL (unfold_thms_tac ctxt fp_or_nesting_rel_eqs); 89 in 90 unfold_thms_tac ctxt (xtor_un_fold_defs @ rel_defs) THEN 91 HEADGOAL (CONJ_WRAP' 92 (fn thm => EVERY' [REPEAT_DETERM_N n o rtac ctxt rel_funI, rtac ctxt thm THEN_ALL_NEW 93 REPEAT_DETERM o (FIRST' [assume_tac ctxt, rtac ctxt @{thm id_transfer}, 94 rtac ctxt @{thm rel_funD[OF rel_funD[OF comp_transfer]]}, 95 resolve_tac ctxt fp_un_fold_transfers, resolve_tac ctxt map_transfers, 96 unfold_once_tac ctxt cache_defs, 97 resolve_tac ctxt Abs_transfers, rtac ctxt @{thm vimage2p_rel_fun}, 98 unfold THEN' rtac ctxt @{thm vimage2p_rel_fun}])]) 99 fp_un_fold_transfers) 100 end; 101 102end; 103