Re: [isabelle] read/print consistency?



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?

- Brian


On Mon, May 11, 2009 at 6:14 PM, Chris Capel <pdf23ds at 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)
>
>




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