1\DOC 2 3\TYPE {mp_then : thm_tactic -> match_position -> thm -> thm -> tactic} 4 5\SYNOPSIS 6Matches two theorems against each other and then continues 7 8\KEYWORDS 9Tactic 10 11\DESCRIBE 12The {mp_then} tactic combines two theorems (one or both of which will 13typically come from the current goal's assumptions) using modus ponens 14in a controlled way, and then passes the result of this to a 15continuation theorem-tactic. 16 17Thus {mp_then ttac pos ith th} is a tactic in the usual ``{_then}'' 18fashion which produces a theorem and then applies the {ttac} 19continuation to that result. The theorems {ith} and {th} are the two 20theorems: {ith} contains the implication, and the other has a 21conclusion matching one of the antecedents of the implication. 22 23An implication's antecedents are calculated by first normalising the implication so that it is of the form 24{ 25 !v1 .. vn. ant1 /\ ant2 .. /\ antn ==> concl 26} 27 28The {pos} parameter indicates how to find the antecedent. There are 29four possible forms for {pos} (constructors for the type 30{mp_then.match_position}). It can be {Any}, which tells {mp_then} to 31search for anything that works. It can be {Pat q}, with {q} a 32quotation, which means to find anything matching {q} that works. It 33can be {Pos f}, where {f} is a function of type {term list -> term}, 34and is typically a value such as {hd}, {el n} for some number {n} or 35{last}. This function is passed the list of all {ith}'s antecedents to 36pick the right one. Finally, the {pos} parameter might be {Concl}, 37meaning that the conclusion of {ith} is treated as a negated 38assumption. This allows implications to be used in a contrapositive 39way. 40 41In practice, there are some common patterns for obtaining {ith} and 42{th}. Apart from the fully applied version above, you might also see: 43{ 44 <sel>_assum (mp_then pos ttac ith) 45 46 <sel>_assum (<sel>_assum o mp_then pos ttac) 47 48 disch_then(<sel>_assum o mp_then pos ttac) 49} 50where {<sel>} is one of {first}, {last}, {qpat} and {goal}, possibly 51with an appended {_x}; the usual ways of obtaining theorems from the 52current goal. Where there are two selectors used, the outermost is 53used for the selection of {th} and the innermost selects the 54implicational theorem. In the first example, the {ith} value is 55provided in the call, and is presumably an existing theorem rather 56than an assumption from the goal. 57 58The {goal_assum} selector is worth special mention since it's 59especially useful with {mp_then}: it turns an existentially quantified 60goal {?x. P x} into the assumption {!x. P x ==> F} thereby providing a 61theorem with antecedents to match on. In conjunction with {mp_then} it 62has the effect of instantiating the existential quantifier in order to 63match a provided subterm (similar to {part_match_exists_tac} or 64{asm_exists_tac}). 65 66Finally, note that the {Pat} and {Any} position selectors will 67backtrack across the set of theorem antecedents to find a match that 68makes the whole application succeed. 69 70\FAILURE 71If the provided implicational theorem doesn't have a match at a 72compatible position for the second provided theorem, or if no such 73match then allows the continuation {ttac} to succeed. 74 75 76\ENDDOC 77