DISJ_CASES_THEN : thm_tactical
Applies a theorem-tactic to each disjunct of a disjunctive theorem.
If the theorem-tactic f:thm->tactic applied to either
ASSUMEd disjunct produces results as follows when applied to a goal
(A ?- t):
then applying DISJ_CASES_THEN f (|- u \/ v)
to the goal (A ?- t) produces two subgoals.
A ?- t A ?- t
========= f (u |- u) and ========= f (v |- v)
A ?- t1 A ?- t2
A ?- t
====================== DISJ_CASES_THEN f (|- u \/ v)
A ?- t1 A ?- t2
- FAILURE CONDITIONS
Fails if the theorem is not a disjunction. An invalid tactic is
produced if the theorem has any hypothesis which is not
alpha-convertible to an assumption of the goal.
Given the theorem
and a goal of the form ?- (PRE m = m) = (m = 0),
applying the tactic
th = |- (m = 0) \/ (?n. m = SUC n)
produces two subgoals, each with one disjunct as an added
DISJ_CASES_THEN MP_TAC th
# let th = SPEC `m:num` num_CASES;;
val th : thm = |- m = 0 \/ (?n. m = SUC n)
# g `PRE m = m <=> m = 0`;;
Warning: Free variables in goal: m
val it : goalstack = 1 subgoal (1 total)
`PRE m = m <=> m = 0`
# e(DISJ_CASES_THEN MP_TAC th);;
val it : goalstack = 2 subgoals (2 total)
`(?n. m = SUC n) ==> (PRE m = m <=> m = 0)`
`m = 0 ==> (PRE m = m <=> m = 0)`
Building cases tactics. For example, DISJ_CASES_TAC could be defined by:
let DISJ_CASES_TAC = DISJ_CASES_THEN ASSUME_TAC
Use DISJ_CASES_THEN2 to apply different tactic generating functions
to each case.
- SEE ALSO
STRIP_THM_THEN, CHOOSE_THEN, CONJUNCTS_THEN, CONJUNCTS_THEN2,
DISJ_CASES_TAC, DISJ_CASES_THEN2, DISJ_CASES_THENL.