Re: [isabelle] Hidding the "int", "nat" and "real" conversion functions



Try the following:

translations
  "N" <= "CONST of_nat N"
  "N" <= "CONST int N"

The "CONST" ensures that the following token is interpreted as the name of a constant, and not a variable.

In your example, you entered
  translations "N" <= "of_nat N"

and the system thought you meant
  translations "N" <= "M N"

which explains why "int 1 + 2" would print out as just "2".

In Isabelle, before the syntax translation mechanism sees a term, most constants are annotated with a "\<^const>" flag; "CONST" ensures that the translation rule works correctly with this flag. (Try ML "set Syntax.trace_ast" if you want to see what's really going on.) This flagging system makes syntax translations more robust, and prevents weird things from happening when you have a variable whose name is also the name of a constant.

However, constants declared using the old-style "consts" command (including, you guessed it, List.set) are not flagged in this manner. This is the only reason why translations "N" <= "set N" actually works at all.

- Brian


Quoting Johannes Hoelzl <hoelzl at in.tum.de>:

I want to hide the "int", "nat" and "real" conversion functions when
Isabelle outputs an term. So that a term like
"nat (x * int y - f (int z))" gets written as "x * y - f z" human users
are usually capable of interfering the correct conversion functions.

First I tried to just add a translation:
translations
"N" <= "of_nat N" (* "int" do not work, it is represented as "of_nat" internally *)

term "int 1 + 2"
(* output: "2"  HUH! *)

This breaks the entire output process! Is this a bug in the pretty
printer or should I just not add this translation. In OptionalSugar the
same is done with the "set :: 'a list => 'a set" conversion function!

As alternative I'm currently using a notation:

notation (output) int ("_" 70)
term "x * int (a + b) + f (int a)"
(* output: "x * (a + b) + f (a)" *)

This nearly works, but I don't get rid of the parenthesis around the
function parameter. I tried several other precedencies but no one
worked. There are parenthesis around the function parameter or the
parenthesis around the addition are missing.

Has anyone a solution to this problem?

Regards,
   Johannes Hölzl












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