條件重寫規則與未知條件

Question

在我的理論中，我有一些更大的定義，從中我使用引理推導出一些簡單的屬性。

我的問題是，用於派生屬性的引理沒有被簡化器使用，我必須手動實例化它們。有沒有辦法讓這個更自動化？

的最小例子如下所示：

definition complexFact :: "int ⇒ int ⇒ int ⇒ bool" where 
"complexFact x y z ≡ x = y + z" 

lemma useComplexFact: "complexFact x y z ⟹ x = y + z" 
by (simp add: complexFact_def) 

lemma example_1: 
assumes cf: "complexFact a b c" 
shows "a = b + c" 
apply (simp add: cf useComplexFact) (* easy, works *) 
done 

lemma example_2a: 
assumes cf: "complexFact a b c" 
shows "a - b = c" 
apply (simp add: cf useComplexFact) (* does not work *) 
oops 

lemma example_2b: 
assumes cf: "complexFact a b c" 
shows "a - b = c" 
apply (simp add: useComplexFact[OF cf]) (* works *) 
done 

lemma example_2c: 
assumes cf: "complexFact a b c" 
shows "a - b = c" 
apply (subst useComplexFact) (* manually it also works*) 
apply (subst cf) 
apply simp+ 
done 

我發現在參考手冊中的下段，所以我想我可以解決我的問題與自定義解算器。 但是，我從來沒有真正觸及伊莎貝爾的內部ML部分，也不知道從哪裏開始。

重寫不實例化未知數。例如，單獨重寫 不能證明是一個ε？A，因爲這需要實例化？A。然而，求解器是一種隨意的策略，可以根據需要實例化未知數 。這是Simplifier處理 條件包含額外變量的條件重寫規則的唯一方法。

Answer 1

Isabelle簡化器本身從不會在條件重寫規則的假設中實例化未知數。然而，求解器可以做到這一點，最可靠的是assumption。因此，如果complex_fact a b c字面上出現在目標的假設中（而不是被添加到simpset中simp add:或[simp]），則假設求解器會啓動並實例化未知量。但是，它只會在假設中使用complex_fact的第一個實例。所以如果有幾個，它不會嘗試所有這些。總之，最好是寫

lemma 
    assumes cf: "complexFact a b c" 
    shows "a = b + c" 
    using cf 
    apply(simp add: useComplexFact) 

與示例中的第二個問題是a = b + c與a，b和c是免費不是一個好重寫規則，因爲在左側頭部符號不是一個常數，而是自由變量a。因此，簡化器將不會使用方程a = b + c來替換a和b + c，而是用方程a = b + c的文字出現替換爲True。您可以在簡化器的蹤跡中看到這個預處理（使用using [[simp_trace]]在本地啓用它）。這就是爲什麼example_1工作，其他人不工作的原因。如果你可以改變你的左手邊，使得頭部符號有一個常數，那麼在不寫一個自定義求解器的情況下，應該有一些體面的自動化證明。

此外，您可以使用useComplexFact作爲銷燬規則，進行一些（有限）形式的轉發推理。也就是，

using assms 
apply(auto dest!: useComplexFact) 

也可以在某些情況下工作。然而，這與在可伸縮性方面展開定義非常接近。

Answer 2

您可以在定義中指定，它應該在前面加上[simp]:這樣的自動輸送到簡化器：

definition complexFact :: "int ⇒ int ⇒ int ⇒ bool" where 
[simp]: "complexFact x y z ≡ x = y + z" 

現在所有的例子引理應該是可以解決的直接using cf by simp。