*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Which parser to use for theorems in a toplevel-command?*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Mon, 26 Aug 2013 15:45:58 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>

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

**Follow-Ups**:

- Previous by Date: Re: [isabelle] frequent jEdit crash (Mac OS10.8.4; Isabelle 2013)
- Next by Date: Re: [isabelle] Which parser to use for theorems in a toplevel-command?
- Previous by Thread: Re: [isabelle] Which parser to use for theorems in a toplevel-command?
- Next by Thread: Re: [isabelle] Which parser to use for theorems in a toplevel-command?
- Cl-isabelle-users August 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list