Определение конечных множеств в Изабель

Question

Как я могу определить наборы констант в Изабель? Например, что-то вроде {1,2,3} (чтобы придать ему более интересный поворот с 1,2,3 реалами), или {x \in N: x

Я думаю, что во всех случаях это должно быть что-то вроде

definition a_set :: set
  where "a_set ⟷ ??? "

но различные попытки замены ??? с чем-то правильным не получилось.

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

Answer 1

definition Команда определяет константу. Требуется одно уравнение с символом, который будет определен слева, например definition "x = 5" или же definition "f = (λx. x + 1)", Для повышения читабельности аргументы функции могут отображаться в левой части уравнения, например f x = x + 1,

Проблема в том, что вы используете ⟷ (оператор "тогда и только тогда", т. е. равенство логических значений). Если у вас есть логические значения, лучше использовать это вместо простого = потому что он сохраняет скобки: вы можете написать "P x ⟷ x = 2 ∨ x = 5" вместо "P x = (x = 2 ∨ x = 5)". (The = оператор связывает сильнее, чем логические связки ∨ а также ∧; ⟷с другой стороны, связывает слабее)

⟷ это просто еще один способ написания = специализируется на Booleans. Это означает, что если вы определяете что-то, что не возвращает логическое значение, ⟷ не собирается работать. Просто используйте регулярный =:

definition A :: "real set" where
  "A = {1, 2, 3}"

Или, для вашего другого примера:

definition B :: "complex set set" where
  "B = {ℕ, ℝ, UNIV}"

Обратите внимание, что HOL - это типизированная логика; это означает, что вы не можете просто сделать

definition a_set :: set

потому что нет типа всех множеств. Существует только тип всех наборов, элементы которых имеют определенный тип, например nat set или же (real ⇒ real) set или действительно nat set set, Просто говорю set выдаст сообщение об ошибке "Не удалось разобрать тип", поскольку set это конструктор типа, который ожидает один аргумент типа, а вы его не указали

Что касается множества {ℕ, ℝ, ℂ}, это постоянная B Я определил выше в качестве примера. Здесь нет ℂ в Изабель, потому что это просто UNIV :: complex set, (UNIV будучи набором всех значений рассматриваемого типа). Обратите внимание, что ℕ и ℝ в этом случае представляют собой набор натуральных и действительных чисел как подмножество комплексных чисел.