Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Question to "lemmas" - instruction

view this post on Zulip Email Gateway (Aug 18 2022 at 10:22):

From: Thomas Goethel <tgoethel@cs.tu-berlin.de>
Hello,

If I have a have a lemma like
lemma two_prime: "isPrime 2"
and a definition
constdefs a:: nat
"a == 2"
then it is of course possible to prove "isPrime a".

This prove is very trivial, so I would like to use the "lemmas" - instruction
of Isabelle.
lemmas a_prime = two_prime [...]
Does a method exist to reach this goal?

Bye,
Thomas

view this post on Zulip Email Gateway (Aug 18 2022 at 10:22):

From: Amine Chaieb <chaieb@in.tum.de>
You can use

lemmas a_prime = two_prime [unfolded a_def[symmetric]]

Amine.

Thomas Goethel wrote:

view this post on Zulip Email Gateway (Aug 18 2022 at 10:24):

From: Brian Huffman <brianh@cs.pdx.edu>
Equivalently, you can use
lemmas a_prime = two_prime [folded a_def]

Last updated: Nov 21 2024 at 12:39 UTC