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