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