src/HOL/BNF/Tools/bnf_tactics.ML
changeset 55058 4e700eb471d4
parent 55057 6b0fcbeebaba
child 55059 ef2e0fb783c6
     1.1 --- a/src/HOL/BNF/Tools/bnf_tactics.ML	Mon Jan 20 18:24:55 2014 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,109 +0,0 @@
     1.4 -(*  Title:      HOL/BNF/Tools/bnf_tactics.ML
     1.5 -    Author:     Dmitriy Traytel, TU Muenchen
     1.6 -    Author:     Jasmin Blanchette, TU Muenchen
     1.7 -    Copyright   2012
     1.8 -
     1.9 -General tactics for bounded natural functors.
    1.10 -*)
    1.11 -
    1.12 -signature BNF_TACTICS =
    1.13 -sig
    1.14 -  include CTR_SUGAR_GENERAL_TACTICS
    1.15 -
    1.16 -  val fo_rtac: thm -> Proof.context -> int -> tactic
    1.17 -
    1.18 -  val mk_flatten_assoc_tac: (int -> tactic) -> thm -> thm -> thm -> tactic
    1.19 -  val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list ->
    1.20 -    int -> tactic
    1.21 -
    1.22 -  val mk_pointfree: Proof.context -> thm -> thm
    1.23 -
    1.24 -  val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
    1.25 -  val mk_Abs_inj_thm: thm -> thm
    1.26 -
    1.27 -  val mk_ctor_or_dtor_rel_tac:
    1.28 -    thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
    1.29 -
    1.30 -  val mk_map_comp_id_tac: thm -> tactic
    1.31 -  val mk_map_cong0_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
    1.32 -  val mk_map_cong0L_tac: int -> thm -> thm -> tactic
    1.33 -end;
    1.34 -
    1.35 -structure BNF_Tactics : BNF_TACTICS =
    1.36 -struct
    1.37 -
    1.38 -open Ctr_Sugar_General_Tactics
    1.39 -open BNF_Util
    1.40 -
    1.41 -(*stolen from Christian Urban's Cookbook*)
    1.42 -fun fo_rtac thm = Subgoal.FOCUS (fn {concl, ...} =>
    1.43 -  let
    1.44 -    val concl_pat = Drule.strip_imp_concl (cprop_of thm)
    1.45 -    val insts = Thm.first_order_match (concl_pat, concl)
    1.46 -  in
    1.47 -    rtac (Drule.instantiate_normalize insts thm) 1
    1.48 -  end);
    1.49 -
    1.50 -(*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*)
    1.51 -fun mk_pointfree ctxt thm = thm
    1.52 -  |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
    1.53 -  |> pairself (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp)
    1.54 -  |> mk_Trueprop_eq
    1.55 -  |> (fn goal => Goal.prove_sorry ctxt [] [] goal
    1.56 -    (K (rtac ext 1 THEN unfold_thms_tac ctxt [o_apply, mk_sym thm] THEN rtac refl 1)))
    1.57 -  |> Thm.close_derivation;
    1.58 -
    1.59 -
    1.60 -(* Theorems for open typedefs with UNIV as representing set *)
    1.61 -
    1.62 -fun mk_Abs_inj_thm inj = inj OF (replicate 2 UNIV_I);
    1.63 -fun mk_Abs_bij_thm ctxt Abs_inj_thm surj = rule_by_tactic ctxt ((rtac surj THEN' etac exI) 1)
    1.64 -  (Abs_inj_thm RS @{thm bijI});
    1.65 -
    1.66 -
    1.67 -
    1.68 -(* General tactic generators *)
    1.69 -
    1.70 -(*applies assoc rule to the lhs of an equation as long as possible*)
    1.71 -fun mk_flatten_assoc_tac refl_tac trans assoc cong = rtac trans 1 THEN
    1.72 -  REPEAT_DETERM (CHANGED ((FIRST' [rtac trans THEN' rtac assoc, rtac cong THEN' refl_tac]) 1)) THEN
    1.73 -  refl_tac 1;
    1.74 -
    1.75 -(*proves two sides of an equation to be equal assuming both are flattened and rhs can be obtained
    1.76 -from lhs by the given permutation of monoms*)
    1.77 -fun mk_rotate_eq_tac refl_tac trans assoc com cong =
    1.78 -  let
    1.79 -    fun gen_tac [] [] = K all_tac
    1.80 -      | gen_tac [x] [y] = if x = y then refl_tac else error "mk_rotate_eq_tac: different lists"
    1.81 -      | gen_tac (x :: xs) (y :: ys) = if x = y
    1.82 -        then rtac cong THEN' refl_tac THEN' gen_tac xs ys
    1.83 -        else rtac trans THEN' rtac com THEN'
    1.84 -          K (mk_flatten_assoc_tac refl_tac trans assoc cong) THEN'
    1.85 -          gen_tac (xs @ [x]) (y :: ys)
    1.86 -      | gen_tac _ _ = error "mk_rotate_eq_tac: different lists";
    1.87 -  in
    1.88 -    gen_tac
    1.89 -  end;
    1.90 -
    1.91 -fun mk_ctor_or_dtor_rel_tac srel_def IJrel_defs IJsrel_defs dtor_srel {context = ctxt, prems = _} =
    1.92 -  unfold_thms_tac ctxt IJrel_defs THEN
    1.93 -  rtac (unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
    1.94 -    @{thms Collect_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel RS trans) 1 THEN
    1.95 -  unfold_thms_tac ctxt (srel_def ::
    1.96 -    @{thms pair_collapse Collect_mem_eq mem_Collect_eq prod.cases fst_conv snd_conv
    1.97 -      split_conv}) THEN
    1.98 -  rtac refl 1;
    1.99 -
   1.100 -fun mk_map_comp_id_tac map_comp0 =
   1.101 -  (rtac trans THEN' rtac map_comp0 THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1;
   1.102 -
   1.103 -fun mk_map_cong0_tac m map_cong0 {context = ctxt, prems = _} =
   1.104 -  EVERY' [rtac mp, rtac map_cong0,
   1.105 -    CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1;
   1.106 -
   1.107 -fun mk_map_cong0L_tac passive map_cong0 map_id =
   1.108 -  (rtac trans THEN' rtac map_cong0 THEN' EVERY' (replicate passive (rtac refl))) 1 THEN
   1.109 -  REPEAT_DETERM (EVERY' [rtac trans, etac bspec, atac, rtac sym, rtac @{thm id_apply}] 1) THEN
   1.110 -  rtac map_id 1;
   1.111 -
   1.112 -end;