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

TL;DR

This paper presents a method in Isabelle/HOL for automatically generating symmetrical facts related to list reversal, reducing the need for separate proofs and aiding formal reasoning in combinatorics.

Contribution

The paper introduces an attribute-based method in Isabelle/HOL that automatically produces symmetrical facts for lists using user-declared symmetry rules, including domain-specific rules for combinatorics.

Findings

Automates the derivation of symmetrical facts in Isabelle/HOL.

Supports user-declared symmetry rules for customization.

Facilitates reasoning in combinatorics on words.

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.