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)?
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.