Определение функций между константами в Isabelle

Question

Я математик, только начинающий привыкать к Изабель, и что-то, что должно быть невероятно простым, оказалось разочаровывающим. Как определить функцию между двумя константами? Скажем, функция f: {1,2,3} \ to {1,2,4} отображает от 1 до 1, от 2 до 4 и от 3 до 2?

Я полагаю, мне удалось определить наборы как константы t1 и t2 без инцидентов, но (я думаю, так как они не типы данных), я не могу попробовать что-то вроде

definition f ::"t1 => t2" where 
"f 1 = 1" | 
"f 2 = 4" | 
"f 3 = 2" 

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

Answer 1

В вашем вопросе есть ряд аспектов.

Во-первых, чтобы получить что-то работает быстро, используйте fun ключевое слово вместо definition, например, так:

fun test :: "nat ⇒ nat" where 
    "test (Suc 0) = 1" | 
    "test (Suc (Suc 0)) = 4" | 
    "test (Suc (Suc (Suc 0))) = 2" | 
    "test _ = undefined" 

Вы не можете шаблон матч на любые аргументы непосредственно в головке определения с помощью definition ключевого слова, в то время как вы можете с fun. Также обратите внимание, что я заменил перегруженные числовые литералы (1, 2, 3 и т. Д.) Конструкторами для типа данных nat (0 и Suc) в совпадении с шаблоном.

Альтернатива будет придерживаться definition, но подтолкнуть анализ случае аргумент функции внутри тела определения с помощью case заявления, например, так:

definition test2 :: "nat ⇒ nat" where 
    "test2 x ≡ 
    case x of 
     (Suc 0) ⇒ 1 
    | (Suc (Suc 0)) ⇒ 4 
    | (Suc (Suc (Suc 0))) ⇒ 2 
    | _ ⇒ undefined" 

Обратите внимание, что такие определения, как test2 не является разворачивается по упрощению по умолчанию, и вам нужно будет вручную добавить теорему test2_def к симпсету упростителя, если вы хотите развернуть вхождения test2 в доказательство.

Вы также можете определить новые типы (вы не можете использовать наборы как типы, непосредственно, как вы пытаетесь сделать), соответствующие вашим двум трехэлементным наборам с typedef, но лично я бы придерживался nat.

EDIT: использовать typedef, сделать что-то вроде:

typedef t1 = "{x::nat. x = 1 ∨ x = 2 ∨ x = 3}" 
    by auto 

definition test :: "t1 ⇒ t1" where 
    "test x ≡ 
    case (Rep_t1 x) of 
    | Suc 0 ⇒ Abs_t1 1 
    | Suc (Suc 0) ⇒ Abs_t1 4 
    | Suc (Suc (Suc 0)) ⇒ Abs_t1 2" 

Хотя, я действительно никогда не использовать typedef себя, и поэтому это не может быть лучшим способом использования этого и другие, возможно предположить, каким-то другим способом. То, что typedef делает, выдает новый тип из существующего, идентифицируя непустой набор жителей для нового типа. Обязательное доказательство, закрытое на auto, просто демонстрирует, что определяющий набор для нового типа действительно не пуст, и в этом случае я вырезаю трехэлементный набор naturals в новый тип, называемый t1, поэтому доказательство довольно тривиально. Созданы две новые константы: Abs_t1 и Rep_t1, которые позволяют перемещаться между naturals и новым типом. Если вы положите print_theorems после команды typedef, вы увидите несколько новых теорем о t1, которые автоматически генерирует вам Isabelle.