Search code examples
isabelle

Combine OF and of

I recently began using more OF as a way to discharge assumptions of a lemma with local theorems. I also use of as a way to give concrete values to the variables of a theorem. For instance in the following theorem:

periodic ?f ?k ⟹
0 < ?k ⟹
0 < ?d ⟹ sum ?f {0..?k - 1} = sum ?f {?d..?d + ?k - 1}

I would like to discharge periodic ?f ?k and 0 < ?k with OF and then apply of to instantiate ?d = 1. The current way I do this is by a two step process:

note lem = my_lemma[OF ...]
using lem[of ...]

I was wondering if there is a more elegant syntax for this.

Solution

  • You can just write my_lemma[OF …, of …, OF …, of …] etc. This works for any attribute, e.g. my_lemma[OF …, where x = …, simplified, symmetric]