I merely provide the details based on Brian's comment that a choice function is defined only for a collection of non-empty sets.
From the Wikipedia entry on Choice_function:
A choice function (selector, selection) is a mathematical function f that is defined on some collection X of nonempty sets and assigns to each set S in that collection some element f(S) of S.
By now, you probably already have what you need from Brian's coment, but I do this anyway. The definition of chooser
only needs the requirement that the set isn't empty:
definition chooser :: "('a set => 'a) => bool" where
"chooser f <-> (!A. A ~= {} --> f A ∈ A)"
theorem "(finite A & A ~= {} & chooser f) ==> (f A ∈ A)"
by(metis chooser_def)
theorem "(A ~= {} & chooser f) ==> (f A ∈ A)"
by(metis chooser_def)
You said that you don't want to use the Axiom of Choice, but a standard choice function demonstrates a good template to follow, not that you need it.
definition choice :: "'a set => 'a" where
"choice T = (SOME x. x ∈ T)"
theorem "T ~= {} ==> choice T ∈ T"
by(unfold choice_def, metis ex_in_conv someI
--GC