CASE_TAC : tactic
STRUCTURE
SYNOPSIS
Case splits on a term t that features in the goal as case t of ..., and then performs some simplification.
DESCRIPTION
BasicProvers.CASE_TAC first calls BasicProvers.PURE_CASE_TAC, which searches the goal for an instance of case t of ... and performs a BasicProvers.Cases_on `t`. If this succeeds, it then simplifies the goal using definitions of case constants, plus distinctness and injectivity theorems for datatypes.
COMMENTS
When there are multiple case constants in the goal, it can be very convenient to execute the tactic REPEAT CASE_TAC. bossLib.CASE_TAC is the same as BasicProvers.CASE_TAC.
FAILURE
BasicProvers.CASE_TAC fails precisely when BasicProvers.PURE_CASE_TAC fails.
SEEALSO
HOL  Kananaskis-14