### 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.

### License

BSD License

### History

November 15, 2021
  integration with SpecCheck (revision 61e152c118d4)

### Topics

- Tools

### Session Types_To_Sets_Extension

- ETTS_Tools
- ETTS
- ETTS_Auxiliary
- Manual_Prerequisites
- ETTS_Tests
- 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

### Depends on

- Conditional Transfer Rule
- SpecCheck - Specification-Based Testing for Isabelle/ML

### Auto-related entries

- A verified algorithm for computing the Smith normal form of a matrix
- The Factorization Algorithm of Berlekamp and Zassenhaus

## Cite

×

Types_To_Sets_Extension-AFP

    @article{Types_To_Sets_Extension-AFP,
      author  = {Mihails Milehins},
      title   = {Extension of Types-To-Sets},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Types_To_Sets_Extension.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Oct 5, 2021 : Isabelle2021
- Sep 14, 2021 : Isabelle2021