Re: [isabelle] lexical matters

On a related topic, what does Isabelle do for parsing/printing irregular
variable/constant names?  E.g. a variable with a space in its name.  Is it
possible to parse such a variable name, and, whether it is or not, what does
the printer output?


on 16/1/11 12:45 PM, Makarius <makarius at> wrote:

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

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