6 General tactics for bounded natural functors. |
6 General tactics for bounded natural functors. |
7 *) |
7 *) |
8 |
8 |
9 signature BNF_TACTICS = |
9 signature BNF_TACTICS = |
10 sig |
10 sig |
11 val ss_only : thm list -> Proof.context -> Proof.context |
11 include CTR_SUGAR_GENERAL_TACTICS |
12 |
12 |
13 val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic |
|
14 val fo_rtac: thm -> Proof.context -> int -> tactic |
13 val fo_rtac: thm -> Proof.context -> int -> tactic |
15 val unfold_thms_tac: Proof.context -> thm list -> tactic |
|
16 val mk_unfold_thms_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic |
14 val mk_unfold_thms_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic |
17 |
15 |
18 val mk_flatten_assoc_tac: (int -> tactic) -> thm -> thm -> thm -> tactic |
16 val mk_flatten_assoc_tac: (int -> tactic) -> thm -> thm -> thm -> tactic |
19 val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list -> |
17 val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list -> |
20 int -> tactic |
18 int -> tactic |
33 end; |
31 end; |
34 |
32 |
35 structure BNF_Tactics : BNF_TACTICS = |
33 structure BNF_Tactics : BNF_TACTICS = |
36 struct |
34 struct |
37 |
35 |
|
36 open Ctr_Sugar_General_Tactics |
38 open BNF_Util |
37 open BNF_Util |
39 |
|
40 fun ss_only ths ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths |
|
41 |
|
42 fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl, |
|
43 tac, REPEAT_DETERM_N (n - k) o etac thin_rl]); |
|
44 |
38 |
45 (*stolen from Christian Urban's Cookbook*) |
39 (*stolen from Christian Urban's Cookbook*) |
46 fun fo_rtac thm = Subgoal.FOCUS (fn {concl, ...} => |
40 fun fo_rtac thm = Subgoal.FOCUS (fn {concl, ...} => |
47 let |
41 let |
48 val concl_pat = Drule.strip_imp_concl (cprop_of thm) |
42 val concl_pat = Drule.strip_imp_concl (cprop_of thm) |
49 val insts = Thm.first_order_match (concl_pat, concl) |
43 val insts = Thm.first_order_match (concl_pat, concl) |
50 in |
44 in |
51 rtac (Drule.instantiate_normalize insts thm) 1 |
45 rtac (Drule.instantiate_normalize insts thm) 1 |
52 end); |
46 end); |
53 |
|
54 fun unfold_thms_tac _ [] = all_tac |
|
55 | unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms); |
|
56 |
47 |
57 fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x; |
48 fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x; |
58 |
49 |
59 (*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*) |
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*) |
60 fun mk_pointfree ctxt thm = thm |
51 fun mk_pointfree ctxt thm = thm |