ASM_CASES_TAC : term -> tactic

- SYNOPSIS
- Given a term, produces a case split based on whether or not that term is true.
- LIBRARY
- bool
- STRUCTURE
- DESCRIPTION
- Given a term u, ASM_CASES_TAC applied to a goal produces two subgoals, one with u as an assumption and one with ~u:ASM_CASES_TAC u is implemented by DISJ_CASES_TAC(SPEC u EXCLUDED_MIDDLE), where EXCLUDED_MIDDLE is the axiom |- !u. u \/ ~u.
A ?- t ================================ ASM_CASES_TAC u A u {u} ?- t A u {~u} ?- t

- FAILURE
- By virtue of the implementation (see above), the decomposition fails if EXCLUDED_MIDDLE cannot be instantiated to u, e.g. if u does not have boolean type.
- EXAMPLE
- The tactic ASM_CASES_TAC u can be used to produce a case analysis on u:
- let val u = Term `u:bool` val g = Term `(P:bool -> bool) u` in ASM_CASES_TAC u ([],g) end; ([([`u`], `P u`), ([`~u`], `P u`)], fn) : tactic_result

- USES
- Performing a case analysis according to whether a given term is true or false.
- SEEALSO

HOL Kananaskis-14