HOL: Reference

match

DB.match : string list -> term -> data list

Attempt to find matching theorems in the specified theories.

An invocation DB.match [s1,...,sn] M collects all theorems, definitions, and axioms of the theories designated by s1,...,sn that have a subterm that matches M. If there are no matches, the empty list is returned.

The strings s1,...,sn should be a subset of the currently loaded theory segments. The string "-" may be used to designate the current theory segment. If the list of theories is empty, then all currently loaded theories are searched.

Failure

Never fails.

Example

> DB.match ["bool","pair"] (Term `(a = b) = c`);
<<HOL message: inventing new type variable names: 'a>>
val it =
   [(("bool", "bool_case_eq"),
     (⊢ (if x then t1 else t2) = v ⇔ (x ⇔ T) ∧ t1 = v ∨ (x ⇔ F) ∧ t2 = v,
      Thm,
      Located
       {exact = true, linenum = 3552, scriptpath =
        "$(HOLDIR)/src/bool/boolScript.sml"})),
    (("bool", "EQ_CLAUSES"),
     (⊢ ∀t. ((T ⇔ t) ⇔ t) ∧ ((t ⇔ T) ⇔ t) ∧ ((F ⇔ t) ⇔ ¬t) ∧ ((t ⇔ F) ⇔ ¬t),
      Thm,
      Located
       {exact = true, linenum = 1310, scriptpath =
        "$(HOLDIR)/src/bool/boolScript.sml"})),
    (("bool", "EQ_EXPAND"),
[...Output elided...]

Comments

The notion of matching is a restricted version of higher-order matching.

For locating theorems when doing interactive proof.

See also

DB.matcher, DB.matchp, DB.find, DB.theorems, DB.thy, DB.listDB