*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Types-To-Sets: a question about further development of the framework (may be of interest to the topic Re: abelian_group)*From*: mailing-list anonymous <mailing.list.anonymous at gmail.com>*Date*: Sat, 13 Apr 2019 14:06:51 +0300

Dear All, I would like to ask a question in relation to the further development of the functionality of the framework "Types-To-Sets". I am working on several personal projects that rely on "Types-To-Sets". However, as was previously noted on the mailing list, the framework does have its limitations. I would be interested in improving the functionality of the framework. However, before I do any work in this direction I would like to understand if anyone else is already working towards this goal and whether or not there exists a development plan for this framework. Naturally, if anyone has any particular ideas about how the framework can be improved, I would be interested in learning about them. *Background information* In the last two months I relativised a substantial number of results about algebraic structures and abstract spaces from the main HOL library using the methodology suggested in [1] and collected the results in an independent library (of course, please keep in mind that the library is a work in progress): https://github.com/xanonec/HOL-Types_To_Sets_Ext The initial goal was to obtain a locale-based topology library similar to HOL-Algebra. As it stands now, the library can be seen as a complement to the HOL main library. For each axiomatic type class/locale whose carrier set is a universe (of course, not every class/locale was relativised yet), the library provides a relativised locale with an explicitly defined carrier set. For example, for the class topological_space from the main library class topological_space = "open" + assumes open_UNIV [simp, intro]: "open UNIV" assumes open_Int [intro]: "open S ⟹ open T ⟹ open (S ∩ T)" assumes open_Union [intro]: "∀S∈K. open S ⟹ open (⋃K)" the library of relativised results provides a locale locale topological_space_ow = fixes 𝔘 :: "'at set" and τ :: "'at set ⇒ bool" assumes open_UNIV[simp, intro]: "τ 𝔘" assumes open_Int[intro]: "⟦ S ⊆ 𝔘; T ⊆ 𝔘; τ S; τ T ⟧ ⟹ τ (S ∩ T)" assumes open_Union[intro]: "⟦ K ⊆ Pow 𝔘; ∀S∈K. τ S ⟧ ⟹ τ (⋃K)" Of course, the definitions associated with a given type class or even a combination of type classes were relativised as well. For example, the nhds filter for the type class topological_space definition (in topological_space) nhds :: "'a ⇒ 'a filter" where "nhds a = (INF S∈{S. open S ∧ a ∈ S}. principal S)" is relativised as definition nhds :: "'at ⇒ 'at filter" where "nhds a = (Inf_on 𝔘 (principal ` {S. S ⊆ 𝔘 ∧ τ S ∧ a ∈ S}))" In certain cases, more creative approaches were employed. For example, for reasons of compatibility with the main class-based library, the type filter was reused by providing new constants filter_on, inf_on and Inf_on to make the type suitable for interpretation as complete/distributive lattices on an explicit carrier sets, e.g. interpretation filter_clow: complete_lattice_ow "{F. filter_on 𝔘 F}" "(≤)" "(<)" "inf_on 𝔘" sup bot "principal 𝔘" "Inf_on 𝔘" Sup Once all definitions were provided, the theorems were relativised in a semi-automatic manner. For example, lemma tendsto_compose: "g ─l→ g l ⟹ (f ⤏ l) F ⟹ ((λx. g (f x)) ⤏ g l) F" is relativised as lemma tendsto_compose: assumes "g ` 𝔘A ⊆ 𝔘B" and "l ∈ 𝔘A" and "f ` 𝔘C ⊆ 𝔘A" and "filter_on 𝔘C F" and "(on 𝔘B with τb: g ⤏⇩o⇩w g l) (on 𝔘A with τa at l)" and "(on 𝔘A with τa: f ⤏⇩o⇩w l) F" shows "(on 𝔘B with τb: (λx. g (f x)) ⤏⇩o⇩w g l) F" Nevertheless, as noted previously, "Types-To-Sets" does have limitations and, at the moment, it is not very user-friendly. The library certainly contains a substantial amount of boilerplate code, which I would like to reduce. However, it seems that this cannot be done without providing extensions/amendments to "Types-To-Sets" at the ML level. Thank you [1] F. Immler and B. Zhan, “Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL,” in Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, ser. CPP 2019. New York, NY, USA: ACM, 2019, pp. 65–77, event-place: Cascais, Portugal.

**Follow-Ups**:

- Previous by Date: Re: [isabelle] abelian_group
- Next by Date: [isabelle] Natural expression of group theory – Re: abelian_group
- Previous by Thread: [isabelle] on formalization of predicate abstraction in Isabelle
- Next by Thread: Re: [isabelle] Types-To-Sets: a question about further development of the framework (may be of interest to the topic Re: abelian_group)
- Cl-isabelle-users April 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