Применить упрощение к произвольному термину

AFAIK не имеет встроенной функции, но есть несколько способов добиться этого. Вы уже открыли один из них, а именно формулируете термин как лемму, а затем вызываете упрощение. Недостатком является то, что это нельзя использовать во всех контекстах, например, не внутри скрипта проверки применения.

В качестве альтернативы вы можете вызвать упрощение через атрибут [simplified]. Это работает во всех контекстах с помощью команды thm и производит вывод в выходной буфер. Во-первых, термин должен быть введен в теорему, затем вы можете применить simplify к теореме и отобразить результат с помощью thm. Вот подготовительный материал, который может войти в вашу теорию разных вещей.

definition simp :: "'a ⇒ bool" where "simp _ = True"
notation (output) simp ("_")
lemma simp: "simp x" by(simp add: simp_def)

Затем вы можете написать

thm simp[of "foo 1 2 a b", simplified]

и увидеть упрощенный термин в окне вывода.

Механизм оценки, вероятно, не то, что вам нужно, потому что оценка использует другой набор правил перезаписи (а именно, уравнения кода), чем обычно использует упрощение (симпсет). Следовательно, это, вероятно, приведет к другому термину, чем при применении упрощения. Чтобы увидеть разницу, примените code_simp вместо simp в вашем подходе с lemma "foo 1 2 a b = blah". Метод доказательства code_simp использует уравнения кода так же, как и value [simp].

При использовании команды value оценка аргумента проводится зарегистрированными оценщиками (см. Справочное руководство Isabelle2013-2).

Раньше в предыдущих версиях Isabelle (например, Isabelle2013-2) можно было явно выбрать оценщика, задав дополнительный аргумент команде value. Например.,

value [simp] "foo 1 2 a b"

Похоже, что в Isabelle2014 этот параметр был удален и согласно Справочному руководству Isabelle 2014, стратегия теперь исправлена, чтобы сначала использовать генерацию кода ML, а в случае сбоя - нормализацию путем оценки.

Из файла NEWS в разрабатываемой версии (e82c72f3b227) Isabelle похоже, что этот параметр снова будет включен в предстоящем выпуске Isabelle.

ОБНОВЛЕНИЕ: как отметил Андреас, value [simp] не использует тот же набор правил упрощения, что и apply simp. Таким образом, даже если решение, которое я описал выше, возможно, не даст желаемого результата.