Email Gateway (Aug 18 2022 at 13:28): Email Gateway (Aug 18 2022 at 13:28):From: Chris Capel <pdf23ds@gmail.com>
Is there supposed to be any sort of guarantee of consistency between a
term A and the term B that results from printing A and then reading
the result, when the "show types" option is off? I have found a case
where the types in B are more general, in a way that caused problems
trying to do a lemma. I can give more details if desired.
Chris Capel
Email Gateway (Aug 18 2022 at 13:29):From: Brian Huffman <brianh@cs.pdx.edu>
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 would say that the "show types" and "show sorts" options were designed
solely for making terms easier for humans to parse; I don't think any
guarantees about re-parsing by Isabelle were intended.
With the prevalence of Isar-style proofs nowadays, users are doing a lot
more cut-and-paste from the goals buffer back into their proof scripts than
they used to. Maybe it is time to add a new option, "show exactly enough
type annotations for Isabelle to be able to re-parse terms". Maybe the other
developers could comment on the feasibility of this?
Email Gateway (Aug 18 2022 at 13:29):From: Tobias Nipkow <nipkow@in.tum.de>
I would say that the "show types" and "show sorts" options were designed
solely for making terms easier for humans to parse; I don't think any
guarantees about re-parsing by Isabelle were intended.
'Fraid you are right, Brian. Although these options do help ;-)
Tobias
On Mon, May 11, 2009 at 6:14 PM, Chris Capel <pdf23ds@gmail.com> wrote:
Is there supposed to be any sort of guarantee of consistency between a
term A and the term B that results from printing A and then reading
the result, when the "show types" option is off? I have found a case
where the types in B are more general, in a way that caused problems
trying to do a lemma. I can give more details if desired.Chris Capel
--
"What is it like to be a bat? What is it like to bat a bee? What is it
like to be a bee being batted? What is it like to be a batted bee?"
-- The Mind's I (Hofstadter, Dennet)
Email Gateway (Aug 18 2022 at 13:30):From: Michael Norrish <Michael.Norrish@nicta.com.au>
Brian Huffman wrote:
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.
Last updated: May 03 2024 at 08:18 UTC