Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL
Logic in Computer Science
2022-05-10 v2
Abstract
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.
Keywords
Cite
@article{arxiv.2104.11622,
title = {Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL},
author = {Martin Raška and Štěpán Starosta},
journal= {arXiv preprint arXiv:2104.11622},
year = {2022}
}
Comments
accepted at FMM 2021