Re: [isabelle] quotient over record type

On Wed, 20 Feb 2013, Brian Huffman wrote:

On Sat, Feb 16, 2013 at 4:40 AM, John Wickerson <jpw48 at> wrote:
Dear Isabelle,

Does the Quotient package works with record types? I'm beginning to suspect that it doesn't, because when I type ...


record my_record =
  foo :: "nat"
  bar :: "int"

declare [[mapQ3 my_record = (something,something_else)]]


... I get "Bad type name: my_record".

The problem here is that "my_record" is really just a type
abbreviation for "unit my_record_ext".

It used to be just a type abbreviation many years ago, when I made the first version of the record package with Wolfgang Naraschewski. Later the package has acquired more and more features and sophistication, both for syntax and proof tools.

Note that as plain type abbreviation, you would see the expansion directly, which is sometimes not exactly desired, but would help here for clarity. Since the record package puts its own syntax translation candy over the basic type syntax it is hard to see to the bottom of it.

Anyway, using Isabelle/jEdit "CONTROL hover click" over the 'record' keyword, or other means to get to ~~/src/HOL/Tools/record.ML, easily reveals some (undocumented) configuration options. For example:

record my_record =
  foo :: "nat"
  bar :: "int"

declare [[record_type_abbr = false]]
declare [[record_type_as_fields = false]]
typ my_record

An old version of these options were mentioned in Isabelle2004/NEWS, but they did not make it into the IsarRef manual so far.

I have also a question about quotients. The "Q3" seen above has passed by several in times recently, but I did not find an explanation of it. Are there now three quotient packages? Is there a chance to get back to just one?


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