Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Propositions: value vs lemma


view this post on Zulip Email Gateway (Aug 19 2022 at 10:16):

From: Jonathan Balkind <0807932B@student.gla.ac.uk>
Hi there,

I've been trying to formulate a proof based on some functions that I've created and I've become a little confused. While I've tried to search a little through the mailing list for related questions, I had trouble because I'm looking for something involving three common keywords in Isabelle.

Essentially I've got a proposition which I can use the "value" command to evaluate as True, in the form of a proposition. However, when I try making this into a lemma of the same form, I seem to be unable to prove it using any of the proof methods I'm aware of. What approaches does value use to evaluate its argument, and can I apply those methods via apply in proof mode too? Otherwise, could you point me toward what assumption I might be making that could be incorrect? I've also tried nitpick, which showed no counterexamples to this proposition.

value "(circ1 [False, False] [x, y] 2) ≡ [False, False, False]"
lemma "(circ1 [False, False] [x, y] 2) ≡ [False, False, False]"

I'm probably just making a ridiculous rookie error, so any help here would be much appreciated.

Thanks,
Jonathan

view this post on Zulip Email Gateway (Aug 19 2022 at 10:16):

From: Christian Sternagel <c.sternagel@gmail.com>
Could you also post the definition of circ1? (Remark: it would be more
standard to use "=" instead of "==".)

cheers

cheers

view this post on Zulip Email Gateway (Aug 19 2022 at 10:17):

From: Tobias Nipkow <nipkow@in.tum.de>
Chances are that your lemma can be proved "by eval".

Tobias

view this post on Zulip Email Gateway (Aug 19 2022 at 10:17):

From: "C. Diekmann" <diekmann@in.tum.de>
Not sure if this is helpful:
sledgehammer was always helpful in such cases for me.
Did you unfold all definitions?

Cornelius


Last updated: Mar 28 2024 at 16:17 UTC