在應用風格下降一個目標變量

Question

最近了解到how to drop an unwanted premise in an apply-style proof，我現在想知道如何刪除不需要的變量變量。也就是說，假設我有目標

1. !!x y z. A ⟹ B ⟹ C 

其中y不A，B或C出現。我如何將它轉換爲以下內容？

1. !!x z. A ⟹ B ⟹ C 

Answer 1

triv_forall_equality確實是純粹的規則去除冗餘參數。也有prune_params_tac做爲ML戰術，它在所有子目標上運作。請注意，後者不是作爲伊薩爾證明方法公開的，因爲它在實踐中幾乎不需要：默認情況下，像simp和auto這樣的工具已經包含它。

請注意，通過(simp only: triv_forall_equality)的方法適用於許多情況，但也存在一個障礙：Isabelle/HOL中的only修飾符比使用給定的simp規則的「only」更多一點。它包括諸如算術解算器之類的東西，這可能會在某些情況下引起驚訝或混亂。

要伊薩爾方法語言中準確地模仿prune_params_tac，你可以使用(unfold triv_forall_equality)雖然是一個很小的概念障礙：其使用任意改寫，而不是隻內折式c = t只是歷史的偶然。

Answer 2

簡單：

apply simp 

會做的伎倆。如果你不想執行的目標狀態的任何其他轉換，您可以嘗試：

apply (simp only: triv_forall_equality) 

這將刪除不必要的元量詞，但在其他方面不修改目標狀態。