为什么不会在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中找到关于同余规则的更多信息。