Re: [isabelle] Which parser to use for theorems in a toplevel-command?

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