Определение конечных множеств в Isabelle

Question

Как определить постоянные множества в Isabelle? Например, что-то вроде {1,2,3} (чтобы дать ему более интересный поворот с 1,2,3, являющимся реалами) или {x \ in N: x < m}, где m - некоторое фиксированное число - или, возможно, сложнее, множество {N, R, C}, где N - натуральные числа, R - вещественное и C - комплексное.

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

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

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

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

Answer 1

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

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

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

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 - множество всех значений рассматриваемого типа). Обратите внимание, что в этом случае ℕ и case представляют собой набор натуральных и вещественных чисел как подмножество комплексных чисел.