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



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




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