[isabelle] Record selectors operate only on _scheme and not on _ext?
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Record selectors operate only on _scheme and not on _ext?
- From: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
- Date: Mon, 20 Jul 2015 09:39:01 +0200
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.7.0
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and