src/HOL/BNF/Tools/bnf_tactics.ML
author blanchet
Fri Jun 07 09:30:13 2013 +0200 (2013-06-07)
changeset 52334 705bc4f5fc70
parent 51893 596baae88a88
child 52913 2d2d9d1de1a9
permissions -rw-r--r--
tuning
     1 (*  Title:      HOL/BNF/Tools/bnf_tactics.ML
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4     Copyright   2012
     5 
     6 General tactics for bounded natural functors.
     7 *)
     8 
     9 signature BNF_TACTICS =
    10 sig
    11   val ss_only : thm list -> Proof.context -> Proof.context
    12 
    13   val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
    14   val fo_rtac: thm -> Proof.context -> int -> tactic
    15   val unfold_thms_tac: Proof.context -> thm list -> tactic
    16   val mk_unfold_thms_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic
    17 
    18   val mk_flatten_assoc_tac: (int -> tactic) -> thm -> thm -> thm -> tactic
    19   val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list ->
    20     int -> tactic
    21 
    22   val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
    23   val mk_Abs_inj_thm: thm -> thm
    24 
    25   val mk_ctor_or_dtor_rel_tac:
    26     thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
    27 
    28   val mk_map_comp_id_tac: thm -> tactic
    29   val mk_map_cong0_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
    30   val mk_map_cong0L_tac: int -> thm -> thm -> tactic
    31 end;
    32 
    33 structure BNF_Tactics : BNF_TACTICS =
    34 struct
    35 
    36 open BNF_Util
    37 
    38 fun ss_only ths ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths
    39 
    40 fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,
    41   tac, REPEAT_DETERM_N (n - k) o etac thin_rl]);
    42 
    43 (*stolen from Christian Urban's Cookbook*)
    44 fun fo_rtac thm = Subgoal.FOCUS (fn {concl, ...} =>
    45   let
    46     val concl_pat = Drule.strip_imp_concl (cprop_of thm)
    47     val insts = Thm.first_order_match (concl_pat, concl)
    48   in
    49     rtac (Drule.instantiate_normalize insts thm) 1
    50   end);
    51 
    52 fun unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
    53 
    54 fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x;
    55 
    56 
    57 (* Theorems for open typedefs with UNIV as representing set *)
    58 
    59 fun mk_Abs_inj_thm inj = inj OF (replicate 2 UNIV_I);
    60 fun mk_Abs_bij_thm ctxt Abs_inj_thm surj = rule_by_tactic ctxt ((rtac surj THEN' etac exI) 1)
    61   (Abs_inj_thm RS @{thm bijI});
    62 
    63 
    64 
    65 (* General tactic generators *)
    66 
    67 (*applies assoc rule to the lhs of an equation as long as possible*)
    68 fun mk_flatten_assoc_tac refl_tac trans assoc cong = rtac trans 1 THEN
    69   REPEAT_DETERM (CHANGED ((FIRST' [rtac trans THEN' rtac assoc, rtac cong THEN' refl_tac]) 1)) THEN
    70   refl_tac 1;
    71 
    72 (*proves two sides of an equation to be equal assuming both are flattened and rhs can be obtained
    73 from lhs by the given permutation of monoms*)
    74 fun mk_rotate_eq_tac refl_tac trans assoc com cong =
    75   let
    76     fun gen_tac [] [] = K all_tac
    77       | gen_tac [x] [y] = if x = y then refl_tac else error "mk_rotate_eq_tac: different lists"
    78       | gen_tac (x :: xs) (y :: ys) = if x = y
    79         then rtac cong THEN' refl_tac THEN' gen_tac xs ys
    80         else rtac trans THEN' rtac com THEN'
    81           K (mk_flatten_assoc_tac refl_tac trans assoc cong) THEN'
    82           gen_tac (xs @ [x]) (y :: ys)
    83       | gen_tac _ _ = error "mk_rotate_eq_tac: different lists";
    84   in
    85     gen_tac
    86   end;
    87 
    88 fun mk_ctor_or_dtor_rel_tac srel_def IJrel_defs IJsrel_defs dtor_srel {context = ctxt, prems = _} =
    89   unfold_thms_tac ctxt IJrel_defs THEN
    90   rtac (unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
    91     @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel RS trans) 1 THEN
    92   unfold_thms_tac ctxt (srel_def ::
    93     @{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv
    94       split_conv}) THEN
    95   rtac refl 1;
    96 
    97 fun mk_map_comp_id_tac map_comp =
    98   (rtac trans THEN' rtac map_comp THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1;
    99 
   100 fun mk_map_cong0_tac m map_cong0 {context = ctxt, prems = _} =
   101   EVERY' [rtac mp, rtac map_cong0,
   102     CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1;
   103 
   104 fun mk_map_cong0L_tac passive map_cong0 map_id' =
   105   (rtac trans THEN' rtac map_cong0 THEN' EVERY' (replicate passive (rtac refl))) 1 THEN
   106   REPEAT_DETERM (EVERY' [rtac trans, etac bspec, atac, rtac sym, rtac @{thm id_apply}] 1) THEN
   107   rtac map_id' 1;
   108 
   109 end;