Re: [isabelle] Which parser to use for theorems in a toplevel-command?
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 at sketis.net> schrieb:
>On Mon, 26 Aug 2013, Lars Noschinski wrote:
>> I want to write a toplevel command which takes a theorem and some options as
>> input and creates a list of theorems
>> 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?
>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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and