HOL: Reference

apropos_in

DB.apropos_in : term -> data list -> data list

Attempt to select matching theorems among a given list.

An invocation DB.apropos_in M data_list selects all theorems, definitions, and axioms within data_list that have a subterm that matches M. If there are no matches, the empty list is returned.

Failure

Never fails.

Example

> DB.apropos (Term `(!x y. P x y) ==> Q`);
<<HOL message: inventing new type variable names: 'a, 'b>>
val it =
   [(("bool", "LCOMM_THM"),
     (⊢ ∀f. (∀x y z. f x (f y z) = f (f x y) z) ⇒
            (∀x y. f x y = f y x) ⇒
            ∀x y z. f x (f y z) = f y (f x z), Thm,
      Located
       {exact = true, linenum = 4445, scriptpath =
        "$(HOLDIR)/src/bool/boolScript.sml"})),
    (("cardinalityCore", "CARD_EQ_IMAGE"),
     (⊢ ∀f s.
          (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒ cardeq (IMAGE f s) s,
      Thm,
      Located
       {exact = true, linenum = 2268, scriptpath =
[...Output elided...]

> DB.apropos_in (Term `(x, y)`) it ;
  [(("pair", "pair_induction"),
    (|- (!p_1 p_2. P (p_1,p_2)) ==> !p. P p, Thm))] :
  ((string * string) * (thm * class)) list
Exception- unknown symbol .
unknown symbol .
Fail "Static Errors" raised

Comments

The notion of matching is a restricted version of higher-order matching. It uses DB.matches.

Finding theorems in interactive proof sessions. The second argument will normally be the result of a previous call to DB.find, DB.match, DB.apropos, DB.listDB, DB.thy etc.

See also

DB.apropos, DB.match, DB.matches, DB.find, DB.find_in, DB.listDB, DB.thy, DB.theorems