Учитывая теорему «P (t) ⟶ (∃x. P (x))» с логической импликацией объекта, почему доказательная цель «P (t) ⟹ (∃x. P (x))» задана с мета -логическое значение?

Question

Я только начинаю с Изабель/HOL и пытается доказать простую инструкцию HOL «P (t) ⟶ (∃x. P (x))» с правилами естественной дедукции. Я начал с теорией файлом, содержащим только теоремой:

theory simple imports Main 
begin 

lemma T: shows "P(t) ⟶ (∃x . P(x))" 
proof 
    (* x *) 
qed 

end 

В положении, обозначенной х в комментариях, текущая цель уже «Р (т) ⟹ (. ∃x Р (х))», т.е. логическая импликация уже упрощена до мета-логической импликации.

Via проб и ошибок, я пришел к следующему доказательству:

proof 
    assume "P(t)" then 
    have "∃ x . P(x)" by (rule exI) then 
    have "P(t) ⟶ (∃x . P(x))" by (rule impI) 
    then show "P(t) ⟹ (∃x . P(x))" by (rule impE) 
qed 

который выглядит как-то странным: я представляю импликации, просто устранить ее в следующем шаге.

Мои вопросы сейчас:

1. Где переписывание моей цели прийти и где я могу найти больше об этом?
2. Как я могу упростить доказательство (без обхода ND с помощью авто)?

Answer 1

Откуда возникает переписывание моей цели и где я могу найти больше об этом?

Если вы используете proof, это делается простым шагом в направлении вашей цели. В вашем случае применяется rule impI. Если вы этого не хотите, используйте proof -.

Но вы, вероятно, do хотите использовать неявный rule impI здесь. Обратите внимание, что это изменяет вашу цель, и вы можете просто написать:

proof 
    assume "P(t)" 
    then show "∃ x . P(x)" by (rule exI) 
qed 

Ответы на ваш второй вопрос.