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