Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] parse translations and lexical matters

Email Gateway (Aug 18 2022 at 16:55):

From: Matthias Schmalz <Matthias.Schmalz@inf.ethz.ch>
-----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-----

Last updated: Nov 21 2024 at 12:39 UTC