Re: [isabelle] lemma tempates
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 "
lemma zero: "f 0 = 0" ...
Now you can instantiate X with f, g, h:
(the name before the column is the name of the interpretation used to
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:
Am Dienstag, den 22.07.2014, 18:21 -0700 schrieb Vadim Zaliva:
> 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?
> 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