1\DOC match
2
3\TYPE {match : string list -> term -> data list}
4
5\SYNOPSIS
6Attempt to find matching theorems in the specified theories.
7
8\KEYWORDS
9matching, database.
10
11\DESCRIBE
12An invocation {DB.match [s1,...,sn] M} collects all theorems, definitions,
13and axioms of the theories designated by {s1},...,{sn} that have a subterm
14that matches {M}. If there are no matches, the empty list is returned.
15
16The strings {s1},...,{sn} should be a subset of the currently loaded
17theory segments. The string {"-"} may be used to designate the
18current theory segment. If the list of theories is empty, then all
19currently loaded theories are searched.
20
21\FAILURE
22Never fails.
23
24\EXAMPLE
25{
26- DB.match ["bool","pair"] (Term `(a = b) = c`);
27<<HOL message: inventing new type variable names: 'a>>
28> val it =
29    [(("bool", "EQ_CLAUSES"),
30      (|- !t.((T = t) = t) /\ ((t = T) = t) /\
31             ((F = t) = ~t) /\ ((t = F) = ~t), Db.Thm)),
32     (("bool", "EQ_EXPAND"),
33      (|- !t1 t2. (t1 = t2) = t1 /\ t2 \/ ~t1 /\ ~t2, Db.Thm)),
34     (("bool", "EQ_IMP_THM"),
35      (|- !t1 t2. (t1 = t2) = (t1 ==> t2) /\ (t2 ==> t1), Db.Thm)),
36     (("bool", "EQ_SYM_EQ"), (|- !x y. (x = y) = (y = x), Db.Thm)),
37     (("bool", "FUN_EQ_THM"), (|- !f g. (f = g) = !x. f x = g x, Db.Thm)),
38     (("bool", "OR_IMP_THM"), (|- !A B. (A = B \/ A) = B ==> A, Db.Thm)),
39     (("bool", "REFL_CLAUSE"), (|- !x. (x = x) = T, Db.Thm)),
40     (("pair", "CLOSED_PAIR_EQ"),
41      (|- !x y a b. ((x,y) = (a,b)) = (x = a) /\ (y = b), Db.Thm)),
42     (("pair", "CURRY_ONE_ONE_THM"),
43      (|- (CURRY f = CURRY g) = (f = g), Db.Thm)),
44     (("pair", "PAIR_EQ"), (|- ((x,y) = (a,b)) = (x = a) /\ (y = b), Db.Thm)),
45     (("pair", "UNCURRY_ONE_ONE_THM"),
46      (|- (UNCURRY f = UNCURRY g) = (f = g), Db.Thm))] :
47  ((string * string) * (thm * class)) list
48}
49
50
51\COMMENTS
52The notion of matching is a restricted version of higher-order matching.
53
54\USES
55For locating theorems when doing interactive proof.
56
57\SEEALSO
58DB.matcher, DB.matchp, DB.find, DB.theorems, DB.thy, DB.listDB, holyHammer.hh.
59\ENDDOC
60