equal
deleted
inserted
replaced
8 |
8 |
9 signature BNF_TACTICS = |
9 signature BNF_TACTICS = |
10 sig |
10 sig |
11 val ss_only: thm list -> simpset |
11 val ss_only: thm list -> simpset |
12 |
12 |
|
13 val prefer_tac: int -> tactic |
13 val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic |
14 val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic |
14 val fo_rtac: thm -> Proof.context -> int -> tactic |
15 val fo_rtac: thm -> Proof.context -> int -> tactic |
15 val subst_asm_tac: Proof.context -> thm list -> int -> tactic |
16 val subst_asm_tac: Proof.context -> thm list -> int -> tactic |
16 val subst_tac: Proof.context -> thm list -> int -> tactic |
17 val subst_tac: Proof.context -> thm list -> int -> tactic |
17 val substs_tac: Proof.context -> thm list -> int -> tactic |
18 val substs_tac: Proof.context -> thm list -> int -> tactic |
34 struct |
35 struct |
35 |
36 |
36 open BNF_Util |
37 open BNF_Util |
37 |
38 |
38 fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms; |
39 fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms; |
|
40 |
|
41 (* FIXME: why not in "Pure"? *) |
|
42 fun prefer_tac i = defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1); |
39 |
43 |
40 fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl, |
44 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]); |
45 tac, REPEAT_DETERM_N (n - k) o etac thin_rl]); |
42 |
46 |
43 (*stolen from Christian Urban's Cookbook*) |
47 (*stolen from Christian Urban's Cookbook*) |