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