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 -> unit 32 val export_rewrites : string list -> unit 33 val delsimps : string list -> unit 34 val temp_delsimps : string list -> unit 35 val thy_ssfrag : string -> simpLib.ssfrag 36 val thy_simpset : string -> simpset option 37 val temp_setsimpset : simpset -> unit 38 val merge_simpsets : string list -> simpset 39 datatype srw_update = ADD_SSFRAG of simpLib.ssfrag | REMOVE_RWT of string 40 val simpset_state : unit -> simpset * bool * srw_update list 41 val logged_update : {thyname : string} -> (simpset -> simpset) -> unit 42 val logged_addfrags : {thyname : string} -> simpLib.ssfrag list -> unit 43 val do_logged_updates : {theories : string list} -> unit 44 val apply_logged_updates : {theories : string list} -> (simpset -> simpset) 45 val augment_with_typebase : TypeBasePure.typeBase -> simpset -> simpset 46 val temp_set_simpset_ancestry : string list -> unit 47 val set_simpset_ancestry : string list -> unit 48 val recreate_sset_at_parentage : string list -> unit 49 50 (* LET and Abbrev manoeuvres *) 51 val LET_ELIM_TAC : tactic 52 val new_let_thms : thm list -> unit 53 val TIDY_ABBREVS : tactic 54 55 (* Compound automated reasoners. *) 56 57 val PRIM_STP_TAC : simpset -> tactic -> tactic 58 val STP_TAC : simpset -> tactic -> tactic 59 60 (* Other reasoning support. *) 61 val SPOSE_NOT_THEN : (thm -> tactic) -> tactic 62 val spose_not_then : (thm -> tactic) -> tactic 63 64 val by : term quotation * tactic -> tactic (* infix *) 65 val byA : term quotation * tactic -> tactic 66 val suffices_by : term quotation * tactic -> tactic (* infix *) 67 val on : (thm -> tactic) * (term quotation * tactic) -> tactic 68 (* infix *) 69 val subgoal : term quotation -> tactic 70 val sg : term quotation -> tactic 71 72 datatype tmkind 73 = Free of term 74 | Bound of term list * term 75 | Alien of term 76 77 val dest_tmkind : tmkind -> term 78 val prim_find_subterm : term list -> term -> goal -> tmkind 79 val find_subterm : term quotation -> goal -> tmkind 80 val primInduct : tmkind -> tactic -> tactic 81 val Cases : tactic 82 val Induct : tactic 83 val namedCases : string list -> tactic 84 85 val tmCases_on : term -> string list -> tactic 86 val Cases_on : term quotation -> tactic 87 val Induct_on : term quotation -> tactic 88 val namedCases_on : term quotation -> string list -> tactic 89 90 val PURE_TOP_CASE_TAC : tactic (* top-most case-split *) 91 val PURE_CASE_TAC : tactic (* smallest case-split (concl) *) 92 val PURE_FULL_CASE_TAC: tactic (* smallest case-split (goal) *) 93 94 val PURE_CASE_SIMP_CONV : thm list -> conv 95 val CASE_SIMP_CONV : conv (* Apply case rewrites in theTypeBase *) 96 97 val CASE_TAC : tactic (* PURE_CASE_TAC then simplification *) 98 val TOP_CASE_TAC : tactic (* PURE_TOP_CASE_TAC then simplification *) 99 val FULL_CASE_TAC : tactic (* PURE_FULL_CASE_TAC then simplification *) 100 val full_case_tac : tactic 101 val EVERY_CASE_TAC : tactic (* Repeat FULL_CASE_TAC *) 102 val every_case_tac : tactic 103 104end 105