Email Gateway (Aug 19 2022 at 11:42): Email Gateway (Aug 19 2022 at 11:42):From: Lars Noschinski <noschinl@in.tum.de>
Hi,
I want to write a toplevel command which takes a theorem and some
options as input and creates a list of theorems (hence I cannot use an
attribute) from that.
In an attribute I would use the Attrib.thm parser to parse the input
theorem. Is Parse_Spec.xthm the right thing to use in a command, or is
there something more ready-made, where I don't need to care about
applying the attributes myself?
-- Lars
Email Gateway (Aug 19 2022 at 11:42):From: Makarius <makarius@sketis.net>
For outer syntax commands, the parser does not know the context yet, so
the actual formal content is only produced later when the command
transaction is applied. For example, this works for terms via Parse.term
and Syntax.read_term, with many canonical examples found in the libraries.
For facts it is more difficult to find examples, since passing theorems to
tools is relatively rare (such tools are often ports from HOL4).
Normally the proof problem is exposed to the user as a proof state,
potentially with multiple conclusions, which is then solved by standard
means. Often the proof is just ".", ".." or "by (fact myfacts)+". See
for example the 'rep_datatype' command.
If you really need to pass facts directly, it can be done like "inductive
monos ...", which uses Parse_Spec.xthms1 and Attrib.eval_thms.
Makarius
Email Gateway (Aug 19 2022 at 11:43):From: Lars Noschinski <noschinl@in.tum.de>
Thanks for the pointers.
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).
Makarius <makarius@sketis.net> schrieb:
Email Gateway (Aug 19 2022 at 11:43):From: Makarius <makarius@sketis.net>
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
Last updated: Nov 21 2024 at 12:39 UTC