[isabelle] parse translations and lexical matters



-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hi,

I have two questions:

1. Consider the following contrieved parse translation translating
"foo x. t" to "(\<forall> x. t) \<and> (\<forall> x. t)":

syntax
  "_foo" :: "idt => 'a => bool" ("foo _. _")

parse_translation {*
let
  val forall_tr = snd (mk_binder_tr ("\<forall> ", @{const_syntax All}))
  fun foo_tr [idt, t] =
    let
      val all = forall_tr [idt, t]
    in
      @{const "op &"} $ all $ all
    end
in [(@{syntax_const "_foo"}, foo_tr)] end
*}

When I execute
term "foo x. True"
(with show_types activated) I get
"(\<forall> x::'a. True) \<and> (\<forall> x::'b. True)".
(The two occurrences of x have different types.)

Is it possible to change the parse translation so that
term "foo x. True"
yields "(\<forall> x::'a. True) \<and> (\<forall> x::'a. True)".
(The two occurrences of x have the same type.)

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.

Thanks for any help,
Matthias
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFNMLQBczhznXSdWggRAp7UAJ9M74KKj3Lid6OTneUENvnwms2TXACgprT9
CedcBF7gH5x5ArSZC5M04sg=
=UBu+
-----END PGP SIGNATURE-----





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