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



Hi Johannes,

this "hack" is certainly no replacement for properly hiding constants. By changing the precedences, you can also enforce that parenthesis are used whenever the argument to "int" is not a single identifier:

notation (output) int ("_" [1000] 1000)

This should work for all of your examples, but:

term "x * int (a * b) + f (int a)"
produces: "x * (a * b) + f a"

Regards,
Andreas

Johannes Hoelzl schrieb:
Hi Andreas,

But this is probably not, what you wanted because the parenthesis ? around a+b are missing, so set the precedence of the parameter to 66 (+ has 65 and * 70):
notation (output) int ("_" [66] 1000)
term "x * int (a + b) + f (int a)"
(* output: "x * (a + b) + f a" *)

Wow, great! Works perfectly for me. I discoverd just a small flaw:

notation (output) int ("_" [66] 1000)
term "f (int (g a))"
(* output: "f g a" *)

notation (output) int ("_" [66] 999)
term "f (int (g a))" (* output: "f g a" *)
term "f (int (a + a))" (* output: "f ((a + a))" *)

Hence the parenthesis around "g a" is missing. When the precedence is
decreased the additional parenthesis is again shown. So it is probably
not enough as a replacement for the set-hidding in
"HOL/Library/OptionalSugar.thy".

Regards,
  Johannes







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