# Extension of Types-To-Sets

 Title: Extension of Types-To-Sets Author: Mihails Milehins (user9716869 /at/ gmail /dot/ com) Submission date: 2021-09-06 Abstract: In their article titled From Types to Sets by Local Type Definitions in Higher-Order Logic and published in the proceedings of the conference Interactive Theorem Proving in 2016, Ondřej Kunčar and Andrei Popescu propose an extension of the logic Isabelle/HOL and an associated algorithm for the relativization of the type-based theorems to more flexible set-based theorems, collectively referred to as Types-To-Sets. One of the aims of their work was to open an opportunity for the development of a software tool for applied relativization in the implementation of the logic Isabelle/HOL of the proof assistant Isabelle. In this article, we provide a prototype of a software framework for the interactive automated relativization of theorems in Isabelle/HOL, developed as an extension of the proof language Isabelle/Isar. The software framework incorporates the implementation of the proposed extension of the logic, and builds upon some of the ideas for further work expressed in the original article on Types-To-Sets by Ondřej Kunčar and Andrei Popescu and the subsequent article Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL that was written by Fabian Immler and Bohua Zhan and published in the proceedings of the International Conference on Certified Programs and Proofs in 2019. BibTeX: @article{Types_To_Sets_Extension-AFP, author = {Mihails Milehins}, title = {Extension of Types-To-Sets}, journal = {Archive of Formal Proofs}, month = sep, year = 2021, note = {\url{https://isa-afp.org/entries/Types_To_Sets_Extension.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Conditional_Transfer_Rule, SpecCheck Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.