Изабель: как напечатать результат 1 + 2?

Это мой вопрос. Один новичок другому, как повезло.

Я не знаю всех подробностей, но когда вы не указываете тип для ваших констант 1 и 2, вы работаете с numeral, все изложено в Num.thy.

Попробуйте это и посмотрите на панель вывода:

declare[[show_consts=true]]
declare[[show_types=true]]
declare[[show_sorts=true]]
value "1 + 2"
value "1 + (2::nat)"

theorem "1 + 2 = z"
  apply simp
  oops

Вы увидите, что 1+2 равно numeral и не упрощается автоматически, или, скорее, упрощается слишком сильно, расширяясь до формы сложения «преемник».

value "1 + (2::nat)" действительно упрощается до «предпочтительной человеческой формы».

После simp 1 + 2 упрощается до «предпочтительной формы», хотя это numeral.

В Isabelle целочисленные литералы (также называемые числовыми константами), такие как ..., -2, -1, 0, 1, 2, ... перегружены.

Существуют классы типов для нуля (zero), единицы (one), положительных цифр (numeral) и отрицательных цифр (neg_numeral). Последние два также включают классы типов для аддитивной полугруппы (semigroup_add), позволяющей использовать +, и аддитивной группы (group_add), позволяющей использовать + и - (также унарные), соответственно. . (Также обратите внимание, что сам знак плюс (op +) перегружен в классе plus.)

Теперь, если вы введете выражение, Изабель выведет самый общий тип. Часто это более общее, чем можно было бы ожидать. Это именно то, с чем вы столкнулись. Рассмотрим несколько примеров:

input      inferred type      type class
 0           'a                 'a::zero
 1           'a                 'a::one
 op +        'a => 'a => 'a     'a::plus
 1 + 2       'a                 'a::numeral
 x + y       'a                 'a::plus
 Suc 0 + y   nat                (nat is an instance, among others,
                                of class semigroup_add)

В такой ситуации вы можете сообщить системе, что имеете в виду менее общий тип, явно добавив ограничение типа, например, (1::nat) + 2 приводит к общему типу nat.

Если вы используете Isabelle/jEdit, вы можете удобно исследовать такие ситуации, не вводя шум вроде declare [[...]] в свою теорию. Например, при входе

value "1 + 2"

на панели Вывод вы видите

"1 + (1 + 1)"
  :: "'a"

Теперь вы можете нажать Ctrl (т. е. удерживать кнопку управления нажатой и щелкнуть мышью) на 'a в выводе. Который скажет вам, что 'a находится в классе numeral. Вы можете далее Ctrl-щелкнуть numeral, чтобы перейти к определению этого класса типов.

Если вы измените свой ввод на (для натуральных чисел)

value "(1::nat) + 2"

или (для целых чисел)

value "(1::int) + 2"

вывод будет

"Suc (Suc (Suc 0)))" :: "nat"

а также

"3" :: "int"

как и ожидалось.

Обновление: обратите внимание, что натуральные числа (тип nat) будут печататься в унарном представлении, например: 0, Suc 0, Suc (Suc 0), ... . Однако его не следует путать с 1 + (1 + (1 + ...)) (который относится к произвольному типу класса numeral). Такие «числа Пеано» представляют собой правильные натуральные числа, как если бы nat было определено следующим образом:

datatype nat = 0 | Suc nat

Так что это всего лишь красивая печать, но логически нерелевантная.