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.

翻译：许多事实都具有对称性,往往需要根据所涉对称性的性质单独提出正式证据。我们在伊莎贝尔/HOL中采用了一种方法,为列表数据类型和列表逆转映射所引出的对称性提供这种对称性事实。该方法作为一种属性加以实施,其结果以用户宣布的对称规则为基础。除了一般规则外,我们还提供了旨在适用于词汇组合领域的规则。