Определение без рекурсии, в случаях, в Isabelle

Question

Я пытаюсь определить унарную операцию на множестве stalk x, типичные элементы которого имеют вид germ x U s. В этом случае невозможно определить операцию над общими вещами того же типа, что и germ x U s, таким образом, чтобы это уменьшалось до того, что я хочу, поэтому мне кажется, что мне действительно приходится прибегать к определению по случаям. Я попытался следующий

definition stalk_mop2 :: "'a ⇒(('a set × 'a) set ⇒ ('a set × 'a) set) " where 
"stalk_mop2 x y = ((λ z . if (∃ U s. y= germ x U s) then 
(germ x U (-⇩a ⇘objectsmap U⇙ s)) else undefined) z) " , 

и получил сообщение об ошибке, что U s являются дополнительными переменными на РИТАХ. Похоже, что с помощью этого синтаксиса Isabelle не устанавливает связь между гипотезой if и следующим термином, так что, хотя я и связывал U и s в условном выражении, он, по-видимому, интерпретирует следующие вхождения U и s (после then) как свободные переменные.

Что я действительно хочу, это просто функция, которая принимает x и что-то вроде формы germ x U s и возвращает germ x U (-⇩a ⇘objectsmap U⇙ s). Здесь нет ничего рекурсивного.

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

Answer 1

Помните, что это не что-то странное в синтаксисе Изабель, но там нет связи между if-условием и ветвями then- и else. Объем экзистенциального квантификатора, естественно, заканчивается then.

Если вы хотите, чтобы получить свидетельство на то, что вы знаете, существует, вы можете использовать оператор выбора Гильберта, например, SOME (U, s). y = germ x U s) дает пару (U, s), которая удовлетворяет y = germ x U s если такая пара существует (который вы убедились вашим, если-условия), и в противном случае это не определено.

Так как насчет:

definition stalk_mop2 :: "'a ⇒(('a set × 'a) set ⇒ ('a set × 'a) set)" 
where 
    "stalk_mop2 x y = ((λz . 
    if ∃U s. y = germ x U s then 
     let (U, s) = (SOME (U, s). y = germ x U s) in 
     germ x U (-⇩a ⇘objectsmap U⇙ s) 
    else undefined) z)" 

Update: Вы можете использовать несколько let с в одном из следующих способов

let x1 = e1 in let x2 = e2 in ... 

или

let x1 = e1; x2 = e2; ... in ...