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).


	Makarius




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