Stream: Beginner Questions

Topic: Extracting Lemmas and Definitions from Isabelle Proofs


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Gergely Buday (Apr 20 2023 at 13:56):

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

view this post on Zulip Andreas Gittis (Apr 20 2023 at 18:38):

@Gergely Buday Yes exactly


Last updated: Feb 27 2024 at 08:17 UTC