1\DOC DISJ_CASES_THEN2 2 3\TYPE {DISJ_CASES_THEN2 : (thm_tactic -> thm_tactical)} 4 5\SYNOPSIS 6Applies separate theorem-tactics to the two disjuncts of a theorem. 7 8\KEYWORDS 9theorem-tactic, disjunction, cases. 10 11\DESCRIBE 12If the theorem-tactics {f1} and {f2}, applied to the {ASSUME}d left and right 13disjunct of a theorem {|- u \/ v} respectively, produce results as follows when 14applied to a goal {(A ?- t)}: 15{ 16 A ?- t A ?- t 17 ========= f1 (u |- u) and ========= f2 (v |- v) 18 A ?- t1 A ?- t2 19} 20then applying {DISJ_CASES_THEN2 f1 f2 (|- u \/ v)} to the 21goal {(A ?- t)} produces two subgoals. 22{ 23 A ?- t 24 ====================== DISJ_CASES_THEN2 f1 f2 (|- 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_THEN2 SUBST1_TAC ASSUME_TAC th 43} 44to the goal will produce two subgoals 45{ 46 ?n. m = SUC n ?- (PRE m = m) = (m = 0) 47 48 ?- (PRE 0 = 0) = (0 = 0) 49} 50The first subgoal has had the disjunct {m = 0} used 51for a substitution, and the second has added the disjunct to the 52assumption list. Alternatively, applying the tactic 53{ 54 DISJ_CASES_THEN2 SUBST1_TAC (CHOOSE_THEN SUBST1_TAC) th 55} 56to the goal produces the subgoals: 57{ 58 ?- (PRE(SUC n) = SUC n) = (SUC n = 0) 59 60 ?- (PRE 0 = 0) = (0 = 0) 61} 62 63 64\USES 65Building cases tacticals. For example, {DISJ_CASES_THEN} could be defined by: 66{ 67 let DISJ_CASES_THEN f = DISJ_CASES_THEN2 f f 68} 69 70 71\SEEALSO 72Thm_cont.STRIP_THM_THEN, Thm_cont.CHOOSE_THEN, Thm_cont.CONJUNCTS_THEN, Thm_cont.CONJUNCTS_THEN2, Thm_cont.DISJ_CASES_THEN, Thm_cont.DISJ_CASES_THENL. 73\ENDDOC 74