Почему мое определение функции, которая выбирает элемент из конечного множества непоследовательным?

Question

Я хотел бы рассказать о функциях, которые выбирают один элемент из конечного множества.

Я попытался определить предикат, который говорит мне, что некоторые данная функция является ли такая функция «Chooser»:

definition chooser :: "('a set ⇒ 'a) ⇒ bool" 
where "chooser f ⟷ (∀ A . finite A ⟶ f A ∈ A)" 

На самом деле эти конечные множества, из которого я хотел бы, чтобы выбрать элементы имеют конкретного типа , но помещение конкретного типа в место 'a вызывает такую ​​же проблему.

Я также попытался опустить finite A, но наборы я имею дело с являются конечно, и я даже не хочу думать о аксиоме выбора здесь.

Теперь это определение кажется несовместимым:

lemma assumes "chooser f" shows "False" using assms chooser_def by force 

Как я могу определить chooser в разумных пределах? Я хотел бы использовать его следующим образом:

assume "finite A" 
moreover assume "chooser f" 
moreover assume "choice = f A" 
ultimately have "choice ∈ A" by ??? 

Большую часть времени он просто имеет значение , что выбирается членом множества, не как она выбрана.

---

фон: Я хотел бы формализовать галстук выключатели на аукционах (раздел 4 из this paper). Предположим, что есть два наивысших ставки для предмета, выставленного на аукцион, нам нужно произвольно выбрать одного участника, который должен выиграть аукцион.

---

Вот, кстати, действительно минимальный пример (который немного сложнее понять):

lemma "(∀ A . finite A ⟶ f A ∈ A) ⟹ False" by force 

Answer 1

Я просто предоставить детали, основанные на комментарий Брайана, что функция выбора определена только для набор непустых множеств.

Из записи Википедии на Choice_function:

функция выбора (селектор, выбор) является математической функцией F, определенная на некотором набор X непустых множеств и присваивает каждое множество S в этой коллекции некоторые элемент f (S) S.

К настоящему времени у вас, вероятно, уже есть то, что вам нужно от коллажа Брайана, но я все равно это делаю. Определение chooser необходимо только требование о том, что множество не пусто:

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) 

Вы сказали, что вы не хотите использовать аксиому выбора, но стандартная функция выбора демонстрирует хороший шаблон для подражания, не то, что вам нужно.

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