В ожидании своего рода гипотезы

Question

Что может быть причиной следующее сообщение об ошибке:

Pending sort hypotheses: trelations 

Здесь

• trelations тип генерируется класс

• ошибка при доказав сбор отрывков от противного. Субгонии имеют форму: «предпосылка1 ==> предпосылка2 ==> ложь»

• состояние доказательства говорит «Нет никаких подцелей!».

• предположения trelations согласуются со мной (https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-July/msg00023.html)

Спасибо.

Answer 1

Ошибка возникает из-за того, что Изабель не может точно знать, что ваши предположения непротиворечивы. Вот надуманный пример (от Brian Хаффман):

class impossible = 
    assumes impossible: "∃x. x ≠ x" 

lemma False: "False" 
proof - 
    obtain x :: "'a::impossible" where "x ≠ x" 
    using impossible .. 
    then show "False" by simp 
qed 

Очевидно, что система необходимо отклонить это доказательство, потому что impossible рода пуст. Техническая причина отказа в том, что система не знает ни одного экземпляра impossible.

Есть два способа предотвратить это:

1. Перед выполнением каких-либо доказательств по классам, зарегистрировать экземпляр.
2. Добавьте «ограничение сортировки» в качестве предположения для вашей леммы: SORT_CONSTRAINT('a::trelations). Он автоматически списывается при использовании леммы (как только вы зарегистрировали экземпляр где-нибудь).