Isabelle: новая аксиома для неопределенных функций

Question

Я работаю над теорией, где я довольно сильно использую экстенсиональные функции, определенные в теории Funcset. Мне нужно работать с функциональнозначными функциями, где и функция, и значения являются экстенсиональными. Весьма раздражает то, что некоторые из моих лемм терпят неудачу, потому что функция undefined не отображает все в undefined. Таким образом, цель

undefined x = undefined 

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

axiomatization where 
    undefined_at [simp]: "undefined x = undefined" 

? Меня это волнует, потому что

1) Я не уверен, что я должен поиграть с такой логикой.

2) После того, как я добавить эту аксиому, для целей, таких как «неопределенного \ в А», придираться производит ошибку: Limit reached: too many nested axioms (256).

3), казалось бы, так же невинной аксиома

axiomatization where 
    at_undefined [simp]: "f undefined = undefined" 

производит странные цели, как "P ==> undefined".

Answer 1

Постоянная undefined на самом деле не моделирует математическое понятие undefined. Скорее это означает, что это не указано, как я объяснил в thread в списке рассылки Isabelle.

Back in 2008, undefined фактически был определен с аксиомой undefined x = undefined, то есть, функция undefined отображает все, чтобы undefined. Вскоре люди поняли, что это не то, что должно было представлять undefined, поскольку оно ограничивало функцию undefined постоянной функции, которая вообще не является произвольной функцией. Добавление этой аксиомы не делает HOL неудовлетворительным, но это серьезно ограничивает общность доказанного, потому что undefined используется многими пакетами Изабель.

Другая аксиома at_undefined однако ведет к несоответствиям. Как указано, это означает, что каждая функция f должна быть тождественной по неуказанному значению undefined. Рассмотрим тип bool булева. undefined должен быть True или False. Поэтому, если вы принимаете отрицание для f, тогда для аксиомы требуется, чтобы ~ True = True или ~ False = False. Очевидно, что это не соответствует спецификации op ~, поэтому аксиома несовместима.