не определено в Изабель / HOL

Question

Я пытался доказать эту лемму в Изабель / HOL.

lemma "(0::nat) ≠ undefined"

Но Нитпик находит контрпримеры и к этому, и к его отрицанию

lemma "(0::nat) = undefined"

Как это возможно? Я посмотрел, как определяется undefined, и это аксиома:

axiomatization undefined :: 'a

Но это все еще классическая логика c, верно? Так что либо "(0::nat) = undefined", либо "(0::nat) ≠ undefined" должно быть истинным.

Фон:

У меня есть функция типа:

type_synonym myfun = "nat ⇒ nat"

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

Заранее спасибо :)

Answer 1

По аксиоматизации каждый тип имеет одно обозначенное значение, которое undefined. Это не какое-то отдельное значение, которое находится за пределами нормального диапазона этого типа, то есть undefined :: nat - это натуральное число, но вы не знаете , какое это натуральное число, и фактически вы не сможете доказать любое нетривиальное свойство около undefined. Тривиальным свойством в этом контексте является свойство, которое сохраняется для всех значений типа.

Следовательно, оператор undefined ≠ (0 :: nat) недопустим в Изабель / HOL, и его отрицание не является об ошибках и несоответствиях) Однако для типа единицы (одноэлементный тип, состоящий только из значения () :: unit) вы можете доказать undefined = (), поскольку это тривиальное свойство.

Что касается Ваша первоначальная проблема звучит так, как будто вы должны изменить способ моделирования неопределенности в вашем приложении. Поскольку вы не дали никаких подробностей о том, что вы делаете, на самом деле невозможно дать какой-либо конкретный c совет о том, что делать. Но попытка доказать что-либо о undefined не сработает.