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