How to use lambda expression in Isabelle/HOL?

Question

In my exercise to learn Isabelle/HOL syntax, I tried to prove a toy lemma below. It's about lambda expressions (and things like the "Greatest" notation that takes a predicate as input). The intended content of the lemma is that "the greatest natural number that is l.e. 1 is 1".

lemma "1 = Greatest (λ x::nat. x ≤ 1)"
proof - 
  show ?thesis 
    by auto
qed

However, the above proof doesn't work either by auto or simp, and generates a message that.

Failed to finish proof⌂:
goal (1 subgoal):
 1. Suc 0 = (GREATEST x. x ≤ Suc 0)

Can someone help explain what went wrong with the statement or how to prove this correctly (if the statement is correct)?

Manuel Eberl Manuel Eberl · Accepted Answer · 2021-01-12T17:56:51

There is nothing wrong with the lemma, it's just that none of the rules for Greatest are declared in such a way that auto knows about them. Which is probably good, because these kinds of rules tend to mess with automation a lot.

You can prove your statement using e.g. the rule Greatest_equality:

lemma "1 = Greatest (λ x::nat. x ≤ 1)"
proof - 
  have "(GREATEST (x::nat). x ≤ 1) = 1"
    by (rule Greatest_equality) auto
  thus ?thesis by simp
qed

You can find rules like this using the Query panel in Isabelle/jEdit or the find_theorems command by searching for the constant Greatest.

If the GREATEST thing confuses you, the syntax GREATEST x. P x is just fancy syntax for Greatest (λx. P x). Such notation is fairly standard in Isabelle, we also have ∃x. P x for Ex (λx. P x) etc.

How to use lambda expression in Isabelle/HOL?

1 Answers