Re: [isabelle] Which parser to use for theorems in a toplevel-command?

On Mon, 26 Aug 2013, Lars Noschinski wrote:

In my case, the lemma is not used to prove a goal, but is used as a basis to generate new theorems from. My application is transforming between two different styles of lemmas defining a function. A rule attribute would have been my first choice, but these are limited to 1:1 mappings, whereas I need 1:n and m:1 (the form [[my_attr thms]] could be used for m:1, but it feels pretty unusual for rule attributes).

The 1:n or m:1 thing would indeed introduce a lot of additional complexity, for something that is already quite complex. Rule attributes were historically introduced to capture many small ad-hoc operations on theorems, such as "rule_format". It was successful in that respect, but at some costs that we are still paying back until today.

What you describe sounds like a regular 'declaration' within a local theory context. This should all work without requiring to stretch attributes beyond their usual use (although they are in principle as powerful as that).


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.