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