爲什麼不會在lambda表達式中簡單處理這個術語？

Question

我已經證明了這SIMP規則：

lemma AAA: the_sector (log_update ?f ?s) ?p = the_sector ?s ?p 

規則不用於簡化如下：

lemma BBB: "(λA. if A then (the_sector (log_update f s) p) else B) 
    = 
    (λA. if A then (the_sector s p) else B)" 

我知道，我可以申請自動或（規則EXT）其次通過simp來證明這個引理，但我的最終目標是比功能平等更加棘手。我相信這個關鍵點是在if條件中使用函數變量A.我想明白爲什麼simp在這種情況下不會簡化一個術語。

以下說明爲什麼我相信這是癥結所在（兩者都證明）：

lemma CCC: "(λf s p. the_sector (log_update f s) p) = (λf s p. the_sector s p)" 
    by simp 

lemma DDD: "(if A then (the_sector (log_update f s) p) else B) 
     = 
     (if A then (the_sector s p) else B)" 
    by simp 

感謝您的任何意見。

Answer 1

在簡化器的默認設置中，同餘規則會阻止在術語的某些部分重寫。大多數控制操作員（例如if x then ... else ...）和案例表達式（例如case x of None => ... | Some y => ...）都默認聲明這些規則。它們將簡化限定爲決定採用哪個分支的術語，即上述示例中的x。這是出於這樣的想法，即由於採取了其他分支而無法簡化不相關的術語這一觀點。在你的情況下，要重寫的術語the_sector ...發生在then分支內部，所以簡化器根本就沒有看到它。

相關的一致性規則是if_weak_cong和option.weak_case_cong（對於其他數據類型也是類似的）。您可以用declare if_weak_cong[cong del]或在本地用(simp cong del: if_weak_cong)全局刪除它們。我建議將它們留在全球範圍內，因爲一些默認的簡單規則假定針對案例區分的弱同餘規則已經就位。否則，簡化器可能不會終止。

還有另一套同餘規則（if_cong和option.case_cong），它們在簡化分支時利用關於x的知識。如果你將它們聲明爲同餘規則（if_cong[cong]或cong: if_cong），那麼當前分支將被簡化，並且知道條件成立，相應的else分支也會被分支。同樣，在案例區分的分支中，簡化器知道被仔細檢查的術語是適當的形式。

您可以在9.1.3節的Tutorial on Isabelle/HOL中找到關於同餘規則的更多信息。