Ручное добавление предположение к Simplifier (Isabelle)

Question

Я пытался завершить доказательство в Изабеллу, которая в настоящее время работает:

lemma axiom1: " x = y ⟹ Δ x y z = 0" 
    proof - 
    assume 1[simp]: "x = y" 
    have 1: "Δ x y z = Δ y z x" by (rule axiom0_a) 
    also have "… = Δ y z y" by simp 
    also have "… = Δ z y y" by (rule axiom0_a) 
    moreover have "Δ y y z = - Δ z y y" by (rule axiom0_b) 
    moreover have "⋀r. ((r::real) = - r ⟹ r = 0)" by simp 
    ultimately show "Δ x y z = 0" by simp 
    qed 

Однако мне пришлось вручную добавить предположение к Simplifier. Мой вопрос заключается в том, останется ли дополнительное правило в упростителе x=y локальным для этого доказательства или оно будет использоваться в других доказательствах (что может вызвать некоторые проблемы)? Кроме того, я думал, что предположения были автоматически добавлены в упроститель: является ли это причиной того, что это предположение было не потому, что это могло бы вызвать некоторую опасность петли?

Answer 1

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

Если вы структурированное доказательство, он часто работает лучше и записать лемму в структурированном виде с assumes и shows:

lemma axiom1: 
assumes 1[simp]: "x = y" 
shows "Δ x y z = 0" 
...