#isabelle
#isabelle
Вопрос:
Я пытаюсь переписать следующее arg_min выражение в Isabelle (2020) в более удобный синтаксис ARG_MIN.
lemma "1 = arg_min (λ(x::int). x*x) ((<) 0)"
Что у меня есть до сих пор:
lemma "1 = (ARG_MIN ((x::int)*x). 0 < x)"
Но это выдает мне «Внутреннюю синтаксическую ошибку».
Мне просто интересно, как правильно использовать ARG_MIN выше.
Ответ №1:
Посмотрите на синтаксический перевод из ARG_MIN (найденный с помощью C-щелчка по arg_min и просмотра нескольких строк после этого определения):
translations
"ARG_MIN f x. P" ⇌ "CONST arg_min f (λx. P)"
Вы хотите иметь arg_min (λ(x::int). x*x) (λx. x < 0) . Таким образом, сопоставляя значения P, x и f, обозначение становится:
ARG_MIN (λ(x::int). x*x) x. (x < 0)
Комментарии:
1. Тьфу, этот синтаксис ужасен. Я думаю, что я изменю это на что-то более приемлемое в ближайшие несколько месяцев, возможно
ARG_MIN x∈A. f x, или в этом случаеARG_MIN x | x < 0. x * x.2. Пожалуйста, сделайте! Синтаксис не дает мне никакой интуиции о том, что здесь происходит. (Но я все равно не использую такие вещи).