1signature BasicProvers = 2sig 3 include Abbrev 4 type simpset = simpLib.simpset 5 6 (* Eliminate v = M or M = v from hypotheses *) 7 8 val VAR_EQ_TAC : tactic 9 val var_eq_tac : tactic 10 11 (* First order automatic proof *) 12 13 val PROVE : thm list -> term -> thm 14 val PROVE_TAC : thm list -> tactic 15 val prove_tac : thm list -> tactic 16 val GEN_PROVE_TAC : int -> int -> int -> thm list -> tactic 17 18 (* Simplification *) 19 20 val bool_ss : simpset 21 val srw_ss : unit -> simpset 22 val Abbr : term quotation -> thm 23 val LEAVE_LETS : thm 24 25 val RW_TAC : simpset -> thm list -> tactic 26 val rw_tac : simpset -> thm list -> tactic 27 val NORM_TAC : simpset -> thm list -> tactic 28 val SRW_TAC : simpLib.ssfrag list -> thm list -> tactic 29 val srw_tac : simpLib.ssfrag list -> thm list -> tactic 30 val augment_srw_ss : simpLib.ssfrag list -> unit 31 val diminish_srw_ss : string list -> simpLib.ssfrag list 32 val export_rewrites : string list -> unit 33 val thy_ssfrag : string -> simpLib.ssfrag 34 35 (* LET manoeuvres *) 36 val LET_ELIM_TAC : tactic 37 val new_let_thms : thm list -> unit 38 39 (* Compound automated reasoners. *) 40 41 val PRIM_STP_TAC : simpset -> tactic -> tactic 42 val STP_TAC : simpset -> tactic -> tactic 43 44 (* Other reasoning support. *) 45 val SPOSE_NOT_THEN : (thm -> tactic) -> tactic 46 val spose_not_then : (thm -> tactic) -> tactic 47 48 val by : term quotation * tactic -> tactic (* infix *) 49 val byA : term quotation * tactic -> tactic 50 val suffices_by : term quotation * tactic -> tactic (* infix *) 51 val on : (thm -> tactic) * (term quotation * tactic) -> tactic 52 (* infix *) 53 val subgoal : term quotation -> tactic 54 val sg : term quotation -> tactic 55 56 datatype tmkind 57 = Free of term 58 | Bound of term list * term 59 | Alien of term 60 61 val dest_tmkind : tmkind -> term 62 val prim_find_subterm : term list -> term -> goal -> tmkind 63 val find_subterm : term quotation -> goal -> tmkind 64 val primInduct : tmkind -> tactic -> tactic 65 val Cases : tactic 66 val Induct : tactic 67 val Cases_on : term quotation -> tactic 68 val Induct_on : term quotation -> tactic 69 70 val PURE_TOP_CASE_TAC : tactic (* top-most case-split *) 71 val PURE_CASE_TAC : tactic (* smallest case-split (concl) *) 72 val PURE_FULL_CASE_TAC: tactic (* smallest case-split (goal) *) 73 74 val PURE_CASE_SIMP_CONV : thm list -> conv 75 val CASE_SIMP_CONV : conv (* Apply case rewrites in theTypeBase *) 76 77 val CASE_TAC : tactic (* PURE_CASE_TAC then simplification *) 78 val TOP_CASE_TAC : tactic (* PURE_TOP_CASE_TAC then simplification *) 79 val FULL_CASE_TAC : tactic (* PURE_FULL_CASE_TAC then simplification *) 80 val full_case_tac : tactic 81 val EVERY_CASE_TAC : tactic (* Repeat FULL_CASE_TAC *) 82 val every_case_tac : tactic 83 84end 85