stating multiple lemmas simultaneously

[lsf37]

We often want to state a set of lemmas that all have the same proof and all have the same form, but differ in what function they are applied to or what property the function is preserving or both.

I.e. we might say

crunch f, g
  p1: prop1
  p2: prop2

and get 4 lemmas out of this.

But sometimes the property is not crunchable, or we are not stating something that is a Hoare triple, etc.

We could imagine a command like the following

lemma_instances name[attribs]:
   "f {| %s. P (c s) |}"
   where f = some_fun, some_other_fun
   and c = proj1, proj2
   <proof>

This would generate the following goal statements:

   name_some_fun_proj1[attribs]: "some_fun {| %s. P (proj1 s) |}"
   name_some_fun_proj2[attribs]: "some_fun {| %s. P (proj2 s) |}"
   name_some_other_fun_proj1[attribs]: "some_other_fun {| %s. P (proj1 s) |}"
   name_some_other_fun_proj2[attribs]: "some_other_fun {| %s. P (proj2 s) |}"

and switch into proof mode, so that normal apply scripts or Isar proofs can commence from here.

There could be more than two instantiations. The command would need to try to extract the name from the constants provided, but that only works if the instances are all directly constants (we could allow arbitrary terms).

The main use case would be to state projection preservation lemmas over multiple predicates (invs, valid_state, etc) or over monads.

I'm not quite sure if the attributes always want to be the same for all of them. They could be accumulative, if we annotated/named each of the clauses.

[lsf37]

This is still a bit half baked and needs more refinement (the concrete syntax in any case, but also the concept).

One potential consequence of having this is that you might need a proof method that can figure out what you want to unfold. In the example above for instance, you are likely to want to unfold some_fun_def and some_other_fun_def, but if you have to list those theorem names in the proof method then you immediately get duplication of those names and it becomes annoying to add another function.

Of course such a method could be written. Maybe it would get a pattern where to expect a constant in the goal term and then use the same unfolding logic that crunch currently uses. (With the benefit that crunch could then use this more general method).