*To*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Revisiting records, structures, locales, abelian_group, HOL-Algebra and Types-To-Sets*From*: mailing-list anonymous <mailing.list.anonymous at gmail.com>*Date*: Mon, 5 Aug 2019 16:37:15 +0300

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.

**Follow-Ups**:**Re: [isabelle] Revisiting records, structures, locales, abelian_group, HOL-Algebra and Types-To-Sets***From:*Fabian Immler

**Re: [isabelle] Revisiting records, structures, locales, abelian_group, HOL-Algebra and Types-To-Sets***From:*Andreas Lochbihler

**Re: [isabelle] Revisiting records, structures, locales, abelian_group, HOL-Algebra and Types-To-Sets***From:*mailing-list anonymous

**Re: [isabelle] Revisiting records, structures, locales, abelian_group, HOL-Algebra and Types-To-Sets***From:*mailing-list anonymous

- Previous by Date: [isabelle] New AFP entry: Stellar Quorum Systems
- Next by Date: [isabelle] cmod
- Previous by Thread: [isabelle] New AFP entry: Stellar Quorum Systems
- Next by Thread: Re: [isabelle] Revisiting records, structures, locales, abelian_group, HOL-Algebra and Types-To-Sets
- Cl-isabelle-users August 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list