Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL

Autor:	Raška, Martin, Starosta, Štěpán
Rok vydání:	2021
Předmět:	Computer Science - Logic in Computer Science 03B35 68R15 68V20 68V15 D.2.4
Druh dokumentu:	Working Paper
Popis:	Many facts possess symmetrical counterparts that often require a separate formal proof, depending on the nature of the involved symmetry. We introduce a method in Isabelle/HOL which produces such a symmetrical fact for the list datatype and the symmetry induced by the list reversal mapping. The method is implemented as an attribute and its result is based on user-declared symmetry rules. Besides general rules, we provide rules that are aimed to be applied in the domain of Combinatorics on Words. Comment: accepted at FMM 2021
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2104.11622 Zobrazit plný text záznamu View this record from Arxiv