[isabelle] Revisiting records, structures, locales, abelian_group, HOL-Algebra and Types-To-Sets



Dear All,

I would like to ask a question in the context of one of the existing
threads:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2019-April/msg00090.html
.

To set the context for the question, I would like to provide two quotes
from the aforementioned thread:

On Fri, 12 Apr 2019 22:36:17 Clemens Ballarin wrote:

>

... The approach of combining locales with records dates back to that time.
> Definitions in locales were unavailable, and the solution was to extract
> the signature part of an algebraic structure into a record, on which
> definitions could be made globally.  ...




On Fri, 12 Apr 2019 22:51:32 Manuel Eberl wrote (in reply to the comments
made by Clemens Ballarin on Fri, 12 Apr 2019 22:36:17):

>

... That's interesting. It would certainly be of interest to think of a
> large-scale overhaul of HOL-Algebra using modern locale features. ...
>



I would like to understand if one was to, hypothetically, implement a
large-scale overhaul of HOL-Algebra using the modern locale features, what
would the structure of the new library look like? Would the records still
be used or would it be implemented in the style of the main HOL library
with all parameters stated explicitly and all definitions stated implicitly
in the locale context? Would it be too much to ask to provide a small
example that demonstrates this modern approach based on the existing
locales in HOL-Algebra?

The primary reason why I am asking the question is that I would like to
understand what is considered to be a canonical methodology for the
implementation of a library about abstract spaces/algebraic structures with
the explicit carrier sets using locales.

-------------------------------------------------

I provide further (and, perhaps, superfluous) details with regard to my
enquiry. I am working on the relativization of the main HOL library using
Types-To-Sets: https://github.com/xanonec/HOL-SML-Relativization. I believe
that this development directly addresses some of the existing concerns of
the users of HOL. For example, in the context of the previously referenced
thread:

On Sat, 13 Apr 2019 10:37:23 Dominique Unruh wrote:

>
> The classes have the advantage of being easier to use than locales in many
> cases (at least I feel that way), but they have the limitation of always
> having UNIV as the carrier.
>


As far as I know, all proofs are simply done twice. And someone building a
> development on these things needs to pick on approach and is then "locked
> in", which is problematic, since some material is only available in the HOL
> approach and some only in the HOL-Algebra approach. In case of an overhaul,
> perhaps these concepts could be unified as well?


>
My own development, effectively, unifies both approaches using
Types-To-Sets as the conceptual glue. The proofs of the set-based theorems
no longer need to be stated explicitly: the type-based theorems from the
main library are converted to the set-based theorems automatically.
Moreover, the adopted methodology explicitly establishes an injection
(potentially, there can be several distinct relativisations of the same
type-based theorem) from the set-based theorems to the type-based theorems
and this injection can be visualised using the features of the framework.

However, I am still not certain as to what would be the best way to
structure the set-based library. At the moment, the development follows the
approach that merely extends the locales that exist in the main HOL library
with an additional locale parameter that represents a carrier set (or
several locale parameters for multiple carrier sets) - this approach is
consistent with the existing library of relativised results (primarily,
about vector spaces) that was previously developed by Bohua Zhan and Fabian
Immler. This approach, straightforward as it may seem, has several
problems. Firstly, whenever reasoning about the spaces/algebraic structures
themselves, the long list of the locale parameters always needs to be
provided explicitly in each theorem. This problem is exaggerated further
whenever dealing with pairs/triples of spaces/algebraic structures - the
lists of parameters can become dramatically long. For example, a context
that describes a pair of complete lattices would look similar to (of
course, explicit context can be replaced with a locale named, for example,
complete_lattice_pair_ow, but the problem remains the same)

context
  fixes 𝔘A :: "'at set"
  fixes 𝔘B :: "'bt set"
  fixes lea leb
    and lsa lsb
    and infa infb
    and supa supb
    and bota botb
    and topa topb
    and Infa Infb
    and Supa Supb
  assumes clow_a: "complete_lattice_ow 𝔘A Infa Supa infa lea lsa supa bota
topa"
  assumes clow_b: "complete_lattice_ow 𝔘B Infb Supb infb leb lsb supb botb
topb"

Furthermore, the notation associated with the locale parameters for a
single space/algebraic structure, as far as I know, cannot be reused
directly when dealing with pairs/triples of spaces/algebraic structures due
to overlaps. Also, I am not aware of any methodology that would enable one
to make the notation associated with the locale parameters to depend on,
for example, other locale parameters. In the context of the example above,
if one is to define the notation for Infa as (‹⨅⇩o⇩w⇩a›), then it becomes
non-sensical if 𝔘A is interpreted as a set named 𝔘B and 𝔘B is
interpreted as a set named 𝔘A. The same problem also occurs when trying to
transfer the notation for the implicit definitions (i.e. definitions stated
in a locale context) from a single space/algebraic structure to a pair of
spaces/algebraic structures. Moreover, even restating the notation for the
locale parameters and implicit definitions when providing the locales for
the pairs/triples of algebraic structures/abstract spaces can be a very
irritating, tedious and error-prone process that results in a substantial
amount of seemingly boilerplate code.

I believe that the use of records/schemes with the explicitly stated
definitions (i.e. outside of the context of locales), as archaic as it may
seem, resolves all of the aforementioned issues. However, the lack of
support for multiple inheritance creates its own problems. While in some
cases, using a scheme that has more fields than necessary is bearable (as
the referenced example from HOL-Algebra demonstrates), in certain cases, it
becomes impossible. For example, in my attempt to use records/structures in
the library of relativised results, I defined

record 'a ord =  "'a partial_object" +
  le :: "['a, 'a] ⇒ bool" (infix ‹⊑ı› 50)
  ls :: "['a, 'a] ⇒ bool" (infix ‹⊏ı› 50)

and

record 'a topology = "'a partial_object" +
  τ :: "'a set ⇒ bool" (‹τı›)

Now, I would like to define an order topology. It does not seem that
records provide a natural way to combine the two concepts together. The
best methodology that I was able to come up with is exhibited via the
following locale that uses two structures:

locale order_topology_ow =
  order_ow 𝒪 for 𝒪 :: "('at, 'bt) ord_scheme" (structure) +
  fixes 𝒯 :: "('at, 'bt) topology_scheme" (structure)
    and 𝔘 :: "'at set"
  assumes 𝔘𝒪: "𝔘 = carrier 𝒪"
    and 𝔘𝒯: "𝔘 = carrier 𝒯"
    and open_generated_order:
      "s ⊆ 𝔘 ⟹ τ⇘𝒯⇙ s = generate_topology_on ((λa. {..⊏a}) ` 𝔘 ∪ (λa.
{a⊏..}) ` 𝔘) 𝔘 s"

In my view, this approach is still better than providing all definitional
elements explicitly. However, this approach is still quite limiting and, in
certain cases, even the list of schemes can become quite long.

I would be curious to know if anyone has dealt with similar problems in the
past and knows a solution that is better than using explicitly listed
parameters. Alternatively, perhaps, someone could suggest a canonical
approach for combining two distinct schemes into one scheme with a 'shared'
field.

Thank you

-- 
Please accept my apologies for posting anonymously. This is done to protect
my privacy. I can make my identity and my real contact details available
upon request in private communication under the condition that they are not
to be mentioned on the mailing list.



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