Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] seven new AFP entries


view this post on Zulip Email Gateway (Sep 14 2021 at 09:26):

From: Gerwin Klein <kleing@unsw.edu.au>
There are seven(!) related new entries available in the AFP, all by Mihails Milehins. Thank you for this substantial contribution.

Extension of Types-To-Sets

In their article titled From Types to Sets by Local Type Definitions in Higher-Order Logicand 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.

https://www.isa-afp.org/entries/Types_To_Sets_Extension.html

IDE: Introduction, Destruction, Elimination

The article provides the command mk_ide for the object logic Isabelle/HOL of the formal proof assistant Isabelle. The command mk_ide enables the automated synthesis of the introduction, destruction and elimination rules from arbitrary definitions of constant predicates stated in Isabelle/HOL.

https://www.isa-afp.org/entries/Intro_Dest_Elim.html

Conditional Transfer Rule

This article provides a collection of experimental utilities for unoverloading of definitions and synthesis of conditional transfer rules for the object logic Isabelle/HOL of the formal proof assistant Isabelle written in Isabelle/ML.

https://www.isa-afp.org/entries/Conditional_Transfer_Rule.html

Conditional Simplification

The article provides a collection of experimental general-purpose proof methods for the object logic Isabelle/HOL of the formal proof assistant Isabelle. The methods in the collection offer functionality that is similar to certain aspects of the functionality provided by the standard proof methods of Isabelle that combine classical reasoning and rewriting, such as the method auto, but use a different approach for rewriting. More specifically, these methods allow for the side conditions of the rewrite rules to be solved via intro-resolution.

https://www.isa-afp.org/entries/Conditional_Simplification.html

Category Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories

This article provides a foundational framework for the formalization of category theory in the object logic ZFC in HOL of the formal proof assistant Isabelle. More specifically, this article provides a formalization of canonical set-theoretic constructions internalized in the type V associated with the ZFC in HOL, establishes a design pattern for the formalization of mathematical structures using sequences and locales, and showcases the developed infrastructure by providing formalizations of the elementary theories of digraphs and semicategories. The methodology chosen for the formalization of the theories of digraphs and semicategories (and categories in future articles) rests on the ideas that were originally expressed in the article Set-Theoretical Foundations of Category Theory written by Solomon Feferman and Georg Kreisel. Thus, in the context of this work, each of the aforementioned mathematical structures is represented as a term of the type V embedded into a stage of the von Neumann hierarchy.

https://www.isa-afp.org/entries/CZH_Foundations.html

Category Theory for ZFC in HOL II: Elementary Theory of 1-Categories

This article provides a formalization of the foundations of the theory of 1-categories in the object logic ZFC in HOL of the formal proof assistant Isabelle. The article builds upon the foundations that were established in the AFP entry Category Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories.

https://www.isa-afp.org/entries/CZH_Elementary_Categories.html

Category Theory for ZFC in HOL III: Universal Constructions

The article provides a formalization of elements of the theory of universal constructions for 1-categories (such as limits, adjoints and Kan extensions) in the object logic ZFC in HOL of the formal proof assistant Isabelle. The article builds upon the foundations established in the AFP entry Category Theory for ZFC in HOL II: Elementary Theory of 1-Categories.

https://www.isa-afp.org/entries/CZH_Universal_Constructions.html

Enjoy!
Gerwin


Last updated: Jul 15 2022 at 23:21 UTC