Andreas Gittis (Apr 20 2023 at 04:14): Andreas Gittis (Apr 20 2023 at 04:14):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.
Gergely Buday (Apr 20 2023 at 07:50):Do you want a
proof -> identifier list
function that gives you the used functions, datatypes and lemmas?
Wolfgang Jeltsch (Apr 20 2023 at 13:08):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.
Gergely Buday (Apr 20 2023 at 13:56):@Wolfgang Jeltsch this was just pseudocode to make the question more precise
Andreas Gittis (Apr 20 2023 at 18:38):@Gergely Buday Yes exactly
Last updated: Apr 28 2024 at 16:17 UTC