Факторинга из леммы предпосылки как определение приводит к сбою в доказательстве методы (авто) применениях в Isabelle

Question

У меня есть следующий код в 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)" 

авто методы не удается доказать в следующем коде:

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

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

Благодаря

Answer 1

Во-первых, на самом деле добавить некоторую ценность, я покажу, как использовать 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.

Вы должны принять ответ на вопрос ответил так

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

Вы задали три вопроса. В частности, это один:

• type_synonym vs consts in Isabelle definition

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

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

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

Answer 2

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

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