Факторизация предпосылки леммы в качестве определения приводит к сбою в применении метода доказательства (авто) в isabelle

У меня есть следующий код в Изабель:

typedecl Person
consts age :: "Person ⇒ int" 

lemma "⟦(∀p::Person. age p > 20);p ∈ Person⟧⟹ age p > 20"
apply (auto)
done

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

definition C1::bool where "C1 ≡ (∀p::Person. age p > 20)"

Методы auto не проходят проверку в следующем коде:

lemma "⟦C1;p ∈ Person⟧⟹ age p > 20"
apply (auto)
done

почему это происходит? Если я делаю что-то неправильно, разбирая первое допущение --- я делаю это, чтобы упорядочить допущение, чтобы оно выглядело аккуратным и структурированным -- как лучше всего это сделать, чтобы это не повлияло на методы доказательства (авто) функциональность.

Спасибо


isabelle isar
person qartal    schedule 06.11.2014    source источник

Ответы (2)


arrow_upward
1
arrow_downward

Во-первых, чтобы действительно добавить некоторую ценность, я покажу, как использовать declare для добавления C1_def в качестве правила simp. Затем я даю вам несколько незапрошенных указаний о вашем lemma, а затем я даю вам несколько незапрошенных указаний об этикете Stackoverflow (с моей точки зрения).

Объявление определения простым правилом

Как отметил Александр, правило definition не добавляется автоматически в качестве правила simp.

Вы можете объявить это как правило simp следующим образом:

declare C1_def [simp add]

Использование простых правил методами автоматического доказательства auto, simp, fastforce и т. д. может привести к неправильному зацикливанию или расширению формул таким образом, что вы не хотите расширять формулы, поэтому после добавления вы можете удалить его как simp правило такое:

declare C1_def [simp del]

Комментарии к вашей лемме

Возможно, формула в вашей лемме именно то, что вам нужно, но ваша запись, на мой взгляд, является потенциальным источником путаницы. В частности, вы используете Person и как имя типа, и как заданную переменную. Я делаю эти комментарии, не прося разъяснений.

Для себя у меня вопрос был, Как это p ∈ Person не выдает ошибку, потому что Person есть набор, где Person в typedecl Person нет набора.

Один из способов получить дополнительную информацию — использовать declare [[show_types, show_consts]].

Чтобы ответить на мой вопрос, я сделал следующее (преобразование символов для переносимости браузера) и показываю часть того, что я видел на панели вывода:

declare [[show_types, show_consts]]
lemma "[|(!p::Person. age p > 20); p ∈ Person|] ==> (age p > 20)"
oops
(*OUTPUT:
  variables:
    Person :: Person set
    p :: Person *)

Это показывает мне, что Person является свободной переменной. Что касается p, то это связанная переменная в (!p::Person. age p > 20), но она свободна в остальной части леммы, поэтому ваша гипотеза включает формулу, согласно которой каждое p типа Person находится в каждом наборе типа Person set.

Возможно, это то, что вы хотите, но в данном случае это не имеет значения, потому что ваша лемма в основном имеет вид A and B implies A.

Вам нужно принять ответ на отвеченный вопрос SO

Прежде чем исчезнуть примерно через 2 часа, за тегом isabelle, я снова исполняю свой любимый долг полиции этикета SO.

Вы задали три вопроса. В частности, есть такой:

Это прямой вопрос, и на него дан прямой ответ. Вы должны принять это как ответ. В противном случае,

  • когда люди нажимают на вкладку без ответа для тега Изабель, она может отображаться как неотвеченная, когда на нее не было ответа,
  • вы не проявляете должной признательности за полученный ответ.

В случае вопроса, на который я ссылался, вы получили ответ от одного из экспертов Isbelle/HOL (в отличие от меня). Человеку требуется значительное количество времени, чтобы ввести такой ответ. Он не очень длинный, но и не однострочный.

person Community    schedule 07.11.2014
comment
Спасибо пользователю 3317019, я был новичком на этом сайте и не знал о механизме принятия-ответа. Я установил тег ответа в упомянутых вопросах как подходящий ответ. - person qartal; 08.11.2014

arrow_upward
1
arrow_downward

Конструкция definition служит способом абстрагирования деталей реализации. Одним из его применений является доказательство некоторых свойств связанного термина, а затем использование свойств вместо самого объявления термина. Поэтому правила упрощения для определенных терминов не добавляются автоматически в simpset. Правила по-прежнему доступны с названием термина с суффиксом _def и могут использоваться явно:

lemma "⟦C1; p ∈ Person⟧ ⟹ age p > 20"
  apply (auto simp add: C1_def)
done
person Alexander Kogtenkov    schedule 07.11.2014