Isabelleにsubst_tacルールのようなものはありますか？

Question

私は補題

lemma ex1_variable: "(∃x. ∀z. x = y z) = (∃!x. ∀z. x = y z)" 

を持っていると私は私があるため∀aの直接by (rule ex1_variable)を使用することはできません

"∀a. ∃!P. ∀z. P = Q z a". 

を表示したいと思い証明

"∀a. ∃P. ∀z. P = Q z a" 

で中間文を持っています。しかし、substメソッドのようなものを使用することが可能なように感じます。

from `∀a. ∃P. ∀z. P = Q z a` have "∀a. ∃!P. ∀z. P = Q z a" 
    by (subst_tac ?x="P" and ?y="λx. Q x a" and ?z="z" in ex1_variable) 

ex1_variableが現在の目標に代入されますが、インスタンス化された後にのみように。この特定の例は機能しませんが、同様の行には何かがありますか？

Answer 1

補題ex1_variableを明示的にインスタンス化する必要はありません。より高次の統一がそれを行います。 ex1_variableは等価ステートメントなので、実際にはプレーンsubstを使用して、左側のインスタンスをインスタンス化された右側に置き換えることができます。しかし、substには、あなたのサブゴールで左辺のインスタンスが発生するので、前提を調べるように指示する必要があります。したがって、次の作業をする必要があります：

lemma ex1_variable: "(∃x. ∀z. x = y z) = (∃!x. ∀z. x = y z)" sorry 

notepad begin 
    fix Q 
    have "∀a. ∃P. ∀z. P = Q z a" sorry 
    then have "∀a. ∃!P. ∀z. P = Q z a" 
    by(subst (asm) ex1_variable) 
end 

また、あなたの周りの定理の側面を反転し、結論にsubstを適用することができます。

by(subst ex1_variable[symmetric])