Email Gateway (Aug 18 2022 at 10:22): 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
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:
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: May 03 2024 at 12:27 UTC