Search code examples
isabelle

How to write ARG_MIN in Isabelle

I am trying to re-write the following arg_min expression in Isabelle (2020) into the more convenient ARG_MIN syntax.

lemma "1 = arg_min (λ(x::int). x*x) ((<) 0)"

What I have so far is:

lemma "1 = (ARG_MIN ((x::int)*x). 0 < x)"

But it's giving me an "Inner syntax error".

I am just wondering what the correct way is to use ARG_MIN above.

Solution

  • Look at the syntax translation from ARG_MIN (found by C-click on arg_min, and looking a few lines after that definition):

    translations
  "ARG_MIN f x. P" ⇌ "CONST arg_min f (λx. P)"

    You want to have arg_min (λ(x::int). x*x) (λx. x < 0). So matching what P, x, and f are, the notation becomes:

    ARG_MIN (λ(x::int). x*x) x. (x < 0)