Re: [isabelle] Syntax translation for types

Hi Andreas,

Isabelle complains that variable a occurs twice in "a list × int × a list".
checking that both "a" are the same goes beyond pattern matching, and hence Isabelle complains.

With an ML print-translation you can actually check wether both occurrences of "a" are the same.
Here is the code:

types 'a my_type = "('a list × int × 'a list)"

print_translation {*
fun tr' [Const ("list",_)$a1, Const ("*",_)$Const ("int",_)$(Const ("list",_)$a2)] =
    if a1=a2 then Syntax.const "my_type"$a1
    else raise Match;
in [("*",tr')]

The syntax tree for applying print-translations is internally represented as Isabelle "terms", for both HOL terms and types.

So ('a list × int × 'a list)


Const ("*",_)$(Const ("list",_)$a1$(Const ("*",_)$Const ("int",_)$ (Const ("list",_)$a2)))

Not that a 3-tuple is a nested pair: ('a list × (int × 'a list)).

The outermost "*" is already removed by declaring tr' as a print translation for "*".
tr' takes a list of the remaining arguments.
In case a print-translation does not match, or you explicitly "raise Match" it is not applied and Isabelle checks for other matching translations.



On 06.10.2009, at 08:49, Andreas Lochbihler wrote:


I would like to have Isabelle print types using the type abbreviations I have introduced with "types". To that end, I have come across translations for types that work reasonably well if type variables occur only once. However, I fail to make it work for type abbreviation like this:

types 'a my_type = "('a list × int × 'a list)"

 "my_type a" <= (type) "a list × int × a list"

Isabelle complains that variable a occurs twice in "a list × int × a list". How can I set up an appropriate print translation for such a type abbreviation? Do I need to write an ML translation function? If so, how can I find out how to do that? Or is there any better support other than translations (similar to abbreviation for constants)?


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