Email Gateway (Aug 19 2022 at 15:01): Email Gateway (Aug 19 2022 at 15:01):From: Vadim Zaliva <vzaliva@cmu.edu>
Hi!
I have several functions for all of which I need to prove some trivial lemmas.
For example
lemma f0: "f 0 = 0"
lemma g0: "g 0 = 0"
lemma h0: "h 0 = 0"
These lemmas might be used further in more complex proofs so I would like them to
be named. As I add more functions I will need to instantiate these lemmas
for newly added ones easily. What would be the best way to do this?
Thanks!
Sincerely,
Vadim Zaliva
Email Gateway (Aug 19 2022 at 15:01):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Vadim,
The best approach is to use locales:
You define a locale X over a function f, and proof the lemma zero:
locale X =
fixes f :: "'a "
assumes "..."
begin
lemma zero: "f 0 = 0" ...
end
Now you can instantiate X with f, g, h:
(the name before the column is the name of the interpretation used to
name the
interpreted lemmas, i.e. f.zero)
interpret f: X f ...
interpret g: X g ...
interpret h: X h ...
You can also find a locales-tutorial on the website:
http://isabelle.in.tum.de/documentation.html
Last updated: Nov 21 2024 at 12:39 UTC