伊莎貝爾：「介紹IMPI」

Question

如果我的目標狀態是foo ==> bar --> qux的對面，我知道我可以使用語句

apply (intro impI) 

產生目標狀態foo ==> bar ==> qux。那另一個方向呢？哪個命令會讓我回到目標狀態foo ==> bar --> qux？

---

我想出了迄今爲止最好的是

apply (rule_tac P="bar" in rev_mp, assumption, thin_tac "bar") 

但這是非常笨拙，我想了解，如果有一個更好的方式。

Answer 1

而不是

apply (rule_tac P="bar" in rev_mp, assumption, thin_tac "bar") 

你可以寫

apply (erule_tac P="bar" in rev_mp) 

其中erule_tac消除了匹配假設給你，讓你不需要thin_tac了。

Answer 2

我假設你想留在應用風格。那麼這只是一個難題，可能有很多可能的解決方案。這裏是一個：

apply (unfold atomize_imp, rule) 

或略偏明確

apply (unfold atomize_imp, rule impI) 

其中unfold atomize_imp通過-->取代所有出現==>。然後，通常，您可以指定應由==>（從左側開始）替換的-->的編號，編號爲rule（或rule impI）。

無論如何，如果你會使用伊莎士風格比你剛剛明確表示你想要明確的和幾乎任何自動工具都能夠填補其餘。