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.