*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] read/print consistency?*From*: Michael Norrish <Michael.Norrish at nicta.com.au>*Date*: Mon, 18 May 2009 12:02:47 +1000*Cc*: isabelle-users at cl.cam.ac.uk, Chris Capel <pdf23ds at gmail.com>*In-reply-to*: <cc2478ab0905120836y452277f9w93edfec0adf711dc@mail.gmail.com>*References*: <737b61f30905111814g3bfc809bpe2611478f43de35d@mail.gmail.com> <cc2478ab0905120836y452277f9w93edfec0adf711dc@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.21 (Macintosh/20090302)

Brian Huffman wrote:

Similar situations can also arise even when "show types" is on. This happens often if you use functions like "of_nat :: nat => 'a::semiring_1" or "of_int :: int => 'a::ring_1" that are polymorphic in the return type. For example, if you type "thm of_int_less_iff", you get:

"(of_int (?w::int) < of_int (?z::int)) = (?w < ?z)"

Even with "show sorts" enabled, you get no indication that this lemma applies only to class "ordered_idom".

I thought a bit about this recently when fiddling with HOL4's pretty-printer. In the absence of user code getting in the way, I believe you can do a reasonable job with the following algorithm: * all variables get type annotations * terms with constants at their head, and where the constant "might be polymorphic" (see below) get their types printed as well if the constant is applied to n arguments and there are type variables that occur after the nth argument that don't appear in the first n. For example, K is a constant with type : 'a -> 'b -> 'a. If the term is K x Then the term K x will get a type annotation because the 'b of the term's type doesn't occur among the arguments that are present (the x). K itself will not get an annotation. Nil, the empty list constant, would always get a type annotation in this scheme. In Isabelle, so too would constants like zero. This is because they are never applied to any arguments, so their polymorphism would always be left dangling. The "might be polymorphic" test has to do with HOL4's overloading system. Terms that are known to print with a form that can in turn parse back to multiple possible terms are considered polymorphic, even though they are not in fact polymorphic at all. With user code about (users can dynamically update the parser/printer systems with their own code in both Isabelle and HOL4), all bets are off of course. Michael.

**References**:**[isabelle] read/print consistency?***From:*Chris Capel

**Re: [isabelle] read/print consistency?***From:*Brian Huffman

- Previous by Date: [isabelle] First Call for Papers: DAMP 2010
- Next by Date: Re: [isabelle] Non-terminating function domain qualifier
- Previous by Thread: Re: [isabelle] read/print consistency?
- Next by Thread: [isabelle] how to eliminate ALL
- Cl-isabelle-users May 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list