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


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