Re: [isabelle] Record selectors operate only on _scheme and not on _ext?



Hey Andreas.

The record package builds records out of layers of "ext" record
extensions, as you've understood.

In the distant past, the record package defined two layers of selectors
and updators, one (mostly hidden) for each "ext" layer, and surface
selectors/updators which operate on the "completed" type. These were all
new constant definitions - it may be relevant that this design predates
abbreviations.

When I last attacked the record package, I got rid of the duplication in
order to reduce the proof times, and just kept the surface
selectors/updators.

In hindsight, we could have instead kept the layer-by-layer
selectors/updators, and turned them into the final selectors/updators
with abbreviations or other syntax tricks. I didn't think of this at the
time. Also, I wanted to change as little of the old design as possible,
in particular I didn't want to try to understand the syntax aspects.

I suspect that making this change would require a modest amount of work,
probably a few weeks for someone who knows what they're doing. It would
also simplify the simprocs a little - they have to think a lot about the
special cases for the more/"..." selector/updator.

A final complexity you might want to think about: the reason I got
involved in this in the first place is that the record package *can* be
used to define some really big records (> 500 fields). I don't think
that the corresponding datatype proofs can be done in a reasonable
amount of time. This is one reason why records aren't given the datatype
treatment by default. There might be an argument for switching the
default here, and providing a richer theorem set by default with a
"simple mode" switch available for bigger records.

Cheers,
    Thomas.

On 20/07/15 17:39, Andreas Lochbihler wrote:
Dear experts of the record package,

Last week, Jasmin and I had a long discussion about integrating the
record package further with the free_constructors package. In the end,
we found out that things are not so simple. The main obstacle was the
somewhat non-uniform treatment of record extensions when it comes to
the different generated constants. Let me illustrate the problem with
an example.

  record foo = foo :: nat
  record bar = foo + bar :: int

The first command creates a type "'m1 foo_ext"
and synonyms "'m1 foo_scheme = 'm1 foo_ext" and "foo = unit foo_scheme".
The second a type "'m2 bar_ext"
and synonyms "'m2 bar_scheme == 'm2 bar_ext foo_ext" and "bar = unit
bar_scheme".

The record notation (| ... |) gets translated to constants foo_ext and
bar_ext, which serve as free constructors for the types foo_ext and
bar_ext. Thus, a value of type 'm2 bar_scheme is composed of two
nested constructors, namely bar_ext in the extension parameter for
foo_ext. If it were only for this, it would be easy to register the
constants foo_ext and bar_ext as free constructors of the respective
types.

However, the free_constructor command also supports selectors and
therefore, it would be good to register them too. Unfortunately, I
have not been able to find a proper selector for the bar_ext type. The
selector bar is generated as a constant of its own rather than an
abbreviation like

  bar x == bar_ext.bar (foo.more x) (* bar_ext.bar does not exist at
the moment *)

Can anyone remember why the selectors for _scheme are constants rather
than abbreviations of selectors for the _ext types?

In the present form, free_constructors cannot handle compound types
such as bar_scheme. So we cannot register bar reasonably with
free_constructors.

Best,
Andreas



________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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