Re: [isabelle] Record selectors operate only on _scheme and not on _ext?
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:
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
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
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
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
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