src/HOL/Codatatype/Tools/bnf_tactics.ML
author blanchet
Tue Sep 11 18:39:47 2012 +0200 (2012-09-11)
changeset 49286 dde4967c9233
parent 49284 5f39b7940b49
child 49391 3a96797fd53e
permissions -rw-r--r--
added "defaults" option
     1 (*  Title:      HOL/Codatatype/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 -> simpset
    12 
    13   val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
    14   val fo_rtac: thm -> Proof.context -> int -> tactic
    15   val subst_asm_tac: Proof.context -> thm list -> int -> tactic
    16   val subst_tac: Proof.context -> thm list -> int -> tactic
    17   val substs_tac: Proof.context -> thm list -> int -> tactic
    18 
    19   val mk_flatten_assoc_tac: (int -> tactic) -> thm -> thm -> thm -> tactic
    20   val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list ->
    21     int -> tactic
    22 
    23   val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
    24   val mk_Abs_inj_thm: thm -> thm
    25 
    26   val mk_pred_unfold_tac: thm -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
    27 
    28   val mk_map_comp_id_tac: thm -> tactic
    29   val mk_map_cong_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
    30   val mk_map_congL_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 thms = Simplifier.clear_ss HOL_basic_ss addsimps thms;
    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 (*unlike "unfold_tac", succeeds when the RHS contains schematic variables not in the LHS*)
    53 fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt [0];
    54 fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt [0];
    55 fun substs_tac ctxt = REPEAT_DETERM oo subst_tac ctxt;
    56 
    57 
    58 
    59 (* Theorems for open typedefs with UNIV as representing set *)
    60 
    61 fun mk_Abs_inj_thm inj = inj OF (replicate 2 UNIV_I);
    62 fun mk_Abs_bij_thm ctxt Abs_inj_thm surj = rule_by_tactic ctxt ((rtac surj THEN' etac exI) 1)
    63   (Abs_inj_thm RS @{thm bijI});
    64 
    65 
    66 
    67 (* General tactic generators *)
    68 
    69 (*applies assoc rule to the lhs of an equation as long as possible*)
    70 fun mk_flatten_assoc_tac refl_tac trans assoc cong = rtac trans 1 THEN
    71   REPEAT_DETERM (CHANGED ((FIRST' [rtac trans THEN' rtac assoc, rtac cong THEN' refl_tac]) 1)) THEN
    72   refl_tac 1;
    73 
    74 (*proves two sides of an equation to be equal assuming both are flattened and rhs can be obtained
    75 from lhs by the given permutation of monoms*)
    76 fun mk_rotate_eq_tac refl_tac trans assoc com cong =
    77   let
    78     fun gen_tac [] [] = K all_tac
    79       | gen_tac [x] [y] = if x = y then refl_tac else error "mk_rotate_eq_tac: different lists"
    80       | gen_tac (x :: xs) (y :: ys) = if x = y
    81         then rtac cong THEN' refl_tac THEN' gen_tac xs ys
    82         else rtac trans THEN' rtac com THEN'
    83           K (mk_flatten_assoc_tac refl_tac trans assoc cong) THEN'
    84           gen_tac (xs @ [x]) (y :: ys)
    85       | gen_tac _ _ = error "mk_rotate_eq_tac: different lists";
    86   in
    87     gen_tac
    88   end;
    89 
    90 fun mk_pred_unfold_tac pred_def pred_defs rel_unfold {context = ctxt, prems = _} =
    91   Local_Defs.unfold_tac ctxt (@{thm mem_Collect_eq_split} :: pred_def :: pred_defs) THEN
    92   rtac rel_unfold 1;
    93 
    94 fun mk_map_comp_id_tac map_comp =
    95   (rtac trans THEN' rtac map_comp) 1 THEN
    96   REPEAT_DETERM (stac @{thm o_id} 1) THEN
    97   rtac refl 1;
    98 
    99 fun mk_map_cong_tac m map_cong {context = ctxt, prems = _} =
   100   EVERY' [rtac mp, rtac map_cong,
   101     CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1;
   102 
   103 fun mk_map_congL_tac passive map_cong map_id' =
   104   (rtac trans THEN' rtac map_cong THEN' EVERY' (replicate passive (rtac refl))) 1 THEN
   105   REPEAT_DETERM (EVERY' [rtac trans, etac bspec, atac, rtac sym, rtac @{thm id_apply}] 1) THEN
   106   rtac map_id' 1;
   107 
   108 end;