1\DOC DISJ_CASES_THEN 2 3\TYPE {DISJ_CASES_THEN : thm_tactical} 4 5\SYNOPSIS 6Applies a theorem-tactic to each disjunct of a disjunctive theorem. 7 8\KEYWORDS 9theorem-tactic, disjunction, cases. 10 11\DESCRIBE 12If the theorem-tactic {f:thm->tactic} applied to either 13{ASSUME}d disjunct produces results as follows when applied to a goal 14{(A ?- t)}: 15{ 16 A ?- t A ?- t 17 ========= f (u |- u) and ========= f (v |- v) 18 A ?- t1 A ?- t2 19} 20then applying {DISJ_CASES_THEN f (|- u \/ v)} 21to the goal {(A ?- t)} produces two subgoals. 22{ 23 A ?- t 24 ====================== DISJ_CASES_THEN f (|- u \/ v) 25 A ?- t1 A ?- t2 26} 27 28 29\FAILURE 30Fails if the theorem is not a disjunction. An invalid tactic is 31produced if the theorem has any hypothesis which is not 32alpha-convertible to an assumption of the goal. 33 34\EXAMPLE 35Given the theorem 36{ 37 th = |- (m = 0) \/ (?n. m = SUC n) 38} 39and a goal of the form {?- (PRE m = m) = (m = 0)}, 40applying the tactic 41{ 42 DISJ_CASES_THEN ASSUME_TAC th 43} 44produces two subgoals, each with one disjunct as an added 45assumption: 46{ 47 ?n. m = SUC n ?- (PRE m = m) = (m = 0) 48 49 m = 0 ?- (PRE m = m) = (m = 0) 50} 51 52 53\USES 54Building cases tactics. For example, {DISJ_CASES_TAC} could be defined by: 55{ 56 val DISJ_CASES_TAC = DISJ_CASES_THEN ASSUME_TAC 57} 58 59 60\COMMENTS 61Use {DISJ_CASES_THEN2} to apply different tactic generating functions 62to each case. 63 64\SEEALSO 65Thm_cont.CHOOSE_THEN, Thm_cont.CONJUNCTS_THEN, Thm_cont.CONJUNCTS_THEN2, Thm.DISJ_CASES, Tactic.DISJ_CASES_TAC, Thm_cont.DISJ_CASES_THEN2, Thm_cont.DISJ_CASES_THENL, Thm_cont.STRIP_THM_THEN. 66\ENDDOC 67