What is the best way to search through general definitions, theorems, functions, etc for Isabelle?

Question

I was trying to go through the Isar chapter for Isabelle (theorem Prover) and the first statement has:

lemma "¬ surj(f :: 'a ⇒ 'a set)"

I wanted to understand what the constant surj was. I know that it's easy to look up theorems with:

thm notI

which displays:

(?P ⟹ False) ⟹ ¬ ?P

I tried googling surj but nothing useful came up.

I went to the documentation (https://isabelle.in.tum.de/documentation.html) but I couldn't find an easy way to search through it (e.g. with a search bar).

How do people search for definitions or general stuff when doing proofs? How do you look up things for Isabelle in an effective manner without having to resort to SO etc for trivial stuff (that I should probably be able to look up myself)? Like a man command or a -help flag etc?

---

I realized that there is a Query box at the bottom so I gave it a go. But it showed me 38 theorems. Thats good progress BUT I feel that because when I stated my lemma Isabelle knows exactly which one it is using. Is there a way to force Isabelle to reveal what definition it's using (since it obviously HAS to know what it's using).

---

I just noticed that:

thm surj_def

displays:

surj ?f = (∀y. ∃x. y = ?f x)

does display something...the question was worth it cuz I discovered the Query box but it would still be great how people develop in Isabelle regardless.

---

Edit:

it would also be nice if it linked to docs of tactics explaining what they did or something like that...

Addressee

Answer 1

If you have loaded the theory, you can jump to the definition by ctrl+click.

If not, and you don't know where the constant is defined, you can use the FindFacts web search (full disclaimer: I built it).

Here is a query for your surj question.

Recency

I tried searching blast (search.isabelle.in.tum.de/#search/…) but nothing came up. Is that a bug? What are the limits of your tool? – Addressee

Are you sure that that's the correct link? Because that query is empty. When I search for blast, I get the definition. – Recency

Seems like your tool does not work for Chrome, probably the issue. I tried a new search for auto and it gave me way too much. Perhaps a small markdown tutorial (+ 5 minute video) of how to use would make your tool more usable. Seems to have a lot of potential. – Addressee

Thanks. There is an extensive help page that explains usage, as well as an example page that gives an interactive walk-through for typical search scenarios. Regarding your browser Issue, could you tell me the exact version and the Issue you had? The tool is cross-tested with the most popular browsers and should work without problems. – Recency