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