Stream: Beginner Questions

Topic: `find_theorems "(?a :: nat) + ?b = ?b + ?a"` finds nothing.

Mario Xerxes Castelán Castro (Sep 11 2026 at 01:33):

Why does find_theorems "(?a :: nat) + ?b = ?b + ?a" find nothing, but find_theorems "(?a :: num) + ?b = ?b + ?a" does find Num.add_One_commute? How do I find the theorem about commutativity of natural number addition with find_theorems?

Kevin Kappelmann (Sep 11 2026 at 08:19):

find_theorems on the top level, by default, uses matching: it returns theorems that are instances of your pattern. But you don't want to find instances of the pattern, you want to find theorems of which your pattern is an instance of (the reverse direction).

There's unfortunately no way to flip the matching direction when using find_theorems on the top level (I think you could write a patch to include that and propose that to the mailing list), but you can flip the direction by writing the pattern in a lemma and use it this way:

lemma "(a :: nat) + b = b + a"
find_theorems solves

Note that there are more modifiers next to solves, e.g. intro, dest,...

Kevin Kappelmann (Sep 11 2026 at 08:24):

NB. in order to answer your question, I used PIDE MCP and prompted my coding agent your question to find the cause, which it did in a few seconds.

That's just a shameless plug - I don't mind your questions, but wanna increase adoption of the MCP ;)

David Wang (Sep 12 2026 at 22:15):

Another shameless plug on my part and that of @András Salamon. His isabelle-query tool implemented something like this for callers of a function or constant. I saw that this had a use case and exposed this functionality through jEdit's UI. See the fork.

I have vibe coded an addition for instances/instantiations and code equations as well. It's not done yet, because it doesn't compute the transitive closure of the class hierarchy. It fails in your exact use case. I'll let a Claude session implement this over night. It still works, but might be more suitable for LLMs, who can manually find the closure.

Here's what Claude has to say:

What the fork answers today, from the sources and without a prover. isabelle query instances <class> lists every declared instantiation, instance, interpretation and sublocale site naming the subject. It is the reverse direction of find_theorems: start from the class that owns the lemma and ask who instantiates it.
sh cd <Isabelle>/src/HOL isabelle query instances ab_semigroup_add # 8 direct sites: prod, fun, set, vec, fps, ... no nat isabelle query instances comm_monoid_diff # 3 sites, incl. Nat:213 instantiation nat :: comm_monoid_diff isabelle query callers ab_semigroup_add # the class/subclass declarations that extend it isabelle query enclosing Nat:213 # the block around any reported locus
nat never instantiates ab_semigroup_add by name, so the first command does not list it. The instances verb deliberately excludes hierarchy edges so that a count means one relation. The planned addition is a closure over the class and subclass declarations in the same sources, so that instances ab_semigroup_add can report nat via comm_monoid_diff.

In jEdit. Right-clicking an identifier in a theory buffer adds an Isabelle Query: <name> submenu with Find usages, Find external usages, Find definition, Peek definition, and, when the name resolves to a locale or class, Find instantiations (likewise Find code equations for a constant). Hits land in the Isabelle Query dockable grouped by file; double-click or Enter opens, shift-click opens a new pane, alt-click peeks. The index reads dirty buffers, so the answer arrives before the prover has processed the file.

PIDE MCP. The optional pide_mcp_query component exposes the same CLI as a query tool on the isabelle-pide-mcp server. An agent passes the argument vector and gets back exit, stdout and stderr:
json {"argv": ["-R", "/path/to/Isabelle/src/HOL", "instances", "comm_monoid_diff"]}
The root comes from -R, else from the single directory of the running PIDE session, so an agent can combine this structural answer with a live find_theorems through the prover-side tools on the same server.

David Wang (Sep 12 2026 at 22:50):

On another note, if you install the query fork, its features are exposed through the PIDE MCP as well.

David Wang (Sep 13 2026 at 00:40):

Implemented in the fork. No guarantees that the code is free of bugs.

Last updated: Sep 28 2026 at 16:33 UTC