matcher
DB.matcher : (term -> term -> 'a) -> string list -> term -> data list
All theory elements matching a given term.
An invocation matcher pm [thy1,...,thyn] M collects all elements of
the theory segments thy1,...,thyn that have a subterm N such that
pm M does not fail (raise an exception) when applied to N. Thus
matcher potentially traverses all subterms of all theorems in all the
listed theories in its search for 'matches'.
If the list of theory segments is empty, then all currently loaded
segments are examined. The string "-" may be used to designate the
current theory segment.
Failure
Never fails, but may return an empty list.
Example
> DB.matcher match_term ["relation"] (Term `P \/ Q`);
val it =
[(("relation", "IN_RDOM_RUNION"),
(⊢ x ∈ RDOM (R1 ∪ᵣ R2) ⇔ x ∈ RDOM R1 ∨ x ∈ RDOM R2, Thm,
Located
{exact = true, linenum = 2392, scriptpath =
"$(HOLDIR)/src/relation/relationScript.sml"})),
(("relation", "RC_DEF"),
(⊢ ∀R x y. RC R x y ⇔ x = y ∨ R x y, Def, Unknown)),
(("relation", "RINSERT"),
(⊢ ∀R a b. RINSERT R a b = (λx y. R x y ∨ x = a ∧ y = b), Def, Unknown)),
(("relation", "RTC_cases"),
(⊢ ∀R a0 a1. R꙳ a0 a1 ⇔ a1 = a0 ∨ ∃y. R a0 y ∧ R꙳ y a1, Thm, Unknown)),
(("relation", "RTC_CASES1"),
(⊢ ∀R x y. R꙳ x y ⇔ x = y ∨ ∃u. R x u ∧ R꙳ u y, Thm,
Located
[...Output elided...]
> DB.matcher (ho_match_term [] empty_varset) [] (Term `?x. P x \/ Q x`);
<<HOL message: inventing new type variable names: 'a>>
val it =
[(("arithmetic", "ODD_OR_EVEN"),
(⊢ ∀n. ∃m. n = SUC (SUC 0) * m ∨ n = SUC (SUC 0) * m + 1, Thm,
Located
{exact = true, linenum = 1571, scriptpath =
"$(HOLDIR)/src/num/theories/arithmeticScript.sml"})),
(("bool", "EXISTS_OR_THM"),
(⊢ ∀P Q. (∃x. P x ∨ Q x) ⇔ (∃x. P x) ∨ ∃x. Q x, Thm,
Located
{exact = true, linenum = 1604, scriptpath =
"$(HOLDIR)/src/bool/boolScript.sml"})),
(("bool", "LEFT_OR_EXISTS_THM"),
(⊢ ∀P Q. (∃x. P x) ∨ Q ⇔ ∃x. P x ∨ Q, Thm,
Located
[...Output elided...]
Comments
Usually, pm will be a pattern-matcher, but it need not be.