Re: [isabelle] lexical matters

On Fri, 14 Jan 2011, Matthias Schmalz wrote:

2. I am translating terms from some other logic (i.e., Event-B) to Isabelle/HOL. For that I need to know which identifiers (i.e., tokens of the category ident, p. 28 of the reference manual) I can use as variable names.

I do already know that I cannot use the tokens listed in the section "lexicon" of the output of "print_syntax". I have also discovered that tokens with a trailing underscore and the token "dummy_pattern" cannot be used as variable names. I wonder whether there are more such tokens and how I can get an at least approximate list of them.

It depends what you want to do in the end. Generating sources that are fed back into the system is inherently hard. I have occasionally seen people doing it empirically, e.g. trying Syntax.read_term on some identifier and checking if they get a "Free" term -- but this does not really take the scoping rules of const vs. free vs. bound into account.

Unless your output needs to be inspected directly by users it is easier to avoid generating sources altogether, and use the Isabelle/ML interfaces to get logical content into the system. This is the norml way in LCF-style provers. Concrete syntax is just a superficial add-on for end-users.


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