isabelle - Выберите произвольный, но фиксированный элемент

Question

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

Моя первая попытка была:

theory Scratch 
imports Main Orderings 
begin 
    value "(let el ∈ {3::int, 4, 5} in el)" 
end 

Но дает синтаксическую ошибку.

Моя вторая попытка была:

theory Scratch 
imports Main Orderings 
begin 
    value "(let el = (SOME x . x ∈ {{3::int, 4}, 
            {5::int, 6} , 
            {7::int, 8}}) 
        in el)" 
end 

давая тип int set и не ожидаемый тип int.

Редактировать 1

Новый пример:

theory Scratch 
imports Main Orderings 
begin 

fun add :: "int set ⇒ int" where 
    "add st = (let el = (SOME x . x ∈ st) in el + (10::int))" 

value "add {3::int, 4, 5, 6}" 

end 

Результат кода:

"(SOME u. 3 = u ∨ 4 = u ∨ 5 = u ∨ 6 = u) + 10" 
    :: "int" 

вместо того, чтобы целое значение. Как написать add, чтобы результаты были либо 13, 14, 15, либо 16? Точное значение не имеет значения, оно должно быть различным при каждом выполнении функции.

Answer 1

Причина, по которой вы получили int set, состоит в том, что вы выбираете элемент из int set set. Во второй попытке вместо использования «плоского» набора вы использовали вложенный набор.

Помимо вашего конкретного вопроса, я бы порекомендовал вам взглянуть на локаль folding в теории Finite_Set. Он обеспечивает комбинатор для сгибания над наборами (при условии, что оператор коммутирует).

Answer 2

Вы можете определить

definition "el = (SOME x. x ∈ {(3::int), 4, 5})" 

Вы можете доказать, например,

lemma "el ∈ {3,4,5}" 
    unfolding el_def by (rule someI_ex) auto 

Логически, el некоторые фиксированный элемент {3, 4, 5} (как мы только что доказали), и это всегда тот же элемент - но вы не знаете, какой из них. Вы можете думать о нем, как «Когда вселенная появилась, он выбрал значение для SOME x. x ∈ {3,4,5}, либо 3, 4 или 5, но он никогда не скажет вам, какая она есть.»

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