[isabelle] Types-To-Sets: a question about further development of the framework (may be of interest to the topic Re: abelian_group)



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.



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