Search code examples
dictionaryisabelleisar

Can I "map" an "OF" over a list of lemmas

I just wrote this code:

lemmas gc_step_intros =
  normal[OF step.intros(1)] normal[OF step.intros(2)] normal[OF step.intros(3)]
  normal[OF step.intros(4)] normal[OF step.intros(5)] drop

where step.intros really only has 5 lemmas. Is there a convenient way to avoid this repetition, i.e. something that might look like the following?

lemmas gc_step_intros = normal[OF_EACH step.intros] drop
Solution

  • You can use THEN instead of OF and exploit the fact that an attribute is applied to all theorems in a list of theorems. The following should do what you want:

    lemmas gc_step_intros = step.intros[THEN normal] drop