### Abstract

In their article titled

BSD License*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.### Depends On

### Topics

### Theories

- ETTS_Tools
- files/More_Library.ML
- files/More_Term.ML
- files/More_Logic.ML
- files/More_Tactical.ML
- files/More_Simplifier.ML
- files/More_HOLogic.ML
- files/More_Transfer.ML
- files/ETTS_Writer.ML
- ETTS
- files/ETTS_Tactics.ML
- files/ETTS_Utilities.ML
- files/ETTS_RI.ML
- files/ETTS_Substitution.ML
- files/ETTS_Context.ML
- files/ETTS_Algorithm.ML
- files/ETTS_Active.ML
- files/ETTS_Lemma.ML
- files/ETTS_Lemmas.ML
- ETTS_Auxiliary
- Manual_Prerequisites
- files/ISABELLE_HOME/src/Doc/antiquote_setup.ML
- ETTS_Tests
- files/ETTS_TEST_AMEND_CTXT_DATA.ML
- files/ETTS_TEST_TTS_ALGORITHM.ML
- files/ETTS_TEST_TTS_REGISTER_SBTS.ML
- ETTS_Introduction
- ETTS_Theory
- ETTS_Syntax
- ETTS_Examples
- ETTS_CR
- Introduction
- SML_Introduction
- Set_Ext
- Lifting_Set_Ext
- Product_Type_Ext
- Transfer_Ext
- SML_Relations
- SML_Simple_Orders
- SML_Semigroups
- SML_Monoids
- SML_Groups
- SML_Semirings
- SML_Rings
- SML_Semilattices
- SML_Lattices
- SML_Complete_Lattices
- SML_Linorders
- SML_Topological_Space
- SML_Topological_Space_Countability
- SML_Ordered_Topological_Spaces
- SML_Product_Topology
- SML_Conclusions
- VS_Prerequisites
- VS_Groups
- VS_Modules
- VS_Vector_Spaces
- VS_Conclusions
- FNDS_Introduction
- FNDS_Set_Ext
- FNDS_Definite_Description
- FNDS_Auxiliary
- Type_Simple_Orders
- Set_Simple_Orders
- Type_Semigroups
- FNDS_Lifting_Set_Ext
- Set_Semigroups
- FNDS_Conclusions