Why is my definition of a function that chooses an element from a finite set inconsistent?

Why is my definition of a function that chooses an element from a finite
set inconsistent?

I would like to reason about functions that choose one element from a
finite set.
I tried to define a predicate that tells me whether some given function is
such a gchooserh function:
definition chooser :: "('a set Ë 'a) Ë bool"
where "chooser f ⟷ (Í A . finite A ⟶ f A ¸ A)"
Actually those finite sets from which I'd like to choose elements are of a
concrete type, but putting a concrete type in 'a's place causes the same
trouble.
I have also tried to omit finite A, but the sets I'm dealing with are
finite, and I don't even want to think about the axiom of choice here.
Now this definition seems to be inconsistent:
lemma assumes "chooser f" shows "False" using assms chooser_def by force
How can I define chooser in a reasonable way? I would like to use it as
follows:
assume "finite A"
moreover assume "chooser f"
moreover assume "choice = f A"
ultimately have "choice ¸ A" by ???
Most of the time it merely matters that a member of the set is chosen, not
how it is chosen.



Background: I'd like to formalise tie-breakers in auctions (section 4 of
this paper). Suppose there are two highest bids for the item being
auctioned, we need to arbitrarily choose the one bidder who should win the
auction.



Here is, BTW, a really minimal example (which is a bit harder to understand):
lemma "(Í A . finite A ⟶ f A ¸ A) ⟹ False" by force