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

Martin Raška, Štěpán Starosta

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 whic…