I'm very new to Isabelle and I'm trying to automatically extract definitions and lemmas that appear in a proof. For example in the following lemma:

lemma step_suc_sem: \<open>step (n,\<sigma>) = (suc n \<sigma>, sem n \<sigma>)\<close> unfolding suc_def sem_def by auto

Since suc/sem are in my list of identifiers, I can see they appear in the proof. Moreover, when something ends in _def I can check to see which identifier appears before it. However when I encounter a term like "linorder_neqE_nat" even though linorder is in my list of identifiers it's not clear which options can appear at the end of linorder from the definition I find associated to it. Maybe this doesn't come from the definition of linorder at all and is just the name of a lemma, but when I checked the Nat.thy file I didn't recognize the syntax with which the term appeared - my understanding is lemmas show up in the form "lemma <name> : <statement>".

In any case, I want to know if there's a list of ways a definition or lemma can make an appearance in a proof, syntactically speaking. I couldn't tell from checking the Isabelle manual. Thanks.

Do you want a

```
proof -> identifier list
```

function that gives you the used functions, datatypes and lemmas?

This looks like the type of an ML function to me. I guess @Andreas Gittis doesn’t want to do ML meta-programming but is rather looking for a tool he can use in the IDE.

@Wolfgang Jeltsch this was just pseudocode to make the question more precise

@Gergely Buday Yes exactly

Last updated: Jun 20 2024 at 12:31 UTC