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