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

Hi Thomas,

Thanks for the clarification, I did not know that the theorems are only generated inside the simproc on demand. This indeed adds some complication.

For the moment, I'll wait and see what Dmitriy's new tool for lifting BNFs over typedefs brings and how he integrates the record selectors.


On 22/07/15 06:52, Thomas Sewell wrote:
The "NICTA record problem" is with a single flat record that has a lot
of fields (~ 500 I think). I don't think we use record extensions much
at all. I've never seen a record extension more than 2 deep.

The change would impact syntax performance somehow, more work, or
different work. I don't understand the syntax layer at all though, so I
can't really comment on that.

There are less selector/updator pairs, but this essentially doesn't
matter. There are in any case far too many pairs (for a record with >
100 fields) to generate all the simp rules ahead of time. Anyway, only a
tiny proportion of them would be syntactically encountered. The record
simproc proves the relevant rules each time they are needed. The proof
of each one is O (log(n)), so we don't even bother to cache them.

Your suggested change would make this simproc proof process fire
multiple times for some cases where it currently fires once, but I think
the total amount of work would stay about the same, so I suspect the
performance impact would be minor.


On 20/07/15 23:39, Andreas Lochbihler wrote:
Hey Thomas,

Thanks for the quick reply. I still wonder how a change from selectors
on _scheme to layer-by-layer would affect efficiency. With
layer-by-layer, we'd get less selector/updator pairs, because we only
need them for the fields of one record specification, not for the
fields inherited from existing records. On the other hand, selectors
then consist of several constants and pretty-printing has to collapse
the abbreviations. In the end, it certainly depends on the depth of
the record extensions. I myself have never exceeded depth 5, but how
about at NICTA?

Despite the explanation at the beginning of Record.thy, I have not yet
understood how you manage to state and prove O(n ^ 2) theorems (for
the selector-updator rules) in O(log(n)^2) step. In the end, there are
O(n ^ 2) theorems, aren't there?


On 20/07/15 10:45, Thomas Sewell wrote:
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

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

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.


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
The second a type "'m2 bar_ext"
and synonyms "'m2 bar_scheme == 'm2 bar_ext foo_ext" and "bar = unit

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

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 == (foo.more x) (* 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



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.


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.