Учитывая (схематическую) теорему:
add (add 2 3) 1 = ...
Я хотел бы использовать упрощенный атрибут Изабель для применения коммутативности и получить:
add 1 (add 2 3) = ...
Однако команда:
some_theorem[OF ..., simplified commutativity]
даст в моем случае:
add (add 3 2) 1 = ...
Есть ли способ указать термин позиция, чтобы применить упрощение, используя этот синтаксис?
Я не думаю, что это отражено в документации (см. Пункт 9.3.7 isar-ref).