Structure Tactical

signature Tactical =
sig
  include Abbrev

  (* The `_in` forms take the context to prove against explicitly; the
     historical spellings read the ambient context and are defined in
     terms of them. *)
  val TAC_PROOF_in   : Context.t -> goal * tactic -> thm
  val prove_in       : Context.t -> term * tactic -> thm
  val prove_goal_in  : Context.t -> goal * tactic -> thm
  val store_thm_in   : Context.t -> string * term * tactic -> thm
  val TAC_PROOF      : goal * tactic -> thm
  val prove          : term * tactic -> thm
  val prove_goal     : goal * tactic -> thm
  val store_thm      : string * term * tactic -> thm
  val CONV_TAC       : conv -> tactic
  val THEN           : ('a,'b) gentactic * tactic -> ('a,'b) gentactic
  val >>             : ('a,'b) gentactic * tactic -> ('a,'b) gentactic
  val \\             : ('a,'b) gentactic * tactic -> ('a,'b) gentactic
  (* could be used as
  val THEN           : tactic * tactic -> tactic
  val THEN           : list_tactic * tactic -> list_tactic
  *)
  val THENL          : ('a,'b) gentactic * tactic list -> ('a,'b) gentactic
  val >|             : ('a,'b) gentactic * tactic list -> ('a,'b) gentactic
  (* could be used as
  val THENL          : tactic * tactic list -> tactic
  val THENL          : list_tactic * tactic list -> list_tactic
  *)
  val ORELSE         : tactic * tactic -> tactic
  val ORELSE_LT      : list_tactic * list_tactic -> list_tactic
  val THEN1          : ('a,'b) gentactic * tactic -> ('a,'b) gentactic
  val >-             : ('a,'b) gentactic * tactic -> ('a,'b) gentactic
  val THEN_LT        : ('a,'b) gentactic * list_tactic -> ('a,'b) gentactic
  val >>>            : ('a,'b) gentactic * list_tactic -> ('a,'b) gentactic
  (* could be used as
  val THEN_LT        : tactic * list_tactic -> tactic
  val THEN_LT        : list_tactic * list_tactic -> list_tactic
  *)
  val >>-            : tactic * int -> tactic -> tactic
  val ??             : ('a -> 'b) * 'a -> 'b
  val TACS_TO_LT     : tactic list -> list_tactic
  val NULL_OK_LT     : list_tactic -> list_tactic
  val ALLGOALS       : tactic -> list_tactic
  val TRYALL         : tactic -> list_tactic
  val NTH_GOAL       : tactic -> int -> list_tactic
  val LASTGOAL       : tactic -> list_tactic
  val HEADGOAL       : tactic -> list_tactic
  val SPLIT_LT       : int -> list_tactic * list_tactic -> list_tactic
  val ROTATE_LT      : int -> list_tactic
  val REVERSE        : tactic -> tactic
  val reverse        : tactic -> tactic
  val REVERSE_LT     : list_tactic
  val FAIL_TAC       : string -> tactic
  val NO_TAC         : tactic
  val FAIL_LT        : string -> list_tactic
  val NO_LT          : list_tactic
  val ALL_TAC        : tactic
  val all_tac        : tactic
  val cheat          : tactic
  val ALL_LT         : list_tactic
  val TRY            : tactic -> tactic
  val TRY_LT         : list_tactic -> list_tactic
  val REPEAT         : tactic -> tactic
  val rpt            : tactic -> tactic
  val REPEAT_LT      : list_tactic -> list_tactic
  (* Feedback.trace round a tactic sets the flag only while `tac g'
     builds its closure: a tactic does its work when that closure is
     applied to the context, by which time the flag has been restored.
     This spans the context application too.  Rules and conversions are
     fully applied and so need no such thing. *)
  val trace_tac      : string * int -> tactic -> tactic

  val VALID          : tactic -> tactic
  val VALID_LT       : list_tactic -> list_tactic
  val VALIDATE       : tactic -> tactic
  val VALIDATE_LT    : list_tactic -> list_tactic
  val GEN_VALIDATE   : bool -> tactic -> tactic
  val GEN_VALIDATE_LT: bool -> list_tactic -> list_tactic
  val CONJ_VALIDATE  : tactic -> tactic
  val ADD_SGS_TAC    : term list -> tactic -> tactic
  val EVERY          : tactic list -> tactic
  val EVERY_LT       : list_tactic list -> list_tactic
  val FIRST          : tactic list -> tactic
  val FIRST_LT       : tactic -> list_tactic
  val SELECT_LT_THEN : tactic -> tactic -> list_tactic
  val SELECT_LT      : tactic -> list_tactic
  val MAP_EVERY      : ('a -> tactic) -> 'a list -> tactic
  val map_every      : ('a -> tactic) -> 'a list -> tactic
  val MAP_FIRST      : ('a -> tactic) -> 'a list -> tactic
  val IF             : tactic -> tactic -> tactic -> tactic
  val FIRST_PROVE    : tactic list -> tactic
  val EVERY_ASSUM    : thm_tactic -> tactic
  val every_assum    : thm_tactic -> tactic
  val FIRST_ASSUM    : thm_tactic -> tactic
  val first_assum    : thm_tactic -> tactic
  val FIRST_X_ASSUM  : thm_tactic -> tactic
  val first_x_assum  : thm_tactic -> tactic
  val LAST_ASSUM     : thm_tactic -> tactic
  val last_assum     : thm_tactic -> tactic
  val LAST_X_ASSUM   : thm_tactic -> tactic
  val last_x_assum   : thm_tactic -> tactic
  val goal_assum     : thm_tactic -> tactic
  val hdtm_assum     : term -> thm_tactic -> tactic
  val hdtm_x_assum   : term -> thm_tactic -> tactic

  val ASSUM_LIST     : (thm list -> tactic) -> tactic
  val POP_ASSUM      : thm_tactic -> tactic
  val pop_assum      : thm_tactic -> tactic
  val POP_LAST_ASSUM : thm_tactic -> tactic
  val pop_last_assum : thm_tactic -> tactic
  val PRED_ASSUM     : (term -> bool) -> thm_tactic -> tactic
  val PAT_ASSUM      : term -> thm_tactic -> tactic
  val PAT_X_ASSUM    : term -> thm_tactic -> tactic
  val POP_ASSUM_LIST : (thm list -> tactic) -> tactic
  val SUBGOAL_THEN   : term -> thm_tactic -> tactic
  val USE_SG_THEN    : thm_tactic -> int -> int -> list_tactic
  val CHANGED_TAC    : tactic -> tactic
  val check_delta    : exn -> (goal * goal list -> bool) -> tactic -> tactic
  val count0         : (term -> int) -> (goal * goal list -> bool)
  val count_decreases: (term -> int) -> (goal * goal list -> bool)


  val Q_TAC0         : {traces : (string * int) list} -> hol_type option ->
                       (term -> tactic) -> term quotation -> tactic
  val Q_TAC          : (term -> tactic) -> term quotation -> tactic
  val QTY_TAC        : hol_type -> (term -> tactic) -> term quotation -> tactic

  val default_prover_in : Context.t -> term * tactic -> thm
  val default_prover : term * tactic -> thm
  val set_prover     : (Context.t -> goal * tactic -> thm) -> unit
  val restore_prover : unit -> unit

end

HOL 4, Trindemossen-2