# Re: [isabelle] lemma tempates

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 ...
note f.zero g.zero ....
You can also find a locales-tutorial on the website:
http://isabelle.in.tum.de/documentation.html
- Johannes
Am Dienstag, den 22.07.2014, 18:21 -0700 schrieb Vadim Zaliva:
> 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
>
> --
> CMU ECE PhD student
> Mobile: +1(510)220-1060
> Skype: vzaliva
>
>

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*