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: Feb 27 2024 at 08:17 UTC