1(*  Title:      HOL/Tools/BNF/bnf_tactics.ML
2    Author:     Dmitriy Traytel, TU Muenchen
3    Author:     Jasmin Blanchette, TU Muenchen
4    Copyright   2012
5
6General tactics for bounded natural functors.
7*)
8
9signature BNF_TACTICS =
10sig
11  include CTR_SUGAR_GENERAL_TACTICS
12
13  val fo_rtac: Proof.context -> thm -> int -> tactic
14  val clean_blast_tac: Proof.context -> int -> tactic
15  val subst_tac: Proof.context -> int list option -> thm list -> int -> tactic
16  val subst_asm_tac: Proof.context -> int list option -> thm list -> int -> tactic
17
18  val mk_rotate_eq_tac: Proof.context -> (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list ->
19    ''a list -> int -> tactic
20
21  val mk_pointfree2: Proof.context -> thm -> thm
22
23  val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
24  val mk_Abs_inj_thm: thm -> thm
25
26  val mk_map_comp_id_tac: Proof.context -> thm -> tactic
27  val mk_map_cong0_tac: Proof.context -> int -> thm -> tactic
28  val mk_map_cong0L_tac: Proof.context -> int -> thm -> thm -> tactic
29end;
30
31structure BNF_Tactics : BNF_TACTICS =
32struct
33
34open Ctr_Sugar_General_Tactics
35open BNF_Util
36
37(*stolen from Christian Urban's Cookbook (and adapted slightly)*)
38fun fo_rtac ctxt thm = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
39  let
40    val concl_pat = Drule.strip_imp_concl (Thm.cprop_of thm)
41    val insts = Thm.first_order_match (concl_pat, concl)
42  in
43    rtac ctxt (Drule.instantiate_normalize insts thm) 1
44  end
45  handle Pattern.MATCH => no_tac) ctxt;
46
47fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of \<^theory_context>\<open>HOL\<close>) ctxt);
48
49(*unlike "unfold_thms_tac", it succeed when the RHS contains schematic variables not in the LHS*)
50fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt o the_default [0];
51fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt o the_default [0];
52
53(*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*)
54fun mk_pointfree2 ctxt thm = thm
55  |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
56  |> apply2 (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp)
57  |> mk_Trueprop_eq
58  |> (fn goal => Goal.prove_sorry ctxt [] [] goal
59    (K (rtac ctxt ext 1 THEN
60        unfold_thms_tac ctxt ([o_apply, unfold_thms ctxt [o_apply] (mk_sym thm)]) THEN
61        rtac ctxt refl 1)))
62  |> Thm.close_derivation \<^here>;
63
64
65(* Theorems for open typedefs with UNIV as representing set *)
66
67fun mk_Abs_inj_thm inj = inj OF (replicate 2 @{thm UNIV_I});
68fun mk_Abs_bij_thm ctxt Abs_inj_thm surj = rule_by_tactic ctxt ((rtac ctxt surj THEN' etac ctxt exI) 1)
69  (Abs_inj_thm RS @{thm bijI'});
70
71
72(* General tactic generators *)
73
74(*applies assoc rule to the lhs of an equation as long as possible*)
75fun mk_flatten_assoc_tac ctxt refl_tac trans assoc cong = rtac ctxt trans 1 THEN
76  REPEAT_DETERM (CHANGED ((FIRST' [rtac ctxt trans THEN' rtac ctxt assoc, rtac ctxt cong THEN' refl_tac]) 1)) THEN
77  refl_tac 1;
78
79(*proves two sides of an equation to be equal assuming both are flattened and rhs can be obtained
80from lhs by the given permutation of monoms*)
81fun mk_rotate_eq_tac ctxt refl_tac trans assoc com cong =
82  let
83    fun gen_tac [] [] = K all_tac
84      | gen_tac [x] [y] = if x = y then refl_tac else error "mk_rotate_eq_tac: different lists"
85      | gen_tac (x :: xs) (y :: ys) = if x = y
86        then rtac ctxt cong THEN' refl_tac THEN' gen_tac xs ys
87        else rtac ctxt trans THEN' rtac ctxt com THEN'
88          K (mk_flatten_assoc_tac ctxt refl_tac trans assoc cong) THEN'
89          gen_tac (xs @ [x]) (y :: ys)
90      | gen_tac _ _ = error "mk_rotate_eq_tac: different lists";
91  in
92    gen_tac
93  end;
94
95fun mk_map_comp_id_tac ctxt map_comp0 =
96  (rtac ctxt trans THEN' rtac ctxt map_comp0 THEN' K (unfold_thms_tac ctxt @{thms comp_id}) THEN' rtac ctxt refl) 1;
97
98fun mk_map_cong0_tac ctxt m map_cong0 =
99  EVERY' [rtac ctxt mp, rtac ctxt map_cong0,
100    CONJ_WRAP' (K (rtac ctxt @{thm ballI} THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1;
101
102fun mk_map_cong0L_tac ctxt passive map_cong0 map_id =
103  (rtac ctxt trans THEN' rtac ctxt map_cong0 THEN' EVERY' (replicate passive (rtac ctxt refl))) 1 THEN
104  REPEAT_DETERM (EVERY' [rtac ctxt trans, etac ctxt @{thm bspec}, assume_tac ctxt,
105      rtac ctxt sym, rtac ctxt @{thm id_apply}] 1) THEN
106  rtac ctxt map_id 1;
107
108end;
109