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